每年夏天，來(lái)自全球的青年數(shù)學(xué)天才匯聚一堂，參加被譽(yù)為「數(shù)學(xué)世界杯」的國(guó)際數(shù)學(xué)奧林匹克競(jìng)賽（IMO）。

比賽6道題分兩天完成，每題滿(mǎn)分7分，總分42分，難度極高，往往只有不到1%的參賽者能全對(duì)所有題目。

橫軸為分?jǐn)?shù)（7分滿(mǎn)），縱軸為人數(shù)

近年來(lái)，IMO也被視為AI領(lǐng)域的終極挑戰(zhàn)之一，是測(cè)試AI高級(jí)數(shù)學(xué)推理能力的理想舞臺(tái)。

2024年，谷歌DeepMind團(tuán)隊(duì)讓一位特殊的「選手」參與了IMO角逐——一個(gè)名為AlphaProof的AI系統(tǒng)。

它取得了28分的高分，僅以1分之差無(wú)緣金牌，達(dá)到了銀牌水平。

這是有史以來(lái)AI系統(tǒng)首次在IMO這樣的頂級(jí)賽事中獲得相當(dāng)于獎(jiǎng)牌的成績(jī)，標(biāo)志著機(jī)器在數(shù)學(xué)難題上的攻關(guān)能力邁上新臺(tái)階。

AlphaProof：數(shù)學(xué)解題AI高手登場(chǎng)

AlphaProof是DeepMind最新研發(fā)的「數(shù)學(xué)解題AI」系統(tǒng)，專(zhuān)門(mén)為證明復(fù)雜數(shù)學(xué)命題而設(shè)計(jì)。

簡(jiǎn)單來(lái)說(shuō)，如果把數(shù)學(xué)題視作需要攻克的「迷宮」，AlphaProof就是一個(gè)自學(xué)成才的AI解題高手。

不同于我們常見(jiàn)的ChatGPT這類(lèi)純粹用自然語(yǔ)言「思考」的模型，AlphaProof走了一條獨(dú)特的道路：它在計(jì)算機(jī)可驗(yàn)證的形式化語(yǔ)言中進(jìn)行推理，從而確保每一步推導(dǎo)都嚴(yán)格正確，不會(huì)出現(xiàn)憑空捏造的「靈光一閃」卻實(shí)則謬誤的步驟。

AlphaProof使用了數(shù)學(xué)領(lǐng)域流行的形式化證明語(yǔ)言L(fǎng)ean來(lái)書(shū)寫(xiě)證明。

Lean語(yǔ)言示例

Lean的語(yǔ)法接近數(shù)學(xué)和編程語(yǔ)言的結(jié)合體，允許AI輸出的每一步推理都被自動(dòng)檢查驗(yàn)證，避免了常規(guī)語(yǔ)言模型可能出現(xiàn)的謬誤。

AlphaProof給出的答案不是靠人類(lèi)評(píng)審的文字解釋?zhuān)且环萦?jì)算機(jī)逐行檢驗(yàn)通過(guò)的嚴(yán)謹(jǐn)證明。

這種將AI思維「硬化」成機(jī)械可核查形式的方式，讓AlphaProof在解答再難的題目時(shí)也沒(méi)有半點(diǎn)僥幸成分。

技術(shù)秘訣：大模型牽手強(qiáng)化學(xué)習(xí)

AlphaProof成功的核心秘訣在于將預(yù)訓(xùn)練大語(yǔ)言模型的「聰明直覺(jué)」和AlphaZero強(qiáng)化學(xué)習(xí)算法的「勤學(xué)苦練」巧妙結(jié)合。

語(yǔ)言模型擅長(zhǎng)從海量數(shù)據(jù)中學(xué)習(xí)人類(lèi)解題的經(jīng)驗(yàn)和模式；

而強(qiáng)化學(xué)習(xí)則讓AI通過(guò)不斷嘗試錯(cuò)誤，不斷改進(jìn)策略，正如小孩反復(fù)練習(xí)最終學(xué)會(huì)騎自行車(chē)。

DeepMind團(tuán)隊(duì)先利用大模型為AlphaProof打下「學(xué)識(shí)」基礎(chǔ)，然后讓它在模擬的數(shù)學(xué)環(huán)境中反復(fù)練習(xí)，自己發(fā)現(xiàn)解題策略。

研究者首先收集了近一百萬(wàn)道數(shù)學(xué)題（涵蓋不同領(lǐng)域和難度），利用谷歌最新的Gemini將這些自然語(yǔ)言描述的題目自動(dòng)翻譯成形式化的Lean代碼表述。

這一過(guò)程相當(dāng)于為AlphaProof打造了一個(gè)規(guī)模空前的題庫(kù)——團(tuán)隊(duì)共獲得了約8000萬(wàn)條形式化的數(shù)學(xué)命題，可以讓AI來(lái)練習(xí)證明。

有了這個(gè)「題海」后，AlphaProof先經(jīng)過(guò)監(jiān)督學(xué)習(xí)微調(diào)，掌握基本的Lean語(yǔ)言證明技巧。

接著，它進(jìn)入強(qiáng)化學(xué)習(xí)階段：像AlphaGo下棋自我對(duì)弈一樣，AlphaProof在Lean證明環(huán)境中與自己切磋。

每當(dāng)AlphaProof找到一道題的正確證明并通過(guò)驗(yàn)證，就用這一成功案例來(lái)立即強(qiáng)化自身的模型參數(shù)，使它下次能更有效地解決更有難度的新問(wèn)題。

這種邊練邊學(xué)的訓(xùn)練循環(huán)持續(xù)進(jìn)行，AlphaProof在數(shù)以百萬(wàn)計(jì)的問(wèn)題證明中不斷進(jìn)步，逐漸掌握高難度問(wèn)題所需的關(guān)鍵技能。

AlphaProof在搜索證明的時(shí)候并非毫無(wú)頭緒地「暴力窮舉」。

它采用了類(lèi)似于棋類(lèi)AI中蒙特卡羅樹(shù)搜索的策略，會(huì)智能地將復(fù)雜問(wèn)題拆解成若干子目標(biāo)各個(gè)擊破，并靈活調(diào)整搜索方向。

在某些情況下，AlphaProof能在看似無(wú)限的可能推導(dǎo)中邁出恰到好處的一步，展現(xiàn)出仿佛人類(lèi)數(shù)學(xué)家般的「靈光一閃」。

這既歸功于大模型提供的直覺(jué)指導(dǎo)，也離不開(kāi)強(qiáng)化學(xué)習(xí)反復(fù)探索帶來(lái)的全面搜索能力——兩者結(jié)合，使得AlphaProof比以往的任何AI系統(tǒng)都更善于在復(fù)雜的數(shù)學(xué)迷宮中找到出路。

奧賽奪銀：AI解題里程碑

DeepMind的AlphaProof與AlphaGeometry 2聯(lián)手在2024年IMO的6道競(jìng)賽題中解出了4道，獲得了28分（滿(mǎn)分42分），達(dá)到了銀牌選手的成績(jī)。

這一得分距離當(dāng)年金牌線(xiàn)僅差一分（29分），幾乎觸及金牌門(mén)檻。

在解出的題目中，AlphaProof單獨(dú)解決了其中3題（包括2道代數(shù)題和1道數(shù)論題），其中就包括了整場(chǎng)比賽最難的第6題——該題在600多名頂尖學(xué)生中也只有5人滿(mǎn)分解決。

剩余的一道幾何題則由專(zhuān)攻幾何的AlphaGeometry 2模型完成，而兩道組合數(shù)學(xué)題由于難以形式化和搜索爆炸等原因未能攻克。

最終，這套AI系統(tǒng)拿下4題滿(mǎn)分（其余2題為0分），分?jǐn)?shù)正好處于銀牌段的頂端。

要知道，在人類(lèi)選手中也只有不到10%的人能拿到金牌，今年共有58名選手得分不低于29分。

AlphaProof取得的銀牌水平成績(jī)，足以比肩一位受過(guò)多年訓(xùn)練的國(guó)際頂尖高中生天才選手。

這一成果令許多專(zhuān)家感到震撼：著名數(shù)學(xué)家、菲爾茲獎(jiǎng)得主高爾斯評(píng)價(jià)說(shuō)，AlphaProof給出的某些巧妙構(gòu)造「遠(yuǎn)超出我以為AI目前能夠做到的水平」。

AlphaProof在IMO上的表現(xiàn)具有里程碑意義。

這是AI首次在如此高難度的數(shù)學(xué)競(jìng)賽中達(dá)到人類(lèi)獎(jiǎng)牌選手的水準(zhǔn)，表明AI的數(shù)學(xué)推理能力實(shí)現(xiàn)了重大飛躍。

過(guò)去，大模型即便掌握了海量教材和定理，也常常難以完整解決奧賽級(jí)別的挑戰(zhàn)，更不用說(shuō)給出嚴(yán)格證明。

而AlphaProof通過(guò)形式化證明和強(qiáng)化學(xué)習(xí)，真正讓AI具備了解決開(kāi)放性數(shù)學(xué)難題的實(shí)力。

它成功證明了IMO中最困難題目的事實(shí)也讓人看到了希望：或許將來(lái)AI有潛力輔助人類(lèi)攻克懸而未決的數(shù)學(xué)猜想。

局限與未來(lái)

AI數(shù)學(xué)家的進(jìn)階之路

盡管AlphaProof令人眼前一亮，但目前它仍有不少局限。

其一，解題效率是個(gè)問(wèn)題。

人類(lèi)選手必須在4.5小時(shí)內(nèi)完成3題，而AlphaProof雖然最后找出了3題的解法，卻耗費(fèi)了將近3天時(shí)間。

這表明當(dāng)前AI證明方法在搜索速度和計(jì)算資源上還有很大提升空間。

其二，AlphaProof并非萬(wàn)能，它未能解決的兩道組合數(shù)學(xué)題恰恰反映了某些類(lèi)型的問(wèn)題對(duì)AI而言依然棘手。

這類(lèi)題目往往涉及高度非結(jié)構(gòu)化的創(chuàng)新思維，超出了AlphaProof主要從訓(xùn)練中「見(jiàn)過(guò)」的范疇。

因此，如何讓AI擁有更強(qiáng)的通用性和適應(yīng)性，去應(yīng)對(duì)未曾遇見(jiàn)的新穎難題，是下一步的重要挑戰(zhàn)。

其三，目前AlphaProof需要人工先將題目翻譯成Lean的形式化表達(dá)，它自己并不理解自然語(yǔ)言問(wèn)題。

這意味著它無(wú)法自主讀題，也無(wú)法像人類(lèi)數(shù)學(xué)家那樣提出新的問(wèn)題或判斷哪些問(wèn)題值得研究。

正如倫敦?cái)?shù)學(xué)科學(xué)研究所的何楊輝所指出的，AlphaProof可以作為協(xié)助數(shù)學(xué)家證明的有力工具，但它還不能替代人類(lèi)去發(fā)現(xiàn)和選擇研究課題。

何楊輝

面對(duì)這些局限，DeepMind團(tuán)隊(duì)表示他們將繼續(xù)探索多種途徑來(lái)提升AI的數(shù)學(xué)推理能力。

未來(lái)的研發(fā)方向之一是讓AI擺脫對(duì)人工翻譯的依賴(lài)，直接閱讀理解自然語(yǔ)言表述的數(shù)學(xué)題，并給出形式化證明。

同時(shí)，針對(duì)不同類(lèi)別的數(shù)學(xué)問(wèn)題（如組合數(shù)學(xué)或幾何），可能需要引入更專(zhuān)業(yè)的策略，比如融合符號(hào)計(jì)算、知識(shí)庫(kù)或分領(lǐng)域訓(xùn)練的模型，從而全面提高AI的解題覆蓋面。

還有研究者設(shè)想，將來(lái)數(shù)學(xué)家可以與這樣的AI證明助手協(xié)同工作：

AI快速驗(yàn)證人類(lèi)猜想和小引理，甚至嘗試大膽的思路攻克長(zhǎng)期懸而未決的難題；

人類(lèi)則專(zhuān)注于提出有意義的問(wèn)題和整體證明構(gòu)想。

可以預(yù)見(jiàn)，隨著AlphaProof這類(lèi)系統(tǒng)的不斷完善，我們正迎來(lái)人機(jī)攜手探尋數(shù)學(xué)前沿的新紀(jì)元。

AlphaProof展現(xiàn)出的形式化推理能力對(duì)AI安全和可靠性也有啟發(fā)意義。

它輸出的每一步推理都可追溯、驗(yàn)證，這種「嚴(yán)謹(jǐn)求證」的風(fēng)格或許可用于改進(jìn)未來(lái)的大模型，讓它們?cè)诨卮痖_(kāi)放性問(wèn)題時(shí)減少荒誕的臆測(cè)。

當(dāng)AI變得越來(lái)越強(qiáng)大，我們更希望它是一個(gè)踏實(shí)嚴(yán)謹(jǐn)?shù)摹笖?shù)學(xué)家」。

經(jīng)過(guò)此次奧賽洗禮，AlphaProof讓我們看到了AI在純粹理性領(lǐng)域逼近人類(lèi)頂尖水平的曙光。

當(dāng)然，人類(lèi)頂尖數(shù)學(xué)家的創(chuàng)造力和洞察力依然不可替代——至少在提出問(wèn)題和宏觀思路上，AI還有很長(zhǎng)的路要走。

但毫無(wú)疑問(wèn)，AI正在成為人類(lèi)探索數(shù)學(xué)未知的一雙有力之手。

無(wú)論人類(lèi)或AI，攀登真理高峰的道路上，永遠(yuǎn)需要勇氣、耐心與對(duì)未知的敬畏。