ひっそり登場の中国AI「Seed-Prover」、国際数学オリンピックで「金メダル」 さくっとGoogleを抜く：Innovative Tech（AI+）

[山下裕毅，ITmedia]

Innovative Tech（AI+）：

このコーナーでは、2014年から先端テクノロジーの研究を論文単位で記事にしているWebメディア「Seamless」（シームレス）を主宰する山下裕毅氏が執筆。新規性の高いAI分野の科学論文を山下氏がピックアップし、解説する。

X： ＠shiropen2

　中国ByteDanceに所属する研究者らが発表した論文「Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving」は、国際数学オリンピック（IMO）で金メダル相当のパフォーマンスを獲得したAI推論モデル「Seed-Prover」を提案した研究報告だ。

　AIにおける数学レベルを評価する場合、国際数学オリンピックが用いられるケースが多い。2月には、Google DeepMindが開発したAIシステム「AlphaGeometry2」（AG2）が幾何学問題で金メダル相当を獲得した。またOpenAIも7月、2025年国際数学オリンピックで金メダルレベルのパフォーマンスを達成したと報告している。

　今回提案された自動定理証明システム「Seed-Prover」は、2025年国際数学オリンピックで6問中5問の完全証明に成功し、人間の金メダリストに匹敵する実力を示した。2025年だけでなく、過去の国際数学オリンピック問題においても78.1％という高い証明成功率を達成している。

　標準的なベンチマークテストでも卓越した性能を発揮している。形式的数学オリンピック問題集である「MiniF2F」では、検証セットで100％、テストセットで99.6％という、ほぼ完璧な成績を記録。これは従来の最高記録92.2％を大きく上回る結果だ。

MiniF2Fのスコア結果

　米国の大学生向け数学競技会である「PutnamBench」では657問中331問（50.4％）の証明に成功した。これは、前回の最高記録である86問の約4倍という改善である。

　幾何学問題においては、Seed-Proverと幾何学専用の推論エンジン「Seed-Geometry」を組み合わせて挑戦している。GoogleのAIモデル「AlphaGeometry2」を上回る性能を示し、国際数学オリンピックの幾何問題50問中43問を解決した。特筆すべきは、2025年国際数学オリンピックの幾何問題をわずか2秒で証明したことだ。

　C++で書き直された推論エンジンは、従来のPython実装と比べて約100倍の高速化を実現し、2億3000万個以上の幾何学問題データベースを構築している。

　Seed-Proverのアプローチは、人間の数学者のように、まず有用な中間的な補題を生成し、それらを組み合わせて主定理を証明する手法を採用。技術面では、Leanというプログラミング言語を活用し、証明の正しさを自動的に検証できる仕組みを構築している。

Lean 4における全体証明と補題形式の証明の例

Source and Image Credits: Chen, Luoxin, et al. "Seed-Prover: Deep and Broad Reasoning for Automated Theorem Proving." arXiv preprint arXiv:2507.23726（2025）.