Google、数学の難問を解くAI「AlphaProof」「AlphaGeometry 2」を発表 国際数学オリンピックで「銀メダル」レベルに到達：数学の推論における新たなステップ

Google DeepMindは数学の難問を解くために構築されたAIシステム「AlphaProof」「AlphaGeometry 2」を発表した。2024年に開催された国際数学オリンピックの問題を基に能力を測定した結果、銀メダル水準のレベルに到達したという。

[＠IT]

　GoogleのAI（人工知能）部門であるGoogle DeepMindは2024年7月25日（米国時間）、数学の難問を解くために構築されたAIシステム「AlphaProof」「AlphaGeometry 2」を発表した。

　Google DeepMindによると、これらのAIシステムを組み合わせることで、2024年に開催された国際数学オリンピック（IMO）で出題された6つの問題の内、4つを解き、「AIシステムが銀メダル水準のレベルに初めて到達した」としている。

2024年のIMOにおけるAlphaProofやAlphaGeometry 2を組み合わせたAIシステムと競技参加者とのパフォーマンス比較。42ポイント中、28ポイントを獲得して銀メダリストと同等のレベルを達成したという（提供：Google DeepMind）

　Google DeepMindは「AlphaProofは、2024年のIMOで出題された2つの代数問題と1つの整数論の問題を解いた。これらにはわずか5人しか解けなかった難問も含まれていた。AlphaGeometry 2は幾何学の問題を証明したが、2つの組み合わせ論の問題は解けなかった」と述べている。

　Google DeepMindによると、AlphaProofやAlphaGeometry 2の回答を採点したティモシー・ガワーズ氏（ケンブリッジ大学教授、IMO金メダリストでフィールズ賞受賞者）は「このプログラムが簡単には思い付かない解法を発見できるという事実は非常に印象的であり、現在の技術水準をはるかに超えている」と評価しているという。

　Google DeepMindはAlphaProofやAlphaGeometry 2について、次のように紹介している。

AlphaproofとAlphaGeometry 2とは　どのように学習させ、構築したのか

AlphaProof

　AlphaProofは、同社の「AlphaZero」の強化学習アルゴリズムと、事前学習済み言語モデルを組み合わせて構築された自己学習可能なAIシステムだ。数学的命題を証明するために、定理証明に特化したプログラミング言語「Lean」を活用している。Leanのような言語を使用することで、数学的推論を含む証明が本当に正しいかどうかを機械的に検証できるという。

　一方で、構築に当たっては、人間が記述した証明に関するデータ量が乏しく機械学習での応用が難しいという課題や、自然言語ベースのアプローチに頼る場合、データ量が桁違いに多くなるものの、誤った推論ステップや解答をもっともらしく生成するリスクもあった。そこで、この2つの問題を解決するために、GoogleのAIモデルである「Gemini」をファインチューニングし、自然言語の問題文を自動的に形式化された命題に翻訳し、難易度の異なる形式化された問題を集めた大規模なライブラリを作成したという。

　AlphaProofは問題が提示されると解答の候補を生成し、Leanで検証しながら証明または反証する。見つかった証明は、AlphaProofの言語モデルを強化し、難しい問題を解決させる能力の向上につながる。難易度や数学の分野が異なる何百万もの問題を数週間にわたり証明また反証させることでAlphaProofを訓練したという。

　「このトレーニングプロセスはIMOの競技中にも適用され、自己生成した問題の変種を証明し続けることで、完全な解答を見つけるまで強化された」とGoogle DeepMindは述べている。

AlphaProofの強化学習トレーニングプロセスの可視化イメージ（提供：Google DeepMind）

AlphaGeometry 2

　AlphaGeometry 2は、複雑な幾何学の問題を解くことに特化したAIシステム「AlphaGeometry」の改良バージョンだ。Geminiを活用し、前世代よりも桁違いに多くの合成データでゼロからトレーニングされている。

　AlphaGeometry 2では、前世代より2桁高速なシンボリックエンジン（数式や記号を扱うための計算システム）を採用している。また、問題が提示されると、新しい知識共有メカニズムを使用して、異なる検索木を高度に組み合わせる。これにより、物体の移動や角度、比率、距離の方程式に関する問題など、幾何学の難問を解くことができるという。

　過去25年間のIMOで出題された幾何学問題の正答率が前世代では53％だったのに対し、AlphaGeometry 2は83％だった。2024年のIMOで出題された「問題4」を、19秒で解くこともできたという。

AlphaGeometry 2が19秒で解いた「∠KILと∠XPYの和が180度に等しいことを証明せよ」という問題4の図。AlphaGeometry 2は、∠AEB＝90度となるように直線BI上の点Eを構成することを提案したという。点EはABの中点Lに目的を与えるのに役立ち、結論を証明するのに必要な△ABE〜△YBIや△ALE〜△IPCのような多くの相似三角形の組を作る（提供：Google DeepMind）

数学の推論における新たなステップ

　Google DeepMindは、研究の一環として、Geminiと最新の研究を基に構築された自然言語推論システムも試験している。このシステムでは数学の問題を形式的な言語に翻訳する必要がなく推論可能で、他のAIシステムと組み合わせることもできるという。このアプローチを2024年のIMO問題に対してテストした結果、非常に有望な結果が得られたとしている。

　Google DeepMindは「数学者がAIツールと協力して仮説を探求し、大胆な新しいアプローチで長年の問題を解決し、証明で時間のかかる過程を迅速化できる未来や、GeminiのようなAIモデルが数学の推論においてさらに有能になる未来に、非常に期待している」と述べている。