LLMとLeanでLLVM変換を自動検証
LLVM Translation Validation Automated with Large Language Models and Lean
この論文をやさしく読む
ひとことで言うと
コンパイラによるプログラムの書き換えが正しいかを、LLMの提案とLeanの厳密な検査を組み合わせて確かめます。148件中147件について、証明または反例による否定に到達しました。
何に役立つ？
考えられる用途は、LLVMの最適化変換の検証作業を省力化することです。ビット幅を固定しない変換や一部のループを含む変換にも対応した評価例があります。
この研究の面白いところ
先に証明の骨組みを作り、機械的に解ける部分とLLMに任せる部分を分けています。成立した判定はLeanのカーネルで確認するため、LLMの回答だけを正しさの根拠にしません。
どこまで分かった？
不正な変換1件は未解決で、ループを含む成功例は限定されたクラスです。時間75.9%減・費用88%減は、骨組みの有無の両設定で解けた事例における平均であり、全LLVM変換への保証ではありません。
v1のアブストラクトに基づくAI解説。日本語訳とは別に、用途の解釈を含みます。
アブストラクトの日本語訳
LLVMは現代のコンパイラの中核であるが、その中間表現（IR）の意味論は微妙であり、変換は誤りを起こしやすいため形式検証が必要になる。充足可能性モジュロ理論に基づく最先端の変換バリデータAlive2は、LLVM変換の検証を自動化することに大きく成功している。しかし、拡張性に限界があり、記号的なビット幅を扱えず、ループについては有界な保証しか提供しない。一方、Leanなどの対話型定理証明器はこれらのケースを扱えるが、多大な証明工学を必要とする。 本研究では、LLMとLeanを組み合わせてLLVM変換を自動検証する枠組みTrivetを提示する。Trivetは、変換前後の関数をもとに構造化された証明の足場を生成し、決定的な推論で扱える義務を自動的に解消し、変換固有の義務をLLMに委ねる。精密化証明、または反例に基づく反証を生成し、成功した判定はすべてLeanカーネルが検査する。LLVM変換148件では、147件を検証または反証し、無効な1件は未解決のまま残った。成功例には、記号的ビット幅を持つループなし変換60件、限定されたクラスのループを含む変換27件、Alive2がタイムアウトした複雑で有効な固定ビット幅のケース10件が含まれる。足場を使わないベースラインと比べ、足場によって追加で26件の証明が可能になった。両構成で解けたケースでは、平均証明時間を75.9%、平均費用を88%削減した。
v1の要旨から自動生成。本文の精読・人による確認は未実施。
- 初稿
- 2026-09-17（UTC）
- 最新改訂
- 2026-09-17 · v1
- 査読・掲載
- 査読状況未確認
更新履歴
- v1 2026-09-17 この版を読む
取得できた版を表示。版の更新は査読済みを意味しません。過去版の本文差分は未解析です。
原文の要旨
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%.
arXiv ID: 2609.19583 ／ 要約の誤りについて