Verified Learning for Compiler Optimization: An LLM-Guided Architecture with Formal Control
Source
Dev Pratap Singh, Rong Feng, Suman Saha
Author
Dev Pratap Singh, Rong Feng, Suman Saha
Date
Key takeaways · AI-distilled
The case study is lazification in LLVM IR: a code LLMA large language model — the neural network behind tools like Claude and ChatGPT, trained on huge amounts of text to predict what comes next.Full definition → is fine-tuned on transformations produced by the Wyvern optimizer.
Correctness is enforced outside the model: Alive2 symbolically validates each candidate rewrite, and failing candidates are regenerated rather than accepted.
Wyvern itself stays faster on most benchmarks; 9.8% of benchmarks reached comparable or better runtime under the learned system, with no semantic violations observed.
The authors report that verification overhead stayed bounded and the regenerate-until-valid loop converged stably.
Terms in this piece · Glossary
LLM — A large language model — the neural network behind tools like Claude and ChatGPT, trained on huge amounts of text to predict what comes next.
Why it matters
Demonstrates a workable pattern for letting an LLM propose code transformations while a formal verifier, not the model itself, guarantees correctness.
articleGraphAlignCoder: Aligning Program and Proof Graphs for Code GenerationYueke Zhang, Zihan Fang, Kevin Leach, Yu Huang
articleCompiler-Guided Adaptive Proof Search with Cross-Model Synergy on Context-Dependent Theorem ProvingZhuo Liu, Ding Yu, Hangfeng He
articleNeuro-Formal Verification: Agentic Language-Agnostic Formal Program ReasoningShuvendu K. Lahiri