「Gemini with Deep Think」が国際数学オリンピックで金メダル基準を正式に達成

2025年7月22日原文(deepmind.google)

概要

Google DeepMind のGemini Deep Thinkが IMO 2025 で金メダル基準を達成
自然言語 のみで厳密な証明を生成、4.5時間以内に5問完全正解
Deep Thinkモード による高度な並列推論と強化学習技術の活用
数学界との連携を通じて AIによる数学進歩 への貢献を目指す
今後は AI Ultra ユーザーや数学者向けにモデルを展開予定

IMO 2025でのGemini Deep Thinkの画期的成果

International Mathematical Olympiad（IMO） は1959年から毎年開催される世界最高峰の高校生数学コンテスト
各国から6名の精鋭が参加し、 代数・組合せ・幾何・数論 の超難問6題に挑戦
上位半数にメダル、上位約8%が金メダルを獲得
近年、 AIの数学的推論能力 の試金石としても注目
2024年は AlphaGeometry 2/AlphaProof が4問正解・銀メダル相当（28点）を達成
2025年は Gemini Deep Think が5問完全正解・35点で金メダル基準を突破
IMO公式採点者が「 明確・精密・理解しやすい」と高評価
2024年のAIは 専門言語変換 と2~3日かかる計算が必要だったが、2025年は 自然言語のみ ・4.5時間内で完結

Deep Thinkモードの技術的特徴

Gemini Deep Think は複雑な問題に対応するための強化推論モード
並列的思考 で複数の解法を同時に探索・統合し最適解を導出
強化学習 とマルチステップ推論・定理証明データで追加学習
IMO問題へのアプローチ法や高品質な数学解答例も学習データに追加
今後、信頼できる数学者や Google AI Ultra 契約者向けに段階的公開予定

AIと数学の未来

Google DeepMind は数学コミュニティとの連携を継続
AIの柔軟かつ直感的な推論能力の向上を目指す
自然言語推論 と 形式的証明（AlphaGeometry/AlphaProof） の双方を強化
自然言語流暢性と厳密な形式的推論を兼ね備えたAIは、数学者や研究者の貴重なツールとなる可能性
AGI（汎用人工知能） への道筋として数学分野でのAI活用を推進

主要開発メンバー・関係者への謝辞

Thang Luong がGemini Deep Thinkの技術指導とIMO 2025全体調整を担当
Dawsen Hwang, Junehyuk Jung が学習データと専門家評価を主導
Jonathan Lee, Nate Kushman, Pol Moreno, Yi Tay がGemini Deep Thinkの学習を担当、 Lei Yu が評価を指揮
Golnaz Ghiazi, Garrett Bingham, Lalit Jain がDeep Think推論、 Vincent Cohen-Addad らが推論手法を強化
AlphaGeometry チームや形式数学分野の専門家、評価・インフラ・法務・運用・計算資源・プログラムサポートなど、多数の専門家が貢献
IMO理事会 のProf. Gregor Dolinarからも公式な支援と承認

IMO公式コメントと今後の課題

IMO審査員が 提出解答の完全性と正確性 を公式に認定
ただし、 システム全体やモデルの検証は対象外 であることに留意
今後はさらなるAIの数学的能力向上と、幅広い分野への応用が期待

Hackerたちの意見

まだ必要な計算量についての情報はないけど、GoogleやOpenAIからこの成果を達成するために何が必要だったのか、詳しい内訳を見てみたいな。スレッドで熱く議論されたのは、OpenAIの結果に関してで、「Geminiには数学問題の高品質な解法のキュレーションされたコーパスへのアクセスを提供し、IMO問題に取り組むための一般的なヒントやコツを指示に追加しました。」ということ。一般的なモデルがそんなことができるかどうかの答えは、モデルが特にIMO問題に特化して訓練されたということのようで、これは多くの人が予想していたことだね。結果を否定するわけじゃないけど、データの質が出力の質に直結するなら、古典的な機械学習技術とあまり変わらない気もする。

└

一般的なモデルがそんなことをできるかどうかの答えは、モデルが特にIMO問題に特化して訓練されたということのようで、これは多くの人が予想していたことだね。それが正確に何を意味するのかはよくわからないな。これらのモデルには、事前学習からIMO問題や解法が含まれている可能性が高いと思う。もしかしたら、システムプロンプトにそれらが含まれていたのかもしれないね。

└

でも、大衆メディアが報じるとき、SI単位を使わずに図書館や象みたいな単位を使う場合、AIと子供の計算エネルギーを比較するために、メディアはどんな単位を使うべきなんだろう？

└

公開モデルのコストとの非公式な比較（パフォーマンスが悪い）: https://matharena.ai/imo/ だから、実際のコストはもっと高いってことだね。

└

彼らは「Crux Mathematicorum」や似たようなジャーナルでトレーニングできるよ。そこには「面白い」問題とその解答が集められてる。 https://cms.math.ca/publications/crux

昨年の専門的なLeanベースのシステムから、より汎用的なLLM + RLアプローチに移行したのは超興味深いね。これが数学コンペティション以外でもパフォーマンス向上につながると思う。どこまでこのフロンティアが進むのか、楽しみだな。記事によると、使われているシステムは、今夏に発表される一般的な「DeepThink」モデル/機能とはそれほど遠くないみたいだね。

「Gemini Deepthinkの“進化版”」って、違うモデルだったり、今後のGemini UltraサブスクリプションのDeepthinkよりもかなり多くの計算時間を使ったことを意味してると思う。OpenAIとGoogleが互角なのを見るのはやっぱりクールだね。

今、競技数学の世界では、Deep Blue対カスパロフの瞬間が起きてると思う。数年前からの大きな進歩だけど、まだまだ半分尊敬できるAI数学者には遠い気がする。生きている今が本当にワクワクする時代だね！

└

テレンス・タオが最近のポッドキャストで「これらのツールと一緒に働くことに非常に興味がある」と言ってた。彼は、近い将来の最良の使い方を「人間のセットビジョンの探検者」と見ているみたいだね。（つまり、いくつかのアイデアやパラメータを設定して、LLMに探検させたり、並行検索や証明をさせたりすること）君のチェスエンジンとの比較は的確だね。今のトッププレイヤーたちは、こうやって準備をしているんだ。以前のように、ポジションを分析してアドバイスをする複数の専門家チームはもういない。今は、スーパーコンピュータを使って無限のポジションを検索し、最良のアイデアを抽出して、プレイヤーに提供するアナリストがいるんだ。

AlphaGeometryとAlphaProofは、まず専門家が自然言語からドメイン特化型言語（Leanなど）に問題を翻訳し、証明についても逆に行う必要があった。それには2〜3日かかる計算も必要だった。今年、私たちの進化したGeminiモデルは自然言語でエンドツーエンドで動作し、公式の問題記述から直接厳密な数学的証明を生成した。だから、問題は最初にLeanに翻訳されたわけじゃない。でも、モデルは内部の思考プロセスでLeanやインターネット検索、計算機、Python、その他のツールを使ったのかな？OpenAIはそれを使っていないと言ってたけど、これが同じ主張かどうかはわからない。ここについてもう少し明確にしてほしいな。両システムが使用した計算量の大まかな規模を、ドルで測定したい。できること自体はもちろんすごいけど、価格が高すぎるとまだ役に立たないからね。開示がない限り、価格は実際に高いと思っておくよ。編集:「ツール使用なし、インターネットアクセスなし」が確認された: https://x.com/FredZhang0/status/1947364744412758305

└

そうみたいだね: > 今年、私たちの高度なGeminiモデルは自然言語でエンドツーエンドで動作し、公式の問題説明から直接厳密な数学的証明を生成しました – すべて4.5時間の競技時間内で。

スコアを見る限り、彼らも質問6には答えられなかったみたい？それって確認されたの？

Hacker Newsで議論の続きを見る

ハクソク