LLVM transformation validation improved with AI and formal proofs
LLVM Translation Validation Automated with Large Language Models and Lean
Programming Languages
Summary
Transforming programs inside compilers can introduce hidden errors because the rules are complex. The authors combine artificial intelligence models with a proof system called Lean to check if these transformations are correct. Their tool, Trivet, automatically builds proofs or finds errors for nearly all tested cases, including tricky loops and large program parts where previous tools struggled. This approach speeds up proof checking and cuts costs significantly compared to simpler methods.
What this means in practice
- •For compiler engineers: Automatically verify correctness of complex code optimizations in LLVM with reduced manual effort and higher scalability.
- •For software verification teams: Detect subtle errors in program transformations using combined AI and proof checking techniques improving reliability of critical software.
Authors
Chunhao Liao, Hongxu Xu, Xintong Zhou, Yizhou Zhang, Chengnian Sun
Abstract
LLVM is the cornerstone of modern compilers, but its subtle intermediate representation (IR) semantics make transformations error-prone and necessitate formal verification. Alive2, a state-of-the-art translation validator based on satisfiability modulo theories, has achieved substantial success in automating the validation of LLVM transformations. However, it still faces scalability limitations, does not support symbolic bitwidths, and offers only bounded guarantees for loops. In contrast, interactive theorem provers such as Lean can address these cases but require substantial proof engineering. In this paper, we present Trivet, a framework combining large language models (LLMs) and Lean for automated translation validation of LLVM transformations. Trivet generates structured proof scaffolds based on source and target functions, automatically discharges obligations amenable to deterministic reasoning, and delegates transformationspecific obligations to LLMs. It produces refinement proofs or counterexample-based refutations, with every successful verdict checked by the Lean kernel. On 148 LLVM transformations, Trivet verifies or refutes 147, leaving one invalid case unresolved. Successful cases include 60 loop-free transformations with symbolic bitwidths, 27 cases from a restricted class of loop-containing transformations, and 10 complex valid fixed-bitwidth cases on which Alive2 times out. Compared with an unscaffolded baseline, scaffolding enables 26 additional proofs. On cases solved by both configurations, it reduces mean proof time by 75.9% and mean monetary cost by 88%.