国際数学オリンピック（IMO）はAIの数学能力について何を教えてくれるか？

今年の国際数学オリンピック（IMO）は、7月15日と16日にオーストラリアのサンシャインコーストで開かれる。高校生の数学コンテストの頂点に立つ大会だ。オリンピックと同じく、懸かっているのは国の誇りと個人の栄誉である。

AIモデルの開発者たちも、自分たちが誇りと栄誉を手にする見込みを推し量っているに違いない。IMOの金メダルに相当する得点を挙げたAIシステムはまだなく、満点などなおさらだ。今年こそがその年になるのだろうか？

この記事では、さまざまな結果がAIの数学能力について何を意味しうるかについて、私の考えを述べる。特に、話題をさらうかもしれない結果と、実際に何か新しいことを教えてくれる結果との間には、いくつか重要な違いがあると考えている。

私が念頭に置いている主な背景事実は次のとおりだ。

• 出発点はすでに高い。 形式的な数学の証明を出力する特化型システムであるGoogleのAlphaProof¹は、2024年のIMOで6問中4問を解いた。IMOに似たコンテストである2025年のUSAMOでは、最良の汎用LLMがすでに6問中2問を解ける。進歩とは、これを上回ることを意味する。
• LLMは特に証明が苦手である。 LLMを数学に強くする強化学習（RL）は、短い形式の答えをもつ問題に大きく依存している。IMOの問題は違う。解答は、与えられた命題を厳密に証明しているかどうかで判定される。AlphaProofはそもそもそのように設計されているが、LLMはこの点でそれほど巧みではなかった。
• どのAIシステムにも創造性の欠如が見られる。 2024年のIMOでAlphaProofが解いた唯一の超難問を、AlphaProofはきわめて力ずくのやり方で解いた。これはLLMにも一貫して見られる限界のようだ。しかしIMOの問題の中には、人間なら創造性と認めるようなものを必要とするように見えるものがある。
• メダルは当てにならない指標である。 人間とAIシステムでは、問題を難しく感じる理由が異なるが、金メダルに必要な得点は人間の得点分布だけで決まる。「AIが金メダルを獲得」の意味は、問題がAIの得意分野に合っていて人間には特に難しいものだったのか、それともその逆だったのかによって、まったく違ってくる。

これを踏まえて、ありうる結果を次のように整理したい。

• まったく改善が見られない可能性も十分にある。 AlphaProofが2〜4問、LLMが1〜2問を解くかもしれない。これは従来の能力からの進歩がないことと整合するし、単に問題がAIシステムにとって異例に難しかったためということもありうる。
• AlphaProofが金メダルを獲っても、何もわからないかもしれない。 運が悪ければ、創造性をあまり必要としないIMOの問題ばかりということもありうる。その場合でも問題は人間にとって難しいが、AIシステムは力ずくの解法を見つけられるかもしれず、それは特に興味深い能力や新しい能力を示すものにはならない。AlphaProofにとっては、これが最も起こりそうな結果ですらあるかもしれない。昨年、AlphaProofは少し運が悪かったのだ。
• LLMが金メダルか銀メダルを獲れば、証明の能力が向上していることになる。 LLMがAlphaProofの証明を書く能力に追いつくには、まだ道のりがある。金メダルか銀メダルを獲れば、その差をいくらか縮めたのだろう。しかし、この達成の意義は限られる。数学者には役立つが、それ以上のものかどうかははっきりしない。
• 最も興味深い結果は、創造的な問題解決の証拠だろう。 これが本命だ。新しい数学的能力を示すだけでなく、より広い有用性に向けた実質的な進歩も示唆するだろう。良くも悪くも、これが起きたかどうかは、個々の問題を詳しく見て、AIシステムがそれをどう解いたかを判断することでしかわからない。

創造的な問題解決は、ある未解決の問いに関わる。AIシステムは学習分布の外にどこまで汎化できるのか、という問いだ。汎化できればできるほど、あらゆる分野でAIによる飛躍的進歩が見られる可能性が高まる。何を予想すべきかはわかりにくい。一方では、この種の創造性の例はこれまでほとんどない。他方では、ゲームのプレイのように数少ない例のいくつかは、スケールアップしたRLから生まれている。そしてモデルの開発者たちは、まさにRLのスケールアップに明け暮れてきた。それは実を結ぶのか、それとも行き詰まるのか？　IMOはその兆しを示してくれるかもしれない。ただし、メダルの色によってではない。²

記事の残りでは、これらの論点を裏づけていく。では、詳しく見ていこう！

Epoch AI の最新情報を受け取る 購読する

IMOの背景

IMOは2日間にわたって行われ、参加者は各日4.5時間で3問を解く。各国は最大6人の参加者からなるチームを送り込み、全員が個人で試験を受ける。解答は自然言語による証明の形をとり、人間の専門家が採点する。各解答は0〜7点で採点され、部分点はめったに与えられない。命題の証明を求める問題もあれば、特定の量や式を求めさせる問題もある。後者の問題でも、解答は証明の厳密さに基づいて採点される。正しい最終的な答えを見つけただけで、それが正しいことを証明していない解答は、最大でも1点しかもらえない。

メダルはおおむね参加者の上位半分に授与される。上位約8%に金、次の約16%に銀、次の約24%に銅だ。過去10年のうち3年は、4問で満点を取れば金メダルに十分だった。それ以外の年は5問が必要だった。

各国は人口や教育制度の発達度にかかわらず6人の参加者を送るので、IMOの参加者全員が世界で最も数学のできる高校生の一人だというわけでは、おそらくない。とはいえ、各国のトップは参加しているとみてよいだろう。スター級の才能が集まっているのは確かだ。フィールズ賞受賞者の少なくとも3分の1は、若い頃にIMOのメダリストだった。³

IMOの各日には通常、易しい問題、中程度の問題、難しい問題が1問ずつ出る。⁴ たとえば、2024年の問題に対する人間の得点分布は次のとおりだ。P1とP4はほとんどの参加者が解いた。P2とP5の分布は二峰性で、約3分の1が満点を取った。P3とP6を解いた参加者はごくわずかだった。⁵

IMOの問題はどれも、ある程度の厳密さと正確さを要する。証明は注意深く組み立てなければならない。また、競技向けの高度な高校のカリキュラムで学ぶ背景知識を、的確に応用することも通常必要になる。

易しめの問題に必要なのは、それくらいだ。難しめの問題には、さらに三つの要素が加わると私は考えている。抽象化、創造性、深さである。抽象化とは、公式を機械的に当てはめるだけでなく、問題の対象について一般的な真理を導き出す必要があることを指す。創造性とは、背景知識を素直に応用するだけでなく、何か新しいものを考え出す必要があることを指す。深さとは、解法をやり遂げるのに必要なステップの数を指す。もちろん、これらの要素は組み合わさることもある。最も難しい問題は多くのステップを必要とし、その一つひとつに新しい抽象化が関わる。

IMOの評判を作っているのは、最も難しい問題だ。P1とP4は、有能な数学科の学部生にとっては手慣れたものかもしれない。P3とP6は、プロの数学者にとってさえ非常に難しいことがある。⁶

AlphaProofはすでに高い水準を打ち立てたが、いくつかの重要な能力が欠けていた

IMOでのAIの現在の記録をもつのはAlphaProofである。その構成には少なくとも一つのファインチューニングされたLLMが含まれているが、AlphaProofは今日の主要なLLMとはあまり似ていない。多くのタスクをこなせるのではなく、数学の問題を解くことしかできない。自然言語を生成するのではなく、Leanと呼ばれる数学の証明を書くための専用言語しか出力しない。したがって、この種のシステムは分けて分析するのが最善だと考える。

AlphaProofは最も難しい問題を、意外なほど面白みのないやり方で解いた

2024年のIMOで、AlphaProofはP1、P2、P6を解いた。易しい問題、中程度の問題、難しい問題が1問ずつである。⁷ 易しい問題と中程度の問題は、その後、より汎用的なLLMも解けるようになったとみてよいだろう。これについては後で述べる。AlphaProofが名を上げた本当の理由は、今もP6を解いたことにある。この問題を解いた人間はほとんどいなかった。

しかし、さらに詳しく見ると、AlphaProofがP6を解いたやり方が多くを物語っている。P6は代数の問題だ。ある関数が与えられた性質を満たすならば、別の性質も満たすことを証明せよ、というものである。人間の解き方は、そうした関数についてさまざまな抽象的な性質を証明し、それを積み上げて目的の性質を証明することだ。たとえば、自然な第一歩は、与えられた性質からその関数が単射であることが導かれると気づくことである。そこから先は難しくなるが、各ステップは質的には似ている。

AlphaProofはこうしなかった。代わりに、与えられた性質を何度も何度も適用して証明を生成した。大まかに言えば、それは長く退屈な場合分けの分析に等しい。論理的には成り立っている（Leanがそれを保証する）が、人間が読みたいと思うようなものではまったくなく、ましてや書きたいと思うようなものではない。さらに、ほとんどの数学者は、この種の「力ずくでやり抜く」推論は、興味深い数学の問題の大半にとって行き止まりだと考えるのではないかと思う。言い換えれば、これはおそらく、特に重要な能力を示すものではない。⁸

AlphaProofは、より創造性を必要とする問題を解けなかった

同じくらい興味深いのは、AlphaProofが解けなかった問題、P3とP5である。これらの問題には「力ずくでやり抜く」解き方がないようだ。参加者は何らかの抽象的なレベルで、より深い構造を理解しなければならず、さもなければ先に進めなかった。また、どちらも組合せ論の問題で、組合せ論の問題は最も独創的で型破りな設定をもつことが多い。⁹ 組合せ論の問題は、比較的少ない背景知識と比較的多くの創造性に頼ることが多く、P3とP5もそうだと思う。

今年もおそらく、少なくとも1問は難しい組合せ論の問題が出るだろう。評価の高い問題難易度の格付けシステムによれば、過去10回のIMOのうち8回で、そうした問題が少なくとも1問出ている。しかしこの格付けは、2024年が少し異例だったことも示している。名目上「中程度」のP5が、難しい側に位置していたのだ。少なくともそれと同程度に難しい組合せ論の問題が2問出たのは、過去10回のIMOのうち3回だけである。2025年の結果を解釈するときには、この問題構成を念頭に置く必要がある。

幾何はあまり多くを教えてくれない

ユークリッド幾何の問題はIMOの定番だが、AlphaProof自体は幾何の問題を解かなかった。AlphaGeometry2という特化型システムに任せたのである。このシステムは、Googleがユークリッド幾何を表現するために考案したドメイン固有言語で証明を生成するよう学習させられている。それ以前のバージョンであるAlphaGeometryも、すでにIMOの難しい幾何の問題を解くことができた。AlphaGeometry2は、2024年のIMOで唯一の幾何の問題だったP4をあっさり片づけた。

残念ながら、これはそれほど興味深いことではないと思う。きわめて限定された領域に特化したシステムなので、汎用的なAIについて多くを教えてくれるとは思わない。

AlphaProofのようなシステムが高得点を挙げたら、個々の問題を見る必要がある

ここで、先に述べたシナリオの区別を、もっと細かく説明できる。

2025年のIMOで難しい組合せ論の問題がたまたま0問か1問しかなければ、AlphaProofが6問中5問か6問を力ずくで解くだけで金メダルを獲る可能性は十分にある。難しい幾何の問題にたまたま偏っていれば、なおさらだ。これは見出しを飾るだろうが、現在の能力から見て大した新情報にはならない。それでも、かなり起こりそうなことだと思う。私はAlphaProofが金メダルを獲る確率を全体で70%と見ており、その確率のほぼすべてがまさにこのシナリオによるものだ。

「力ずくでやり抜く」解法かどうかは「見ればわかる」という面もあるが、IMOの主催者が採点者のために用意する詳細な解答ガイドと、AIの解答を比べることもできる。たとえば2024年のガイドにはP6の解法が7通り載っているが、AlphaProofの解法に似たものは一つもない。人間が見落とした洞察に富む解法をAIシステムが見つける可能性もあるが、IMOの主催者は問題をあらゆる角度から検討しようと本当に努めている。特に、意図しない近道がないことを確かめている。したがって、もしAlphaProofが解答ガイドに載っていない解法を見つけたとしたら、それはおそらく面白みのない解法を見つけたからだろう。

しかし、2025年のIMOに難しい組合せ論の問題、あるいはより一般に「力ずくでやり抜く」解法を許さない問題が出る可能性もある。その場合、5問か6問を解けば、間違いなく新境地を開いたことになる。何らかの理由でAlphaProofが易しめの問題で失敗しつつも、この新境地を開くことさえありうる。その場合も、ほぼ同じくらい大きな新情報だと私は考える。AlphaProofがその創造性で私たちを感心させる確率は、5%にすぎないと見ている。

以上の議論はAlphaProofに限ったものだが、形式的な証明を生成するよう特別に設計されたどのシステムにも、おおむね同じことが言えると思う。¹⁰

AlphaProofについての補足

ほかに触れておく価値のあることが二つある。

第一に、2024年のIMOでは、AlphaProofは問題を解くのに数日与えられた。人間に与えられる4.5時間よりはるかに長い。私はこれを特に重要だとは思わない。最も興味深い問いは、AIシステムがそもそもこれらの問題を解けるかどうかである。事後的な高速化は、「単なる」工学で実現できることが多い。

第二に、昨年のIMO以来、AlphaProofについての話はほとんど聞かない。これは意外だ。その後も、USAMOや大学生向けの最高峰のコンテストであるPutnamなど、ほかの有名な数学コンテストがあったからだ。なぜGoogleはそこで注目を浴びようとしなかったのか？　AlphaProofは、AlphaEvolveのような数学システムと比べてさえ比較的アカデミックなタスクなので、それ以上投資しないことにしたのかもしれない。¹¹ あるいは、進歩させるにはコストがかかりすぎる、あるいは単に不可能だと判断したのかもしれない。いずれにせよ、AlphaProofについて何も発表されない可能性もある程度あると思う。上で示した確率は、AlphaProofの結果がそもそも公表されることを条件としたものだ。¹²

汎用LLMには伸びしろがもっとある

LLMについての最良の参照点は、おそらく2025年のUSAMOだろう。USAMOは米国のIMO代表チームの選考に使われる米国の全国大会で、形式はIMOと同一、難易度も同程度である。¹³ データはMathArenaから得られる。MathArenaは、USAMOの各問題をモデルに出題し（4回サンプリング）、人間の採点者を立てて出力を判定させた。

結果をまとめると、モデルはP1とP4は解けるが、残りは解けない、ということになる。¹⁴ 他の問題でも10%未満の得点を取るモデルがいくつかある（つまり、ときおり約1/7点の部分点を得る）が、これもあまり重く見るべきではないと思う。結果を調べたところ、モデルは本当の進歩の兆しを見せているのではなく、たまたまこの部分点にありついているのだと思う。

Deep Thinkは、これより良い結果が出ることを示唆している

Gemini 2.5 Proのまだ公開されていないDeep Thinkモードは、2025年のUSAMOのP2を解いたと発表された。大まかに言えば、2025年のUSAMOのP2は、2024年のIMOのP2（AlphaProofが解いた唯一の中程度の問題）と、問題のタイプも難易度も似ていると思う。¹⁵ どちらのAIの解答も「力ずくでやり抜く」ものだとは言わない。かなり人間らしい解答だ。とはいえ私の見るところ、これらの問題に必要なのは、背景知識の注意深い応用とある程度の深さであり、特に高い創造性ではない。¹⁶

言い換えれば、IMOの中程度の問題には、おそらくLLMの手の届く範囲にある、少なくともGemini 2.5 Pro Deep Thinkの手の届く範囲にあるタイプのものがある。¹⁷ 2025年のIMOの中程度の問題が2問ともこのタイプなら、LLMは4問を解けるかもしれない。しかし2024年のIMOのP5が示すように、より創造性を必要とする中程度の問題もあり、それについては、AIシステムが解けるところまで来ているという公開された証拠はない。¹⁸ 2025年のIMOの中程度の問題が2問ともこのタイプなら、LLMは2問しか解けないかもしれない。

したがって、LLMが3問か4問を解けば、証明を要する問題を解く能力で、漸進的な進歩が続いていることは間違いない。さらに、上振れの余地もある。もしそのうちの1問が2024年のP5に匹敵する創造性を必要とするなら、それは質的に新しいことだ。確かめるには問題を詳しく見る必要がある。

難しい問題についても、おおむね同じことが言える。LLMがP3かP6を解けば、少なくとも、証明を書く能力の大きな飛躍を意味するだろう。ほかに何もなくとも、それは長い証明になるはずだからだ。LLMの証明がAlphaProofのような「力ずくでやり抜く」スタイルなら、本当にそれ以上の意味はない。そうではなく、LLMの証明がかなりの創造性と抽象化を含んでいれば、それは「すごい」と言える領域だ。

あまり知られていない背景知識で問題が解けてしまうなら、話はまったく変わる

IMOの問題は、あまり知られていない知識を必要としないことになっている。しかし、問題の作者は実際の数学研究から着想を得ることがある。問題を解くための技巧が専門誌のマイナーな論文で扱われていて、コンテストの主催者は、参加者がそうした論文を読んでいるリスクをごく小さいとみなしている、ということもありうる。一方、LLMはほぼすべてを読んでいる。

たとえば、2025年のUSAMOのP3は、ガブリエルグラフと呼ばれる主題に関係していた。LLMの解答の試みを見ると、LLMがこのつながりに気づいていたことがわかる。この場合、それは問題を解けるほどのヒントにはならなかったが、コンテストの主催者は、参加者がこのつながりに気づくことなどまったく想定していなかったに違いない。

したがって、LLMが解いたすべての問題について、特に難しめの問題を解いた場合には、高度な知識を利用していないかどうか、解答を調べる必要がある。これはいかなる意味でも「ずる」ではないが、引き合いに出された知識によって創造的な抽象化を考え出す必要がなくなるのなら、生来の数学的能力が見かけより低いことを示しているのは確かだ。

幾何はやはり、あまり多くを教えてくれないだろう

LLMには、幾何の問題に取り組むLLMなりの、面白みのないやり方がある。より直観的で空間的なやり方で解くのではなく、問題をxy平面やxyz空間などの座標系に変換し、何ページにもわたる代数方程式を延々と処理するのだ。この手法でうまくいくこともあるが、人間がコンテスト中に試すには、たいてい時間がかかりすぎる。また、エレガントでないとみなされる。

2025年のUSAMOで唯一の幾何の問題はP4で、今ではいくつかのLLMがこれを解ける。この座標に基づく手法を、かなり難しい幾何の問題に適用できるところまでは、LLMはまだ来ていないと思うが、それも時間の問題かもしれない。LLMがより人間らしい空間的推論で幾何の問題を解いたなら興味深いが、それがより広い意義をもつかははっきりしないだろうし、そもそもそうなるとはあまり予想していない。

LLMについての補足

では、何が起こるだろうか？　少なくとも一つのLLM（最も可能性が高いのはDeep Think）がIMOの3問を解き、銅メダルか銀メダルを獲る確率は60%だと思う。創造性や、IMOの難しめの問題を解く能力の証拠は、どのLLMについてもあまり見ていない。すでに得られている結果からこれほどすぐにそれが見られたら驚くだろう。来年ならありうるかもしれないが、今年について、LLMが質的に創造的な解答を出すか、P3かP6を解く確率は5%にすぎないと見ている。

結論

結局のところ、IMOから何か意外なことを学べる可能性はやや低いと思う。最も起こりそうな結果はこうかもしれない。AlphaProofが、好都合な幾何の問題に後押しされて金メダルを獲る。LLMはP2かP5を解いて、数学コンテストの階段を上り続ける。どちらの場合も、創造的な問題解決の明確な証拠は見られない。それについては、ほかのベンチマークが教えてくれるのを待つ必要があるだろう。

この記事にフィードバックをくれたGreta Panovaに感謝する。