新智元報道
新智元報道
編輯：編輯部
【新智元導讀】谷歌DeepMind奧數奪金了，得到IMO官方認證！新模型Gemini Deep Think僅用自然語言，在4.5小時攻克了5題，拿下35分。這次，具體解題過程也一併公開了。
今天，谷歌DeepMind正式官宣拿下IMO金牌！
他們憑藉Gemini Deep Think（高階版），一個通用模型，成功破解前5題，斬獲35分（滿分42分）。
而且， AI在極限4.5小時之內，就達到了IMO金牌標準。
最最重要的是，Gemini僅用純自然語言——英語完成了解題。
與OpenAI不同的是，這一結果得到了IMO組委會官方認證。
Demis Hassabis連發兩彈，一再強調「谷歌模型是首個獲得官方金牌級別認可的AI系統」。
谷歌DeepMind，正式摘金
作為數學界的奧林匹克，IMO自1959年以來每年舉辦一次，每年吸引了全球各界優秀的學生參與。
參賽者需在4.5小時內解決6道極具深度的數學問題，涵蓋代數、幾何、組合數學和數論。
而且只有排名前8%的選手才能摘得金牌，象徵著無上的學術榮耀。
近年來，IMO逐漸成為AI能力的試煉場。數學問題不僅需要邏輯推理，還考驗創造性思維和嚴謹性，這對AI系統提出了極高要求。
2024年，AlphaProof和AlphaGeometry 2破解了6題中的4題，獲得28分，達到了銀牌水平。
這一突破利用專業的「形式語言」，表明AI開始接近頂尖人類的數學推理能力。
今天，Gemini Deep Think再創里程碑，完美破解5道題，躋身金牌行列。
那麼，這款模型是如何做到的呢？
我們在此確認，谷歌DeepMind已經達成了一個萬眾矚目的里程碑，在滿分42分的競賽中取得了35分的成績——這足以摘得金牌
他們的解法在諸多方面都堪稱驚豔。IMO的評委認為，這些解法思路清晰、表述精確，且大部分內容都簡單易懂。
——IMO主席Gregor Dolinar教授
自然語言解題，端到端推理
AlphaProof和AlphaGeometry 2解決IMO難題前，需要專家將問題翻譯為「形式語言」，如Lean。
而且，證明過程也是如此，且需要兩到三天的計算時間。
今年，Gemini Deep Think完全以自然語言端到端執行，直接從官方問題描述中生成嚴謹的數學證明，並在4.5小時的比賽時間限制內完成。
借用Karpathy經典語錄，「英語是熱門的程式語言」。如今看來，確實如此。
Deep Think模式
之所以能夠取得金牌，團隊使用了Gemini Deep Think的高階版本——一種針對複雜問題的增強推理模式。
並且，結合並行思考技術，允許模型同時探索多種解題路徑，最終整合出最優答案。
這種多執行緒推理方式，突破了傳統單一線性思考的侷限。
為了充分發揮Deep Think的推理能力，谷歌還對Gemini進行了新穎的強化學習訓練，讓其利用更多多步推理、問題解決和定理證明資料。
此外，谷歌研究團隊還透過以下方式，進一步升級了Gemini版本：
· 更多思考時間
· 獲取過往問題的一系列高質量解決方案集
· 提供解決IMO問題的通用提示與技巧
這種「訓練+知識庫+策略」的組合，讓Gemini在IMO的舞臺上大放異彩。
值得一提的是，接下來，谷歌將向一部分數學家等測試者提供這個版本的Deep Think模型，隨後向Google AI Ultra訂閱者推出。
解題過程
那就讓我們來看看，這次谷歌Gemini Deep Think具體的解題過程吧。
官方報告：https://storage.googleapis.com/deepmind-media/gemini/IMO_2025.pdf
對於第一題這道解析幾何題，模型的解法是設n>3是一個給定的整數。
證明思路是將問題簡化到n=k且所有直線必須是陽光線的這一特定情況。具體來說，設C(k)表示「P可被k條不同陽光線覆蓋」，定義P_0=ø。
然後模型設定了一個引理：在集合L中，所有N_v豎直直線必須是{x=1,2,…,N_v}，所有N_H水平線必須是{y=1,2,…,N_H}，所有N_D對角線必須是形如x+y=s的直線，s的取值範圍為n+2−N_D,…,n+1。
然後，模型對這個引理進行了證明。
接下來，模型證明了定理1：當n≥3且0≤k≤n時，若存在一個由n條不同的直線組成的集合，剛好覆蓋點集P_n，且其中恰好有k條陽光線，那麼充要條件便是命題C(k)為真。
接下來，模型對核心問題C(k)展開了分析：對於哪些k>0，點集P_k可以恰好被k條陽光線覆蓋。
最終，模型成功證明了C(k)成立的充要條件是k∈{0,1,3}，由此證明了唯一可能的陽光線數量為：0、1或3條。
對於第二題這道平面幾何題，模型把證明過程分成了五步。
步驟1：確定點P是△AMN的旁心。
步驟2： 求∠EBF。
步驟3： 引入輔助點V及其性質。
步驟4： 點V落在外接圓Σ上。
步驟5： 垂心H與切線條件。
最終，模型證明了直線VH是圓Σ在點V處的切線，由此證畢。
第三題是一道函式題。
在解題過程中，模型將關鍵步驟分為三步。
首先，是確定Bonza函式的性質與分類。
第二步和第三步中，模型分別完成了上界證明c≤4，以及下界證明c≥4。
最終結論可得：滿足條件的最小實數常數c為c=4。
第四題是一道數論題，前提給出了一個真因數的定義，對於一個正整數N，除了N本身以外的正整數因數，都叫作N的真因數。
數列中，每一個數a_n都是正整數，且都至少有3個真因數，先找出a_n的三個最大的真因數，再把它們相加得到下一項a_{n+1}。
問題是，起始值a_1有哪些數值可以取？
谷歌Gemini Deep Think給出了5個解題步驟，想要確定a_1取值，前提是讓a_n+1=S(an) 定義的序列是無限正整數。
步驟1：證明對所有n，a_n都是偶數。
步驟 2： 證明對所有n，a_n都能被3整除。
步驟 3： 當6∣N時，分析序列的動態行為。
步驟 4： 研究序列的演變過程並給出對a_1的限制條件。
步驟 5： 對起始值a_1進行全面刻畫與分類。
整體過程亮點，在於化繁為簡，用不變性和增長率把大範圍列舉壓縮到獨一無二的固定點。
第五題，是一道組合博弈+不等式分析題。
簡單來說，題幹要求：
· 輪到Alice（奇數回合）時，她必須給出一個非負數，使得目前所有數的總和≤ λ×當前回合數；
· 輪到Bazza（偶數回合）時，他必須給出一個非負數，使得目前所有數的平方和≤當前回合數。
· 誰在自己回合找不到合法數就輸；若雙方都能一直出數，遊戲無勝負。
題目要找出哪些 λ 能保證Alice必勝，哪些 λ 能保證 Bazza必勝？
Gemini Deep Think在解題時假設了2種情況，如下所示：
前者巧妙之處在於，把連續引數問題瞬間離散化：只要在λ<λ_c情形下構造必勝策略，就完成了整個區間的判定。
而後者關鍵點是「先蓄力，再一擊致命」，具體來說，讓Alice把總和一次性抬高，讓Bazza下一回合無法去滿足平方和條件，於是當場獲勝。
最終，Gemini得出如果λ=1√2時，兩者都不會贏。只有當λ＞1√2，Alice獲勝；當0＜λ＜1√2時，Bazza獲勝。
對此，來自Anthropic AI研究員點評道，「乍一看，它們的解法比OpenAI要清晰得多」。
團隊介紹
Thang Luong
官博稱，Gemini Deep Think整體技術方向由Thang Luong帶隊，現任Google DeepMind高階主任研究員，曾任Google Brain研究員。
他於2016年獲得斯坦福大學計算機科學博士學位，在讀博期間開創了深度學習在機器翻譯領域的應用先河。
在Google DeepMind工作期間，Thang Luong構建了多個語言（QANet、ELECTRA）和視覺（UDA、NoisyStudent）領域的尖端模型。
2020年，他推出全球最強聊天機器人Meena專案，該專案後續發展為Google LaMDA、Bard及現Gemini系列，也是經典注意力機制「LuongAttention」的發明者。
自2022年起，Thang Luong共同領導Bard多模態功能的開發，並擔任能解決IMO級別幾何題的AlphaGeometry專案負責人。
所有成員名單如下：
上下滑動檢視
AI+數學未來
谷歌DeepMind長期與數學界保持著合作，但AI為數學做出貢獻的潛力才剛剛嶄露頭角。
透過訓練Gemini學會更靈活、更直觀地推理，谷歌正逐步構建出能夠解決更復雜、更前沿數學問題的AI。
今年，奪下IMO金牌雖然完全基於Gemini自然語言能力，但團隊也在AlphaGeometry和AlphaProof等形式化系統方面也取得了持續的進展。
谷歌堅信，那些能夠將流暢的自然語言能力與嚴謹的推理能力（包括形式化語言中的可驗證推理）相結合的AI智慧體，將成為數學家、科學家、工程師和研究人員不可或缺的工具。
在通往AGI的道路上，AI將推動人類知識的進步。
OpenAI回應了！
其實，谷歌DeepMind早在7月19日週五下午就拿下了金牌，只是在等內部驗證流程才未對外公佈。
谷歌DeepMind超級推理團隊的Thang Luong表示：因為IMO內部有一份官方評分指南，外界根本無法獲取。
要知道，OpenAI自評的金牌成績只是剛剛過35分的線而已，如果有微小的扣分，都會讓成績從金牌跌到銀牌。
而且IMO組委會還特地明確要求，希望各個大模型公司在閉幕式一週後再公佈成績，不要搶走孩子們的風頭。
但OpenAI的Naom Brown卻表示，他們的確尊重了IMO的要求，是等閉幕式之後才釋出的。
就在谷歌DeepMind官宣奪金之後，Naom Brown又雙叒代表OpenAI發聲了，還是連發7推。
他首先肯定了GDM的成就，並指出OpenAI與之並行取得的成功，印證了AI進化的迅速。
不過，在具體測試中，兩家的方法各有千秋。
在總結自家模型結果的思考前，Naom Brown澄清了，早在2個月前，IMO組委會曾電郵邀請OpenAI參與基於Lean語言的正式競賽。
然而，當時OpenAI正忙於自然語言通用推理研究（不受Lean約束），就給婉拒了。
他特別強調了，OpenAI通用模型參賽IMO時，並沒有使用任何RAG等工具。
而且，團隊提交的證明均由三位外部 IMO 獎牌獲得者進行了評分，並且在正確性上達成了完全一致的意見。
接下來，Naom再次重申，「OpenAI是在開幕式結束之後公開的結果」。
昨日澄清的那一套話，再次公開陳述了一遍。
另一位OpenAI研究員Aidan McLaughlin還譏諷GDM，「他們為模型提供上下文，純屬帶著小抄進入了考場作弊」。
但現在事實已經擺在眼前——
一邊是谷歌經IMO官方認證的成績，模型即將在未來可用；一邊是OpenAI不講武德提前邀功，模型是未公開版本，以後很可能也不會公開。
這一輪過後，OpenAI急功近利的做法，更加失了民心。
參考資料：
https://deepmind.google/discover/blog/advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/