論文「Compile to Compress: Boosting Formal Theorem Provers by Compiler Outputs」の技術的サマリー

本論文は、形式定理証明（Formal Theorem Proving）における大規模言語モデル（LLM）の拡張性を向上させるための新しいフレームワーク「Compile to Compress」を提案しています。従来の手法が抱える「テスト時の計算コストの増大」と「コンテキストウィンドウの制限」というボトルネックを、コンパイラ出力の構造的な圧縮特性を利用することで解決し、効率的な定理証明を実現しています。

以下に、問題定義、手法、主要な貢献、実験結果、および意義について詳細をまとめます。

---

1. 背景と問題定義

背景

形式定理証明（特に Lean 4 言語を用いた証明）において、LLM は有望なアプローチとなっています。しかし、現在の最先端の手法は、大量の試行（Roll-outs）や長いコンテキストウィンドウを必要とする「自己修正（Self-correction）」プロセスに依存しています。

課題

1. 計算コストとスケーラビリティ: 従来の自己修正は、過去の失敗履歴全体をコンテキストに保持し続ける必要があるため、計算リソースが莫大になり、探索の深さが制限されます。
2. コンパイラフィードバックの過小評価: 既存の手法では、コンパイラからのエラーメッセージを単なる「成功/失敗」のバイナリ信号や、単純なテキストとして扱っています。しかし、コンパイラ出力には、多様な失敗試行を構造化された失敗モード（Failure Modes）に圧縮する豊富な情報（構造的なパターン）が含まれています。
3. 探索の非効率性: 単純な生成（Direct Generation）は、正解が分布の中心から遠く離れた場合（Out-of-Distribution）、発見が困難です。

2. 提案手法：Compile to Compress

本研究の核心は、**「コンパイラを次元圧縮器（Dimension Compressor）」**と見なすという洞察です。多様な不正な Lean プログラムが、限られた数の構造化されたエラーメッセージにマッピングされる性質を利用します。

2.1. 主要な概念

• 失敗モード駆動の修正（Failure-Mode Driven Refinement）:
  構文が異なっていても、同じコンパイラエラーを発生させるプログラムは、類似した修正戦略で直せる可能性が高いと仮定します。これにより、個々の問題インスタンスに特化した学習ではなく、エラータイプに一般化された修正戦略を学習できます。
• 分布の連鎖（Chain of Distributions, CoD）:
  従来の直接生成は単一の固定分布からサンプリングしますが、提案手法では、コンパイラフィードバックに基づいて条件付き分布を逐次更新します。これにより、モデルは静的な分布の範囲を超えて、正解が存在する領域へ適応的に移動（探索）できます。

2.2. フレームワークの構成

1. 学習-to-修正（Learning-to-Refine）フレームワーク:
   • 教師あり微調整（SFT）: 失敗した証明とコンパイラエラー、そして修正後の正解（およびその思考プロセス）を用いて、モデルに「エラーに基づいた修正」を学習させます。
   • エキスパート反復（Expert Iteration）: 生成された証明を反復的に修正し、成功した軌跡を新たな教師データとして利用することで、モデルの修正能力を継続的に向上させます。
2. マルコフ的修正プロセス:
   修正ステップにおいて、過去の長い履歴全体ではなく、「現在の失敗した証明」と「そのエラーメッセージ」のみを入力とします。これにより、コンテキスト長の制限を回避し、効率的な学習を可能にします。
3. テスト時の探索戦略:
   • ランダム木探索: 根ノード（新規生成）と内部ノード（修正）をランダムに選択。
   • 価値ガイド木探索（Value-Guided Tree Search）: 各ノードの「修正成功の可能性」を推定するニューラル価値関数を学習し、有望な分枝（新規生成か、特定の修正か）に計算リソースを集中させます。

3. 主要な貢献

1. コンパイラフィードバックの構造化利用:
   コンパイラ出力を「次元圧縮された構造的な失敗モード」として捉え直し、これを修正学習の条件付けに利用する新しいパラダイムを提案しました。
2. 効率的な自己修正メカニズム:
   長い履歴を保持する必要なく、現在のエラー状態に基づいて局所的に修正を行うマルコフ的なアプローチにより、テスト時の計算コストを大幅に削減しつつ、探索の深さを確保しました。
3. 分布の連鎖（CoD）の定式化と検証:
   修正プロセスが単一の分布から、フィードバックに依存する動的な分布の連鎖へと遷移することを理論的に定式化し、統計的検定により直接生成と修正生成が異なる分布からサンプリングされることを実証しました。
4. 高性能なベースラインの確立:
   公開されている 8B および 32B パラメータモデルにおいて、PutnamBench などの難易度の高いベンチマークで SOTA（State-of-the-Art）性能を達成しました。

4. 実験結果

評価ベンチマーク

• MiniF2F-test: 高校レベルの数学問題。
• ProofNet: 大学レベルの数学（解析、線形代数など）。
• MathOlympiadBench: 数学オリンピックレベル。
• PutnamBench: プットナム数学コンペティション（1962-2024 年）の 660 問。

主要な結果

• 性能向上:
  • Kimina-8B（80 億パラメータ）: PutnamBench で 25 問を正解（ベースラインの 10 問から大幅向上）。同サイズモデルの中でトップ。
  • Goedel-32B（320 億パラメータ）: PutnamBench で 110 問を正解（ベースラインの 32 問から大幅向上）。同サイズモデルの中でトップ。
• 比較優位性:
  • 単純な「直接生成（Direct Synthesis）」のみを学習させたモデルと比較して、提案手法（Refinement）は ProofNet や PutnamBench などで 50% 以上の相対的な改善を示しました。
  • 大規模な推論コストを要する閉源モデルや、多数のツールを駆使するエージェントシステムと比較しても、限られたテスト時予算（256 試行など）内で同等以上の性能を発揮しました。
• 探索戦略の効果:
  • 「価値ガイド木探索（Value-Guided Tree Search）」は、ランダム探索や単純な DFS/BFS を凌駕し、特に難問において高いサンプル効率を示しました。
  • 簡単な問題では直接生成が有効ですが、難しい問題では反復的な修正（Refinement）が不可欠であることが示されました。

5. 意義と将来展望

学術的・実用的意義

• スケーラブルな推論: 計算リソースが限られる環境でも、コンパイラフィードバックを活用することで、LLM の推論能力を効率的に引き出せることを示しました。
• 検証器ガイドの推論の新たな指針: 「検証器（コンパイラ）の出力を構造的な抽象化として利用する」という視点は、形式証明だけでなく、他の検証可能なタスク（コード生成、数式処理など）への応用可能性を示唆しています。
• モデルサイズとの親和性: 大規模モデルに依存せず、中規模モデル（8B-32B）でも SOTA 性能を達成できるため、オープンソースコミュニティやリソース制約のある環境での実用化に寄与します。

限界と将来の課題

• 修正の限界: 局所的な修正で解決できるエラー（構造的なミス）には効果的ですが、意味論的に複雑なエラーや、証明全体の方針転換が必要な場合は修正が困難な場合があることが分析されました。
• ノイズの多い検証信号: 現在の手法は厳密な形式検証（Lean）に特化しており、検証信号が曖昧な領域への転用にはさらなる研究が必要です。

結論

本論文は、形式定理証明において「コンパイラ出力を圧縮された失敗モードの集合」として再解釈し、これを利用した効率的な学習・探索フレームワークを提案しました。その結果、テスト時の計算コストを抑制しつつ、中規模 LLM においても最先端の定理証明性能を達成することに成功しました。これは、検証器ガイドの推論における新しいパラダイムを示す重要な成果です。