這項(xiàng)由華為諾亞方舟實(shí)驗(yàn)室的Matthieu Zimmer、Xiaotong Ji、Rasul Tutunov等研究人員聯(lián)合帝國(guó)理工學(xué)院、UCL人工智能中心、華為拉格朗日中心共同完成的研究發(fā)表于2025年7月的arXiv預(yù)印本平臺(tái)。有興趣深入了解的讀者可以通過(guò)arXiv:2507.02726v1訪問(wèn)完整論文。

當(dāng)我們解決一道復(fù)雜的數(shù)學(xué)題時(shí)，很少會(huì)一步到位直接找到答案。更常見(jiàn)的做法是將大問(wèn)題分解成幾個(gè)小問(wèn)題，一步步解決，最終達(dá)成目標(biāo)。這正是人類數(shù)學(xué)家證明定理時(shí)的自然思路。然而，當(dāng)前的人工智能在自動(dòng)定理證明方面卻往往采用"蠻力"搜索，就像無(wú)頭蒼蠅一樣盲目嘗試，效率極低。

研究團(tuán)隊(duì)意識(shí)到了這個(gè)問(wèn)題的關(guān)鍵所在。在自動(dòng)定理證明這個(gè)領(lǐng)域，AI面臨著一個(gè)被稱為"獎(jiǎng)勵(lì)稀疏"的挑戰(zhàn)。這就好比在黑暗的迷宮中尋找出口，只有當(dāng)你真正找到出口時(shí)才會(huì)有光亮指引，在此之前的所有探索都得不到任何反饋。對(duì)于AI來(lái)說(shuō)，只有當(dāng)它完整地證明了一個(gè)定理時(shí)才會(huì)獲得"成功"的信號(hào)，而在漫長(zhǎng)的證明過(guò)程中，它完全不知道自己是在朝著正確方向前進(jìn)還是越走越遠(yuǎn)。

為了解決這個(gè)問(wèn)題，研究團(tuán)隊(duì)開發(fā)了一個(gè)名為"自生成目標(biāo)條件馬爾科夫決策過(guò)程"的新框架，簡(jiǎn)稱sG-MDP。這個(gè)拗口的名字背后其實(shí)是一個(gè)很直觀的想法：讓AI學(xué)會(huì)像人類數(shù)學(xué)家一樣，在證明過(guò)程中自己設(shè)定中間目標(biāo)，然后逐步實(shí)現(xiàn)這些小目標(biāo)，最終完成整個(gè)證明。

傳統(tǒng)的目標(biāo)條件方法就像給學(xué)生一份詳細(xì)的學(xué)習(xí)計(jì)劃，告訴他每一步應(yīng)該做什么。而這個(gè)新方法則更像是培養(yǎng)學(xué)生的自主學(xué)習(xí)能力，讓AI自己判斷在證明過(guò)程的每個(gè)階段應(yīng)該設(shè)定什么樣的中間目標(biāo)。當(dāng)AI在證明一個(gè)復(fù)雜定理時(shí)，它會(huì)根據(jù)當(dāng)前的證明狀態(tài)動(dòng)態(tài)地提出一些有用的子命題或引理，然后專注于證明這些中間步驟，從而獲得更密集的反饋信號(hào)。

研究團(tuán)隊(duì)將這個(gè)理論框架具體應(yīng)用到了Lean4這個(gè)形式化數(shù)學(xué)證明系統(tǒng)中。Lean4就像是數(shù)學(xué)界的"代碼檢查器"，它能夠嚴(yán)格驗(yàn)證每一步推理是否正確，確保證明的絕對(duì)可靠性。在這個(gè)系統(tǒng)中，AI的"狀態(tài)"就是當(dāng)前的證明進(jìn)度，"動(dòng)作"包括兩類：一類是執(zhí)行具體的數(shù)學(xué)推理步驟（比如應(yīng)用某個(gè)定理或公式），另一類是提出新的中間目標(biāo)（比如"我先證明這個(gè)不等式成立"）。

為了在這個(gè)復(fù)雜的證明空間中高效搜索，研究團(tuán)隊(duì)采用了蒙特卡洛樹搜索算法。這種算法就像是一個(gè)經(jīng)驗(yàn)豐富的探險(xiǎn)家，它會(huì)根據(jù)之前的探索經(jīng)驗(yàn)來(lái)決定接下來(lái)應(yīng)該往哪個(gè)方向深入探索。與傳統(tǒng)方法不同的是，他們的搜索算法不僅僅以最終證明成功作為獎(jiǎng)勵(lì)，還會(huì)對(duì)每個(gè)被驗(yàn)證的中間命題給予獎(jiǎng)勵(lì)，這樣AI就能得到更豐富的學(xué)習(xí)信號(hào)。

基于這個(gè)框架，研究團(tuán)隊(duì)開發(fā)了一個(gè)名為Bourbaki的具體系統(tǒng)。這個(gè)名字來(lái)源于20世紀(jì)法國(guó)的一個(gè)數(shù)學(xué)家團(tuán)體，他們以嚴(yán)謹(jǐn)?shù)墓砘椒ㄖ貥?gòu)現(xiàn)代數(shù)學(xué)而聞名。Bourbaki系統(tǒng)的一個(gè)重要特點(diǎn)是它可以集成多個(gè)不同的大語(yǔ)言模型，讓它們各自發(fā)揮優(yōu)勢(shì)。在實(shí)際實(shí)現(xiàn)中，研究團(tuán)隊(duì)將DeepSeek-Prover-v2-7B和Kimina-7B兩個(gè)模型進(jìn)行了組合，形成了Bourbaki 7B版本。

這種集成策略類似于組建一個(gè)專家團(tuán)隊(duì)來(lái)解決復(fù)雜問(wèn)題。不同的模型可能在不同類型的推理上有各自的強(qiáng)項(xiàng)，通過(guò)協(xié)作可以彌補(bǔ)單個(gè)模型的不足。比如，一個(gè)模型可能擅長(zhǎng)代數(shù)操作，另一個(gè)模型可能在幾何推理方面更強(qiáng)，通過(guò)合理的任務(wù)分工可以顯著提升整體性能。

研究團(tuán)隊(duì)在PutnamBench這個(gè)極具挑戰(zhàn)性的數(shù)學(xué)競(jìng)賽數(shù)據(jù)集上測(cè)試了Bourbaki系統(tǒng)。Putnam數(shù)學(xué)競(jìng)賽被譽(yù)為北美最難的大學(xué)數(shù)學(xué)競(jìng)賽之一，其題目需要高度的創(chuàng)造性和復(fù)雜的多步推理。這個(gè)數(shù)據(jù)集包含了658個(gè)歷年競(jìng)賽題目，每一個(gè)都是大學(xué)水平的高難度證明題，遠(yuǎn)超普通教科書練習(xí)的復(fù)雜程度。

實(shí)驗(yàn)結(jié)果令人振奮。Bourbaki 7B成功證明了26個(gè)定理，大幅超越了之前7B參數(shù)規(guī)模模型的最佳成績(jī)。相比之下，此前的最強(qiáng)7B模型Kimina-7B只能解決10個(gè)問(wèn)題，而DeepSeek-Prover-v2-7B在最好情況下也只能解決23個(gè)問(wèn)題，而且需要更多的計(jì)算資源。這個(gè)結(jié)果不僅在數(shù)量上有顯著提升，更重要的是展現(xiàn)了方法論上的優(yōu)越性。

為了驗(yàn)證方法的普適性，研究團(tuán)隊(duì)還在其他基礎(chǔ)模型上測(cè)試了sG-MDP框架。結(jié)果顯示，無(wú)論是應(yīng)用到STP模型還是DeepSeek-Prover-v2模型上，這個(gè)框架都能帶來(lái)一致的性能提升。比如，在STP模型上，使用64次采樣時(shí)原本只能解決6個(gè)問(wèn)題，加入Bourbaki框架后能解決7個(gè)問(wèn)題；使用128次采樣時(shí)，從7個(gè)問(wèn)題提升到8個(gè)問(wèn)題。在DeepSeek-Prover-v2模型上，使用128次采樣時(shí)從15個(gè)問(wèn)題大幅提升到23個(gè)問(wèn)題。

這種一致性的提升說(shuō)明了sG-MDP框架的通用價(jià)值。它不是針對(duì)特定模型的定制化改進(jìn)，而是一種可以廣泛應(yīng)用的方法論創(chuàng)新。這就像是發(fā)明了一種新的學(xué)習(xí)方法，不管是哪個(gè)學(xué)生使用都能提高學(xué)習(xí)效率。

除了解題數(shù)量的提升，Bourbaki系統(tǒng)還展現(xiàn)出了更好的證明多樣性。對(duì)于同一個(gè)問(wèn)題，它能夠生成更多不同的正確證明路徑。例如，在求解putnam_1990_a1這個(gè)問(wèn)題時(shí)，DeepSeek-V2-7B只能生成1種正確證明，而Bourbaki能生成4種不同的證明；在putnam_2001_a1問(wèn)題上，DeepSeek-V2-7B生成36種正確證明，Bourbaki則能生成105種。這種多樣性不僅體現(xiàn)了系統(tǒng)的魯棒性，也為數(shù)學(xué)教育和研究提供了更豐富的參考。

研究團(tuán)隊(duì)在實(shí)現(xiàn)過(guò)程中還遇到了一些有趣的技術(shù)挑戰(zhàn)。他們發(fā)現(xiàn)有些模型會(huì)生成"啟發(fā)式"策略，比如Lean4中的apply?命令，這個(gè)命令會(huì)自動(dòng)嘗試多種可能的證明步驟。這就像是一個(gè)"萬(wàn)能鑰匙"，但它的結(jié)果具有一定的隨機(jī)性。為了處理這種情況，研究團(tuán)隊(duì)采用了混合策略，在遇到這類命令時(shí)會(huì)調(diào)用基礎(chǔ)模型來(lái)完成剩余的證明步驟。

在獎(jiǎng)勵(lì)函數(shù)的設(shè)計(jì)上，研究團(tuán)隊(duì)也進(jìn)行了精心考慮。他們不僅獎(jiǎng)勵(lì)最終的證明成功，還對(duì)證明深度、解決的子命題數(shù)量等中間指標(biāo)給予獎(jiǎng)勵(lì)。這種設(shè)計(jì)就像是在馬拉松比賽中不僅關(guān)注最終成績(jī)，還對(duì)通過(guò)每個(gè)檢查點(diǎn)給予鼓勵(lì)，這樣能夠更好地指導(dǎo)AI的探索方向。

從技術(shù)架構(gòu)角度來(lái)看，Bourbaki系統(tǒng)使用了Pantograph作為與Lean4的交互接口。Pantograph提供了執(zhí)行策略、跟蹤依賴關(guān)系、管理目標(biāo)狀態(tài)等功能，同時(shí)解決了Lean特有的一些技術(shù)難題，比如元變量耦合問(wèn)題。這個(gè)接口的設(shè)計(jì)支持子目標(biāo)的獨(dú)立執(zhí)行和狀態(tài)回溯，這對(duì)于實(shí)現(xiàn)蒙特卡洛樹搜索算法至關(guān)重要。

在搜索算法的實(shí)現(xiàn)上，研究團(tuán)隊(duì)對(duì)傳統(tǒng)的蒙特卡洛樹搜索進(jìn)行了專門的改進(jìn)。他們的選擇策略基于上置信界算法，平衡探索和利用；擴(kuò)展策略會(huì)查詢策略模型來(lái)建議候選動(dòng)作，一旦驗(yàn)證有效就添加到搜索樹中；估值策略會(huì)根據(jù)當(dāng)前狀態(tài)設(shè)置初始值；反向傳播策略會(huì)更新從擴(kuò)展節(jié)點(diǎn)到根節(jié)點(diǎn)路徑上所有節(jié)點(diǎn)的訪問(wèn)計(jì)數(shù)和累積值。

這項(xiàng)研究的意義遠(yuǎn)不止于在一個(gè)特定數(shù)據(jù)集上取得好成績(jī)。它代表了自動(dòng)定理證明領(lǐng)域的一個(gè)重要方向轉(zhuǎn)變：從盲目搜索轉(zhuǎn)向結(jié)構(gòu)化推理。傳統(tǒng)的方法往往依賴大量的計(jì)算資源進(jìn)行暴力搜索，而這種新方法通過(guò)模擬人類數(shù)學(xué)家的思維模式，能夠更加高效和優(yōu)雅地解決復(fù)雜問(wèn)題。

從更廣闊的視角來(lái)看，這種自生成目標(biāo)的思想也可能對(duì)其他需要復(fù)雜推理的AI任務(wù)產(chǎn)生啟發(fā)。無(wú)論是科學(xué)發(fā)現(xiàn)、工程設(shè)計(jì)還是戰(zhàn)略規(guī)劃，很多復(fù)雜任務(wù)都可以受益于這種將大目標(biāo)分解為小目標(biāo)的方法。

當(dāng)然，這項(xiàng)研究也存在一些局限性和未來(lái)的改進(jìn)方向。目前的系統(tǒng)主要在數(shù)學(xué)定理證明領(lǐng)域進(jìn)行了驗(yàn)證，在其他形式推理任務(wù)上的表現(xiàn)還有待進(jìn)一步探索。此外，如何更好地設(shè)計(jì)獎(jiǎng)勵(lì)函數(shù)、如何處理更復(fù)雜的子目標(biāo)依賴關(guān)系、如何進(jìn)一步提升搜索效率等問(wèn)題都值得繼續(xù)研究。

研究團(tuán)隊(duì)在論文中還提到了一些技術(shù)細(xì)節(jié)的處理。比如，他們使用vLLM來(lái)實(shí)現(xiàn)基礎(chǔ)模型的高效批量生成，每個(gè)節(jié)點(diǎn)最多允許10個(gè)策略候選，最大迭代次數(shù)設(shè)為512。這些參數(shù)的設(shè)置都是通過(guò)實(shí)驗(yàn)優(yōu)化得出的，體現(xiàn)了工程實(shí)現(xiàn)中的精細(xì)考量。

值得一提的是，這項(xiàng)研究采用了開放的實(shí)驗(yàn)設(shè)置，使用的基礎(chǔ)模型和數(shù)據(jù)集都是公開可獲得的，這為其他研究者復(fù)現(xiàn)和擴(kuò)展這項(xiàng)工作提供了便利。這種開放性對(duì)于推動(dòng)整個(gè)領(lǐng)域的發(fā)展具有重要意義。

說(shuō)到底，這項(xiàng)研究最引人注目的地方在于它成功地將人類數(shù)學(xué)家的直覺(jué)思維模式轉(zhuǎn)化為了可操作的AI算法。通過(guò)讓AI學(xué)會(huì)自主設(shè)定中間目標(biāo)，研究團(tuán)隊(duì)不僅解決了獎(jiǎng)勵(lì)稀疏的技術(shù)難題，更重要的是為AI推理能力的提升開辟了一條新的道路。這種方法論上的創(chuàng)新可能會(huì)對(duì)未來(lái)的AI系統(tǒng)設(shè)計(jì)產(chǎn)生深遠(yuǎn)影響，讓機(jī)器能夠更像人類一樣進(jìn)行復(fù)雜的邏輯推理和問(wèn)題解決。

對(duì)于普通人來(lái)說(shuō)，這項(xiàng)研究雖然看起來(lái)很技術(shù)化，但它實(shí)際上關(guān)系到AI能否在需要深度思考的任務(wù)上真正幫助人類。從自動(dòng)化的數(shù)學(xué)證明到科學(xué)發(fā)現(xiàn)，從復(fù)雜系統(tǒng)的驗(yàn)證到教育輔導(dǎo)，這種能夠進(jìn)行結(jié)構(gòu)化推理的AI系統(tǒng)將在越來(lái)越多的領(lǐng)域發(fā)揮重要作用。未來(lái)，當(dāng)我們面對(duì)復(fù)雜問(wèn)題時(shí)，也許真的可以依靠AI助手來(lái)幫我們分解問(wèn)題、制定策略、逐步解決，就像有了一個(gè)永不疲倦的智能伙伴。

有興趣深入了解這項(xiàng)研究技術(shù)細(xì)節(jié)的讀者，可以通過(guò)arXiv平臺(tái)訪問(wèn)完整論文，論文編號(hào)為arXiv:2507.02726v1。

Q&A

Q1：Bourbaki是什么？它能做什么？ A：Bourbaki是華為諾亞方舟實(shí)驗(yàn)室開發(fā)的AI數(shù)學(xué)定理證明系統(tǒng)。它的核心能力是像人類數(shù)學(xué)家一樣，在證明復(fù)雜定理時(shí)自己設(shè)定中間小目標(biāo)，然后逐步解決這些子問(wèn)題，最終完成整個(gè)證明。它在PutnamBench數(shù)學(xué)競(jìng)賽數(shù)據(jù)集上成功證明了26個(gè)定理。

Q2：這項(xiàng)技術(shù)會(huì)不會(huì)讓數(shù)學(xué)家失業(yè)？ A：目前不會(huì)。Bourbaki主要是在幫助驗(yàn)證和尋找數(shù)學(xué)證明，就像一個(gè)強(qiáng)大的計(jì)算工具。數(shù)學(xué)家的創(chuàng)造性思維、問(wèn)題發(fā)現(xiàn)能力和數(shù)學(xué)直覺(jué)仍然是不可替代的。這項(xiàng)技術(shù)更可能成為數(shù)學(xué)家的得力助手，幫助處理繁瑣的證明驗(yàn)證工作。

Q3：普通人能使用這個(gè)系統(tǒng)嗎？ A：目前這還是一個(gè)研究階段的系統(tǒng)，主要在學(xué)術(shù)環(huán)境中使用。不過(guò)隨著技術(shù)發(fā)展，未來(lái)可能會(huì)出現(xiàn)基于類似原理的數(shù)學(xué)學(xué)習(xí)輔助工具，幫助學(xué)生理解復(fù)雜的數(shù)學(xué)證明過(guò)程或驗(yàn)證作業(yè)答案。