编译器优化的验证学习：具有形式控制的大语言模型指导架构

编译器优化传统上依赖于手工启发式方法，而这些启发式方法通常无法跨程序和体系结构进行泛化。我们研究大型语言模型是否可以通过以验证为中心的系统架构参与编译器优化，该架构将生成重写与形式等价检查相结合。使用 LLVM IR 中的惰性化作为案例研究，我们在 Wyvern 生成的转换上微调以代码为中心的 LLM，并将 Alive2 嵌入到反馈循环中，该反馈循环强制为每个生成的重写进行语义保留。正确性是作为运行时控制层在外部强制执行的，而不是隐式学习的。在推理过程中，候选转换会在必要时进行符号验证和重新生成，以确保接受的重写满足形式约束。在 LLVM 测试套件上，微调模型重现了核心优化行为，同时总体上应用了更少的转换。尽管 Wyvern 在大多数基准测试中仍然更快，但 9.8% 在学习系统下实现了可比较或改进的运行时间，并且没有观察到语义违规。验证开销保持有限且收敛稳定。这些结果表明，生成式人工智能组件可以通过确定性验证和结构化反馈安全地集成到编译器管道中，为值得信赖的人工智能驱动的软件基础设施提供可扩展的架构模式。