AI 技術(shù)與數(shù)學(xué)發(fā)現(xiàn)的進(jìn)展，正前所未有地交織在一起。

前段時(shí)間，著名數(shù)學(xué)家陶哲軒在牛津數(shù)學(xué)公開講座中做了主題為「AI 在科學(xué)和數(shù)學(xué)中的潛力」的主題分享。他指出，將 AI 整合到數(shù)學(xué)領(lǐng)域?qū)⑹剐问交C明的編寫速度超過人類證明（人類證明容易出錯(cuò)）。這將成為一個(gè)關(guān)鍵轉(zhuǎn)折點(diǎn)，意味著形式化證明的使用將不僅限于驗(yàn)證現(xiàn)有的證明，還將用于創(chuàng)造新的數(shù)學(xué)知識(shí)。這將通過廣泛的人類數(shù)學(xué)家與 AI 數(shù)學(xué)家之間的協(xié)作來(lái)實(shí)現(xiàn)。我們將迎來(lái)一個(gè)「大數(shù)學(xué)」時(shí)代！

正如陶哲軒所說(shuō)，將 AI 應(yīng)用于形式化定理證明已經(jīng)成為數(shù)學(xué)家的日常操作。在另一頭，AI 科學(xué)家們也在努力提高 AI 在形式化定理證明中的性能和效率，比如 DeepSeek 剛剛推出的新模型 ——DeepSeek-Prover-V1.5。

DeepSeek-Prover-V1.5 是一個(gè) 70 億參數(shù)的開源模型。它通過結(jié)合強(qiáng)化學(xué)習(xí)（基于證明助手反饋的強(qiáng)化學(xué)習(xí)，RLPAF）和蒙特卡洛樹搜索（特別是提出的 RMaxTS 變體），顯著提升了證明生成的效率和準(zhǔn)確性。DeepSeek-Prover-V1.5 在 Lean 4 的形式定理證明方面優(yōu)于所有開源模型。

以下是技術(shù)報(bào)告的詳細(xì)內(nèi)容。

技術(shù)報(bào)告概述

• 報(bào)告標(biāo)題：DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Search
• 報(bào)告鏈接：https://arxiv.org/pdf/2408.08152
• GitHub 鏈接：https://github.com/deepseek-ai/DeepSeek-Prover-V1.5

近年來(lái)，在大型語(yǔ)言模型領(lǐng)域取得的進(jìn)展極大地推動(dòng)了人工智能在數(shù)學(xué)推理和定理證明方面的發(fā)展。但語(yǔ)言模型在形式化定理證明方面仍面臨重大挑戰(zhàn)。例如，使用 Lean 和 Isabelle 這類系統(tǒng)進(jìn)行證明時(shí)，需要進(jìn)行嚴(yán)格的推導(dǎo)，以滿足驗(yàn)證系統(tǒng)的形式規(guī)范。即便是像 GPT-4 這樣的先進(jìn)模型，在處理復(fù)雜的形式證明時(shí)也顯得力不從心，這凸顯了形式化證明中編碼和數(shù)學(xué)推理的復(fù)雜性。一個(gè)高效的形式化定理證明模型不僅需要理解 Lean 證明助手等形式化系統(tǒng)的語(yǔ)法和語(yǔ)義，還需要將抽象的數(shù)學(xué)推理與精確的形式化表達(dá)方式相結(jié)合。

在形式化定理證明中，語(yǔ)言模型通常采用兩種策略：證明步驟生成（proof-step generation）和完整證明生成（whole-proof generation）。

證明步驟生成通過預(yù)測(cè)并驗(yàn)證每一個(gè)策略，利用形式化驗(yàn)證器獲取當(dāng)前策略狀態(tài)的更新信息，并常結(jié)合樹搜索技術(shù)來(lái)構(gòu)建有效的證明。而完整證明生成則在計(jì)算上更為高效，它基于定理陳述一次性生成整個(gè)證明代碼，減少了證明模型與形式化定理驗(yàn)證器之間協(xié)調(diào)所需的通信量。

盡管 DeepSeek-Prover-V1 在 Lean 4 中通過完整證明生成取得了 SOTA 成果，但這種方法也有其獨(dú)特的挑戰(zhàn)。它需要在沒有中間策略狀態(tài)信息的情況下進(jìn)行長(zhǎng)期序列預(yù)測(cè)，而未來(lái)的策略依賴于這些隱藏的結(jié)果。在 Lean 的策略模式中，證明是通過一系列改變證明狀態(tài)的策略來(lái)構(gòu)建的。這種順序性可能導(dǎo)致錯(cuò)誤累積，一個(gè)小的誤差就可能使證明偏離正確的路徑。具體來(lái)說(shuō)，自回歸模型在生成長(zhǎng)證明時(shí)可能會(huì)對(duì)中間策略狀態(tài)有錯(cuò)誤的認(rèn)識(shí)。

為了在不犧牲完整證明生成的簡(jiǎn)便性和計(jì)算效率的同時(shí)，無(wú)縫地整合中間策略狀態(tài)，研究者在 DeepSeek-Prover-V1.5 中開發(fā)了一種統(tǒng)一方法。這種方法通過截?cái)嗪椭匦麻_始（truncate-and-resume）機(jī)制，結(jié)合了證明步驟生成和完整證明生成的優(yōu)勢(shì)。

該過程從標(biāo)準(zhǔn)的完整證明生成開始，語(yǔ)言模型根據(jù)定理陳述前綴完成證明代碼，然后由 Lean 證明器進(jìn)行驗(yàn)證。如果證明正確無(wú)誤，流程就此結(jié)束。如果發(fā)現(xiàn)錯(cuò)誤，就從第一個(gè)錯(cuò)誤信息處截?cái)啻a，并丟棄后續(xù)代碼。然后，使用成功生成的證明代碼作為提示，生成下一個(gè)證明段。

為了提高模型新完成部分的準(zhǔn)確性，研究者在提示的末尾添加了 Lean 4 證明器的最新狀態(tài)作為注釋。值得注意的是，該方法并不局限于從上次成功應(yīng)用的策略中重新開始。研究者將截?cái)嗪椭匦麻_始機(jī)制集成到了蒙特卡洛樹搜索（MCTS）中，由樹搜索策略來(lái)安排截?cái)帱c(diǎn)。此外，他們提出了一種新的無(wú)獎(jiǎng)勵(lì)（reward-free）探索算法，用于解決證明搜索中的獎(jiǎng)勵(lì)稀疏問題。他們賦予樹搜索智能體內(nèi)在的驅(qū)動(dòng)力，也就是好奇心，以廣泛探索策略狀態(tài)空間。這些算法模塊擴(kuò)展了他們的完整證明生成模型，使其成為一個(gè)靈活的交互式定理證明工具，能夠有效利用證明助手的反饋，生成多樣化的解決方案。

核心貢獻(xiàn)

研究者提出了一個(gè)全面的框架，用于開發(fā)基于語(yǔ)言模型的形式化數(shù)學(xué)證明工具，他們整合了幾個(gè)關(guān)鍵組件：大規(guī)模數(shù)學(xué)預(yù)訓(xùn)練、形式化數(shù)學(xué)語(yǔ)料庫(kù)的構(gòu)建和增強(qiáng)、基于證明助手反饋的在線強(qiáng)化學(xué)習(xí)，以及用于定理證明長(zhǎng)期規(guī)劃的樹搜索方法論。預(yù)訓(xùn)練模型、監(jiān)督微調(diào)模型、強(qiáng)化學(xué)習(xí)模型以及蒙特卡洛樹搜索算法的代碼都公開提供，以供進(jìn)一步研究和應(yīng)用。

1、預(yù)訓(xùn)練

研究者通過進(jìn)一步在高質(zhì)量數(shù)學(xué)和代碼數(shù)據(jù)上預(yù)訓(xùn)練，增強(qiáng)了基礎(chǔ)模型在形式化定理證明和數(shù)學(xué)推理方面的能力，重點(diǎn)關(guān)注 Lean、Isabelle 和 Metamath 等廣泛用于證明助手的形式語(yǔ)言。

2、監(jiān)督微調(diào)

研究者通過實(shí)現(xiàn)兩種數(shù)據(jù)增強(qiáng)技術(shù)，改進(jìn)了 Lean 4 代碼補(bǔ)全數(shù)據(jù)集。首先，他們使用 DeepSeek-Coder V2 236B 在 Lean 4 代碼旁注釋 CoT（chain-of-thought）評(píng)論，將形式化定理證明與自然語(yǔ)言推理對(duì)齊。其次，他們?cè)?Lean 4 證明代碼中插入中間策略狀態(tài)信息，使他們的模型能夠更有效地利用編譯器反饋。然后，他們使用這個(gè)數(shù)據(jù)集對(duì)預(yù)訓(xùn)練模型進(jìn)行微調(diào)。

3、強(qiáng)化學(xué)習(xí)

研究者采用 GRPO 算法對(duì)監(jiān)督微調(diào)模型進(jìn)行 RLPAF（reinforcement learning from proof assistant feedback，基于證明助手反饋的強(qiáng)化學(xué)習(xí)）。Lean 證明器的驗(yàn)證結(jié)果作為獎(jiǎng)勵(lì)監(jiān)督，增強(qiáng)了模型與驗(yàn)證系統(tǒng)的形式規(guī)范的一致性。

4、蒙特卡洛樹搜索

研究者通過引入一種新的抽象和相應(yīng)的搜索算法，推進(jìn)了形式化定理證明中的樹搜索方法。他們的截?cái)嗪椭匦麻_始機(jī)制作為狀態(tài) - 動(dòng)作抽象，將樹搜索過程無(wú)縫集成到完整證明生成框架中。他們展示了 RMaxTS，這是一種創(chuàng)新的蒙特卡洛樹搜索算法，利用 RMax 策略來(lái)解決證明搜索問題中稀疏獎(jiǎng)勵(lì)的探索挑戰(zhàn)。通過分配內(nèi)在獎(jiǎng)勵(lì)，這種算法鼓勵(lì)證明智能體生成多樣化的規(guī)劃路徑，從而促進(jìn)對(duì)證明空間的廣泛探索。

評(píng)估和度量

1、高中水平 miniF2F 數(shù)據(jù)集

在單通道法完整證明生成設(shè)置中，DeepSeek-Prover-V1.5 在 miniF2F 的測(cè)試集上達(dá)到了 60.2% 的通過率，比 DeepSeek-Prover-V1 的 50.0% 提高了 10.2 個(gè)百分點(diǎn)。結(jié)合樹搜索技術(shù)后，通過率進(jìn)一步提升，達(dá)到了 63.5% 的新 SOTA。

2、大學(xué)本科水平 ProofNet 數(shù)據(jù)集

DeepSeek-Prover-V1.5 在 ProofNet 的單通道法完整證明生成設(shè)置中也展現(xiàn)出強(qiáng)大的性能，在驗(yàn)證集上通過率為 21.6%，在測(cè)試集上為 23.7%。結(jié)合樹搜索技術(shù)之后，這些結(jié)果被進(jìn)一步增強(qiáng)，在驗(yàn)證集上達(dá)到了 25.4% 的新 SOTA，在測(cè)試集上達(dá)到了 25.3%。

模型訓(xùn)練

為了提高語(yǔ)言模型生成形式證明和通過數(shù)學(xué)語(yǔ)言進(jìn)行推理的能力，研究者對(duì)基礎(chǔ)模型進(jìn)行了進(jìn)一步預(yù)訓(xùn)練，并將這個(gè)改進(jìn)的模型命名為 DeepSeek-ProverV1.5-Base。

接著文章探討了 DeepSeek-Prover-V1.5 的監(jiān)督微調(diào) (SFT) 所涉及的方法和流程。具體來(lái)說(shuō)，研究者通過添加詳細(xì)的解釋性注釋來(lái)擴(kuò)充 DeepSeekProver-V1 的證明數(shù)據(jù)集。此增強(qiáng)旨在改善自然語(yǔ)言描述與 Lean 4 代碼之間的一致性，從而促進(jìn)更好的形式數(shù)學(xué)推理。此外，研究者將中間策略狀態(tài)信息作為輔助預(yù)測(cè)任務(wù)納入其中，以支持蒙特卡洛樹搜索過程中使用的截?cái)嗪椭匦麻_始機(jī)制，并將生成的模型稱為 DeepSeek-ProverV1.5-SFT。

基于證明助手反饋的強(qiáng)化學(xué)習(xí)

為了進(jìn)一步提高 DeepSeek-Prover-V1.5-SFT 的性能，該研究引入了一個(gè)強(qiáng)化學(xué)習(xí)階段，從而得到了 DeepSeek-Prover-V1.5-RL 模型。這一階段利用強(qiáng)化學(xué)習(xí)（RL）根據(jù) Lean 4 證明器的驗(yàn)證反饋來(lái)提升性能。以下是該 RL 過程的具體細(xì)節(jié)。

訓(xùn)練提示。在強(qiáng)化學(xué)習(xí)階段，該研究使用來(lái)自監(jiān)督微調(diào)數(shù)據(jù)集的部分定理陳述作為訓(xùn)練提示。經(jīng)過篩選保留了大約 4,500 個(gè)獨(dú)特的定理陳述。每個(gè)定理都帶有 CoT 和非 CoT 引導(dǎo)提示，以增強(qiáng)模型在這兩種模式下的證明生成能力。 

獎(jiǎng)勵(lì)。當(dāng)通過 RL 訓(xùn)練 LLM 時(shí)，訓(xùn)練好的獎(jiǎng)勵(lì)模型通常會(huì)提供反饋信號(hào)。相比之下，形式化定理證明受益于證明助手對(duì)生成的證明的嚴(yán)格驗(yàn)證，從而提供了顯著的優(yōu)勢(shì)。具體來(lái)說(shuō)，如果驗(yàn)證正確，則每個(gè)生成的證明將獲得 1 的獎(jiǎng)勵(lì)，否則將獲得 0 的獎(jiǎng)勵(lì)。雖然這種二元獎(jiǎng)勵(lì)信號(hào)是準(zhǔn)確的，但它也很稀疏，尤其是對(duì)于那些對(duì)監(jiān)督微調(diào)模型具有挑戰(zhàn)性的定理而言。為了緩解這種稀疏性，研究者選擇了對(duì)監(jiān)督微調(diào)模型具有挑戰(zhàn)性但可實(shí)現(xiàn)的訓(xùn)練提示，如上所述。

強(qiáng)化學(xué)習(xí)算法。該研究采用組相對(duì)策略優(yōu)化（GRPO）作為本文的 RL 算法，與 PPO 相比，該算法顯示出更高的有效性和效率。具體而言，GRPO 為每個(gè)定理提示抽取一組候選證明，并根據(jù)組內(nèi)輸出的相對(duì)獎(jiǎng)勵(lì)優(yōu)化模型。

評(píng)估。圖 3 給出了 miniF2F 和 ProofNet 數(shù)據(jù)集上每個(gè)訓(xùn)練階段的比較分析。在大多數(shù)設(shè)置中，CoT 模式始終優(yōu)于非 CoT 模式。

面向探索的蒙特卡洛樹搜索

為了在整體證明生成設(shè)置中實(shí)現(xiàn)樹搜索方法，該研究引入了證明樹抽象來(lái)定義定制的狀態(tài)和動(dòng)作空間，并利用了截?cái)嗪椭匦麻_始機(jī)制。研究者首先將不完整的證明分解為與各個(gè)證明步驟相對(duì)應(yīng)的樹節(jié)點(diǎn)序列，然后利用存儲(chǔ)在這些樹節(jié)點(diǎn)中的部分內(nèi)容繼續(xù)證明生成過程。圖 4 說(shuō)明了從整體證明生成構(gòu)建證明搜索樹的過程。

截?cái)啵涸撗芯吭诓呗约?jí)別構(gòu)建證明搜索樹，其中每條樹邊代表策略狀態(tài)的單個(gè)轉(zhuǎn)換步驟。首先，該研究將模型生成的整個(gè)證明提交給 Lean 證明器，并將其解析為策略。然后在最早的驗(yàn)證錯(cuò)誤處截?cái)嘧C明，確保所有后續(xù)策略代碼都可以成功應(yīng)用，以將證明推進(jìn)到所需的定理。策略代碼被分割成幾個(gè)代碼片段，每個(gè)代碼片段包含一個(gè)有效的策略代碼及其相關(guān)的思維鏈注釋，對(duì)應(yīng)于代表策略狀態(tài)轉(zhuǎn)換的單個(gè)樹邊。通過這種抽象，每個(gè)策略代碼被轉(zhuǎn)換為一系列樹節(jié)點(diǎn)，形成從根到特定節(jié)點(diǎn)的路徑。

重新開始：在 Lean 4 中，不同的策略可以導(dǎo)致相同的策略狀態(tài)，這意味著證明樹中的每個(gè)節(jié)點(diǎn)可能對(duì)應(yīng)多種能夠?qū)崿F(xiàn)相同結(jié)果的策略代碼。為了解決這個(gè)問題，研究者在每個(gè)節(jié)點(diǎn)存儲(chǔ)一組這些等效的策略代碼。當(dāng)樹搜索智能體展開一個(gè)節(jié)點(diǎn)時(shí)，它會(huì)隨機(jī)選擇一個(gè)策略作為語(yǔ)言模型的提示。

蒙特卡洛樹搜索的內(nèi)在獎(jiǎng)勵(lì)

接下來(lái)文章介紹了內(nèi)在獎(jiǎng)勵(lì)驅(qū)動(dòng)的探索算法 —— 應(yīng)用于樹搜索的 RMax（RMax applied to Tree Search，RMaxTS），將無(wú)獎(jiǎng)勵(lì)探索納入證明搜索問題。

RMax 應(yīng)用于 MCTS。該研究采用 RMax 這一經(jīng)典探索機(jī)制來(lái)構(gòu)建蒙特卡洛樹搜索的內(nèi)在獎(jiǎng)勵(lì)。在證明搜索的上下文中，證明完成之前不提供外部獎(jiǎng)勵(lì)，此算法過程類似于 ZeroRMax ，其中智能體的探索僅由內(nèi)在獎(jiǎng)勵(lì)驅(qū)動(dòng)，即設(shè)置。樹擴(kuò)展步驟的內(nèi)在獎(jiǎng)勵(lì)取決于是否向搜索樹中添加新節(jié)點(diǎn)

這種啟發(fā)式方法可以潛在地減少冗余生成并提高樣本效率。

實(shí)驗(yàn)結(jié)果

在本節(jié)中，研究者使用 miniF2F 和 ProofNet 這兩個(gè)基準(zhǔn)來(lái)評(píng)估 DeepSeek-Prover-V1.5 的定理證明能力。前者包括高中水平的練習(xí)和競(jìng)賽問題，后者則涉及本科水平的定理。

為了確保一致性，研究者使用了與評(píng)估中相同的訓(xùn)練模型和推理配置，展示了完整證明生成和蒙特卡洛樹搜索方法的結(jié)果。

首先，論文介紹了 DeepSeek-Prover-V1.5 與之前的一些 SOTA 模型的對(duì)比分析，重點(diǎn)展示了其性能和進(jìn)步。

• 通用模型

GPT-3.5 和 GPT-4 是 OpenAI 開發(fā)的高級(jí)生成式 AI 模型，因其在包括代碼生成在內(nèi)的各種任務(wù)中的有效性而聞名。盡管這些模型并非專為定理證明而設(shè)計(jì)，但其廣泛的參數(shù)范圍提供了重要的能力。

COPRA 促進(jìn)了這些模型在形式定理證明中的評(píng)估，它是一個(gè)上下文學(xué)習(xí)智能體，利用這些大語(yǔ)言模型提出戰(zhàn)術(shù)應(yīng)用。

此外，研究者還討論了 Llemma，這是一系列在廣泛的通用數(shù)學(xué)語(yǔ)料庫(kù)上訓(xùn)練的語(yǔ)言模型，通常用作形式定理證明的基礎(chǔ)模型。

• 形式化數(shù)學(xué)的專用模型

GPT-f 是將 Transformers 應(yīng)用于定理證明任務(wù)的證明步驟生成的初步嘗試，它利用最佳優(yōu)先搜索模塊來(lái)構(gòu)建完整的證明。后續(xù)的一些進(jìn)展包括 ReProver、LLMStep 和 Lean-STaR。

Hypertree Proof Search 利用 Lean 探索了蒙特卡洛樹搜索在形式定理證明中的應(yīng)用。同期的 InternLM2-Math 和 InternLM2-StepProver 也表現(xiàn)出卓越的性能。

然后，研究者將這些模型與 DeepSeek-Prover-V1.5 進(jìn)行了對(duì)比。

miniF2F 上的結(jié)果

表 1 提供了各種定理證明方法在 miniF2F 測(cè)試數(shù)據(jù)集上的對(duì)比分析。

在單通道完整證明生成設(shè)置中，DeepSeekProver-V1.5-RL 的通過率最高，達(dá)到 60.2%，比 DeepSeek-Prover-V1 的 50.0% 提高了 10.2 個(gè)百分點(diǎn)。DeepSeek-Prover-V1.5-RL 將采樣預(yù)算限制在 128 次嘗試，證明了 51.6% 的問題，明顯優(yōu)于其他 whole-proof 生成方法，與領(lǐng)先的樹搜索方法不相上下。在樹搜索方法類別中，DeepSeek-Prover-V1.5-RL + RMaxTS 以 62.7% 的通過率遙遙領(lǐng)先，確立了新的 SOTA 水平，與現(xiàn)有方法拉開了很大差距。

值得注意的是，DeepSeek-Prover-V1.5-RL 只需要 3200 次完整證明采樣就能達(dá)到 54.9% 的通過率，超過了 InternLM2-StepProver 之前的 SOTA 水平，后者需要執(zhí)行 64 × 3200 次樹搜索才能達(dá)到 54.5% 的通過率。

ProofNet 上的結(jié)果

表 2 列出了各種定理證明方法在 ProofNet 數(shù)據(jù)集上的對(duì)比分析。DeepSeek-Prover-V1.5-RL 在整個(gè) ProofNet 數(shù)據(jù)集上的通過率分別達(dá)到了 22.6% 和 25.3%。這些結(jié)果超過了現(xiàn)有的 SOTA 方法 ReProver（13.8%）和 InternLM2-StepProver（18.1%）。當(dāng)完整證明生成嘗試次數(shù)限制為 3200 次時(shí)，DeepSeek-Prover-V1.5 也證明了 21.7% 的定理，比之前最先進(jìn)的 InternLM2-StepProver 提高了 3.6%。

重新審視訓(xùn)練策略在大規(guī)模采樣中的效果

研究者重新審視了多個(gè)訓(xùn)練模塊在大規(guī)模采樣環(huán)境中的效果，重點(diǎn)是單通道完整證明生成和蒙特卡洛樹搜索。

表 3 比較了兩種生成模式，即非 CoT 和 CoT 在 miniF2F-test 數(shù)據(jù)集上的性能，表明隨著樣本預(yù)算的增加，CoT 相對(duì)于非 CoT 模式的優(yōu)勢(shì)被放大。

消融實(shí)驗(yàn)

在消融實(shí)驗(yàn)中，研究者檢驗(yàn)了 RMaxTS 的算法設(shè)計(jì)。實(shí)驗(yàn)是在 miniF2F 測(cè)試數(shù)據(jù)集上使用 DeepSeek-Prover-V1.5-RL 以 CoT 模式進(jìn)行的。如圖 5 所示，左側(cè)顯示了 6400 個(gè)生成樣本內(nèi) Pass@K 準(zhǔn)確率的曲線，右側(cè)顯示了樣本量更大時(shí)的結(jié)果。