Google 数学 AI が Nature に発表: IMO 金メダルの幾何学レベル、定理証明は呉文軍の 1978 年の法則を上回る

Google DeepMindが再びNatureを出版、AIのAlphaシリーズが力強く復活、数学レベルも大きく進歩。

AlphaGeometry は、人間によるデモンストレーションなしで IMO 金メダリストの幾何学レベルに到達します。

AlphaZeroが人知を介さずに囲碁を学んだ「人知を介さずに囲碁を極める」時代のような気がします。

具体的には、IMO 難易度の幾何学定理証明問題 30 問のうち、AlphaGeometry は 25 問正解しましたが、人間の金メダリストは平均 25.9 問正解でした。以前の SOTA 方式 (1978 年の Wu Wenjun の方法) は 10 問正解でした。

AIが生成した回答の評価を担当したIMO金メダリストのエヴァン・チェン氏は次のようにコメントした。

AlphaGeometry の出力は、検証可能かつクリーンで、印象的です。これまでの AI ソリューションは、出力が正しい場合もあれば正しくない場合もあるなど、非常に不安定で、人間によるレビューが必要でした。

AlphaGeometry にはこの弱点がなく、そのソリューションは機械で検証可能な構造を持ち、人間が判読可能です。学生が使用するのと同じように、角度と相似三角形を使用した古典的な幾何学のルールを使用します。

印象的な結果に加えて、この調査には業界の注目を集めた 3 つの重要なポイントがあります。

• 人間によるデモンストレーションは必要ありません。つまり、AI 合成データ トレーニングのみが使用され、これは AlphaZero が Go を自己学習する方法を継承しています。
• この大規模モデルは他の AI 手法を組み合わせたもので、AlphaGo や OpenAI Q* に似ていると噂されています。
• これまでの多くのアプローチとは異なり、AlphaGeometry は人間が読める証明を生成でき、モデルとコードは両方ともオープンソースです。

チームは、AlphaGeometry が高度な推論機能を実現し、新しい知識を発見するための潜在的なフレームワークを提供すると考えています。

これは、AGI 構築の重要なステップと見なされている人工知能における定理証明の進歩に役立つ可能性があります。

さらに、著者のチームとのコミュニケーションの中で、Quantum位は、AlphaGo が人間の囲碁チャンピオンに挑戦したときのように、AlphaGeometry が本当に IMO 大会に参加できるかどうかを知りました。

彼らは、システムの機能を向上させ、AIが幾何学を超えてより広範囲の数学の問題を解けるようにすることに取り組んでいるという。

AIは幾何学でも補助線を描けることを証明

これまで、AI システムは高品質のトレーニング データが不足していたため、幾何学の問題をうまく解決することができませんでした。

人間は紙と鉛筆の助けを借りて幾何学を学び、画像に関する既存の知識を使用して、新しい、より複雑な幾何学的特性と関係を発見します。

この目的のために、Google チームは 10 億個のランダムな幾何学的オブジェクト グラフと、グラフ内の点と線の間のすべての関係を生成し、最終的にさまざまな難易度の 1 億個の固有の定理と証明を選別しました。AlphaGeometry はこれらのデータに基づいて完全にゼロからトレーニングされました。

このシステムは、複雑な幾何学的証明を見つけるために連携して動作する 2 つのモジュールで構成されています。

• 言語モデルは、問題を解決するために使用できる幾何学的構造を予測します（つまり、補助線を追加します） 。
• 論理ルールを使用して結論を​​導き出す記号推論エンジン。

筆頭著者の Trieu Trinh 氏は、AlphaGeometry の動作プロセスは人間の脳のそれに似ており、高速と低速の 2 種類に分けられると紹介しました。

これは、ノーベル経済学賞受賞者のダニエル・カーネマンがベストセラー『ファスト＆スロー』で広めた「システム1とシステム2」という概念です。

システム 1 は素早い直感的な思考を可能にし、システム 2 はより思慮深く合理的な意思決定を可能にします。

一方で、言語モデルはデータ内のパターンや関係を識別するのが得意で、潜在的に有用な補助構造を素早く予測できますが、決定について厳密に推論したり説明したりする能力が欠けていることがよくあります。

一方、記号推論エンジンは形式論理に基づいており、明確なルールを使用して結論を​​導き出します。これらは合理的で説明可能ですが、特に大規模で複雑な問題に単独で取り組む場合には、遅くて柔軟性に欠けます。

たとえば、IMO 2015 の競技問題を解く場合、青い部分は AlphaGeometry の言語モデルによって追加された補助構造であり、緑の部分は最終証明の簡略版であり、合計 109 ステップになります。

AlphaGeometry は、問題を解く過程で、2004 年の IMO コンテストの問題で使用されていない前提も発見し、定理のより一般化されたバージョンを発見しました。

O が BC の中点であるという条件は、P、B、C が同一直線上にあることを証明できます。

さらに、この研究では、人間のスコアが最も低い 3 つの問題についても、AlphaGeometry では、解決するために非常に長い証明プロセスと多くの補助構造の追加が必要であることがわかりました。

しかし、比較的簡単な質問では、人間の平均スコアとAIが生成した証明の長さの間に有意な相関は見られませんでした（p = −0.06） 。

もう一つ

AlphaGeometry と AlphaGo のつながりと違いについて、Google の科学者Quoc Le 氏はチームとのやり取りの中で次のように語っています。

どちらも非常に複雑な決定空間で検索を行いますが、AlphaGo のアプローチはより伝統的です(注: ニューラル ネットワークはパターン認識を担当します) 。一方、AlphaGeometry のニューラル ネットワークは、次に取るべきアクションを提案し、検索アルゴリズムが決定空間内で正しい方向に進むように誘導する役割を担っています。

この成果は Alpha シリーズにちなんで名付けられ、最初のユニットも Google DeepMind ですが、実際の作成者は主に Google Brain の元メンバーです。

偉大な Quoc Le 氏については、あまり多くを紹介する必要はありません。第一著者の Trieu Trinh 氏と責任著者の Thang Luong 氏は、どちらも Google で 6 ～ 7 年間勤務しています。Thang Luong 氏自身も高校時代に IMO に参加していました。

2人の中国人作家のうち、何何氏はニューヨーク大学の助教授である。ウー・ユーフアイ氏は以前、グーグルの大規模数学モデル「ミネルバ」の研究に参加していた。現在はグーグルを離れ、マスク氏のチームに加わり、xAIの共同設立者の一人となっている。

論文アドレス: https://www.nature.com/articles/s41586-023-06747-5.

参考リンク:
[1] https://www.nature.com/articles/d4186-024-00141-5.

[2] https://deepmind.google/discover/blog/alphageometry-an-olympiad-level-ai-system-for-geometry.