金メダルレベルの数学スキル：DeepMindの幾何学的推論モデルがNatureに掲載され、コードはオープンソースで、フィールズ賞受賞者が賞賛

今回、人工知能アルゴリズムが国際数学オリンピック（IMO）で大きな進歩を遂げました。

本日発行された国際的に有名な科学誌「ネイチャー」の最新号では、「人間のデモンストレーションなしでオリンピックの幾何学を解く」という論文で、AlphaGeometryが世界に紹介されました。専門家は、これは人工知能が人間のような推論能力に近づくための重要な一歩であると述べています。

論文リンク: https://www.nature.com/articles/s41586-023-06747-5

DeepMind は論文が発表されるとすぐにコードとモデルをオープンソース化しました。GitHub: https://github.com/google-deepmind/alphageometry

これは、Google DeepMind の研究者による人工知能システムであり、複雑な幾何学の問題を人間のオリンピック金メダリストに近いレベルで解くことができます。

オリンピックの幾何学問題 30 問のベンチマーク テストで、AlphaGeometry はオリンピックの標準制限時間内に 25 問を解きました。比較すると、従来の最先端システムは幾何学の問題を 10 問解き、人間の金メダリストは平均 25.9 問を解きました。

数学のほとんどの分野では、人間による証明を機械で検証可能な言語に翻訳したトレーニング データが不足しているため、学習ベースの AI モデルにとって定理の証明は困難です。 DeepMind は合成データを使用して定理を証明する代替方法を提案しており、このソリューションに基づく一般的なガイダンス フレームワーク AlphaGeometry は多くの分野に適用可能です。

研究

AlphaGeometry は、言語モデルと「シンボリック エンジン」を組み合わせて、シンボルと論理ルールを使用して数学的推論を実行します。その中で、言語モデルはプロセスの次のステップを識別して予測するのに優れていますが、数学的推論に必要な厳密さが欠けています。一方、シンボリック エンジンは形式論理と厳格なルールにのみ基づいており、言語モデルを合理的な意思決定に導くことができます。

AlphaGeometryに関する研究では、DeepMindは2000年から2022年までのオリンピック幾何学問題30問のベンチマークセット（IMO-AG-30）でテストしました。その結果、AlphaGeometryは競技時間制限内に25問の問題を解くことができたことが示されました。これまでの最先端の方法（Wu の方法）では 10 個しか解けませんでした。

AI システムは、推論スキルとトレーニング データの不足により、幾何学や数学の複雑な問題を解決するのが難しい場合が多いことはよく知られています。 AlphaGeometry システムは、ニューラル言語モデルの予測力とルール制約推論エンジンを組み合わせ、連携して新しいソリューションを見つけます。

さらに、データの課題に対処するために、研究者は大量の合成トレーニング データ、つまり 1 億例を生成しました。その多くは 200 ステップを超える証明を含んでおり、これは数学オリンピックの定理の平均証明の長さの 4 倍に相当します。

AlphaGeometry は、AI の論理的推論能力と新しい知識を発見して検証する能力の向上を示しています。オリンピックレベルの幾何学問題を解くことは、AI がより高度で汎用的な人工知能システムへと向かう道のりにおいて重要なマイルストーンです。

「AI研究者がIMO幾何学問題をまず解決しようとする理由が今では完全に理解できます。なぜなら、それらの解法を見つけることは、各ステップで妥当な動きが比較的少ないチェスをすることに少し似ているからです」とフィールズ賞受賞者でIMO金メダリストのゴ・バオ・チャウ氏は語った。「しかし、彼らがこれを達成できたことには今でも驚いています。素晴らしい業績です。」

2010年のフィールズ賞を受賞したバオジュ・ウー氏は現在シカゴ大学の教授である。

AlphaGeometry は、ニューラル言語モデルと記号推論エンジンから構成されるニューラル記号システムであり、これらが連携して複雑な幾何学定理の証明を見つけます。一方のシステムは迅速で直感的なアイデアを提供し、もう一方のシステムはより慎重で合理的な決定を提供します。

言語モデルはデータ内の一般的なパターンや関係を識別するのが得意なので、潜在的に有用な構造をすぐに予測できますが、厳密な推論や説明が欠けていることがよくあります。一方、シンボリック推論エンジンは形式論理に基づいており、明確なルールを使用して結論を​​導き出します。この 2 つが連携して AlphaGeometry を形成します。

AlphaGeometry の言語モデルは、記号推論エンジンをガイドして、幾何学的問題に対する可能な解決策を見つけます。典型的なオリンピックの幾何学の問題はグラフに基づいており、解決するには点、線、円などの新しい幾何学的構造を追加する必要があります。 AlphaGeometry の言語モデルは、無限の可能性の中から、どの新しい構造を追加するのが最も有用かを予測できます。これらの手がかりはギャップを埋めるのに役立ち、シンボリック エンジンがグラフについてさらに推論して解決策に近づくことを可能にします。

たとえば、次の図 (上) は、AlphaGeometry が「AB = AC となる任意の三角形 ABC を仮定します。∠ABC = ∠BCA であることを証明してください。」という簡単な問題を解決する方法を示しています。

AlphaGeometry の証明プロセスは次のとおりです。AlphaGeometry は、シンボリック演繹エンジンを実行して証明検索を開始します。このエンジンは、定理が証明されるか、新しいステートメントが尽きるまで、定理の前提から新しいステートメントを徹底的に導出します。シンボリック エンジンが証明を見つけられない場合、言語モデルは、シンボリック エンジンがやり直す前に、証明可能な条件を追加するための補助ポイントを構築します。このサイクルは解決策が見つかるまで続きます。単純な例では、ループは最初の補助構造「BC の中点に点 D を追加する」の後で終了します。

次の図は、AlphaGeometry による IMO の解を示しています。 「三角形 FKM と KQH の外接円 (O1) と (O2) が互いに接していることを証明してください…」 AlphaGeometry ではこのような複雑な問題も証明でき、証明では補助点も提供されます。証明は説明のために大幅に短縮され、編集されています。

1億個の数学的推論トレーニングデータを生成する

人間は、紙にスケッチしたり、図を調べたり、既存の知識を使って新しい、より複雑な幾何学的特性や関係を発見したりすることで、幾何学を学ぶことができます。この研究の合成データ生成方法は、この知識構築プロセスを大規模にシミュレートします。合成データを生成する方法を図 3 に示します。

システムは、高度な並列コンピューティングを使用して、まず 5 億個の幾何学的オブジェクトのランダム グラフを生成し、各グラフ内の点と線の間の関係をすべて徹底的に導出します。 AlphaGeometry は、各グラフに含まれるすべての証明を見つけ、それらの証明を取得するためにどのような追加の構造が必要か (ある場合) を逆方向に計算します。このプロセスは「記号演繹とバックトラッキング」と呼ばれます。

AlphaGeometry によって生成された合成データの視覚的表現

この膨大なデータプールは、類似の例を除外するためにフィルタリングされ、1億のトレーニング データ セットが生成されました。

画期的なAI推論機能

AlphaGeometry が提供するすべての数学オリンピックの問題の解答は、コンピューターでチェックされ、検証されています。研究者らはまた、その結果を従来の AI アプローチやオリンピック競技における人間のパフォーマンスと比較した。さらに、数学コーチであり、元オリンピック金メダリストのエヴァン・チェン氏が、一連の AlphaGeometry ソリューションを評価してくれました。

Yiting Chen さんは MIT の数学博士課程の学生で、IMO 2014 金メダルを獲得しました。

エヴァン・チェン氏は次のように語っています。「AlphaGeometry の出力は、検証可能でクリーンなため、素晴らしいものです。証明ベースの競争問題に対するこれまでの AI のソリューションは、当てずっぽうなもの (出力が正しくても人間による検査が必要) もありましたが、AlphaGeometry にはこの弱点がありません。ソリューションは機械で検証可能な構造になっています。一方で、出力は人間が判読可能です。座標系を総当たり方式で使って幾何学の問題を解くコンピューター プログラムを想像してみてください。何ページにもわたる面倒な代数計算を想像してみてください。しかし、AlphaGeometry はそうではなく、人間の学生のように、角度や相似三角形を使った古典的な幾何学のルールを使用します。」

最近、金融テクノロジー企業 XTX Markets は、数学的推論が可能な人工知能モデルの開発を奨励するために、人工知能数学オリンピック (AI-MO 賞) を設立しました。各オリンピックには 6 つの問題があり、そのうち 2 つだけが通常幾何学に焦点を当てているため、AlphaGeometry は特定のオリンピックの問題の 3 分の 1 にのみ適用できます。

それにもかかわらず、AlphaGeometry は、幾何学問題解決能力のみに基づいて、2000 年と 2015 年に IMO 銅メダルの基準を満たした世界初の AI モデルとなりました。

DeepMind はすでに次世代の AI システムにおける推論の進歩に取り組んでいます。研究者たちは、大規模な合成データを使用して AI システムをゼロからトレーニングする幅広い可能性を考えると、このアプローチは将来の AI システムが数学やその他の分野で新しい知識を発見する方向に影響を及ぼす可能性があると考えています。

AlphaGeometry は、純粋数学の美しさの探求から言語モデルを使用した数学や科学の問題の解決まで、AI における数学的推論の先駆者です。この技術が今後も改善され、より高度で抽象的な数学の問題が解決されることが期待されます。

AlphaGeometry の影響は、数学を超えて、コンピューター ビジョン、建築、さらには理論物理学など、幾何学の問題に関係するより多くの分野に及ぶ可能性があります。