PaperlayerView exact revision on arXiv

Source-linked AI summary

Verified Learning for Compiler Optimization: An LLM-Guided Architecture with Formal Control

Dev Pratap Singh, Rong Feng, Suman Saha

arXiv:2609.27214v1cs.SE

TL;DR

Handcrafted compiler heuristics can generalize poorly, and learned optimizers often lack transformation-level correctness guarantees. This paper fine-tunes an LLM to propose lazification rewrites and uses Alive2 to validate them during inference. On the LLVM test suite, the model applies fewer transformations overall, with about 10% of benchmarks achieving comparable or improved performance and no semantic violations observed.

  • Problem

    Compiler heuristics can generalize poorly, while most learning-driven optimizers do not provide transformation-level correctness guarantees.

    Source: §1 · p. 1

  • Method

    The system fine-tunes an LLM on Wyvern lazification transformations and uses Alive2 to validate generated rewrites at inference.

    Source: §3 · p. 4

  • Results

    About 10% of benchmarks achieve comparable or improved performance, while the model applies fewer lazifications overall and no semantic violations are observed.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The results support an architecture in which external verification governs generative transformation proposals in compiler pipelines.

    Source: §8 · pp. 14–15

    The study is limited to C programs over LLVM IR with Wyvern as the reference optimizer, and repeated symbolic validation may affect scalability.

    Source: §7 · p. 14

Abstract

from arXiv · show

Compiler optimizations traditionally rely on handcrafted heuristics that often fail to generalize across programs and architectures. We investigate whether large language models can participate in compiler optimization through a verification-centered systems architecture that couples generative rewriting with formal equivalence checking. Using lazification in LLVM IR as a case study, we fine-tune a code-centric LLM on transformations produced by Wyvern and embed Alive2 into a feedback loop that enforces semantic preservation for every generated rewrite. Correctness is enforced externally as a runtime control layer rather than learned implicitly. During inference, candidate transformations are symbolically validated and regenerated when necessary, ensuring accepted rewrites satisfy formal constraints. On the LLVM test suite, the fine-tuned model reproduces core optimization behaviors while applying fewer transformations overall. Although Wyvern remains faster on most benchmarks, 9.8% achieve comparable or improved runtime under the learned system, with no semantic violations observed. Verification overhead remains bounded and convergence stable. These results demonstrate that generative AI components can be safely integrated into compiler pipelines through deterministic validation and structured feedback, offering a scalable architectural pattern for trustworthy AI-driven software infrastructure.

1 Introduction

The paper proposes a compiler architecture in which an LLM proposes lazification rewrites and a verifier enforces semantic correctness. On the LLVM test suite, the fine-tuned model applies fewer transformations than Wyvern, with about 10% of benchmarks achieving comparable or improved performance and no observed semantic violations.

1 Introduction

  • Handcrafted compiler heuristics can generalize poorly across architectures and workloads, while most learning-driven compilers lack transformation-level correctness guarantees.Rare semantic violations limit how aggressively learned optimizers can be deployed in production toolchains.Source: §1 · p. 1
  • The study asks how generative AI can enter critical compiler infrastructure without compromising reliability or formal correctness.Lazification profitability depends on dynamic usage and control-flow context, and can incur thunk and memoization overhead.Source: §1 · p. 2
  • The LLM learns lazification proposals from Wyvern transformations, while Alive2 checks each candidate and triggers regeneration when equivalence is not proved.Correctness is enforced externally at inference rather than learned implicitly by the model.Source: §1 · p. 2
  • About 10% of benchmarks achieve comparable or improved performance, while no semantic violations or over-lazification cases are observed.The model applies fewer lazifications overall; compared with a non-finetuned baseline, it achieves a 2.5% runtime reduction and 9.5% smaller binaries.Source: §1 · p. 2

2 Related Work

Prior work studied compiler heuristics, learned optimization, formal verification, and LLM-based reasoning largely as separate approaches. This paper brings adaptive rewrite generation together with formal semantic validation in a verified learning architecture.

2 Related Work

  • Wyvern uses manually engineered, profiling-guided rules for lazification; this work learns rewrite proposals from its verified transformations and adds external validation.The paper shifts the focus from heuristic design to how learned proposals can be governed by correctness checks.Source: §2 · p. 3
  • Learning-based compiler systems have addressed flags, pass ordering, inlining, and register allocation, but generally frame optimization as performance selection rather than semantics-sensitive rewriting.The paper contrasts its focus on transformation validity with prior systems including Milepost GCC, AutoPhase, and MLGO [10].Source: §2 · p. 3
  • Structural code models and learned optimizers capture compiler structure, but the cited systems assume transformation soundness rather than checking equivalence for each generated rewrite.Examples include Ithemal, inst2vec, ProGraML, NeuroVectorizer, and RL4ReAl.Source: §2 · p. 3
  • Verified superoptimization and LLVM equivalence tools provide correctness checks, but the paper characterizes them as lacking adaptivity in deciding which transformations are profitable.The proposed system embeds Alive2 in a learning-guided pipeline rather than using verification only as a post-hoc filter.Source: §2 · p. 3
  • Prior LLM compiler work evaluates optimization mainly through empirical performance, whereas this work couples generation with formal equivalence enforcement for semantics-sensitive rewrites.The related-work review frames the contribution as unifying adaptive generation and formal validation, rather than treating these directions separately.Source: §2 · pp. 3–4

3 Approach

The approach uses a fine-tuned LLM to propose conditional lazification rewrites and an external verifier to decide whether generated candidates preserve semantics. Training examples come from Wyvern, while inference uses Alive2 validation and diagnostic feedback.

3 Approach

  • Verified learning couples data-driven transformation proposals with formal correctness guarantees, using Wyvern examples, an LLM, and Alive2 validation.The verifier proves equivalence before a generated rewrite is accepted.Source: §3 · p. 4

3.1 Problem Formulation

  • The task is to decide per LLVM IR function whether lazification can improve performance while preserving behavior.The transformation changes eager call-by-value evaluation into deferred call-by-need execution only when profitable.Source: §3.1 · p. 4

3.2 System Overview

  • Training pairs unoptimized LLVM IR with Wyvern-lazified IR; at inference, Alive2 validates generated candidates and diagnostic traces guide regeneration after failures.The compiler remains the correctness authority while the LLM proposes transformations.Source: §3.2 · pp. 4–5, Figure 1 · p. 5

3.3 Research Questions

  • The research questions examine optimization quality relative to a verified heuristic, structural behaviors replacing handcrafted rules, and correctness under verification and feedback.The evaluation frames the study around performance, structural behavior, and stable convergence.Source: §3.3 · p. 6

3.4 Dataset

  • The model is trained on function-level examples from eight open-source C libraries and evaluated on a held-out LLVM test suite with over 8,000 functions.The training corpus retains transformed and untransformed functions; the table reports LOC, function counts, lazifiable functions, and average IR size.Source: §3.4 · pp. 6–7, Table 1 · p. 6

3.5 Wyvern Optimizer Oracle

  • Wyvern supplies verified training exemplars by using control flow, data dependencies, and parameter-use frequency to select lazification candidates.The study treats Wyvern outputs as exemplars for transferable decision features, not as an absolute oracle.Source: §3.5 · p. 7

3.6 Meta Compiler LLM

  • The Code LLaMA-based Meta Compiler LLM is fine-tuned on verified unoptimized-to-Wyvern IR pairs to synthesize context-sensitive transformation proposals.It is presented as complementing deterministic analyses rather than replacing them.Source: §3.6 · p. 7

3.7 Alive2-Guided Verification and Integration

  • Alive2 symbolically checks original and transformed LLVM IR for equivalence; only passing rewrites are accepted, and failures trigger regeneration from diagnostic traces.The verifier acts inline within optimization rather than as a post-hoc filter.Source: §3.7 · p. 7

4 Experimental Setup

The experiments compare Wyvern, unoptimized LLVM, and pre-trained and fine-tuned Meta Compiler LLM variants under fixed settings. Evaluation uses held-out LLVM-test-suite programs and measures correctness, transformation structure, runtime, and binary size.

4 Experimental Setup

  • Experiments compare Wyvern, unoptimized LLVM, and both Meta Compiler LLM variants with compiler flags, seeds, verifier settings, data partitions, and metrics fixed.Runtime measurements are collected on the CPU; the system uses an Intel Core i5-120U under Ubuntu 22.04 LTS, LLVM 14, and Clang 14.Source: §4 · pp. 7–8
  • Training uses eight open-source C libraries with an 80/20 train-validation split, while evaluation uses only the held-out LLVM-test-suite.No evaluation functions are used for model selection or hyperparameter tuning.Source: §4 · p. 8
  • Evaluation measures Alive2 equivalence, structural differences relative to Wyvern, runtime, and binary-size deltas, with medians and bootstrap confidence intervals.The fine-tuned Code LLaMA model uses LoRA, an 8K-token context window, and three training epochs.Source: §4 · p. 8

5 Results

On the LLVM test suite, the fine-tuned model reproduces Wyvern’s optimization patterns while applying fewer lazifications and maintaining semantic correctness. Results also show bounded feedback-loop convergence and efficiency gains from fine-tuning relative to the non-finetuned model.

5 Results

  • The fine-tuned model closely mirrors Wyvern’s optimization quality while applying fewer transformations overall, with full semantic correctness validated by Alive2.Runtime measurements report median execution times across repeated runs.Source: §5 · p. 8

5.1 Optimization Fidelity and Runtime Efficiency

  • The LLM’s mean runtime is nearly double Wyvern’s (+97%), but 9.8% of benchmarks run faster under it; its binaries average 9.5% smaller, with identical median sizes.Table 2 reports bounded runtime variance and no severe regressions.Source: Table 2 · p. 9, §5.1 · p. 9

5.2 Structural Optimization Behavior

  • LLM structural ratios are conservative overall but show up to 3.8× Loads in CMAKE and 2.6× Stores in SINGLESOURCE, while Branches remain near 1.0.LOC expands modestly, by 1.04–1.23×.Source: Figure 4 · p. 10, §5.2 · p. 11

5.3 Feedback-Loop Convergence

  • Among 19 initially failing programs, feedback needed 2–9 iterations (mean 5.32, standard deviation 2.08); most converged in 4–6, with none diverging or oscillating.Each verification step averaged 2.46 ms, and no case required manual intervention or heuristic fallback.Source: §5.3 · p. 11, Figure 5 · p. 12

5.4 Impact of Fine-Tuning

  • Fine-tuning reduces average runtime 2.5% and binary size 9.5% versus baseline; roughly 78% of benchmarks fall below the runtime parity line.Improvements are computed over the full benchmark suite, and median results show similar directional trends.Source: Table 3 · p. 12, §5.4 · p. 12, Figure 6 · p. 13

6 Discussion

The fine-tuned model learns many of Wyvern’s lazification applicability patterns while applying fewer transformations and preserving semantic correctness under Alive2. Its conservative structural behavior and bounded verifier-feedback loop support stable optimization.

6 Discussion

  • The model preserves semantic correctness under Alive2 while learning Wyvern-like applicability patterns and optimizing fewer functions and transformations overall.The discussion attributes this to a cautious transformation policy rather than arbitrary rewrites.Source: §6 · p. 13
  • Instruction counts and memory operations increase relative to Wyvern, while function counts, calls, and branching remain near-stable.The discussion interprets this conservative structural profile as prioritizing correctness and stability over aggressive elimination.Source: §6 · pp. 13–14
  • All 19 initially rejected programs converged to verified outputs within nine iterations, averaging approximately 5.3 iterations with no divergence.Most failures were syntactic; verifier feedback acted as a structured corrective signal.Source: §6 · p. 14
  • The absence of extreme runtime and binary-size deviations suggests fine-tuning improves calibration rather than aggressiveness.The paper presents verified supervision and external enforcement as design principles for predictable generative optimization.Source: §6 · p. 14

7 Limitation and Future Work

The study is limited to C programs over LLVM IR with Wyvern as the reference optimizer, and verification does not account for microarchitectural performance factors. Future work proposes performance-aware learning, cross-IR evaluation, and lighter verification.

7 Limitation and Future Work

  • The evaluation covers C programs over LLVM IR with Wyvern as reference, so generalization to other languages, IRs, and architectures remains unestablished.Alive2 verifies semantic equivalence but does not capture caching or branch prediction, leaving hardware-dependent performance variability possible.Source: §7 · p. 14
  • Wyvern-based supervision may bias the model toward conservative imitation, while repeated symbolic validation adds overhead that could affect scalability.Source: §7 · p. 14
  • Future work proposes performance-aware reinforcement learning with verifier-informed rewards, cross-IR evaluation, and lightweight verification.These directions are intended to assess whether verified learning can scale as a general architectural pattern.Source: §7 · p. 14

8 Conclusion

The paper presents formal verification as a runtime control layer for LLM-generated compiler rewrites, demonstrating semantic preservation while approximating a verified heuristic optimizer. It concludes that deterministic validation and controlled feedback offer a reusable pattern for trustworthy generative systems in software engineering.

8 Conclusion

  • The architecture separates rewrite generation from correctness enforcement, using Alive2 equivalence checking and feedback-guided regeneration to preserve semantics.The paper frames correctness as a control mechanism rather than something learned implicitly.Source: §8 · p. 14
  • The system produces correctness-preserving optimizations relative to a non-finetuned baseline, while verification constraints encourage conservative, reliability-oriented behavior.Source: §8 · p. 15
  • The verified-learning architecture is presented as a reusable design pattern for generative models in software pipelines where correctness, stability, and deployment safety matter.Source: §8 · p. 15
Loading 2609.27214v1…