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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

有興趣深入了解這項研究技術(shù)細節(jié)的讀者，可以通過arXiv平臺訪問完整論文，論文編號為arXiv:2507.02726v1。

Q&A

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

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

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