国際数学オリンピックにおけるAI: AlphaProofとAlphaGeometry 2が銀メダルレベルを達成した方法

数学的推論は、人間の認知能力の重要な側面であり、科学的発見と技術的進歩を促進しています。人間の認知能力に匹敵する汎用人工知能を開発するには、AIに高度な数学的推論能力を備えさせることが不可欠です。現在のAIシステムは基本的な数学問題を処理できますが、代数や幾何学などの高度な数学分野で必要な複雑な推論に苦労しています。しかし、この状況は変化しつつあり、Google DeepMindは、AIシステムの数学的推論能力を向上させるための重要な成果を達成しました。このブレークスルーは、国際数学オリンピック (IMO) 2024で達成されました。1959年に設立されたIMOは、最も古くて最も権威のある数学競技会であり、世界中の高校生に、代数、組合せ論、幾何学、数論の問題を出題しています。毎年、若い数学者のチームが6つの非常に難しい問題を解くために競争しています。この年、Google DeepMindは2つのAIシステムを導入しました。AlphaProofは形式的な数学的推論に焦点を当て、AlphaGeometry 2は幾何学的問題を解決することに特化しています。これらのAIシステムは6つの問題のうち4つを解決し、銀メダリストのレベルで実行しました。この記事では、これらのシステムがどのようにして数学的な問題を解決するのかを探ります。

AlphaProof: AIと形式言語を組み合わせた数学的定理の証明

AlphaProofは、Leanという形式言語を使用して数学的なステートメントを証明するAIシステムです。Geminiという事前学習済み言語モデルと、AlphaZeroという強化学習アルゴリズムを統合しています。

Geminiモデルは、自然言語の問題文を形式的なものに翻訳し、さまざまな難易度レベルの問題のライブラリを作成します。これは2つの目的を果たします。自然言語の不正確さを形式言語の精度に変換し、Geminiの予測能力を使用して形式言語の精度で可能な解決策のリストを生成することです。

AlphaProofが問題に遭遇すると、潜在的な解決策を生成し、Leanで証明ステップを検索してそれらを検証または反証します。これは、基本的にニューラルネットワークであるGeminiが自然言語の指示を形式言語であるLeanに翻訳してステートメントを証明または反証する、ニューロ・シンボリックアプローチです。AlphaZeroのセルフプレイメカニズムと同様に、AlphaProofは数学的なステートメントを証明することで自己を訓練します。各証明の試みは、AlphaProofの言語モデルを精錬し、成功した証明はモデルがより困難な問題に取り組む能力を強化します。

IMOでのAlphaProofの訓練は、さまざまな難易度レベルと数学のトピックを網羅する数百万の問題を証明または反証することで行われました。この訓練は、AlphaProofが問題に対する完全な答えを見つけるまで、競技中に継続されました。

AlphaGeometry 2: LLMとシンボリックAIを統合した幾何学的問題の解決

AlphaGeometry 2は、AlphaGeometryシリーズの最新バージョンであり、幾何学的問題をより高精度で効率的に解決するように設計されています。前身の基礎に基づいて、AlphaGeometry 2は、ニューラルネットワークの予測能力と形式論理を組み合わせるニューロ・シンボリックアプローチを採用しています。この統合により、幾何学的問題を解決するために不可欠な補助点を特定するために、ルールベースのロジックとニューラルネットワークの予測能力が組み合わされます。AlphaGeometryのLLMは、新しい幾何学的構成要素を予測し、シンボリックAIは形式論理を適用して証明を生成します。

幾何学的問題に直面したとき、AlphaGeometryのLLMはさまざまな可能性を評価し、問題を解決する上で重要な構成要素を予測します。これらの予測は、シンボリックエンジンが正確な推論に近づくための貴重なヒントとなります。この革新的なアプローチにより、AlphaGeometryは、従来のシナリオを超えた複雑な幾何学的課題に対処できます。

AlphaGeometry 2の重要な改善点の1つは、Gemini LLMの統合です。このモデルは、前身よりもはるかに多くの合成データで訓練されており、幾何学的問題、特に物体の動きや角度、比率、距離の式を含む問題に対処する能力が向上しています。さらに、AlphaGeometry 2には、2桁の速度で動作するシンボリックエンジンが搭載されており、代替解決策を以前よりも迅速に探索できます。これらの進歩により、AlphaGeometry 2は、複雑な幾何学的問題を解決するための強力なツールとなり、分野の新しい基準を設定しています。

IMOでのAlphaProofとAlphaGeometry 2

今年のIMOでは、参加者は6つのさまざまな問題に挑戦しました。2つの代数問題、1つの数論問題、1つの幾何学問題、2つの組合せ論問題です。Googleの研究者は、これらの問題をAlphaProofとAlphaGeometry 2のために正式な数学的言語に翻訳しました。AlphaProofは、2つの代数問題と1つの数論問題を解決し、今年の競技で5人の人間の参加者だけが解決した最も難しい問題を解決しました。一方、AlphaGeometry 2は幾何学の問題を成功裏に解決しましたが、2つの組合せ論の課題には対処しませんでした。
IMOの各問題は7点価値があり、合計42点になります。AlphaProofとAlphaGeometry 2は28点を獲得し、解決した問題で完全なスコアを獲得しました。これにより、銀メダルの上位レベルに達しました。今年の金メダルの基準は29点で、609人の参加者のうち58人が達成しました。

次の飛躍: 数学的課題のための自然言語

AlphaProofとAlphaGeometry 2は、数学的な問題を解決するAIの能力における重要な進歩を実証しました。ただし、これらのシステムはまだ、数学的な問題を形式言語に翻訳するために人間の専門家に依存しています。さらに、これらの特殊な数学的スキルが他のAIシステム、たとえば仮説の探索、革新的な解決策のテスト、時間のかかる証明の効率的な管理にどのように統合されるかは不明です。
これらの限界を克服するために、Googleの研究者は、Geminiと彼らの最新の研究に基づく自然言語推論システムを開発しています。この新しいシステムは、形式言語の翻訳を必要とせずに問題を解決する能力を向上させることを目的とし、他のAIシステムと無理なく統合されるように設計されています。

まとめ

AlphaProofとAlphaGeometry 2のIMOでのパフォーマンスは、AIが複雑な数学的推論に取り組む能力における重要な進歩です。両方のシステムは、6つの難しい問題のうち4つを解決し、銀メダルレベルのパフォーマンスを示しました。形式的証明と幾何学的問題の解決における重要な進歩を示しました。ただし、これらのAIシステムは依然として、問題を形式言語に翻訳するために人間の入力に依存しており、他のAIシステムとの統合に課題を抱えています。将来的には、これらのシステムをさらに強化し、数学的な課題のより広い範囲にわたる能力を拡大する可能性があります。