发表机构
University of Waterloo（滑铁卢大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
提出 Trivet 框架，结合大语言模型与 Lean 证明器自动化验证 LLVM 变换，在 148 个变换中验证或反驳 147 个，显著提升可扩展性并降低证明成本。
AI 中文摘要
LLVM 是现代编译器的基石，但其微妙的中间表示（IR）语义使得变换容易出错，因此需要形式化验证。Alive2 是一种基于可满足性模理论的最新翻译验证器，在自动化验证 LLVM 变换方面取得了显著成功。然而，它仍面临可扩展性限制，不支持符号位宽，并且对循环仅提供有界保证。相比之下，Lean 等交互式定理证明器可以处理这些情况，但需要大量的证明工程。在本文中，我们提出了 Trivet，一个结合大语言模型（LLMs）和 Lean 的框架，用于 LLVM 变换的自动化翻译验证。Trivet 基于源函数和目标函数生成结构化的证明脚手架，自动处理适合确定性推理的义务，并将特定于变换的义务委托给大语言模型。它生成精化证明或基于反例的反驳，每个成功判定都由 Lean 内核检查。在 148 个 LLVM 变换上，Trivet 验证或反驳了 147 个，留下一个无效案例未解决。成功的案例包括 60 个具有符号位宽的无循环变换，27 个来自受限类别的含循环变换，以及 10 个 Alive2 超时的复杂有效固定位宽案例。与无脚手架基线相比，脚手架使得额外 26 个证明成为可能。在两种配置均解决的案例上，它平均证明时间减少了 75.9%，平均货币成本减少了 88%。
英文摘要
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%.
