ついにAIが数学オリンピックの金メダリストに迫る

以前に、Google DeepMindがプログラミングのアルゴリズム開発にAIで挑戦しているという話をしました。数学の技法へのチャレンジです。

２０２４年になってDeepMindは、新しいアルファシリーズとしてもっと直接的に「数学者」への挑戦を始めました。
１月の発表時点で、数学者の登竜門にあたる「数学オリンピック」の幾何学問題を解くことが出来るようになっています。
AlphaGeometryと呼ばれ、ニューラル言語モデルと記号推論エンジンという2つの部分から構成され、両者が強みを補いあうような仕組みです。過去記事を載せておきます。

そしてついに、さらに進化したAlphaproofと呼ぶAIを開発し、金メダリストまであと一歩のハイスコアをたたき出しました。

DeepMind hits milestone in solving maths problems — AI’s next grand challenge

AI achieves silver-medal standard solving International Mathematical Olympiad problems

前回のAlphaGeometryとは全く異なる新しいAIで、（一般的に）幾何学よりも難しいとされる代数、組合せ論、数論などの分野でも解くことが出来ます。ちなみにAlphaGeometry自体もバージョン2を開発しており幾何学に特化してさらに解くスピードが上がっています。

最近行われた2024年国際数学オリンピック（IMO）で、実際に出題された6問のうち4問を、Alphaproofが解きました。公平を期すため（本番同様に）トップクラスの数学者2人が採点し、金メダルにわずか1点差の28/42点を獲得したということです。

出所：上記Google Blog記事内の図

ちなみに、AI向けの「AI数学オリンピック（AIMO）」と呼ばれる賞金500万ドルの大会も実際にあります。今回開発されたAlphaproofはこの賞金を獲得する能力にふさわしいのですが、コードをオープンソースにすることや限られた計算能力で動作することなどの厳しい基準があり、賞の獲得には至らなかったようです。（それを目指したとは思えませんが）

もう１つケチをつけると、公式コンテストでは、学生は 4.5 時間のセッションを 2 回に分けて回答を提出します。一方AIは、 1 つの問題は数分以内に解きましたが、他の問題を解くのに最大 3 日かかりました。

ということで、公平性を重んじるなら試験を解くという条件なら、まだメダリストと呼ぶには早そうです。

Googleの発表によれば、新たに開発されたAlphaproofは形式言語LEANとAlphaZeroの仕組みを統合した仕組みだそうです。

「形式言語」という言葉は初耳でしたが、どうも数学的推論を伴う証明の正しさを形式的に検証できる利点があるようです。
従来はその学習データ量が少ないのが課題だったのですが、それを自然言語に強いGeminiをチューニングすることで改善したとのこと。

まさに既存の発明を新しく組み合わせた発明で、イノベーションが加速化する１例を目のあたりにしました。

ただ、くれぐれも「数学者 vs AI」という不毛な対立構図にはならないように願っています。