编译器优化的验证式学习：一种具有形式化控制的LLM引导架构
Verified Learning for Compiler Optimization: An LLM-Guided Architecture with Formal Control
- The Pennsylvania State University（宾夕法尼亚州立大学）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
本文提出一种以验证为中心的LLM引导编译器优化架构，通过形式化等价性检查强制语义保持，在LLVM测试套件上以更少变换复现核心优化，9.8%基准性能相当或更优，且无语义违规，展示了生成式AI安全集成于编译器的可行路径。
AI中文摘要：
编译器优化传统上依赖于手工设计的启发式方法，这些方法往往无法在不同程序和架构间泛化。我们研究大型语言模型能否通过一种以验证为中心的系统架构参与编译器优化，该架构将生成式重写与形式化等价性检查相结合。以LLVM IR中的惰性化（lazification）作为案例研究，我们对基于代码的LLM在Wyvern生成的变换上进行微调，并将Alive2嵌入反馈循环中，以强制每个生成的重写在语义上得到保持。正确性通过外部运行时控制层强制实施，而非隐式学习。在推理过程中，候选变换会被符号化验证，并在必要时重新生成，确保被接受的重写满足形式化约束。在LLVM测试套件上，微调后的模型在应用更少变换的情况下复现了核心优化行为。尽管Wyvern在大多数基准上仍然更快，但9.8%的基准在所学系统下实现了相当或更优的运行时性能，且未观察到语义违规。验证开销保持有界，收敛稳定。这些结果表明，通过确定性验证和结构化反馈，生成式AI组件可以安全地集成到编译器流水线中，为可信的AI驱动软件基础设施提供了一种可扩展的架构模式。
英文摘要：
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.
