Goedel-Code-Prover: オープンな最先端コード検証の階層的証明探索

要旨: 大規模言語モデル（LLMs）はもっともらしいコードを生成できるが、その正確性の保証には限界がある。
実装が仕様を満たすことを形式的に検証するには、機械で検証可能な証明を構築する必要があり、それは現在の自動化能力を超える作業である。
Lean~4 における自動コード検証のための階層的証明探索フレームワークを提案する。複雑な検証目標を、戦術レベルの証明を試みる前に、構造的により単純なサブゴールへ分解する。
本手法の核心は、建設的正当化と構造的有効性を組み合わせた原理的な分解スコアである。
特に、このスコアは学習報酬と推論時のランキング基準の双方として機能し、最適化と実運用の間の厳密な整合性を保証する。
私たちは Goedel-Code-Prover-8B を、分解と完遂の両方のための単一の統一ポリシーとして、教師付き初期化を経てハイブリッド強化学習を行い、連続的な分解報酬が計画探索を駆動する一方、教師付きリプレイが証明生成を安定させる。
Leanベースのコード検証ベンチマーク3つ、計427タスクを含む。私たちの8Bパラメータモデルは62.0%の証明成功率を達成し、最も強力なベースラインより2.6倍の改善を示し、最大で84倍大きいニューラル証明器を超える。
さらに、推論時のスケーリングは一貫して観察される。探索繰り返し回数とサンプリング予算の増加に伴い成功率は単調に改善し、我々の訓練済みモデルは同規模の最前線の市販モデルよりも高い効率を達成する。