ニュース

한어Русский языкEnglishFrançaisIndonesianSanskrit日本語DeutschPortuguêsΕλληνικάespañolItalianoSuomalainenLatina

マシンハートレポート

マシーンハート編集部

Gemini 大型モデルと AlphaZero 強化学習アルゴリズムを使用して、幾何学、代数学、数論を習得できます。

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

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

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

今月初め、UCLA 終身教授のテレンス・タオ氏が、100 万ドルの賞金をかけて AI 数学オリンピック (AIMO Progress Award) を宣伝したばかりだったが、予想外なことに、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金メダリストであり、フィールズメダリストでもあるティモシー・ガワーズ氏と、2度のIMO金メダリストであり、IMO2024年問題選択委員会委員長であるジョセフ・マイヤーズ博士は、IMO採点ルールに従って、複合システムによって与えられた解を採点しました。

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

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

AlphaProof: 形式的推論手法

Google が使用するハイブリッド AI システムの 1 つである 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 が主導し、主な貢献者には Hussain Masoom、Aja Huang、Miklós Z. Horváth、Tom Zahavy、Vivek Veeriah、Eric Wieser、Jessica Yung、Lei Yu、Yannick Schroecker、Julian Schrittwieser、オッタヴィア・ベルトーリ、ボルハ・イバルツ、エドワード・ロックハート、エドワード・ヒューズ、マーク・ローランド、グレース・マーガンド。

その中で、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/