AlphaGeometry ── 人の解答例なしでオリンピック幾何を解く AI

AlphaGeometry は、Google DeepMind とニューヨーク大学の研究者が2024年1月17日に Nature で発表した、平面幾何の問題を証明する AI である。2000〜2022年の国際数学オリンピック（IMO）から集めた幾何30問（IMO-AG-30）のうち、競技の制限時間内に25問を解いた。それまでの最高の手法は10問、DeepMind によれば IMO 金メダリストの平均は25.9問である。人間の解答例を一切使わず、機械が自分で合成した1億件の定理と証明だけで学習した点が、この研究の核心だった。

ゲームの AlphaGo（2016年）、タンパク質の AlphaFold（2020年）に続き、DeepMind が「人間の頭脳の競技」として選んだ次の舞台が、高校生の数学オリンピックだった。

なぜ幾何は AI にとって難しかったか

論文は、機械学習で数学の定理を証明させる最大の壁を、学習データの不足に見ている。人間の証明を、計算機が検証できる形式言語に翻訳するには大きな手間がかかる。幾何は特に難しく、汎用の証明支援系 Lean では IMO の幾何問題を書き表すだけでも大量の下準備が要る。そのため幾何の証明例はほとんど存在せず、従来の手法は記号的な計算と、人間が設計した探索の規則に頼っていた。

代表が Wu の方法で、図形の条件を座標の多項式に置き換えて代数的に判定する。すべての問題の真偽を理論上は決められるが、人が読める証明は出てこない。

ニューロシンボリック ── 補助線は言語モデル、推論は記号エンジン

AlphaGeometry は2つの部品を組み合わせた。1つは、角度や比、距離を追いかけて新しい事実を導く記号的な演繹エンジン（論文では DD + AR と呼ぶ）。もう1つは、図に新しい点や線を加える「補助作図」を提案するニューラルネットワークの言語モデルである。DeepMind はこれを「速い直感」と「遅い熟慮」の組み合わせにたとえた。

学習データは自前で作った。ランダムな前提を10億通り近く生成し、記号エンジンで導ける結論とその証明をたどり直して、1億件の合成定理と証明を得た。中には200段を超える証明もあり、論文によればオリンピックの定理の平均の4倍の長さである。Transformer 型の言語モデルをこの全データでゼロから事前学習し、補助作図を要する約9%の証明で追加学習した。

記号エンジンだけで14問、言語モデルの補助作図がさらに11問を加えて25問に達した。論文は、学習データを20%に減らしても21問を解いたと報告している。解けなかった中で最も難しいのは IMO 2008 の第6問で、人間の平均点は7点中0.28点だった。

出力は「人が読める証明」

AlphaGeometry の証明は、計算機で検証されたうえで、人が読める形で出力される。論文によれば、人間の専門家の評価で IMO 2000 と IMO 2015 の幾何問題をすべて解き、IMO 2004 の第1問については、より一般的な形の定理を見つけた。

DeepMind が解答の評価を依頼した数学オリンピックのコーチ Evan Chen は、次のように述べている。「AlphaGeometry's output is impressive because it's both verifiable and clean.」（出力は検証可能で、しかも明快だから印象的だ）。Chen は、AlphaGeometry が座標計算の力技ではなく、生徒と同じように角度や相似三角形といった古典的な幾何の規則を使う点も評価した。フィールズ賞受賞者の Ngô Bảo Châu も、それをやり遂げたことに驚いたとコメントを寄せている。

DeepMind はコードとモデルを公開した。同社は、幾何の能力だけで IMO 2000 と IMO 2015 の銅メダル基準を超えた初の AI だと主張しているが、これは開発元自身の評価である。

基準はどこにあったのか ── 反論と後継

発表から3か月後の2024年4月、Shiven Sinha らの研究者が arXiv に論文を出し、比較の基準そのものを問い直した。彼らによれば、Wu の方法を適切に使うと単独で IMO-AG-30 の15問を解け、従来の記号的手法と組み合わせると21問に達する。AlphaGeometry と組み合わせれば27問になるという。この結果は、成果のどこまでが機械学習によるもので、どこからが記号的手法の底力によるものかを見直す材料になった。

DeepMind 側は改良を続けた。後継の AlphaGeometry2 は 2024年の IMO で AlphaProof と組んで銀メダル水準に貢献し、2025年2月の論文では、2000〜2024年の IMO 幾何問題のうち表現できる割合が66%から88%に、解ける割合が54%から84%に上がったと報告している。

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

AlphaGeometry が解いたのは数学オリンピックのごく一部、幾何だけである。DeepMind 自身、1回の IMO で幾何は6問中おおむね2問しかなく、大会の3分の1にしか使えないと認めていた。それでも、人間のデータが足りない分野で、機械が自分で練習問題を作って学ぶという方法は、同じデータ不足に直面する他の数学分野にも使える枠組みだと論文は位置づけている。

数学オリンピックを教える側にとっては、AI の出力が採点できる証明の形をとったことが大きい。Evan Chen の評価は、過去の AI の解答が当たり外れの多いものだったことと対比されている。この流れは半年後の AlphaProof、翌年の IMO 金メダル水準（2025年）へと続く。全体像は AI と数学の年表 と AI の年表 にある。