論文「Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verification」の技術的サマリー

本論文は、大規模言語モデル（LLM）を用いたコードの形式的検証（Formal Verification）における課題を解決し、Lean 4 環境下で自動証明を可能にする新しい階層的証明探索フレームワーク「Goedel-Code-Prover」を提案するものです。

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

---

1. 背景と問題定義

背景

LLM はコード生成において高い性能を示していますが、生成されたコードの論理的な正しさを保証する能力は限られています。テストやリプロダクションスクリプトでは、微妙な論理エラーや境界条件の違反を検出できないため、安全性が重要な環境では「動くように見えるコード」と「証明可能な正しいコード」のギャップを埋めることが急務です。

既存手法の限界と課題

数学的な定理証明における LLM の成功（IMO レベルの性能など）は、コード検証には直接適用できません。その理由は以下の 3 つの根本的なミスマッチにあります。

1. 根拠のない分解（Ungrounded Decomposition）:
   • 数学では、教科書や論文の膨大なテキストデータから「証明の分解」の直感を LLM が学習できます。
   • しかし、コードの正しさに関する自然言語の記述（「なぜこのコードが正しいか」の論理的な説明）はほとんど存在しません。開発者は形式証明ではなくテストを重視するため、LLM はコード検証において意味の通じない、あるいは単純化されていない部分目標（サブゴール）を提案しがちです。
2. 概念の増殖（Concept Proliferation）:
   • 数学では Mathlib などの共有ライブラリが豊富なレマ（補助定理）を提供しますが、コード検証では各プログラムが独自の制御フロー、データ構造不変条件、計算動作を持ちます。
   • 既存のライブラリに依存できず、証明のたびに新しい概念の性質をゼロから発見・証明する必要があります。
3. 戦術（Tactic）の分布シフト:
   • 数学証明は代数的な正規化（linarith など）に依存しますが、コード検証は離散ドメイン（リスト、ビットベクトル、再帰など）を扱います。
   • これには grind や native_decide（計算反射）など、数学とは異なる専用自動化ツールが必要であり、数学データで訓練されたモデルはこれらを適切に使用できません。

---

2. 提案手法：Goedel-Code-Prover

本論文は、複雑な検証目標を構造的に単純な部分目標に分解し、その後で戦術レベルの証明を行う「階層的証明探索」フレームワークを提案します。

2.1 階層的証明探索の仕組み

フレームワークは 2 つの段階で構成されます（図 2 参照）：

1. 再帰的レマ分解（Recursive Lemma Decomposition）:
   • 上位の検証目標を、構造的に単純な複数の中間レマ（サブゴール）に再帰的に分解します。
   • 各ステップで LLM が候補を提案し、それらが親定理を論理的に導くか、かつ実証的に矛盾しないかを検証します。
2. 反復的レマ完成（Iterative Lemma Completion）:
   • 分解された葉ノード（Leaf Lemmas）に対して、同じポリシーが反復的に戦術（Tactic）を生成し、Lean コンパイラからのフィードバックに基づいて証明を修正・完成させます。

2.2 分解スコア（Decomposition Score）

この手法の中核となるのは、分解スコアです。これはトレーニング時の報酬と推論時のランキング基準の両方として機能し、最適化とデプロイの厳密な整合性を保ちます。

スコア $S$ は以下の 2 つの軸を組み合わせて計算されます：

• 構成的正当性（Constructive Justification）:
  • 提案されたレマ群が親定理を論理的に導くか（証明再構成による検証）。
  • 各レマが quickcheck（自動反例探索）によって反証されないか（意味的な妥当性のフィルタリング）。
• 構造的効果（Structural Effectiveness）:
  • 分解によって目標の複雑さが減少するか。
  • 複雑さの指標として、AST（抽象構文木）における演算子のフットプリント（operator footprint）（論理演算子やドメイン固有演算子の総数）を定義し、分解後の最大サブゴールの複雑さが元の目標より小さくなることを評価します。

スコア計算式：
$$S = r(\{L_i\}; G) \cdot v(\{L_i\}; G)$$
ここで、$v$ は有効性（0 または 1）、$r$ は構造的削減率です。

2.3 学習パイプライン（ハイブリッド強化学習）

分解と完了の両方を単一の統一ポリシー（Goedel-Code-Prover-8B）で行うため、以下のハイブリッド RL アプローチを採用しています。

1. 教師あり微調整（SFT）:
   • 最先端モデル（GPT-5.2, Gemini-3-Flash）から生成された分解と完了の軌跡データを用いて初期化。
2. ハイブリッド強化学習（Hybrid RL）:
   • 分解の最適化: 連続的な分解スコア $S$ を報酬として使用し、GRPO（Group Relative Policy Optimization）で探索を促進。
   • 完了の安定化: 証明成功/失敗というスパースなバイナリ信号に依存せず、高品質な証明軌跡の教師あり再生（Supervised Replay）を用いて安定性を確保。
   • これにより、分解の勾配が支配的になるのを防ぎ、両タスクのバランスを保ちます。

---

3. 主要な貢献

1. 階層的証明探索フレームワーク: Lean 4 におけるコード検証のために、複雑な目標を構造的に単純なサブゴールに分解する新しいアプローチを提案。
2. 原則的な分解スコア: 構成的正当性と構造的単純さを組み合わせたスコアを、トレーニング報酬と推論時の探索基準として一貫して使用。
3. ハイブリッド RL パイプライン: 単一ポリシー内で分解と完了を共同学習し、構造的な探索と安定した証明生成のバランスを実現。
4. 大規模な評価: 3 つのベンチマーク（Verina, Clever, AlgoVeri）において、8B パラメータのモデルが 84 倍大きい既存のニューラルプロバーや最先端モデルを凌駕する性能を示した。

---

4. 実験結果

3 つの Lean ベースのコード検証ベンチマーク（合計 427 タスク）で評価を行いました。

• 全体性能:
  • 提案モデル（Goedel-Code-Prover-8B）の証明成功率は 62.0%。
  • 最強のベースライン（BFS-Prover-V2-32B など）と比較して 2.6 倍 の改善。
  • 84 倍大きいモデル（DeepSeek-Prover-V2-671B など）を上回る性能。
  • ベンチマーク別成績：Verina (68.8%), Clever (54.0%), AlgoVeri (62.3%)。
• 推論時のスケーリング:
  • 探索反復数や並列サンプリング数（pass@k）を増やすと、成功率が単調に向上し、飽和の兆候が見られませんでした。
  • 分解スコアが高い候補ほど、証明成功の可能性が高いことを示し（AUROC = 0.903）、スコアに基づく探索が有効であることを確認。
• アブレーション研究:
  • 分解機能と完了機能の両方を学習させた場合、個別の改善の合計以上の相乗効果が得られました。
  • 特に「階層的分解」が最も重要な設計選択であることが示されました。
• 証明の深さ:
  • 平均して 8〜17 の補助レマと 130 行以上の証明コードを生成し、最も複雑なケースでは 680 行を超える証明を成功させました。

---

5. 意義と結論

本論文は、LLM を用いたコードの形式的検証において、数学的な定理証明とは異なる課題（概念の増殖、戦術の分布シフト、学習データの欠如）を克服するための有効な解決策を示しました。

• 実用的意義: 8B という比較的小さなモデルで、最先端の巨大モデルを上回る性能を発揮することで、計算コストを抑えた実用的なコード検証システムの構築が可能になりました。
• 理論的意義: 「分解スコア」を介して、トレーニングと推論を厳密に整合させるアプローチは、報酬のスパース性という強化学習の課題を解決する新しいパラダイムを提供しています。
• 将来展望: 現在は Lean 形式化済みのコードが前提ですが、自然言語の仕様からの自動翻訳や、より大規模なコードベースへの拡張が今後の課題です。

総じて、Goedel-Code-Prover は、LLM が「動くコード」から「証明可能なコード」への橋渡しを実現する重要なステップであり、安全クリティカルなシステム開発における形式的検証の普及に寄与すると期待されます。