Goedel-Architectとは？ブループリントでIMO 2025の4問を形式証明

補題の依存グラフ（ブループリント）を生成・並列証明・洗練する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%に達します。

大学入試相当の難問集「PutnamBench」（672問）ではpass@11で75.6%、自然言語証明スケッチを組み合わせると88.8%まで向上します。さらに2025年の国際数学オリンピック（IMO）では6問中4問（P1・P3・P4・P5）をLean 4で形式的に証明し、P5については自然言語ガイダンスなしで解決しています。Putnam 2025では12問中11問、USAMO 2026では6問中3問の成績も残しています。P2については「汎用Lean証明器では扱いにくい幾何問題」として未解決のまま課題として残されています。

図1: PutnamBenchにおけるブループリント洗練の繰り返し回数と解決問題数の関係。洗練を重ねるごとに解決数が対数的に増加し、16回の洗練でpass@11が75.6%（508問）、pass@44+NLで88.8%（597問）に達する。

コスト効率の革新

Goedel-Architectはオープンウェイト（公開重みモデル）のDeepSeek-V4-Flash（2840億パラメータの混合エキスパートモデル）をバックボーンとして使用しています。PutnamBench全672問への回答コストは合計約294ドル（1問あたり約0.44ドル）でした。

対して同じDeepSeek-V4-Flashを使うツール統合型エージェントのベースラインでは、1問あたり最大1億トークン分のコスト（約244ドル）かかるケースがあり、Goedel-Architectとの差は最大500倍に上ります。自己進化型LLMエージェントによる自動アルゴリズム発見のように、AIの自律的な問題解決においてコスト効率は実用化の重要な条件です。既に証明済みのノードを保持し、失敗した補題だけを再処理するブループリント設計がこの大幅な効率化を支えています。