ネイチャーニュース：AIは高校数学オリンピックの問題を解く能力で人間の金メダリストに迫る

人工知能（AI）は国際数学オリンピックの難しい問題を解くことを学び、人間の金メダリストに近いレベルに到達しました。

AlphaGeometryと呼ばれるこのAIモデルは、 Google DeepMindとニューヨーク大学の共同チームによって開発されました。これは国際数学オリンピックレベルの幾何学の問題を解くことができるAIシステムであり、本日トップ科学誌「ネイチャー」に掲載されました。

AlphaGeometry は、数百万の定理と証明を自律的に合成することで、最新のオリンピックレベル (優秀な高校生による数学定理証明コンテスト) の問題 30 問のうち 25 問を解決したと報告されています。これは、国際数学オリンピックの金メダリストの平均成績に近く、これまでの自動定理証明システムの最高成績をはるかに上回っています。

この画期的な進歩は、AI が数学の問題を自律的に解決する能力において大きな進歩を示し、人間によるデモンストレーションを必要とせずに複雑な幾何学的課題を解決できるようになります。

この研究は、AI が複雑な論理的課題を人間に近いレベルで解決できる可能性を実証しており、これは AI 研究の主要な目標です。

注目すべきことに、AlphaGeometry は人間が判読可能な証明を生成でき、 2004 年の国際数学オリンピックの定理の新しいバージョンを発見することさえできます。

「人間によるデモンストレーションなしでオリンピックの幾何学を解く」と題された関連研究論文が、Nature 誌に掲載されました。

AIが数学オリンピックの問題を解くのは難しいのでしょうか？

より優れた定理証明能力の追求は、1950 年代以来 AI 研究の焦点となってきました。数学オリンピックは、1959年に始まった世界で最も有名な定理証明コンテストであり、優れた才能を発掘する上で重要な役割を果たしています。

国際数学オリンピックの問題には通常、詳細な数学理論と抽象的な数学概念が含まれており、独立した思考、創造的な問題解決、直感の活用が求められます。これらの問題は、人間の数学者が持つ高度な論理的推論と創造的思考を必要とすることが多いですが、従来の機械学習手法の適用範囲を超えています。

さらに、他の分野と比較して、数学の問題を解く人間のプロセスは、トレーニングに使用できる大規模なデータセットに簡単に変換できません。幾何学は翻訳するのが特に難しく、一般的な数学言語による証明の例はほとんどありません。また、幾何学の言語は非常に正確な定義を持ち、複素数など幾何学以外のものを使用する多くの人間による証明を表現することができません。

図 | IMO2000P6 の人間による証明と AlphaGeometry による証明を並べて比較します。これは、問題文に多数のオブジェクトが含まれる、より難しい問題です (人間の平均スコア = 1.05/7)。左は、人間による解決法で複素数を使用しています。座標系を慎重に選択することで、問題は大幅に簡素化され、代数的な操作によって自然に解が得られます。右: AlphaGeometry ソリューションには 2 つの補助構造と 100 を超える導出ステップが含まれており、その多くは人間が実行するには非常に面倒です。この場合、検索ベースのソリューションは読みにくく、直感的ではありません。より構造化された構成、つまり高レベルの証明アウトラインにより、AlphaGeometry ソリューションの読みやすさが大幅に向上する可能性があります。 AlphaGeometry には多くの高レベルの導出ルールが組み込まれており、低レベルの導出を減らし、証明手順を簡素化するのに役立ちます。 （出典：本論文）

十分なサンプルデータ、特に人間の専門数学者による解決プロセスが不足しているため、機械学習モデルが問題解決方法を学習して理解することが困難になっています。したがって、現在の幾何学的手法は依然として主に記号的手法と手動で設計されたハードコードされた検索ヒューリスティックに依存しています。

人間なしで複雑な問題を自律的に解決する

この研究における AlphaGeometry の重要な革新性は、ゼロからトレーニングされたニューラル言語モデルを使用して自律的にトレーニングされ、複雑さの異なる数百万の定理と証明を合成する能力です。これは、AlphaGeometry が人間の入力に頼ることなく、複雑な問題を独自に学習して解決できることを意味します。

ニューラル言語モデルは、困難な問題における多数の分岐点を検索できる記号推論エンジンをガイドするのに特に適しています。ニューラル モデルの導入により、AlphaGeometry は困難な問題に対処する際に、より正確な推論を行うことができます。記号推論エンジンとニューラル言語モデルを組み合わせるこの方法は、この研究の重要な革新の 1 つです。

図 | AlphaGeometry の概要と、それが単純な問題と IMO2015 の問題 3 を解決する方法を示します。上の行は、AlphaGeometry が単純な問題をどのように解決するかを示しています。 a) 簡単な例とその図。 b) モデルは、シンボリック演繹エンジンを実行して証明検索を開始します。エンジンは、定理が証明されるか、新しいステートメントが尽きるまで、定理の前提から新しいステートメントを徹底的に導出します。 c) シンボリック エンジンが証明を見つけられないため、言語モデルは、シンボリック エンジンが再試行する前に証明状態を増分するための補助ポイントを構築します。解決策が見つかるまでループは継続されます。 d) 単純な例では、ループは最初の補助構造「BC の中点としての D」の後で終了します。証明はさらに 2 つのステップで構成され、どちらも中点特性「BD = DC」および「B、D、および C は同一直線上である」を利用します。下の行は、AlphaGeometry が IMO 2015 問題 3 (IMO 2015 P3) を解決する方法を示しています。 e) IMO 2015 P3 問題ステートメントと図。 f IMO 2015 P3 のソリューションには 3 つの補助ポイントがあります。 （出典：本論文）

AlphaGeometry はオリンピックレベルの幾何学問題を解く上で目覚ましい成功を収めていますが、いくつかの制限もあります。

論文によれば、 AlphaGeometry は主にオリンピックレベルの幾何学の問題を解くことに焦点を当てており、適用範囲は比較的狭い。このため、この方法を他の数学分野や実用的な問題に一般化することは制限されます。今後の研究では、この方法を拡張してより広範囲の数学分野をカバーする方法を探る必要があります。

さらに、研究チームは大規模な人工合成データを使用して AlphaGeometry をトレーニングしました。これにより、モデルに幅広い学習教材が提供されましたが、合成データでは実際の数学の問題の多様性と複雑さを完全にはカバーできない可能性があります。したがって、実際のシナリオでは、データが不十分なためにモデルのパフォーマンスが影響を受ける可能性があります。

さらに、AlphaGeometry は人間が判読可能な証明を生成できますが、極めて複雑な推論を扱う場合には生成された結果が理解しにくくなる可能性があります。これにより、場合によってはモデルの推論プロセスを追跡して説明することが困難になります。

AIは数学の問題を解く上で大きな可能性を秘めている

近年、AI技術を利用して数学の定理を理解し証明することは、科学者が注力している研究方向の1つとなっています。

たとえば、AI を使用すると、数学の定理を独自に導出して証明できる自動定理証明システムを開発できます。このアプローチは、手動証明の負担を軽減し、より効率的な証明方法を提供することを目的としています。

さらに、AI は数学的知識グラフの構築にも使用でき、数学的概念間の関係をグラフ構造にモデル化するのに役立ちます。このグラフを使用すると、定理の推論と証明を改善し、システムが数学の分野における知識体系をより深く理解できるようになります。

AIは創造的思考を発達させる役割も担っています。一部の研究では、生成的敵対的ネットワーク (GAN) などの生成モデルを使用して、数学的な構造と仕様に準拠した新しい定理を生成します。このアプローチは、数学の分野における創造的思考を拡大し、新しい数学的概念や結論を導入するのに役立ちます。

もちろん、AI が数学において人間のトップクラスの数学者と同じレベルの成果を上げるまでには、まだ長い道のりがあります。

それでも、AlphaGeometry は数学における AI の応用の可能性を示しています。この成果は数学の分野に革新をもたらすだけでなく、他の分野への AI の応用にも新たな可能性をもたらします。

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