AlphaProofとAlphaGeometry 2、国際数学五輪で銀メダル相当の成績を達成

国際数学オリンピック（IMO）は、長年にわたりAIにとって最も過酷な知性の試金石とされてきました。最高峰の高校生数学者たちが何千時間も特訓して挑む難問に対し、現在の大規模言語モデルは途中でもっともらしい嘘をつき、論理の破綻を起こすのが常でした。

しかし7月25日、Google DeepMindはその壁を破りました。新たに開発した「AlphaProof」と強化版の「AlphaGeometry 2」を組み合わせ、2024年大会の全6問中4問を完答。42点満点中28点を獲得し、銀メダル最上位に相当する成績を収めました。今年の金メダル基準である29点まで、あとわずか1点でした。

AlphaZeroの手法を形式数学へ応用

今回の挑戦では、まず問題文が手作業で「Lean」と呼ばれる形式数学言語へ翻訳されました。採点はフィールズ賞受賞者であるTimothy Gowers教授と、今年のIMO問題選定委員長を務めたJoseph Myers博士が担当し、正解した4問すべてに満点の7点を与えています。

主役となったAlphaProofは、Geminiベースの言語モデルと、囲碁や将棋を制覇したAlphaZeroの強化学習を組み合わせたシステムです。代数2問と整数論1問を解き明かしました。この中には、参加した精鋭高校生609人のうちわずか5人しか解けなかった今大会最難関の問題も含まれています。

一方のAlphaGeometry 2は、幾何学問題をわずか19秒で解決しました。ただし、残る2問の組合せ論（コンビナトリスク）の問題は解くことができませんでした。また、人間の制限時間が4.5時間2回であるのに対し、AIは問題によっては証明の探索に最大3日間を費やしました。

形式言語Leanで「ハルシネーション」を封じる

なぜ従来のLLMは高度な数学が解けなかったのか。自然言語で書かれた証明は、途中に論理の飛躍や誤りがあっても一見正しそうに見えてしまうからです。

DeepMindはこの課題を巧みに回避しました。自然言語の問題文をLeanの形式記述へ自動変換した上で、AlphaProofに証明のステップを探索させます。Leanの環境では、1ステップ進むごとに論理が正しいかどうかをコンパイラが厳密に検証します。正しい証明だけを報酬として強化学習を回すことで、モデルのハルシネーションを原理的に排除しました。

なぜ重要か

囲碁やチェスのような明確なゲームの枠組みを超え、厳密な純粋数学の領域でもAlphaZero式の自己対局アプローチが通用することを証明した意義は極めて大きいです。

数学者にとっては、信頼できる共同研究ツールの実現が現実味を帯びてきました。Leanによる厳密な検証が担保されているため、AIが提示した証明の真偽を疑う必要がありません。長年放置されてきた難問の補助定理の検証や、人間では時間がかかりすぎる膨大な計算・検証作業をAIに任せられるようになります。

もっとも、手放しで万能と言えるわけではありません。問題文をLeanへ落とし込む作業には依然として人間の専門家による翻訳が必要でした。また組合せ論で完敗したことや、数日がかりの計算リソースを要した点は、柔軟なひらめきや直感が求められる分野における課題を浮き彫りにしています。それでも、厳密な推論をこなす真のAGIへの道筋として、極めて堅実な一歩を踏み出したと言えます。