剛剛，DeepMind再登Nature：AlphaProof首奪國(guó)際數(shù)學(xué)奧林匹克銀牌

今日，首個(gè)達(dá)到國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽（IMO）銀牌水平的人工智能（AI）模型——AlphaProof，登上了權(quán)威科學(xué)期刊 Nature。

論文鏈接：

https://www.nature.com/articles/s41586-025-09833-y

去年，Google DeepMind 憑借 AlphaProof 這一奧賽級(jí)人工智能模型，引發(fā)了學(xué)界轟動(dòng)，被業(yè)內(nèi)比喻為“登月”時(shí)刻。

據(jù)論文描述，AlphaProof 這一成果證明了“自動(dòng)化系統(tǒng)已具備攻克傳統(tǒng)認(rèn)為無(wú)法解決的數(shù)學(xué)難題的能力”，不僅是技術(shù)層面的里程碑，也為“可驗(yàn)證的機(jī)器推理”提供了可行路徑。

新聞與觀點(diǎn)文章鏈接：

https://www.nature.com/articles/d41586-025-03585-5

在同期發(fā)表的新聞與觀點(diǎn)文章中，伊利諾伊大學(xué)厄巴納-香檳分校助理教授 Talia Ringer 表示：

AlphaProof 是她所用過(guò)的第一款“真正實(shí)用的 AI 工具”，擁有著“高度可靠”的證明質(zhì)量，每一步的推理都能獲得來(lái)自證明輔助工具的即時(shí)反饋，從而避免了自然語(yǔ)言推理中常見(jiàn)的模糊與錯(cuò)誤，這一點(diǎn)是自然語(yǔ)言模型所不具備的。

“盡管仍存在局限性......但可以肯定的是，這個(gè)領(lǐng)域正在發(fā)生深刻變革，AlphaProof 或許正是未來(lái)趨勢(shì)的先行者。”

AlphaProof：首次實(shí)現(xiàn)奧數(shù)級(jí)形式化推理

訓(xùn)練能夠在復(fù)雜、開(kāi)放環(huán)境中進(jìn)行有效推理并找到解決方案的智能體（Agent），是人工智能研究面臨的關(guān)鍵挑戰(zhàn)之一。

數(shù)學(xué)，尤其是奧數(shù)題目，要求創(chuàng)造性思維和多步推理能力，因此被視為衡量高級(jí)智能體能力的標(biāo)準(zhǔn)化評(píng)估場(chǎng)景。

在這項(xiàng)工作中，研究團(tuán)隊(duì)延續(xù)了先前在 AlphaZero 等系統(tǒng)中的思路：通過(guò)強(qiáng)化學(xué)習(xí)讓智能體在規(guī)則明確的環(huán)境中進(jìn)行自我博弈與改進(jìn)；不同的是，這一次的“棋盤(pán)”不再來(lái)自圍棋或國(guó)際象棋，而是數(shù)學(xué)定理本身。

在具體實(shí)現(xiàn)上，AlphaProof 將數(shù)學(xué)定理證明過(guò)程轉(zhuǎn)化為一個(gè)強(qiáng)化學(xué)習(xí)任務(wù)。在 Lean 定理證明器環(huán)境中，每一次證明過(guò)程都會(huì)被定義為狀態(tài)、動(dòng)作與獎(jiǎng)勵(lì)，通過(guò)不斷嘗試與反饋，學(xué)習(xí)如何將假設(shè)轉(zhuǎn)化為結(jié)論，逐步形成穩(wěn)定的推理策略。

圖｜AlphaProof 核心推理組件

AlphaProof 的訓(xùn)練過(guò)程分為多個(gè)階段。首先，模型在約 3000 億 token 的數(shù)學(xué)與代碼語(yǔ)料上進(jìn)行預(yù)訓(xùn)練，以學(xué)習(xí)符號(hào)邏輯、語(yǔ)法和基礎(chǔ)的數(shù)學(xué)語(yǔ)言表達(dá)結(jié)構(gòu)。隨后，研究者利用約 30 萬(wàn)條 Lean tactic 證明數(shù)據(jù)對(duì)模型進(jìn)行監(jiān)督微調(diào)，使其能夠理解 Lean 的形式化語(yǔ)法與命令結(jié)構(gòu)。

為了構(gòu)建大規(guī)模訓(xùn)練數(shù)據(jù)，他們開(kāi)發(fā)了基于 Gemini 模型的自動(dòng)形式化系統(tǒng)，將自然語(yǔ)言題目轉(zhuǎn)化為 Lean 的邏輯表達(dá)。該系統(tǒng)自動(dòng)生成了約8000 萬(wàn)個(gè)形式化數(shù)學(xué)問(wèn)題，涵蓋代數(shù)、數(shù)論、幾何與組合數(shù)學(xué)等多個(gè)領(lǐng)域，成為 AlphaProof 強(qiáng)化學(xué)習(xí)的核心訓(xùn)練素材。

在主訓(xùn)練階段，AlphaProof 系統(tǒng)在生成的問(wèn)題上進(jìn)行自我博弈式學(xué)習(xí)：不斷嘗試證明、驗(yàn)證結(jié)果、更新策略，并通過(guò) Lean 核心驗(yàn)證結(jié)果的正確性，形成強(qiáng)化學(xué)習(xí)循環(huán)——每當(dāng)系統(tǒng)找到正確證明時(shí)，就會(huì)獲得正向獎(jiǎng)勵(lì)；若證明失敗，則回溯并嘗試新的路徑，從而逐步掌握復(fù)雜的推理模式。研究團(tuán)隊(duì)稱(chēng)，這一過(guò)程累計(jì)消耗了約 8 萬(wàn) TPU 天的計(jì)算資源。

在推理階段，研究團(tuán)隊(duì)提出了“測(cè)試時(shí)強(qiáng)化學(xué)習(xí)”（TTRL）機(jī)制，當(dāng)AlphaProof 遇到難度較高或從未見(jiàn)過(guò)的題目時(shí)，會(huì)圍繞目標(biāo)問(wèn)題臨時(shí)生成數(shù)千個(gè)結(jié)構(gòu)相似的變體，在這些變體上進(jìn)行短期自我強(qiáng)化學(xué)習(xí)，然后將更新后的策略應(yīng)用回原題求解。

這種“臨場(chǎng)學(xué)習(xí)”的方法顯著增強(qiáng)了模型的泛化與解決新題的能力：實(shí)驗(yàn)結(jié)果顯示，TTRL 讓系統(tǒng)的解題率在多項(xiàng)基準(zhǔn)上提升了約10%–15%。

圖｜AlphaProof 學(xué)習(xí)與自適應(yīng)流程

從結(jié)果上看，AlphaProof 在多個(gè)數(shù)學(xué)推理基準(zhǔn)測(cè)試上展現(xiàn)出了領(lǐng)先的性能。在 miniF2F、PutnamBench、formal-IMO 等形式化數(shù)學(xué)基準(zhǔn)測(cè)試上的結(jié)果，均證明了 AlphaProof 在定理證明成功率和搜索效率方面達(dá)到了 SOTA 水平。

圖｜AlphaProof 在多個(gè)形式化數(shù)學(xué)基準(zhǔn)測(cè)試的表現(xiàn)

在 2024 年的國(guó)際數(shù)學(xué)奧林匹克 IMO 模擬測(cè)試中，AlphaProof 的表現(xiàn)尤其令人矚目——成功獨(dú)立證明三道非幾何題（P1、P2、P6），其中包括整場(chǎng)最難的題目 P6。

圖｜AlphaProof 完整解答 IMO 2024 數(shù)學(xué)競(jìng)賽第一題的證明過(guò)程

與此同時(shí)，Google DeepMind 的另一個(gè)系統(tǒng) AlphaGeometry 2 則負(fù)責(zé)解決幾何題。兩者合計(jì)得到 28 分（滿分 42），相當(dāng)于人類(lèi)參賽者的銀牌水平。

論文指出，這是人工智能首次在國(guó)際數(shù)學(xué)奧林匹克上達(dá)到獎(jiǎng)牌水平，與先前只能解決中學(xué)或大學(xué)低年級(jí)題目的系統(tǒng)相比，AlphaProof 的表現(xiàn)“展示了基于經(jīng)驗(yàn)學(xué)習(xí)的形式化系統(tǒng)在復(fù)雜推理領(lǐng)域的潛力”。

邁向可驗(yàn)證科學(xué)智能

在論文的討論章節(jié)，研究團(tuán)隊(duì)強(qiáng)調(diào)，AlphaProof 的核心貢獻(xiàn)在于證明了強(qiáng)化學(xué)習(xí)可以與形式化邏輯系統(tǒng)結(jié)合，從而實(shí)現(xiàn)高水平的可驗(yàn)證數(shù)學(xué)推理。

與基于自然語(yǔ)言模型的推理不同，AlphaProof 的每一步邏輯均通過(guò) Lean 的驗(yàn)證器審查，這種“形式化可驗(yàn)證”的方法，為人工智能在科學(xué)推理和理論研究中的應(yīng)用奠定了重要基礎(chǔ)。

研究團(tuán)隊(duì)也坦言，AlphaProof 也同樣存在一些局限，包括：訓(xùn)練與推理的計(jì)算成本高；推理速度慢，TTRL 階段常需數(shù)天計(jì)算時(shí)間；仍難以處理開(kāi)放性、創(chuàng)造性極強(qiáng)的數(shù)學(xué)問(wèn)題。

盡管如此，研究團(tuán)隊(duì)認(rèn)為，這一成果展示了人工智能系統(tǒng)向更高層次推理能力邁進(jìn)的可行路徑。

在未來(lái)工作中，他們將重點(diǎn)優(yōu)化模型效率、降低算力需求，并進(jìn)一步探索形式化學(xué)習(xí)在數(shù)學(xué)與其他科學(xué)領(lǐng)域中的應(yīng)用。

此外，他們還計(jì)劃開(kāi)發(fā)交互式工具，使研究人員能夠直接與系統(tǒng)協(xié)作，讓人工智能成為“科學(xué)探索的合作者”。

整理：江江

如需轉(zhuǎn)載或投稿，請(qǐng)直接在本文章評(píng)論區(qū)內(nèi)留言

速來(lái)拼好模，邀你一起薅羊毛！

智譜 GLM Coding Plan，

無(wú)縫支持 Claude Code 等 10+ 主流編程工具，

立即開(kāi)拼，享限時(shí)驚喜價(jià)！