ニュース

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

新しい知恵のレポート

編集者：編集部

【新しい知恵の紹介】たった今、Google DeepMind の最新の数学モデルが IMO 数学オリンピックの銀メダルを獲得しました。 6 問中 4 問を完璧なスコアで解き、金メダルまでわずか 1 点差でした。さらに、4 問目を解くのにかかった時間はわずか 19 秒でした。問題を解く質と速さは、採点した人間の審査員を驚かせました。 。

AI が IMO 数学オリンピック銀メダルを獲得しました!

ちょうど今、Google DeepMind が、今年の国際数学オリンピックの実際の問題が独自の AI システムによって生成されたと発表しました。

その中で、AI は 6 問中 4 問に正解しただけでなく、各質問で銀メダルの最高得点に相当する 28 点の満点を獲得しました。

この結果は金メダルまであと1点！

出場者609名のうち金メダルを獲得したのはわずか58名

公式コンテストでは、人間の出場者は 2 つのセッションに分けて解答を提出し、各回の制限時間は 4.5 時間です。

興味深いことに、AI は 1 つの質問に答えるのに数分しかかかりませんでしたが、残りの質問には丸 3 日かかり、これは重大なタイムアウトであると言えます。

今回大きく貢献したのは、AlphaProof と AlphaGeometry 2 という 2 つの AI システムです。

重要な点: 2024 IMO は、これら 2 つの AI の学習データには含まれていません。

AI エンジニアのデビン氏 (IOI で 3 回金メダリスト) の創設者の 1 人であるスコット ウー氏は、次のように嘆いています。解決しました。」

今年の IMO コンテストでは、代数学、組合せ論、幾何学、数論を含む 6 つの競技問題が出題されます。 6つの道が4つになる、AIのレベルを感じてみよう——

AIの数的推理能力が教授に衝撃を与える

以前の AI では、推論能力とトレーニング データに限界があるため、数学的問題の解決に限界があったことは誰もが知っています。

今日一緒に登場した二人のAIプレイヤーはこの限界を打ち破った。それらはそれぞれ――

- AlphaProof、強化学習に基づく形式的数学的推論のための新しいシステム

- AlphaGeometry 2、第 2 世代の幾何学問題解決システム

2 つの AI によって与えられた回答は、有名な数学者のティモシー ガワーズ教授 (IMO 金メダリストおよびフィールズメダリスト) とジョセフ マイヤーズ博士 (2 度の IMO 金メダリストおよび IMO 2024 問題選択委員会委員長) によってルールに従って採点されました。 。

最終的に、AlphaProof は 2 つの代数の問題と 1 つの数論の問題を正しく解決しました。最も難しい問題の 1 つは、今年の IMO の参加者のみ 5 人によって解決されました。AlphaGeometry 2 は幾何学の問題を解決しました。

まだ克服されていない組み合わせ数学の問題は 2 つだけです。

ティモシー・ガワーズ教授も採点過程で大きなショックを受けました—

プログラムがこのような自明ではない解決策を考え出すことができるということは、本当に印象的であり、現在の最先端技術を考慮すると、私の予想をはるかに超えています。

アルファプルーフ

AlphaProof は、形式言語 Lean で数学的命題を証明できるシステムです。

これは、事前トレーニングされた大規模な言語モデルと、チェス、将棋、囲碁を習得するように学習した AlphaZero 強化学習アルゴリズムを組み合わせたものです。

形式言語の主な利点は、数学的推論を含む証明について形式的に検証できることです。ただし、人間が書き込む関連データの量が非常に限られているため、機械学習への応用は限られています。

対照的に、自然言語ベースのアプローチは、大量のデータにアクセスできるにもかかわらず、もっともらしいが不正確な中間推論ステップと解決策を生成する可能性があります。

これを克服するために、Google DeepMind の研究者は、自然言語の問題ステートメントを正式なステートメントに自動的に翻訳するように Gemini モデルを微調整し、さまざまな難易度の形式的な問題を含む大規模なライブラリを構築し、それによって 2 つの相補的な分野の間に橋を架けました。

問題を解決するとき、AlphaProof は候補解を生成し、Lean で可能な証明ステップを検索することによってそれらを証明または反証します。

見つかって検証された各証明は、AlphaProof の言語モデルを強化するために使用され、将来的にはより困難な問題を解決できるようになります。

AlphaProof をトレーニングするために、研究者はコンテストに先立つ数週間およびコンテスト中に、幅広い難易度および数学的なトピック領域をカバーする何百万もの質問を証明または反証しました。

競技中、彼らはまた、完全な解決策が見つかるまで、競技問題の自己生成バリエーションに対する証明を強化するトレーニング ループを適用しました。

AlphaProof 強化学習トレーニング ループのフローのインフォグラフィック: 約 100 万件の非公式な数学的問題が正式な数学的言語に変換され、その後、ソルバー ネットワークが AlphaZero アルゴリズムを使用してこれらの問題の証明または反駁を検索することで徐々にトレーニングされます。 、より困難な問題を解決するために

アルファジオメトリ 2

AlphaGeometry 2 は、AlphaGeometry のアップグレード バージョンで、Gemini の言語モデルに基づいてゼロからトレーニングされた神経記号ハイブリッド システムです。

前世代よりも一桁多い合成データに基づいて、オブジェクトの動き、角度、比率、距離などを含む方程式を含む、より困難な幾何学的問題を解決できます。

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

今年 IMO に参加する前に、AlphaGeometry 2 はすでに多くの成功を収めていました。過去 25 年間で IMO 幾何学問題の 83% を解決できましたが、第 1 世代は 53% しか解決できませんでした。

この IMO では、AlphaGeometry 2 の速度は誰もが衝撃を受けました。正式な質問を受け取ってから 19 秒以内に、質問 4 が解決されました。

質問 4 では、∠KIL と ∠XPY の合計が 180° に等しいことを証明する必要があります。 AlphaGeometry 2 では、∠AEB=90°となるように BI ライン上に点 E を構築することを推奨しています。点 E は、AB の中点 L を決定するのに役立ち、ABE ～ YBI や ALE ～ IPC など、多くの同様の三角形のペアを形成し、結論を証明します。

AIの問題解決プロセス

これらの質問は、AI に送信される前に、まず手動で正式な数学的言語に翻訳されることは言及する価値があります。
1 位

一般的に、各 IMO テストの最初の質問 (P1) は比較的簡単です。

ネチズンは、「P1は高校数学の知識だけを必要とし、人間のプレイヤーは通常60分以内に完了する」と述べた。

IMO 2024 の最初の問題は、主に実数 α の性質を調べるもので、一定の条件を満たす実数 α を見つけることが求められます。

AI は正しい答えを出しました - α は偶数です。では、正確にはどのように答えられるのでしょうか?

問題を解く最初のステップとして、AIはまず左右の集合が等しいという定理を与えた。

左側のセットは、条件を満たすすべての実数 α が、任意の正の整数 n に対して、 ⌊i*α⌋ を 1 から n まで除算できることを表します。右側のセットは、整数 k が存在することを表します。偶数であり、実数αはkに等しい。

以下の証明は 2 つの方向に分かれています。

まず、右側の集合が左側の集合の部分集合 (単純な方向) であることを証明します。

次に、左側の集合が右側の集合の部分集合であることを証明します (難しい方向)。

コードの最後まで、AI は重要な方程式 ⌊(n+1)*α⌋ = ⌊α⌋+2n(l-⌊α⌋) を考え出し、その方程式を使用して α が次の値でなければならないことを証明しました。偶数。

最後に、DeepMind は、問題解決プロセスで AI が依存する 3 つの公理、propext、Classical.choice、Quot.sound を要約しました。

以下は、P1 の完全な問題解決プロセスです: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P1/index.html

2位

2 番目の質問は、最大公約数の性質を含む、正の整数のペア (a、b) 間の関係を調べます。

AIが解決した答えは次のとおりです。

定理は、特定の条件を満たす正の整数のペア (a, b) の場合、そのセットには (1,1) のみを含めることができるというものです。

次の問題解決プロセスで AI が採用する証明戦略は、まず (1,1) が与えられた条件を満たすことを証明し、次にこれが唯一の解であることを証明することです。

g=2、N=3 を使用して、(1,1) が最終的な解であることを証明します。

(a,b) が解である場合、ab+1 は g を除算しなければならないことを示します。

このプロセスでは、AI はオイラーの定理とモジュラー演算の特性を推論に使用しました。

最後に、a=b=1 が唯一の可能な解であることを証明します。

以下は、P2 の完全な問題解決プロセスです: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P2/index.html

P4

P4 は、特定の幾何学的角度関係を証明する必要がある幾何学的証明問題です。

前述したように、これは AlphaGeometry 2 によって 19 秒で完了し、新記録を樹立しました。

第一世代の AlphaGeometry と同様に、与えられた解に応じて、すべての解の補助点が言語モデルによって自動的に生成されます。

証明では、すべての角度追跡でガウス消去法が使用され、d(AB)-d(CD) は AB から CD への方向角に等しくなります (モジュロ π)。

問題解決のプロセス中に、AI は相似な三角形と合同な三角形のペア (赤でマーク) を手動でマークします。

次に、AlphaGeometry の問題を解く手順ですが、「再矛盾法」を使用して完成します。

まず、リーンを使用して証明する必要がある命題を形式化し、幾何学的構造を視覚化します。

証明の主要な手順は次のとおりです。

完全な問題解決プロセスについては、以下の図を参照してください: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P4/index.html

P6

IMO の 6 番目の質問は「究極のボス」で、関数の特性を調査し、有理数に関する具体的な結論を証明する必要があります。

AI は c=2 を解決します。

まず、定理ステートメントを見てみましょう。この定理ステートメントは、「Aquaesulian 関数」のプロパティを定義し、そのような関数すべてについて、f(r)+f(-r) の値セットには最大 2 つの要素が含まれることを宣言しています。

証明戦略は、まず任意の Aquaesulian 関数について、f(r)+f(-r) の値セットが最大 2 つの要素を持つことを証明することです。次に、f(r)+f(-r) が正確に 2 つの異なる値を持つように特定の Aquaesulian 関数を構築します。

f(0)=0 のとき、f(x)+f(-x) は最大 2 つの異なる値を取ることを証明し、アクアエスル関数 f(0)≠0 が存在しないことを証明します。

関数 f(x)=-x+2⌈x⌉ を作成し、それがアクアエスル関数であることを証明します。

最後に、この関数について、 f(-1)+f(1) =0 と f(1/2)+f(-1/2)=2 が 2 つの異なる値であることを証明します。

完全な問題解決プロセスは次のとおりです: https://storage.googleapis.com/deepmind-media/DeepMind.com/Blog/imo-2024-solutions/P6/index.html

オリンピックの数学の問題を解くことはできますが、9.11 と 9.9 のどちらが大きいかわかりますか?

スタンフォード大学とセコイアの研究者であるアンドリュー・ガオ氏は、この AI の画期的な進歩の重要性を認めています—

重要なのは、最新の IMO テストの問題がトレーニング セットに含まれていないということです。これは、AI が新たな目に見えない問題に対処できることを示すため、重要です。

さらに、AI によってうまく解決される幾何学的な問題は、関係する空間の性質（直観的思考と空間的想像力が必要）のため、常に非常に難しいと考えられてきました。

Nvidiaのシニアサイエンティストであるジム・ファン氏は、大型モデルは謎に満ちた存在だという長い記事を投稿した——

彼らは数学オリンピックで銀メダルを獲得することもありますが、「9.11 と 9.9 のどちらの数字が大きいですか?」などの質問では頻繁に間違います。

Gemini だけでなく、GPT-4o、Claude-3.5、Llama-3 も 100% 正解することはできません。

AI モデルをトレーニングすることで、私たちは自分自身の知性を超えた広大な領域を探索しています。その過程で、私たちは非常に奇妙な領域を発見しました。それは、地球に似ていますが、奇妙な谷でいっぱいの系外惑星です。

これは不合理に思えますが、トレーニング データの分布を使用して説明できます。

AlphaProof と AlphaGeometry 2 は、形式的な証明とドメイン固有のシンボリック エンジンでトレーニングされています。これらは、汎用 LLM に基づいて構築されているにもかかわらず、オリンピックの特殊な問題を解決するのにある程度優れています。 GPT-4o のトレーニング セットには、数学的データをはるかに超える可能性がある大量の GitHub コード データが混合されています。ソフトウェア バージョンのうち、「v9.11 > v9.9」では、データの分布が著しく歪む可能性があります。したがって、このエラーはある程度理解できます。

Google 開発責任者は、難しい数学的および物理的問題を解決できるモデルが AGI への重要な道であると述べ、今日私たちはこの道で新たな一歩を踏み出しました。

他のネチズンは、今週は情報が多すぎると述べた。

参考文献:

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

https://x.com/DrJimFan/status/1816521330298356181