シルバーからゴールドへ: DeepMindのAIが数学オリンピックを制した方法

DeepMindのAIは、わずか1年間で数学的推論において驚くべき進歩を遂げました。2024年に国際数学オリンピック（IMO）で銀メダルを獲得した後、2025年には金メダルを獲得しました。この急速な進歩は、複雑で抽象的な問題に対処するために人間のような創造性と洞察力が必要な分野で、人工知能の能力が急速に成長していることを強調しています。この記事では、DeepMindがこの変革をどのように達成したか、その背後にある技術的および戦略的な選択肢、およびこれらの進歩のより広範な意味について説明します。

IMOの重要性

国際数学オリンピックは、1959年に設立され、世界中で最高の数学競技会として認識されています。毎年、世界中から集まったトップ学生が、代数、幾何、数論、組み合わせ論の6つの問題に挑みます。これらの問題を解くには、単に計算するだけでなく、真正の数学的創造性、厳密な論理的思考、優雅な証明の構築が必要です。

2024年の銀メダルブレイクスルー

2024年、DeepMindは、IMOレベルの問題に取り組むために2つのAIシステム、AlphaProofとAlphaGeometry 2を導入しました。両方のシステムは、”神経記号的” AIの例であり、大規模言語モデル（LLM）と記号論理の強みを組み合わせています。

AlphaProofは、Leanという形式的な数学言語を使用して数学的ステートメントを証明するように設計されました。Gemini、DeepMindの大規模言語モデルと、AlphaZero、ボードゲームで成功を収めた強化学習エンジンを組み合わせました。この設定では、Geminiの役割は、自然言語の問題をLeanに翻訳し、論理的なステップを生成して証明を試みることでした。AlphaProofは、さまざまな数学的分野と難易度のサンプル問題に基づいて訓練され、AlphaZeroと同様に、ゲームを自分自身でプレイすることで学習しました。

AlphaGeometry 2は、幾何学の問題を解決するために設計されました。ここで、Geminiの言語理解により、AIが有用な補助的な構成を予測でき、記号論理エンジンが論理的な推論を管理しました。このハイブリッドアプローチにより、AlphaGeometryは、従来の機械的推論の範囲を超えた幾何学的問題に取り組むことができました。

これらのシステムは、6つのIMO問題のうち4つを解決しました。2つは代数、1つは数論、1つは幾何学で、42点中28点を獲得しました。これは、AIが初めてIMOで銀メダルレベルに達したことになります。しかし、この成功は、問題を形式的な数学言語に翻訳するために人間の専門家に大きく依存していました。また、各問題の処理に数日間の計算リソースが必要でした。

ゴールドメダルを獲得した技術的革新

DeepMindの銀メダルからゴールドメダルへの移行は、数々の重要な技術的改善によって推進されました。

1. 証明のための自然言語

最も重要な変更は、専門家が形式的な言語に翻訳する必要があるシステムから、自然言語を証明の媒体として扱うシステムへの移行でした。これは、Deep Think機能を備えたGeminiの強化版を介して実現されました。問題をLeanに変換するのではなく、モデルはテキストを直接処理し、非公式のスケッチを生成し、内部で重要なステップを形式化し、洗練された英語の証明を生成します。人間のフィードバックからの強化学習（RLHF）は、論理的に一貫性があり、簡潔で、提示された解決策を報酬しました。
Gemini Deep Thinkは、パブリックバージョンのGeminiと2つの重要な点で異なります。まず、Gemini Deep Thinkは、クエリごとにより長いコンテキストウィンドウとより多くの計算トークンを割り当て、モデルが複数ページの思考を維持できるようにします。2つ目は、並列推論を使用し、数百の推測的なスレッドがさまざまな潜在的な解決策のために生成されます。軽量の監督者は、最も約束のあるパスをランク付けして推進し、モンテカルロ木探索の概念を借用し、それをテキストに適用します。このアプローチは、人間のチームがアイデアをブレインストーミングし、非生産的なアイデアを却下し、優雅な解決策に収束するのと同じです。

2. 訓練と強化学習

Gemini Deep Thinkの訓練には、モデルを次のステップを予測するように微調整することが含まれました。 この目的のために、100,000の高品質のオリンピアードと大学のコンテストの解決策のコーパスが作成されました。 コーパスは、主にパブリックマスフォーラム、arXivのプレプリント、および大学の問題セットから収集されました。 人間のメンターは、訓練例をレビューして、非論理的または不完全な証明をフィルタリングしました。 強化学習により、モデルがコンパクトで正確な証明を生成するように導かれました。 初期バージョンは冗長な証明を生成しましたが、冗長なフレーズへのペナルティにより、出力をトリミングすることができました。
従来の微調整とは異なり、フィードバックが二値（証明が正しいかどうか）であるため、報酬が希薄になることが多い。DeepMindは、各検証された部分定理が全体のスコアに貢献するステップごとの報酬システムを実装しました。 この報酬メカニズムは、完全な証明がまれである場合でも、Geminiを導きます。 訓練プロセスは3ヶ月間にわたり、約2500万のTPU時間を使用しました。

3. 大規模な並列化

並列化も、DeepMindの銀メダルからゴールドメダルへの進歩に重要な役割を果たしました。 各問題は、リソースが動的により約束のあるアベニューにシフトされるように、並列に複数の推論ブランチを生成しました。 このダイナミックスケジューリングは、特に組み合わせ論の問題には、解決空間が大きいという点で特に有益でした。 このアプローチは、人間が完全な帰納法にコミットする前に補助的な不等式をテストする方法と似ています。 このテクニックは計算コストが高かったですが、DeepMindのTPU v5クラスターを使用することで管理可能でした。

2025年のDeepMind

競技の完全性を維持するために、DeepMindは、公式の問題が訓練セットに漏洩しないように、IMOの3週間前にモデルの重みを凍結しました。 また、以前未発表のオリンピアード問題の解決策を含むデータをフィルタリングしました。

競技中、Gemini Deep Thinkは、インターネットへのアクセスなしに、6つの公式問題をプレーンテキスト形式で提供されました。 システムは、標準的なラップトップの計算能力をシミュレートするように構成されたクラスターで動作しました。 全体の問題解決プロセスは、3時間以内に完了し、時間制限内で完了しました。 生成された証明は、変更せずにIMOの調整者に提出されました。

Gemini Deep Thinkは、最初の5つの問題で完全なスコアを獲得しました。 最終問題は、人間の参加者の94％と同様に、AIを難渋させた、挑戦的な組み合わせ論のパズルでした。 それにもかかわらず、AIは42点中35点を獲得し、ゴールドメダルを獲得しました。 このスコアは、前年の銀メダルパフォーマンスよりも7点高かったです。 観察者は後に、AIの証明は「勤勉で」、「完全で」、人間の参加者が期待する厳格な正当化に従ったと述べました。

AIと数学への影響

DeepMindの成果は、AIと数学の両方にとって重要な里程標です。 AIにとって、IMOをマスターすることは、人工一般知能（AGI）へのステップであり、システムが人間が実行できる任意の知的タスクを実行できるようになります。 複雑な数学的問題を解決するには、推論と理解が必要であり、これらは一般知能の基本的な要素です。 この成功は、AIがより人間のような認知能力に向けて進歩を遂げていることを示しています。

数学の分野では、Gemini Deep ThinkのようなAIシステムは、数学者にとって貴重なツールになる可能性があります。 これらは、新しい分野の探索、推測の検証、さらには新しい定理の発見を支援できます。 証明の構築のより退屈な側面を自動化することで、AIは、人間の数学者がより高レベルの概念的な作業に集中できるようにします。 さらに、これらのAIシステムのために開発されたテクニックは、人間の努力だけでは不可能な数学研究の新しい方法にインスピレーションを与える可能性があります。

しかし、数学の分野におけるAIの進歩は、教育環境や競技におけるAIの役割について疑問を提起します。 AIの能力がさらに成長するにつれて、数学教育と競技の性質がどのように変わるかについての議論が生じるでしょう。

今後の展望

IMOで金メダルを獲得することは重要な里程標ですが、現在のAIシステムの到達範囲外にある数学的課題はまだ多く残っています。 ただし、わずか1年で銀メダルから金メダルへの急速な進歩は、AIの革新と開発の加速するペースを強調しています。 このペースが続けば、AIシステムは間もなく数学の最も有名な未解決問題のいくつかに取り組むことになるでしょう。 AIが人間の創造性を置き換えるか、強化するかという疑問は未解決のままですが、2025年のIMOは、AIが論理的推論において重要な進歩を遂げていることを明確に示しています。
ments. このペースが続けば、AIシステムは間もなく数学の最も有名な未解決問題のいくつかに取り組むことになるでしょう。 AIが人間の創造性を置き換えるか、強化するかという疑問は未解決のままですが、2025年のIMOは、AIが論理的推論において重要な進歩を遂げていることを明確に示しています。