AIが国際数学オリンピックで『銀メダル級』に届いた — スタートアップが数学に殺到する本当の理由
2024年の夏、AIが国際数学オリンピックの本番6問のうち4問を解いた。42点満点で28点、金メダルの基準にあと1点という銀メダル級の成績だった。場所は紙の上、人間の参加者と同じ問題で。
人間の天才が4時間半かけて挑む問題を、機械が解いた
やったのは Google DeepMind の二つのシステム、AlphaProof と AlphaGeometry 2。舞台は2024年7月にイギリス・バースで開かれた国際数学オリンピック（IMO）の本番問題だ。世界中の高校生トップが2日間、1日4時間半ずつかけて挑むあの試験である。
内訳まで見ると面白い。代数と整数論の3問（1番・2番・6番）を AlphaProof が、幾何の1問（4番）を AlphaGeometry 2 が解いた。残った組合せ論の2問は、最後まで解けなかった。解けた4問はすべて満点。合計28点。その年の金メダルのボーダーが29点だったから、文字どおり「あと1問の最後の1点」に届かなかった。
ここに最初の「へえ」がある。賢さと速さは別物だった、ということ。
鍵は、答えを『機械が採点できる形』で書くこと
ChatGPT に数学を解かせて、堂々と間違えられた経験はないだろうか。あれが起きるのは、AIが文章として「それっぽい答え」を生成しているだけで、正しさを自分で確かめていないからだ。
AlphaProof の作法はそこが違う。証明を Lean という言語で書く。Lean は数学の論理を1行ずつコンピュータが検算できる「形式言語」で、ごまかしが効かない。各ステップが正しいか、機械が真偽を判定する。研究チームによれば、AlphaProof は自分で大量の問題を作って Lean で解いては採点し、その失敗と成功から学んでいく仕組みで鍛えられたという。
数学が特別なのは、答えが「合っているかどうか」を人間の好みなしに判定できる点にある。AIにとって、嘘をついてもすぐバレる珍しい遊び場だ。
つまり数学は、AIに「適当を言わせない」訓練場になりうる。この発想が、いま静かに業界をざわつかせている。
なぜ、毎晩 AI に質問しているあなたに関係あるのか
AIが平気で事実をでっち上げる現象を「ハルシネーション（幻覚）」と呼ぶ。検索のかわりにAIへ聞く頻度が増えた人ほど、これに何度も足をすくわれているはず。
数学の証明は、その逆をいく。すべての手順が検算可能で、嘘が混じれば機械が弾く。だから「数学が解けるAI」を育てることは、回り道に見えて、根拠を一歩ずつ積む思考そのものを仕込む作業に近い。ここを鍛えればAI全体が信用できる方向に寄る、という賭けが成り立つ。
その賭けに本気で乗ったのがスタートアップたちだ。Robinhood の共同創業者 Vlad Tenev らが立ち上げた Harmonic は「数学的超知能」を掲げ、巨額の資金を集めている。研究機関 Epoch AI は FrontierMath という、プロの数学者でも手こずる超難問だけを集めた評価ベンチマークを公開した。発表当時、最先端のAIモデルでも正解率は数%にとどまったとされる（このベンチマークの論文は arXiv に公開された査読前のプレプリント段階である点に注意）。
| IMO 2024 | 人間の参加者 | DeepMind のAI |
|---|---|---|
| 考える時間 | 1日4時間半 × 2日 | 問題により最大3日 |
| 解けた問題 | 金は6問中ほぼ全問の猛者も | 6問中4問（28/42点） |
| 苦手だった分野 | 人それぞれ | 組合せ論の2問は未解決 |
AIが数学者の仕事を本当に変えると思う？
でも、『解いた』の中身をよく見ると
盛り上がりに水を差すようだが、限界もはっきりしている。さっきの表のとおり、AIは1問に何日もかけている。人間が4時間半で出す答えと、同じ「解いた」でくくっていいのかは議論の余地がある。組合せ論の2問を落とした事実も、得意・不得意のムラを示す。
もう一つの壁が、問題を Lean のような形式言語に「翻訳」する工程だ。ここは今もかなりの部分を人手が支えていて、ここが詰まると自動化は途中で止まる。世界の難問を片端から解く万能機械、とはまだ遠い。
数学者の Terence Tao は、こうしたツールを自分の研究に取り込みながらも、AIを「置き換え」ではなく強力な共同作業者として位置づける見方を繰り返し語ってきた。証明を思いつくのは人間、その正しさを高速で検算するのが機械、という分業。
銀メダルまで来たのは事実。金まであと1点も事実。ただ、その1点の重さがどれくらいなのかは、来年の本番が静かに教えてくれる。
参考・出典
- AI achieves silver-medal standard solving International Mathematical Olympiad problems (AlphaProof and AlphaGeometry 2) (Google DeepMind AlphaProof and AlphaGeometry teams, 2024) — Google DeepMind
- FrontierMath: A Benchmark for Evaluating Advanced Mathematical Reasoning in AI (Elliot Glazer et al. (Epoch AI), 2024) — arXiv preprint (査読前)
- Solving olympiad geometry without human demonstrations (AlphaGeometry) (Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, Thang Luong, 2024) — Nature
