Google DeepMindはAlphaProofを開発しました。このAIシステムは2024年の国際数学オリンピックで銀メダル相当のパフォーマンスを達成し、42点中28点を獲得しました。このシステムは、世界で最も名高い学部レベルの数学競技会で金メダルまであと1点及ばずでした。この画期的な成果は、AIの複雑な数学的証明を扱う能力の進歩を示しています。
コンピュータは長らく計算に優れていますが、高度な数学に必要な論理的推論には苦労してきました。Google DeepMindの新しいAI、AlphaProofはこれを解決し、2024年の国際数学オリンピック（IMO）で銀メダル相当のパフォーマンスを達成しました。これは高校レベルのトップ数学競技会です。IMOには各7点の6問の問題があり、合計42点でした。金メダルには29点以上が必要で、609人の参加者のうち58人が達成しました。一方、銀メダルは22〜28点で、123人が受賞しました。AlphaProofは28点を獲得し、4問を独立して解いて21点を得て、幾何学の問題では専門のAlphaGeometry 2に頼って銀レベルに到達しました。
AlphaProofの開発は、形式的な数学証明のための限られたトレーニングデータの克服から始まりました。チームはLeanソフトウェアを使用し、これは正確な数学的定義と検証のためのツールです。データセットを拡大するため、Gemini大規模言語モデルを訓練して自然言語の数学的記述をLeanに翻訳し、約8,000万の形式化された記述を生成しました。DeepMindの研究者で筆頭著者のThomas Hubert氏は、「形式言語で作業する主な難しさは、データが非常に少ないことです」と説明しました。不完全さにもかかわらず、「近似翻訳を活用する方法はたくさんあります」と彼は付け加えました。
システムのアーキテクチャはDeepMindのAlphaZeroから着想を得ており、試行錯誤で訓練されたニューラルネットワークと、証明経路を探るツリー検索アルゴリズムを組み合わせています。正しい証明を報酬し、非効率なステップを罰することで、洗練された解決策を促進します。新機能として、テスト時強化学習（TTRL）が追加され、AlphaProofは難しい問題の変種を生成して即時訓練が可能で、人間の問題解決を模倣します。「私たちはこのゲームを試行錯誤で学ぼうとしていました」とHubert氏は述べました。
しかし、AlphaProofはLeanで問題を形式化するために人間の支援を必要とし、各難問に数日かかり、数百TPU-日を消費しました。これは人間のセッションあたり4.5時間の制限をはるかに超えています。最も難しい問題を解いた人間は6人だけで、AlphaProofは7番目でした。DeepMindは高い計算コストを認めていますが、より広範な使用のための最適化を目指しています。「数学競技会で止まるつもりはありません。研究レベルの数学に本当の貢献ができるAIシステムを構築したいのです」とHubert氏は述べました。チームは信頼できるテスター向けプログラムを計画し、AlphaProofツールを数学者と共有します。
この研究は2025年のNature論文に詳述されています（DOI: 10.1038/s41586-025-09833-y）。