AI-Papers
- 補題の依存グラフ（ブループリント）を生成・並列証明・洗練する3フェーズで、Lean 4による形式証明を効率化する新アーキテクチャ
- MiniF2F-testで99.2%、PutnamBenchで75.6%を達成し、2025年の国際数学オリンピック（IMO）の6問中4問を形式的に証明
- オープンウェイトDeepSeek-V4-Flashを使用し、全PutnamBench（672問）を約294ドルで解答。類似パイプラインと比べて最大500倍のコスト削減を達成
研究の背景
数学の定理を形式的に証明するAI研究は、近年めざましい進歩を遂げています。「形式証明」とは、定理の正しさをLean 4などの証明支援系（コンピュータが厳密に検証できる専用言語）で記述したものです。人間が書いた証明をAIが自動的に形式化・検証できれば、数学教育やソフトウェア検証など幅広い分野への応用が見込めます。
一方、既存のアプローチには課題がありました。問題を再帰的にサブゴールへ分解する方式では証明の全体戦略を俯瞰しにくく、部分的な失敗を活かして方針を修正することも困難です。計算コストが高いため、実用的なスケールでの運用にも壁がありました。
ブループリント生成と洗練
Goedel-Architectが提案するのは「ブループリント」を中心に据えたアーキテクチャです。ブループリントとは、定理の証明に必要な補題（証明の途中で使う小さな命題）をノードとし、ノード間の矢印が依存関係を表す有向グラフを指します。グラフ全体を一括して設計することで、局所的な分解では見えにくい証明戦略の全体像を扱えます。
証明プロセスは次の3フェーズで進みます。
- ブループリント生成: 定理から補題の依存グラフ全体を設計する
- 並列証明: Lean 4コンパイラとMathlib（数学ライブラリ）の検索ツールを使いながら、各補題を並列に証明する
- ブループリント洗練: 失敗した補題の診断を基にグラフ全体を更新する
証明に失敗した補題は、その原因を「命題が偽である」か「証明が難しすぎる」かで分類し、その診断が次の洗練フェーズの入力になります。
このサイクルを繰り返す間、既に証明済みのノードはそのまま保持されます。また、人間が書いた自然言語の証明スケッチをオプションのガイドとして取り込む機能も備えており、解法のヒントがある場合はそれを活用できます。
実験結果と性能比較
Goedel-Architectは複数の数学ベンチマークで最先端の成績を記録しました。競技数学の標準ベンチマーク「MiniF2F-test」では99.2%（pass@11）を達成し、自然言語ガイダンスを加えると100%に達します。主な結果は次の表のとおりです。
ベンチマーク | pass@11 | 自然言語ガイダンスあり |
|---|---|---|
MiniF2F-test | 99.2% | 100% |
PutnamBench（672問） | 75.6% | 88.8%（pass@44+NL） |
IMO 2025 | 6問中4問（P1・P3・P4・P5） | |
Putnam 2025 | 12問中11問 | |
USAMO 2026 | 6問中3問 | |
IMO 2025のP5については、自然言語ガイダンスなしで解決しています。一方でP2は「汎用Lean証明器では扱いにくい幾何問題」として未解決のまま課題に残されました。
コスト効率の革新
Goedel-Architectはオープンウェイト（公開重みモデル）のDeepSeek-V4-Flash（2840億パラメータの混合エキスパートモデル）をバックボーンとして使用しています。PutnamBench全672問への回答コストは合計約294ドル、1問あたり約0.44ドルでした。
対して同じDeepSeek-V4-Flashを使うツール統合型エージェントのベースラインでは、1問あたり最大1億トークン分のコスト（約244ドル）かかるケースがあり、Goedel-Architectとの差は最大500倍に上ります。自己進化型LLMエージェントによる自動アルゴリズム発見のように、AIの自律的な問題解決においてコスト効率は実用化を左右する条件です。既に証明済みのノードを保持し、失敗した補題だけを再処理するブループリント設計が、この大幅な効率化を支えています。
まとめと今後の展望
Goedel-Architectは、ブループリントによる補題の依存グラフ設計と並列証明・洗練のサイクルを組み合わせることで、Lean 4形式証明の精度とコスト効率を大きく向上させました。IMO 2025の4問解決は、AIによる形式的な数学証明が競技数学のレベルに達しつつあることを示す成果といえます。
今後の課題としては、幾何問題への対応強化と、自然言語ガイダンスへの依存を減らした自律的な証明能力の向上が挙げられています。形式証明技術の実用化が進めば、数学の自動検証や証明支援ツール、さらにはソフトウェアの正確性保証といった分野へ応用が広がるでしょう。
論文情報: "Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinement"（Jui-Hui Chung et al., 2026） arXiv:2606.06468, CC BY 4.0
本記事の図（図1〜図2）とサムネイルは上記論文より引用しています（縮小・形式変換あり）。
