LLVM Translation Validation Automated with Large Language Models and Lean

Summary (Overview)

• Trivet is a novel framework that combines Large Language Models (LLMs) with the Lean interactive theorem prover to automate translation validation of LLVM compiler transformations.
• The framework generates structured proof scaffolds from source and target functions, delegating transformation-specific proof obligations to LLMs while relying on the Lean kernel for rigorous certification of all verdicts.
• On a dataset of 148 real-world LLVM transformations, Trivet successfully validates all 74 valid transformations and refutes 73 of 74 invalid ones, leaving only one invalid case unresolved.
• Trivet overcomes three key limitations of Alive2 (the state-of-the-art SMT-based validator): solver scalability issues, lack of symbolic bitwidth support, and bounded loop unrolling.
• Scaffolding reduces mean proof time by 75.9% and mean monetary cost by 88% compared to an unscaffolded baseline, while enabling 26 additional proofs.

Introduction and Theoretical Foundation

Background: LLVM Transformations and Translation Validation

LLVM's Intermediate Representation (IR) is a strongly typed language with highly expressive semantics, including Undefined Behavior (UB). Optimizations must preserve observable program behavior, but the complexity of IR semantics makes correct implementation notoriously difficult. Translation validation addresses this by formally comparing source (pre-transformation) and target (post-transformation) functions.

The fundamental judgment for a transformation is formalized as:

$$PRE \vDash LHS \Rightarrow RHS$$

where LHS denotes the pre-transformation fragment, RHS its replacement, and PRE is a logical predicate over operands defining when the transformation is valid.

Refinement Relation

Correctness is formulated as refinement (not equivalence) because optimizers exploit UB:

Definition 2.1 (Refinement): A target function tgt refines a source function src, denoted $src \supseteq tgt$, if for every input:

• If src triggers immediate UB, tgt may exhibit any behavior
• If src returns poison, tgt may return poison or any other value, but must not trigger immediate UB
• If src returns a well-defined value, tgt must return the same value and must not trigger immediate UB

Limitations of Alive2 (SMT-based Validation)

Alive2, the state-of-the-art translation validator, has three inherent limitations:

1. Solver Scalability: Bit-blasting fixed-width arithmetic to Boolean circuits becomes expensive for nonlinear operations and complex formulas.
2. Fixed-Bitwidth Reasoning: Standard SMT bit-vector logics (QF_BV) cannot validate transformations over symbolic bitwidths.
3. Bounded Loop Unrolling: Loops are validated only up to a fixed unrolling depth, leaving subsequent iterations unchecked.

Motivation: LLMs + Interactive Theorem Provers

Interactive theorem provers (ITPs) like Lean can handle symbolic bitwidths, large bitwidths, and loops, but historically require prohibitive proof engineering effort. Recent advances in LLMs make ITP-based workflows viable—LLMs can iteratively synthesize and repair proof scripts while the ITP kernel rigorously guarantees correctness.

Methodology

Trivet's Workflow Architecture

Trivet launches two parallel branches for each transformation:

1. Refinement branch: Emits a refinement scaffold with typed holes; the LLM fills the holes.
2. Counterexample branch: The LLM proposes a counterexample candidate; Trivet converts it into a complete Lean proof of non-refinement.

Lean checks each proof, with diagnostics guiding LLM revisions until acceptance or time budget expiration.

Refinement Proof Generation

UB-Sensitive Construct Identification

Trivet identifies nine cases where operators or instruction flags may produce UB (e.g., signed overflow for nsw, zero divisor for udiv). The scaffold splits cases on these conditions and automatically discharges obligations whenever the source yields UB.

Illustrative Example

For a transformation with symbolic bitwidth $w$:

$$\underbrace{(y <_s 0) = (T <_s 0) \vDash y <_u T}_{src(w)} \Longrightarrow \underbrace{a +_{nuw} b <_u 1}_{tgt(w)},$$

where $T = w \times w$, $y = (b +_{nuw} (T - 1)) +_{nuw} a$.

The scaffold:

• Identifies five UB-sensitive constructs (C1–C5)
• Performs case analysis on source conditions (C1–C4)
• Leaves proof holes for value equivalence and target-UB absence
• The LLM fills holes; Lean kernel type-checks the assembled proof

Proof Scaffold Generation Categories

1. Source's UB-triggering circumstances (ordered by value demand)
2. Target-specific circumstances that can trigger immediate UB
3. Value-selection conditions (e.g., in select instructions)

Counterexample Proof Generation

For invalid transformations, the LLM proposes a candidate counterexample with concrete bitwidths and input values. A deterministic scaffold then:

1. Assumes the refinement theorem for contradiction
2. Specializes it to the proposed counterexample
3. Uses a computable Decidable instance for the refinement relation to evaluate concrete outcomes
4. Reduces the proposition to False, establishing non-refinement

Loop-Containing Transformations

Trivet provides preliminary support for a restricted class: source functions with canonical loop form (entry preheader, single self-looping body block, dedicated exit block) transforming to loop-free targets.

Loop-specific proof holes include:

• Loop invariant: summarizes reachable source-loop state and function inputs
• Inductive step: preserves the invariant and proves equality with target result at loop exit
• Final assembly: establishes invariant at loop entry and uses induction for any iteration count

Implementation

Built on Lean-MLIR's LLVM dialect, extended with:

1. Refined semantic foundations for immediate UB and transformation preconditions
2. Missing bit-manipulation operators (ctpop, cttz, ctlz)
3. Multi-parameter symbolic bitwidths and multi-block transformations

The LLM (gpt-5.5 via Codex CLI) operates as an agent; Trivet remains a deterministic harness accepting output only after Lean kernel verification.

Empirical Validation / Results

Dataset Composition

RQ1: Validating Transformations

Trivet validates all 60 transformations; Alive2 validates only 20 of 30 fixed-bitwidth cases (10 time out).

RQ2: Refuting Invalid Transformations

RQ3: Loop-Containing Transformations

The one unresolved invalid case: replacing a loop computing $a_{i+1} = a_i + x$ with return (x × n) fails when $x = poison$ and $n = 0$, as the target propagates poison while the source returns 0.

RQ4: Ablation Study (Scaffold Impact)

Theoretical and Practical Implications

Advantages Over SMT-Based Approaches

1. Symbolic Bitwidth Reasoning: A single Trivet proof establishes refinement for all admissible widths, whereas Alive2 requires separate validation per concrete width.

2. Unbounded Loop Guarantees: Trivet proves correctness for all feasible loop iteration counts via induction, unlike Alive2's bounded unrolling which leaves subsequent iterations unchecked.

3. Scalability: Trivet decomposes complex obligations into focused subgoals, avoiding the performance cliff caused by whole-function formulation and bit-blasting in SMT solvers. Example: a simple transformation $(x /_u y) \cdot y \leq x$ times out in Alive2 at i32 but Trivet validates it in 339s.

Cost-Effectiveness of Scaffolding

The scaffold approach reduces proof generation from scratch by:

• Guiding the LLM through well-defined subgoals
• Avoiding extensive tactic exploration
• Reducing monetary costs from $13.23 to$1.47 per refinement proof (88.9% reduction)
• Enabling proofs that unscaffolded generation cannot complete (26 additional proofs)

Conclusion

Trivet demonstrates that combining LLMs with interactive theorem provers offers a viable path for automated translation validation of LLVM transformations, addressing limitations of SMT-based approaches. Key takeaways:

• Comprehensive coverage: Validates all 74 valid transformations and refutes 73 of 74 invalid ones across 148 real-world cases
• Beyond Alive2's scope: Handles symbolic bitwidths, provides unbounded loop guarantees, and solves cases where Alive2 times out
• Trustworthy automation: Every verdict is checked by the Lean kernel, with proofs verified to contain no sorry/admit and depend only on standard axioms

Future directions include:

• Extending formalization to memory operations and floating-point arithmetic
• Supporting richer loop classes beyond the restricted canonical loop form
• Generalizing to arbitrary control-flow graphs with CFG-specific invariants and induction obligations