AI（人工知能）モデルはエッセーなどの文章を簡単に生成できる。しかしながら、数学の問題を解くのは得意とは言い難い。数学の問題を解くには論理的な推論が必要なことが多いが、現在のほとんどのAIシステムでは対処できない。
だが、そうした状況についに変化が訪れるかもしれない。2つの特殊なAIシステムを訓練した結果、高度な推論を含む複雑な数学の問題を解くことに成功した、とグーグル・ディープマインド（Google DeepMind）が発表したのだ。それぞれ「アルファプルーフ（AlphaProof）」「アルファジオメトリー（AlphaGeometry） 2」と名付けられたこれらのシステムは、今年の国際数学オリンピック（IMO、高校生が参加する権威ある大会）の6つの問題のうち合計4つを解いた。これはIMOの銀メダルに相当する成績である。
この手の問題でAIシステムがこれほど大きな成功を収めたのは初めてのことだ。「機械学習やAIの分野における偉大な進展です」。グーグル・ディープマインドで今回のプロジェクトに取り組んだプシュミート・コーリ研究担当副社長はそう語る。「このレベルの汎用性において、このような成功率で問題を解くことができるシステムが開発されたのは初めてです」。
AIシステムにとって、高度な推論を要する数学の問題を解くのが難しい理由はいくつかある。こうした問題では抽象概念を形成し、利用することがしばしば必要となる。また、複雑で階層的な計画や下位目標の設定、バックトラッキングに加え、新しい経路の試行も伴う。AIにとって、これらの作業はすべて難易度が高い。
「例えば、形式言語を使って回答を確認できる方法があれば、AIモデルの数学の訓練は簡単になることが多いです。ですが、自由形式の自然言語と比べて、ネット上には形式的な数学データが少ないのです」。数学とAIを専門とするケンブリッジ大学のケイティ・コリンズ研究員はそう話す（同研究員は今回の研究には参加していない）。
そうしたギャップを埋めることが、アルファプルーフを開発した際のグーグル・ディープマインドの目標だった。アルファプルーフは、形式的なプログラミング言語「リーン（Lean）」で数学的命題を証明するための自己訓練を実行する強化学習ベースのシステムだ。鍵となるのは、自然な非形式言語で書かれた数学の問題を、AIが処理しやすい形式的な内容に自動変換するように調整した、ディープマインド製AI「ジェミニ（Gemini）」の1つのバージョンである。これによって、様々な難易度の形式的な数学の問題を有する大規模なライブラリーが誕生した。
データを形式言語に変換するプロセスの自動化は数学コミュニティにとって大きな前進だ、とエディンバラ大学でハイブリッドAIの講師を務めるウェンダ・リーは言う（今回の研究の査読を担当したが、プロジェクトには参加していない）。
「この証明システムを形式化できれば、公表された結果の正確性に対する確信が深まるでしょう。協力的な体制もより強化されます」とリー講師は付け加える。
このジェミニ・モデルは、グーグル・ディープマインドが碁やチェスなどのゲームを習得するために訓練した強化学習モデル「アルファゼロ（AlphaZero）」と連携し、無数の数学の問題を証明、または反証する。解けた問題が増えるほど、アルファプルーフは複雑さを増す問題にうまく対処できるようになった。
アルファプルーフが幅広い分野の数学の問題を解く訓練を受けたのに対し、アルファジオメトリー2（グーグル・ディープマインドが今年1月に発表したシステムの改良バージョン）は、物体の動きに関する問題や角度・比率・距離が含まれた方程式の処理について最適化された。前のモデルよりも大幅に総合的なデータで訓練されたため、より難易度の高い幾何学の問題に対処できた。
これらのシステムの能力を検証するため、グーグル・ディープマインドの研究チームは、「今年のIMOで競技参加者に出題された6つの問題を解いて回答が正しいことを証明せよ」という課題を与えた。アルファプルーフは代数の問題2つと数論の問題1つを解いた。そのうちの1つはIMOで最高難易度の問題だった。アルファジオメトリー 2は幾何学の問題を1つ解いたが、組み合わせ論（集計と物体の配置を扱う数学分野）の問題2つは未回答だった。
「全体的に、アルファプルーフは組み合わせ論よりも代数や数論の成績が良好です」と、アルファプルーフ・チームのアレックス・デイヴィース研究エンジニアは言う。「私たちはその理由を探るための研究を続けており、それがシステムの改善につながることを願っています」。
ティム・ガワーズとジョゼフ・マイヤーズという2人の高名な数学者が、AIシステムが回答した内容を精査した。その結果、4つの正答に満点（7点中7点）が付き、最大42点のうち計28点の評価がシステムに与えられた。29点以上で金メダルとなるため、人間がこの点数を獲得した場合にはやや足りず、銀メダルが授与される。
IMOの問題でAIシステムがメダルに相当する成績を収めたのは初めてのことだ。「数学者の1人として、この成績には非常に感銘を受けます。以前の能力から大幅な躍進です」とガワーズは記者会見で語った。
マイヤーズも、これまでのAIの能力と比較して2つのシステムの数学の回答が大きな進展を示していることに同意する。「システムの拡張や計算速度アップの可能性は興味深い点です。また、数学の他の分野にも広げられるのか、見ものです」。
さらに高度な数学の問題に対処できるシステムが誕生すれば、人間とAIの素晴らしい連携のための道が開かれ、数学者が新たな種類の問題を解いたり考案したりする助けになる可能性がある、とケンブリッジ大学のコリンズ研究員は言う。そこから、人間が数学に取り組むプロセスをさらに解明する手がかりが得られるかもしれない。
「人間が複雑な数学の問題を解く過程については、まだ分からないことがたくさんあります」と同研究員は話す。