【論文瞬読】Seed-Prover: IMO 2025で5/6問を解いた自動定理証明AI

はじめに

関連する論文の解説は、こちらでも読めます。

こんにちは！株式会社AI Nestです。

今回は、数学界で大きな話題となった自動定理証明システム「Seed-Prover」について解説します。このシステムは2025年の国際数学オリンピック（IMO）で驚異的な成果を上げ、出題された6問中5問を完全に証明することに成功しました。これは人間の金メダリストレベルの成績であり、AIによる数学的推論の新たな可能性を示す画期的な成果です。

図1に示すように、自動定理証明の分野では近年急速な進歩が見られており、Seed-Proverは従来の最高性能を大幅に上回る99.6%という驚異的なスコアを達成しています。

自動定理証明の課題とLeanの役割

まず、なぜ自動定理証明が難しいのかを理解しましょう。

従来のAIシステムは自然言語で数学的推論を行ってきましたが、これには大きな問題がありました。自然言語で書かれた証明は、各ステップが正しいかを自動的に、あるいは手動でさえ検証することが極めて困難だったのです。

そこで注目されているのが「Lean」という形式的証明言語です。Leanは数学的証明をコンピュータが理解できる形式で記述し、その正しさを自動的に検証できる強力なツールです。think of it as「数学の証明を厳密にチェックしてくれる超優秀な査読者」といったところでしょうか。

しかし、既存のLeanベースの証明システムにも課題がありました：

1. ステップレベル証明器：一行ずつコードを生成するが、高次元の推論が困難

2. 全証明生成器：証明全体を一度に生成するが、Leanコンパイラーとの相互作用が不足

Seed-Proverは、これらの問題を解決する革新的なアプローチを提案しています。

Seed-Proverの核心技術：補題スタイル証明

Seed-Proverの最大の特徴は「補題スタイル証明」という手法です。

図2を見ると、従来の手法（左側）では一つの大きな定理を直接証明しようとしていますが、Seed-Prover（右側）では複数の補題を先に証明してから、それらを組み合わせて最終的な定理を証明しています。

この手法の優れた点は：

• モジュール性：各補題は独立してコンパイル・保存・組み合わせが可能

• 進捗の可視化：どの補題が証明済みで、どれが未証明かが明確

• 再利用性：異なる推論経路からの補題を組み合わせて、より難しい問題に対処可能

例えば、複雑な関数方程式を解く際、「この関数は単射か？」「全射か？」「単調性はあるか？」といった性質を補題として先に調べ、それらを組み合わせて最終的な解を導き出すイメージです。

3段階の推論戦略：Light、Medium、Heavy

Seed-Proverは計算リソースと問題の難易度に応じて、3つの推論戦略を使い分けます。

Light設定（1-2時間で完了）

• 8-16回まで証明を反復的に改良

• Leanコンパイラーのフィードバックと自己要約を活用

• 比較的簡単な問題に適用

Medium設定（より複雑な問題向け）

• 外部改良プロセス：メイン問題の証明を改良

• 内部改良プロセス：証明できなかった難しい補題を個別に処理

• 1000行を超える長大な証明も扱える

Heavy設定（数日間の思考）

• 最初に5000個もの予想を生成

• 各予想をLight設定で証明・反証を試みる

• 証明された補題をプールに蓄積

• 最終的に数百の最も有用な補題を選択してMedium設定で最終証明

この段階的アプローチにより、IMO 2017 P2（難易度MOHS=40）やIMO 2025の複数の問題を解決することができました。

Seed-Geometry：幾何学問題への特化システム

Leanは代数的な問題には強いものの、幾何学問題のサポートが不十分でした。そこでSeed-Proverチームは、専用の幾何学推論エンジン「Seed-Geometry」を開発しました。

Seed-Geometryの特徴：

1. 拡張された専用言語：定規とコンパスによる作図を効率的に表現

2. 超高速推論エンジン：C++で書き直され、約100倍の高速化を実現

3. 大規模な問題生成：2億3000万個のユニークな幾何学問題を生成

4. 分散並列処理：複数のGPUプロセスで効率的な探索を実行

実験結果では、IMO幾何学問題（2000-2024年）でAlphaGeometry 2と同等以上の性能を示し、より困難なIMOショートリスト問題では22/39問を解決（AlphaGeometry 2は19/39問）という優秀な成績を収めました。

特筆すべきは、IMO 2025 P2（幾何学問題）をわずか2秒で解決したことです。

圧倒的な実験結果

Seed-Proverの実験結果は圧倒的です：

• 過去のIMO問題：78.1%の成功率（121/155問）

• MiniF2F-test：99.6%（従来最高92.2%）

• PutnamBench：331/657問（従来最高86/657問）

• CombiBench：30.0%（従来最高10.0%）

特に注目すべきは、IMO 2025での実際の成果です：

• 問題2：Seed-Geometryが瞬時に解決

• 問題5：Medium設定で証明

• 問題1、3、4：Heavy設定で証明（問題1は締切後に完成）

この成果により、Seed-Proverは人間の金メダリストレベルの数学的推論能力を持つことが実証されました。

技術的な改良点

Seed-Proverの成功を支える技術的改良には以下があります：

1. 多段階・多タスク強化学習：VAポリシー最適化を採用

2. 多様なプロンプト戦略：自然言語ヒント、類似補題、失敗事例などを組み合わせ

3. LooKeng：Leanとの効率的な相互作用を可能にするPythonインターフェース

これらの技術により、従来手法では不可能だった長時間の深い推論と、幅広い問題空間の探索が可能になりました。

まとめ

Seed-Proverは、補題スタイル証明と3段階の推論戦略により、自動定理証明の分野で画期的な進歩を達成しました。IMO 2025での5/6問正解という成果は、AIが人間レベルの数学的推論能力を獲得しつつあることを示す重要なマイルストーンです。

この研究の意義は単なる性能向上にとどまりません。形式的証明言語と大規模言語モデルの組み合わせにより、将来的には未解決の数学的予想への挑戦も視野に入ってきます。数学研究の新たな可能性を開く、非常に興味深い成果と言えるでしょう。

形式的検証による明確なフィードバックと長い思考連鎖の組み合わせが、いかに強力な推論システムを生み出すかを実証した本研究は、AI研究者だけでなく、数学者にとっても注目すべき成果です。

読んだ論文をあとで見返しやすく整理したい人や、チームで共有したい人には、論文管理サービス「スカコン」もおすすめです。研究論文を書く人向けの整理・蓄積にもかなり相性がいいです。