Google AI が IMO 数学オリンピック銀メダルを獲得、数理推論モデル AlphaProof が発売、強化学習が復活

AI にとって、数学オリンピックはもはや問題ではありません。

木曜日、Google DeepMind の人工知能は、AI を使用して今年の国際数学オリンピック IMO の本当の問題を解決するという偉業を達成し、金メダル獲得まであと一歩のところまで迫りました。

先週終了したばかりの IMO コンテストでは、代数、組合せ論、幾何学、数論を含む合計 6 つの問題が出題されました。 Google が提案したハイブリッド AI システムは 4 問正解し、28 点を獲得し、銀メダルレベルに達しました。

今月初め、UCLA 終身教授のテレンス・タオ氏がAI 数学オリンピック (AIMO Progress Award) を宣伝し、賞金 100 万ドルを獲得したばかりですが、予想外なことに、AI の問題解決のレベルは 7 月以前にこのレベルまで向上しました。

IMO で同時に問題を解き、最も難しい問題を正解しましょう

IMO は、1959 年から毎年開催されている、若い数学者のための最も古く、最大かつ最も名誉あるコンテストです。最近では、IMO コンテストは機械学習の分野における壮大な挑戦としても広く認識されており、人工知能システムの高度な数学的推論能力を測定するための理想的なベンチマークとなっています。

今年の IMO コンテストでは、DeepMind チームが共同開発した AlphaProof と AlphaGeometry 2 が画期的な進歩を達成しました。

その中で、AlphaProof は形式的な数学的推論のための強化学習システムであり、AlphaGeometry 2 は DeepMind の幾何学解決システム AlphaGeometry の改良版です。

このブレークスルーは、高度な数学的推論機能を備えた汎用人工知能 (AGI) が科学技術の新しい分野を開く可能性を示しています。

それでは、DeepMind の AI システムはどのようにして IMO 競争に参加するのでしょうか?

簡単に言うと、まずこれらの数学的問題は、AI システムが理解できるように手動で正式な数学的言語に翻訳されます。公式コンテストでは、人間の出場者は 2 つのセッション (2 日間) で解答を提出し、各セッションの制限時間は 4.5 時間です。 AlphaProof+AlphaGeometry 2 AI システムを組み合わせることにより、1 つの問題は数分で解決されましたが、他の問題を解決するには 3 日かかりました。ただし、ルールに厳密に従えば、DeepMind のシステムはタイムアウトになります。これには大量のブルートフォースクラッキングが含まれるのではないかと推測する人もいます。

Googleによれば、AlphaProofは、答えを決定し、その正しさを証明することで、2つの代数問題と1​​つの数論の問題を解決したとのこと。これらには、今年の IMO でわずか 5 人の出場者だけが解決した、コンテストで最も難しい問題も含まれています。そして、AlphaGeometry 2 は幾何学の問題を証明します。

AI が提供するソリューション: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/index.html

IMO 金メダル受賞者およびフィールズ賞受賞者の Timothy Gowers 氏と2 度の IMO 金メダリストであり、IMO 2024 問題選択委員会の委員長であるジョセフ・マイヤーズ博士は、IMO 採点ルールに従って、複合システムによって与えられた解決策を採点しました。

6 つの質問はそれぞれ 7 ポイントの価値があり、最大合計スコアは 42 ポイントです。 DeepMind のシステムは最終スコア 28 を獲得しました。これは、システムが解決した 4 つの問題すべてが完璧なスコアを獲得したことを意味します。これは、銀メダル カテゴリの最高スコアに相当します。今年の金メダルの基準点は 29 点で、公式競技会の出場者 609 名のうち 58 名が金メダルを獲得しました。

このグラフは、IMO 2024 における人間の競合他社と比較した Google DeepMind の人工知能システムのパフォーマンスを示しています。このシステムは 42 点中 28 点を獲得し、大会の銀メダリストと同等の成績を収めました。さらに、今年は29点で金メダルを獲得できる。

AlphaProof: 形式推論手法

Google が使用するハイブリッド AI システムでは、AlphaProof は形式言語 Lean を使用して数学的ステートメントを証明する自己学習システムです。事前トレーニングされた言語モデルと AlphaZero 強化学習アルゴリズムを組み合わせます。

その中で、形式言語は、数学的推論の証明の正しさを形式的に検証するために重要な利点を提供します。これまで、人間が書き込んだデータの量が非常に限られていたため、これは機械学習での用途が限られていました。

対照的に、自然言語ベースのメソッドは大量のデータにアクセスできますが、合理的であるように見えても正しくない中間推論ステップと解決策を生成します。

Google DeepMind は、Gemini モデルを微調整して自然言語の問題ステートメントを正式なステートメントに自動的に変換することで、これら 2 つの相補的な分野の間に橋を架け、それによってさまざまな難易度の形式的な問題の大規模なライブラリを作成します。

数学的な問題が与えられると、AlphaProof は解の候補を生成し、リーンで可能な証明ステップを検索することでそれらを証明します。発見および検証された各証明ソリューションは、AlphaProof の言語モデルを強化し、その後のより困難な問題を解決する能力を強化するために使用されます。

AlphaProof をトレーニングするために、Google DeepMind は、IMO コンテストまでの数週間で、幅広い困難やトピックをカバーする何百万もの数学的問題を証明または反証しました。トレーニング ループは競技中にも適用され、完全な解決策が見つかるまで自己生成された競技問題のバリエーションの証明を強化します。

AlphaProof 強化学習トレーニング ループ プロセスのインフォグラフィック: 約 100 万件の非公式な数学的問題が、正式なネットワークによって正式な数学言語に翻訳されます。次に、ソルバーは問題の証明または反証を求めてネットワークを検索し、AlphaZero アルゴリズムを通じてより困難な問題を解決できるように徐々に学習します。

より競争力の高い AlphaGeometry 2

AlphaGeometry 2 は、今年 Nature 誌に掲載された数学 AI AlphaGeometry の大幅に改良されたバージョンです。これは、言語モデルが Gemini に基づいており、前任者よりも桁違いに多くの合成データに基づいてゼロからトレーニングされた神経記号ハイブリッド システムです。これは、オブジェクトの動きや角度、比率、距離の方程式など、より困難な幾何学的問題をモデルが解決するのに役立ちます。

AlphaGeometry 2 は、前世代よりも 2 桁高速なシンボリック エンジンを使用します。新しい問題が発生した場合、新しい知識共有メカニズムにより、さまざまな検索ツリーを高度に組み合わせて、より複雑な問題を解決できます。

今年のコンテストに先立って、AlphaGeometry 2 は過去 25 年間のすべての歴史的な IMO 幾何学問題の 83% を解決できましたが、前バージョンの解決率は 53% でした。 IMO 2024 では、AlphaGeometry 2 は形式化を受け取ってから 19 秒以内に問題 4 を解決しました。

問題 4 の例。∠KIL と ∠XPY の合計が 180° に等しいことを証明するよう求めるものです。 AlphaGeometry 2 は、∠AEB = 90°となるように線 BI 上に点 E を構築することを提案しています。点 E は、線分 AB の中点 L に意味を与えるのに役立ち、それによって ABE ～ YBI や ALE ～ IPC のような相似な三角形のペアを多数作成して結論を​​証明します。

Google DeepMind は、IMO の取り組みの一環として、研究者らが高度な問題解決能力の実現を目指して、Gemini に基づく最先端の自然言語推論システムの実験も行っていると報告しています。このシステムは質問を正式な言語に翻訳する必要がなく、他の AI システムと組み合わせることができます。今年のIMOコンテストの問題のテストでは、「大きな可能性を示した」。

Google は数学的推論を進歩させるための AI 手法の研究を続けており、AlphaProof に関する技術的な詳細を間もなくリリースする予定です。

私たちは、数学者が AI ツールを使用して仮説を探索し、長年の問題を解決するための大胆な新しい方法を試み、時間のかかる証明要素を迅速に完了する未来に興奮しています。そして、Gemini のような AI システムが数学とより広範な推論に革命を起こすでしょう。側面がより強力になります。

研究チーム

Googleは、この新しい研究は国際数学オリンピック機構によって支援されたと述べました。さらに、

AlphaProofの開発は、Thomas Hubert、Rishi Mehta、Laurent Sartranによって主導されました。アジャ・ファン、ミクロス・Z・ホルバース、トム・ザハヴィ、ヴィヴェク・ヴェリア、エリック・ヴィーザー、ジェシカ・ヨン、レイ・ユー、ヤニック・シュレッカー、ジュリアン・シュリットヴィーザー、オッタヴィア・ベルトーリ、ボルハ・イバルツ、エドワード・ロックハート、エドワード・ヒューズ、マーク・ローランド、グレース・マーガンド。

その中で、Aja Huang、Julian Schrittwieser、Yannick Schroecker らのメンバーは、8 年前 (2016 年) AlphaGo 論文の中心メンバーでもありました。 8 年前、強化学習に基づいた AlphaGo が有名になりました。 8 年後、強化学習は AlphaProof によって再び輝きを放ちました。友人の輪の中で誰かが「RLが本当に戻ってきた！」と嘆いていました。

AlphaGeometry 2 と自然言語推論の作業は Thang Luong が主導しています。 AlphaGeometry 2 の開発は、Trieu Trinh 氏とYuri Chervonyi 氏が主導し、Mirek Olšák 氏、Xiaomeng Yang 氏、Hoang Nguyen 氏、Junehyuk Jung 氏、Dawsen Hwang 氏、Marcelo Menegali 氏が重要な貢献をしました。

さらに、David Silver、Quoc Le、Hassabis、Pushmeet Kohli がプロジェクト全体の調整と管理を担当しています。

参考コンテンツ:

https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/

以上がGoogle AI が IMO 数学オリンピック銀メダルを獲得、数理推論モデル AlphaProof が発売、強化学習が復活の詳細内容です。詳細については、PHP 中国語 Web サイトの他の関連記事を参照してください。