Google DeepMindが、形式的な数学推論のための新たな強化学習ベースのシステムとして「AlphaProof」および幾何学を解くシステムとして「AlphaGeometry 2」を発表しました。これら2つのシステムを組み合わせることで、国際数学オリンピック(IMO)において銀メダルレベルのスコアを獲得できたと述べられています。

AI achieves silver-medal standard solving International Mathematical Olympiad problems - Google DeepMind

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



国際数学オリンピックでは6問が出題され、それぞれ7点満点で採点されます。全問を満点で正解すれば合計42点になるというしくみで、上位から一定の割合ごとに金メダル・銀メダル・銅メダルが与えられます。

Google DeepMindが開発したAlphaProofは2つの代数問題と1つの数論問題で満点を獲得。また、AlphaGeometry 2が幾何学の問題で満点を獲得し、合計得点は28点となりました。2024年の国際数学オリンピックでは金メダルのラインが29点であり、惜しくも金メダル獲得とはなりませんでした。



AlphaProofはAlphaZeroの強化学習アルゴリズムと事前学習済み言語モデルを組み合わせたモデルで、Learnという形式言語で数学的な文を証明するために自己トレーニングを行います。形式言語は自然言語に比べ、数学的な推論を行う際の「正しさ」を形式的に検証できるという利点があるものの、トレーニングに使用できるデータの量が圧倒的に少ないという欠点がありました。

Google DeepMindのチームはGoogleのAI「Gemini」を使用し、自然言語の問題を形式言語に自動で翻訳してデータ量を補完することで、幅広い難易度と数学のトピック領域を網羅した何百万もの問題をトレーニングに使用することができたとのこと。

AlphaProofのトレーニングループはこんな感じ。約100万個の自然言語の問題が形式化ネットワークによって形式言語に変換され、ソルバーネットワークが問題の証明もしくは反証を検索します。検索に成功すると、AlphaZeroアルゴリズムを通してソルバーネットワークがトレーニングされ、より困難な問題を解決できるようになります。



一方、AlphaGeometry 2は幾何学問題に特化したAIモデルです。前身であるAlphaGeometryの時点で、幾何学問題に限れば国際数学オリンピックの金メダル獲得レベルのスコアを獲得していました。

Google DeepMindが数学オリンピックレベルの幾何学問題を解けるAI「AlphaGeometry」を発表、人間の金メダリストに近い性能を発揮 - GIGAZINE



AlphaGeometry 2は桁違いに多くの合成データでゼロからトレーニングされており、国際数学オリンピックの過去25年に出題された幾何学問題において53%だったAlphaGeometryの正答率を83%へと大幅に改善。2024年の国際数学オリンピックの幾何学問題においては、問題の形式化が完了してから19秒で回答することに成功しました。



Google DeepMindのチームはさらに、問題を形式言語に翻訳せずに解答できる自然言語推論システムの実験も行い、「非常に有望な結果」を得たとのこと。また、AlphaProofの技術的な詳細を近日中に公開する予定と述べられています。