Large language models safely guide compiler optimizations with formal checks
Verified Learning for Compiler Optimization: An LLM-Guided Architecture with Formal Control
Software Engineering
Summary
Compiler optimizations make programs run faster by changing code, but mistakes can break the program. This paper shows how a large language model (LLM) can suggest code changes while a formal system checks each change to keep the program correct. The authors tested this on an existing compiler and found the system often kept changes safe and sometimes improved program speed. This method blends AI creativity with strict safety checks to help build reliable software tools.
What this means in practice
- •For compiler engineers: Integrate AI-driven optimization suggestions with formal correctness checks to improve reliability in compiler toolchains.
- •For software infrastructure teams: Deploy AI-assisted compiler components that maintain safety through runtime validation for dependable software building pipelines.
Authors
Dev Pratap Singh, Rong Feng, Suman Saha
Abstract
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.