- Google DeepMindの Gemini Deep Think モデルが、2025年の 国際数学オリンピック（IMO）で金メダル基準スコア（35点） を達成
- このモデルは 6問中5問を完全に解答 し、IMO公式採点委員会の評価で 明確かつ精密な数学的解法 が認められた
- 昨年のAlphaProof・AlphaGeometry 2による銀メダル相当（28点）から 大きく飛躍 し、自然言語で公式問題を理解し、4.5時間以内に人間のように証明を完成
- Deep Thinkモードは 並列思考（parallel thinking） と最新の 強化学習 を適用し、複数の解法を同時に探索・統合して、IMOスタイルの問題解決に最適化
- Googleは今後 数学者との協業を拡大 し、数学的推論と形式的検証能力を組み合わせた 次世代AGI開発 へ進む計画
Breakthrough Performance at IMO 2025 with Gemini Deep Think
- Google DeepMindの Gemini Deep Think は、2025年の国際数学オリンピック（IMO）で 合計35点（6問中5問を完全解答） を獲得し、金メダル基準を公式に達成
- IMO公式採点委員会は 明確さ、精密さ、分かりやすい解法 を高く評価し、IMO委員長のProf. Dr. Gregor Dolinarは「Google DeepMindが金メダルスコア35点を達成したことを確認する」とする公式声明を発表
- 昨年のAlphaGeometry・AlphaProofでは、専門家が問題を自然言語からドメイン特化言語（Leanなど）へ翻訳する必要があり、計算にも2日以上を要した。今年のGeminiは 問題理解から証明作成までの全工程を自然言語ベースで、IMO本番の制限時間（4.5時間）内に完了 した
Making the most of Deep Think mode
- Gemini Deep Think は、並列思考（parallel thinking）などの最新研究手法を適用した 強化された推論モード であり、複数の解法経路を同時に探索して最適な解決策を導き出す
- モデルは 複雑な数学問題の解決に向けた強化学習手法 と、多様なIMOスタイルの証明データで訓練されており、IMO問題へのアプローチに関する一般的なヒントやコツも追加で取り込まれている
- このDeep Thinkモデルは、信頼できる一部の数学者および専門家に テスト版が先行提供 される予定で、その後Google AI Ultraの購読者向けに公開される計画
The Future of AI and Mathematics
- Google DeepMindは数学コミュニティとの 協力を継続 しつつ、自然言語ベースの推論だけでなく、AlphaGeometry・AlphaProofなどの 形式体系ベースの研究 も並行して進めている
- 今後は、自然言語の理解力と 形式的で検証可能な数学的推論能力 を組み合わせたAIが、数学・科学・工学・研究分野における 中核ツール になると見込まれる
- DeepMindは今回の成果を AGI（汎用人工知能）への道筋 における重要な進展と位置づけており、今後さらに複雑で高度な数学問題の解決に挑戦する計画
回答の検証とIMOの公式見解
- IMO組織委員会は 提出された回答が完全かつ正確な解答であることを公式に確認 した
- ただし、IMOのレビューには システム、プロセス、または基盤モデル自体の検証 までは含まれないことが明記されている
- 詳細および拡大解釈については、IMO公式声明（詳しく見る）を参照可能
5件のコメント
OpenAI、2025 国際数学オリンピック（IMO）で金メダル級の成果を達成と発表
2日前にOpenAIが先に発表してしまったので少し白けましたが、OpenAIのAlexander WeiがIMOと何の協議もなく先に話してしまったのはマナーに欠ける、という声もあったようです。
公式にはIMO側の認定もまだないのに発表してしまい、AIではない一般参加者たちへの祝福や功績を横取りした、ということですね。
おかげで、OAIは独自パネルで検証しただけで、IMOの公式採点すら受けていない状況になったわけですね。しかも回答の質もGeminiのほうがやや良いと見る意見が多いことを考えると……さらに格好のつかない状況ではないかと思います。評判に対するリスクは負わず、成功すれば発表し（それも公式採点ではない状況で）、結果が悪ければ手を引くというのは、ベンチマークではそうしてもよいとしても、参加者が自分の名前を背負って挑む大会で見せるべき正しい姿ではないように思います。
GoogleとOpenAIはLLMの性能がほぼ互角でも、企業としての老練さの差がこういうところで出ますね
Hacker Newsの意見
AlphaGeometryとAlphaProofは、まず自然言語の問題をLeanのようなドメイン特化言語に翻訳し、その後で証明結果を再び自然言語に変換する過程を経ており、計算には2〜3日を要していた。今年のGeminiモデルは、自然言語だけで公式の問題文から数学的証明を直接生成するエンドツーエンド方式を用いた。つまり、先にLeanへ翻訳していないという意味である。ただし、内部的にLean、インターネット検索、電卓、Pythonなどのツールを使ったのかは明確ではない。OpenAIは自社モデルではそうしたツールを使っていないと述べたが、その主張がGeminiにもそのまま当てはまるのかはよく分からない。両システムがそれぞれ使った計算量、つまりコストのおおよその規模も知りたい。もし価格が非常に高いなら、まだ実用性は低いということになる。まだ公開情報がないので、かなり高価なのだろうと推測する。そして、「ツール使用なし、インターネット接続なし」が確認されたというリンクも共有している https://x.com/FredZhang0/status/1947364744412758305
今年のGeminiモデルは自然言語だけで公式の問題文から数学的証明を生成し、4.5時間の競技時間内にすべての過程が行われた。外部ツールは使用していない
公式には、Leanのような形式検証ツールはIMOの問題を実際に解く際には使われていないとされているが、モデルを学習させる過程では使われているのか気になる。Googleの2024年のIMO研究には、自然言語の証明を形式的に検証可能な形式言語へ変換する技術がある。これをRLVR（強化学習による検証報酬）トレーニングに活用するのは自然な次の段階だと思う。数学LLMが生成するすべての推論を翻訳・検証して報酬信号として使えれば、報酬信号ははるかに密になる。完全な形式証明を得るのは依然として難しいだろうが、誤った推論や解釈不能な文を避けるよう誘導するには有用だ。膨大な計算量と組み合わせれば、IMO難度の問題も解けるようになる。AlphaProofのようにLean証明とLLM出力を往復しながら推論空間を効率的に探索すれば、IMO級の問題も解けることはすでに示されている。中間段階を省き、RLVRでLLMに形式推論を模倣するよう教えれば、同様の効率性と問題解決能力が得られるのではないかと思う
なぜLeanを使わないのかも気になる。Leanを使うと今では問題を解くのが簡単になりすぎるという意味なのか、それともLean自体がむしろ妨げになっているのか知りたい
「ツール使用なし、インターネット接続なし」が実際にはGoogleインフラなしのオフラインでも動作できるという意味なのか、つまり必要に応じてローカル配備できるのかも気になる
今年は高度化されたGeminiモデルが自然言語だけで公式の問題文から数学的証明をそのまま生成したというが、私はむしろ形式化技術から離れていることが惜しく感じられる。数学を真に自動化したり、たとえば数千ページ規模の証明を機械的に作り出せる水準に到達するには、形式化以外に道はないと思う。そうでなければ依然として人間の査読者が必要になり、証明を本当に信頼する方法がなくなる
もしLLMが自然言語で厳密な証明を作れるなら、Leanのような形式言語で証明することもそれほど難しくないはずだ。AlphaProofでLeanを使ったのはかなり限定的で、特定の数学問題に特化した方法だった。一方、RL方式と自然言語で同じことを達成できるなら、検証が難しいさまざまな分野にも拡張できる
DeepMindが現在、公式に未解決問題を形式化して記録するリポジトリを集めていることも共有している https://github.com/google-deepmind/formal-conjectures
私は数学者だが、もう研究はしていない。なぜ多くの数学者が形式手法に消極的なのかについて、少し文脈を提供したい。現実的には、数千ページの証明を作るなら当然形式化なしでは不可能であり、何かを「信頼」するには形式的に検証すべきだという点には同意する。しかし実際に数学者たちが本当に求めているのは、その結果がなぜ真なのかという説明である。本当の商品はイエス・ノーの答えではなく、その解釈と理由だ。たとえばリーマン予想はおそらく真だと皆が考えているが、ただ正解を待っているわけではない。さらに、「もしリーマン予想が真ならこのような新しい定理が成り立つ」といった結果も多い。証明に期待するのは、根本的に新しい洞察や、数論についての深い理解を与える形である。Leanのように形式的に真であることだけを検証してくれても、人間が理解すらできないなら、それはほとんど意味がない
正確な形式化は問題を解くことより容易なほうなので、まず問題を解き、その後で形式化して確認することもできる
IMOの問題はそもそも人間が道具なしで解くよう設計された問題だ。より難しい問題をモデルに解かせるなら、そのときは十分にツールを与えればよい。少なくとも人間レベルの能力をまずツールなしで再現するのはよい方向だと思う
OpenAIとGeminiの回答を比較すると、Gemini側の文体のほうがはるかに明快に感じられる。提示の仕方はもう少し良くできそうだが、証明内容そのものは追いやすく、OpenAIの回答よりも短く、それでいて整った文章になっている
Googleの証明は、おそらく事後的に要約した結果かもしれないし、Tree of Thoughtsのようなメカニズムの一部が要約過程である可能性もある。単純かつ受動的に「最終答案を出せ」という命令の結果ではないように思える
言及されたOpenAIとGoogleのIMO証明結果は、それぞれ Google proof PDF と OpenAIの証明例 Repository で見ることができる
「4.5時間の競技内にすべての過程を終えた」という点はOpenAIとGoogleの両方が強調していたが、この制限に重要な意味があるのかは疑問だ。実質的には数百万の並列推論プロセスを同時に回して証明を探せたかもしれない。もちろん、そうするには結果を評価し、最終的に提出する証明を選ぶ評価用モデルにも大量の計算資源が必要になるだろう。実際には数百年分のGPU時間が投入された可能性もある。とはいえ、この方法で解答を見つけられること、そして並列化がここまで可能であること自体は驚くべきだ。結局、AGIをより多くのコンピューティングで達成するかどうかにかかわらず、人間の脳はこのように簡単には拡張できないのだから、結果の意味は明らかだ
昨年のLean特化システムから、自然言語ベースの汎用LLM + RLへと方式が転換した点は非常に興味深い。このアプローチは数学コンテスト以外の領域でも性能向上に寄与すると予想される。今後どこまで拡張できるのか楽しみだし、今回のシステムは夏に公開予定の「DeepThink」モデル/機能とも大きくは違わないように見える
今はまるで、機械との数学競争におけるDeep BlueとKasparovの時代の瞬間を体験しているように感じる。ほんの数年前と比べても途方もない進歩があったが、それでも本物のAI数学者にはまだほど遠いと思う。とはいえ、本当に驚くべき時代に生きている
最近のポッドキャストでTerrence Taoも、こうしたツールと協働することに大きな関心を示していた。彼は当面の最善の活用法は、人間がアイデアやパラメータを設定し、LLMが探索や証明などを並列的に試す形だと述べていた。チェスエンジンの比喩も適切だ。最高のチェスプレイヤーたちも以前は複数の専門家チームの分析支援を受けていたが、現在ではスーパーコンピュータとソフトウェアで無数の局面を分析し、最善のアイデアを選んでプレイヤーに渡している
Deep Blueと天才児の対決に近いと思う。IMO参加者は世界的な数学者ではなく高校生だ
ここでの違いは、単純なブルートフォースだけでは時間内に高得点を取れないという点だ。真の技術的マイルストーンであり、Deep Blueのときの「原理的には可能」とは異なる
6番問題は不可解だ。openaiもdeepmindも回答を出せなかった。人間なら部分点狙いの解答くらいは出すのに、AIには答えがないのが不思議だ。もしかするとLLMは、自分が解けなかったことを自覚したのだろうかという疑問が湧く。LLMの限界の一つは「自分が知らないことを知らない」点であり、そうだとすると、ソルバーなしで論理的一貫性を確認するのはほぼ不可能だと思う
おそらく競技時間制限内に「思考」を終えられず、「出力」の段階に進めなかった可能性が高い
この限界は、最も基本的な事前学習済みLLMのテキスト生成にのみ当てはまる。追加でlinear probe（簡単なニューラルネットワーク層）を訓練し、confidence scoreを出力させることもできる。もちろん100%信頼できるわけではないが、少なくとも数学のような限定領域に適用すればかなり信頼できるかもしれない
形式検証ツールなしで実用に使うには、依然としてリスクが大きいかもしれない。以前のo3も最新ではないとはいえ、参考文献をうまく探したり、新しい不等式を提案したりする点には強みがあった。しかし実際の証明段階では、もっともらしく見えても細部で誤った命題や代数的ミスを含む回答を出すことがある。モデルが良くなるほど、こうした微妙な誤りはむしろ見つけにくくなるかもしれない
なぜ彼らが定理証明器を使わなかったことを強調するのか気になる。結局、モデル性能を高めるためのツールなら何でも使えばよいのではないか。しかもGeminiもIMO向けに特化されている。強化学習によって多段階推論、問題解決、定理証明データでモデルを訓練し、高品質な数学問題解説集やIMO問題へのアプローチに関するヒントも与えられている
「Gemini Deepthinkの上位版」は、実際にはリリース予定のGemini Ultraサブスクリプション製品に入るDeepthinkとはおそらく異なるか、あるいははるかに多くのテスト時演算量（compute）を使っているだろうと推測する。それでもOpenAIとGoogleが競い合う様子を見るのは面白い
1〜6番の問題を全部解いたコンテキストエンジニアリングのシステムプロンプトのリンクを共有しておきます。o3やGemini 2.5で使えます。プロンプトを全部入れて質問を入力し、問題を解いてもらえばOKです。 https://github.com/redcrash0721/freederia/blob/main/imo6kr.pdf