AlphaProof ── AI が国際数学オリンピックで銀メダル水準に届く

AlphaProof は、Google DeepMind が開発した、証明支援系 Lean の形式言語で数学の証明を探す AI である。2024年7月25日、DeepMind は AlphaProof と幾何専用の AlphaGeometry 2 を組み合わせたシステムが、英国バースで開かれた第65回国際数学オリンピック（IMO）の6問中4問を解き、42点満点中28点を得たと発表した。この年の金メダル基準は29点で、28点は銀メダル水準の上限にあたる。DeepMind は、AI が IMO でメダル水準に届いたのはこれが初めてだとしている。

ただし条件は人間と同じではなかった。問題は専門家が人手で Lean に翻訳してから与えられ、1問は数分で解けたが、他は最大3日かかった。人間の参加者は4.5時間の試験を2回受ける。銀メダル水準という見出しと、この条件の差の両方を押さえておく必要がある。

IMO 2024 での結果

IMO の公式記録によれば、2024年大会は7月11〜22日にバースで開かれ、108か国・地域の609人が参加した。メダル基準は金29点、銀22点、銅16点以上で、金メダルは58人だった。

DeepMind の発表は、AlphaProof が代数2問と数論1問を解き、答えを見つけたうえでその正しさを証明したと説明している。そこには大会で最も難しく、人間の参加者のうち5人しか解けなかった問題が含まれる。AlphaGeometry 2 は、形式化された問題を受け取ってから19秒で第4問を証明した。組合せ論の2問は解けなかった。

採点は、IMO 金メダリストでフィールズ賞受賞者の Timothy Gowers と、2度の IMO 金メダリストで IMO 2024 問題選定委員長の Joseph Myers が、IMO の配点規則に従って行った。Gowers は、プログラムが自明でない構成を思いついたことを非常に印象的だと評し、自分が考えていた最先端をはるかに超えているとコメントしている。

AlphaProof のしくみ ── 自動形式化と強化学習

AlphaProof は、事前学習した言語モデルと、チェス・将棋・囲碁を独学した AlphaZero の強化学習アルゴリズムを組み合わせている。形式言語で書かれた証明は、計算機が論理の規則に照らして正しさを確かめられる。その代わり、人間が形式言語で書いた問題や証明は自然言語に比べて桁違いに少ない。これが AlphaGeometry（2024年1月）と同じ「データ不足」の壁だった。

DeepMind はこれを機械翻訳で越えた。Gemini をもとにした大規模言語モデルを、自然言語の問題を形式言語へ訳すよう調整し、2025年の Nature 論文によれば約100万問から約8,000万問の Lean の問題を作った。訳が原文に忠実でなくても、それ自体が有効な練習問題になる。AlphaProof はこれを証明または反証しながら自分を鍛え、主な強化学習には約8万 TPU 日（たとえば TPU 4,000基で20日分）を費やした。

大会中には「テスト時強化学習」と呼ぶ方法も使った。解けない問題に対して、その変種を大量に自分で作って解き、問題ごとに適応していく。論文によれば第1・2・6問はそれぞれ2〜3日のテスト時強化学習を要した。

AlphaGeometry 2 は、言語モデルを Gemini ベースにし、前作より1桁多い合成データで学習した改良版である。

何が言えて、何が言えないか

この結果は、数学 AI の研究者にとって大きな一歩だった。Nature 論文は、多日の計算を要したとはいえ、知る限り AI が初めてメダル水準に達した例だと書いている。形式証明なので、AI が「解けた」と主張する証明は Lean が機械的に検査でき、幻覚のような誤りが入り込む余地が小さい。この点は、ケプラー予想の Flyspeck（2014年）以来の形式検証の流れを AI の側から引き継ぐものだった。

一方で、比較には但し書きが要る。DeepMind 自身が翌年の発表で、2024年の方式は専門家が問題を Lean などの専用言語に翻訳し、証明を逆に訳し戻す必要があり、2〜3日の計算もかかったと総括している。組合せ論の2問がまったく解けなかったことも、得意と不得意の偏りを示した。

誰にとって何が変わったか

数学オリンピックは、この年を境に AI の能力を測る公開の目標になった。参加する高校生にとっては、自分たちの問題が企業の研究発表の舞台にもなるという変化である。数学者にとっては、Lean とその共有ライブラリで形式化された数学が、AI の訓練と検証の基盤として価値を持つようになった。Nature 論文は、Lean と共同ライブラリ Mathlib を、数学の形式化という歴史的な流れの延長に位置づけている。

1年後の IMO 2025 では、DeepMind と OpenAI の汎用モデルが、人手の翻訳なしに自然言語で、しかも制限時間内に金メダル水準に達したと発表する。AlphaProof そのものは、2026年に研究用の証明探索システム AlphaProof Nexus の部品として再び登場する。流れは AI と数学の年表 と、組織としての DeepMind のページにある。