AlphaProof と AlphaGeometry 2 の概要
以下の記事が面白かったので、簡単にまとめました。
・AI achieves silver-medal standard solving International Mathematical Olympiad problems
1. はじめに
高度な数学的推論機能を備えた汎用人工知能 (AGI) は、科学技術の新たな領域を切り開く可能性を秘めています。
私たち (Google DeepMind) は、数学者が新しい洞察、斬新なアルゴリズム、未解決の問題への答えを発見するのに役立つAIシステムの構築で大きな進歩を遂げてきました。しかし、現在のAIシステムは、推論スキルと学習データの制限により、一般的な数学の問題を解くのにまだ苦労しています。
この記事では、形式的な数学推論のための新しい強化学習ベースのシステムである 「AlphaProof」と、幾何学を解くシステムの改良版である「AlphaGeometry 2」を紹介します。これらのシステムを組み合わせることで、今年の国際数学オリンピック(IMO)の問題6問中4問を解き、初めてこの競技で銀メダリストと同等のレベルを達成しました。
2. 複雑な数学問題を解く画期的なAI性能
IMOは、1959年から毎年開催されている、若手数学者のための最も古く、最大規模で、最も権威のあるコンテストです。
毎年、大学進学前の一流数学者たちが、代数、組合せ論、幾何学、数論における極めて難しい6つの問題を解くために、時には数千時間もかけて学習します。数学者にとって最高の栄誉の一つであるフィールズ賞の受賞者の多くは、IMOで自国を代表しています。
最近では、毎年開催されるIMOコンテストも、機械学習における大きな挑戦として、またAIシステムの高度な数学的推論能力を測定するための目標となるベンチマークとして広く認知されるようになりました。
今年、私たちIMO主催者から提供された競技問題に、私たちの統合AIシステムを適用しました。私たちのソリューションは、IMOのポイント付与ルールに従って、IMO金メダリストでありフィールズ賞受賞者の著名な数学者、サー・ティモシー・ガワーズ教授と、IMO金メダリスト2回でIMO 2024問題選定委員会委員長のジョセフ・マイヤーズ博士によって採点されました。
「プログラムがこのような自明でない構成を思いつくことができるという事実は非常に印象的で、私が最先端だと思っていたものをはるかに超えています。」
IMO金メダリストおよびフィールズ賞受賞者のティモシー・ガワーズ教授
まず、問題を私たちのシステムが理解できるように、正式な数学言語に手動で翻訳しました。公式コンテストでは、学生は 4.5 時間のセッションを2回に分けて回答を提出します。私たちのシステムは1つの問題を数分以内に解きましたが、他の問題を解くのに最大3日かかりました。
「AlphaProof」は、答えを決定し、それが正しいことを証明することで、2つの代数問題と1つの数論問題を解きました。これには、今年のIMOで5人の参加者だけが解いた、コンテストで最も難しい問題も含まれていました。「AlphaGeometry 2」は幾何学の問題を証明しましたが、2つの組み合わせ問題は未解決のままでした。
6つの問題はそれぞれ7ポイント獲得でき、合計で最大42ポイントを獲得できます。私たちのシステムは、各問題を解くたびに満点を獲得し、最終スコア 28 ポイントを獲得しました。これは、銀メダルカテゴリの最高点に相当します。今年は、金メダルの基準は29ポイントから始まり、公式大会では609人の参加者のうち58人がこのポイントを獲得しました。
3. AlphaProof
「AlphaProof」は、形式言語「Lean」で数学的なステートメントを証明するために自己学習するシステムです。これは、チェス、将棋、囲碁のゲームをマスターする方法を以前に自己学習した「AlphaZero」強化学習アルゴリズムと、事前学習済みの言語モデルを結合します。
形式言語は、数学的推論を伴う証明の正しさを形式的に検証できるという重要な利点があります。しかし、機械学習における形式言語の使用は、これまで、利用可能な人間が書いたデータの量が非常に限られているという制約がありました。
対照的に、自然言語ベースのアプローチは、桁違いに多くのデータにアクセスできるにもかかわらず、もっともらしいが誤った中間推論ステップとソリューションを幻覚的に提示する可能性があります。私たちは、自然言語の問題ステートメントを正式なステートメントに自動的に翻訳する「Gemini」をファインチューニングし、さまざまな難易度の正式な問題の大規模なライブラリを作成することで、これら2つの補完的な領域の間に橋を架けました。
問題が提示されると、「AlphaProof」は解決策の候補を生成し、「Lean」で可能な証明手順を検索してそれらの解決策を証明または反証します。発見され検証された各証明は、「AlphaProof」の言語モデルを強化するために使用され、その後のより困難な問題を解決する能力を高めます。
私たちは、コンテストまでの数週間にわたって、幅広い難易度と数学のトピック領域を網羅した何百万もの問題を証明または反証することで、IMO向けに「AlphaProof」を学習しました。学習ループはコンテスト中にも適用され、完全な解答が見つかるまで、コンテストの問題の自己生成バリエーションの証明を強化しました。
4. AlphaGeometry 2
「Alpha Geometry 2」は、「AlphaGeometry」の大幅に改良されたバージョンです。これは、言語モデルが「Gemini」に基づいており、前身よりも桁違いに多くの合成データでゼロから学習されたニューロシンボリックハイブリッドシステムです。これによりモデルは、オブジェクトの移動や角度、比率、距離の方程式に関する問題など、はるかに難しい幾何学の問題に取り組むことができるようになりました。
「AlphaGeometry 2」は、前バージョンより2桁高速なシンボリックエンジンを採用しています。新しい問題が提示されると、新しい知識共有メカニズムを使用して、さまざまな検索ツリーを高度に組み合わせ、より複雑な問題に取り組むことができます。
今年の大会前、「AlphaGeometry 2」は過去 25 年間のIMO幾何学問題全体の83%を解くことができました。これは前身の53%の達成率を上回っています。IMO 2024では、「AlphaGeometry 2」は形式化を受けてから19秒以内に問題4を解きました。
5. 数学的推論の新たな境地
IMOの取り組みの一環として、高度な問題解決スキルを可能にする「Gemini」と最新の研究に基づいて構築された自然言語推論システムの実験も行いました。このシステムでは、問題を正式な言語に翻訳する必要がなく、他のAIシステムと組み合わせることもできます。今年の IMO の問題でもこのアプローチをテストしましたが、結果は非常に有望であることが示されました。
私たちのチームは、数学的推論を進化させるための複数のAIアプローチを継続的に模索しており、「AlphaProof」のより技術的な詳細を近日中に公開する予定です。
私たちは、数学者がAIツールを使用して仮説を探求し、長年の課題を解決するための大胆な新しいアプローチを試し、証明の時間のかかる要素を迅速に完了する未来、そして「Gemini」のような AI システムが数学とより広範な推論においてより有能になる未来に期待しています。