AI 技術與數學發現的進展，正前所未有地交織在一起。

前段時間，著名數學家陶哲軒在牛津數學公開講座中做了主題為「AI 在科學和數學中的潛力」的主題分享。他指出，將 AI 整合到數學領域將使形式化證明的編寫速度超過人類證明（人類證明容易出錯）。這將成為一個關鍵轉折點，意味著形式化證明的使用將不僅限于驗證現有的證明，還將用于創造新的數學知識。這將通過廣泛的人類數學家與 AI 數學家之間的協作來實現。我們將迎來一個「大數學」時代！

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

DeepSeek-Prover-V1.5 是一個 70 億參數的開源模型。它通過結合強化學習（基于證明助手反饋的強化學習，RLPAF）和蒙特卡洛樹搜索（特別是提出的 RMaxTS 變體），顯著提升了證明生成的效率和準確性。DeepSeek-Prover-V1.5 在 Lean 4 的形式定理證明方面優于所有開源模型。

以下是技術報告的詳細內容。

技術報告概述

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

近年來，在大型語言模型領域取得的進展極大地推動了人工智能在數學推理和定理證明方面的發展。但語言模型在形式化定理證明方面仍面臨重大挑戰。例如，使用 Lean 和 Isabelle 這類系統進行證明時，需要進行嚴格的推導，以滿足驗證系統的形式規范。即便是像 GPT-4 這樣的先進模型，在處理復雜的形式證明時也顯得力不從心，這凸顯了形式化證明中編碼和數學推理的復雜性。一個高效的形式化定理證明模型不僅需要理解 Lean 證明助手等形式化系統的語法和語義，還需要將抽象的數學推理與精確的形式化表達方式相結合。

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

證明步驟生成通過預測并驗證每一個策略，利用形式化驗證器獲取當前策略狀態的更新信息，并常結合樹搜索技術來構建有效的證明。而完整證明生成則在計算上更為高效，它基于定理陳述一次性生成整個證明代碼，減少了證明模型與形式化定理驗證器之間協調所需的通信量。

盡管 DeepSeek-Prover-V1 在 Lean 4 中通過完整證明生成取得了 SOTA 成果，但這種方法也有其獨特的挑戰。它需要在沒有中間策略狀態信息的情況下進行長期序列預測，而未來的策略依賴于這些隱藏的結果。在 Lean 的策略模式中，證明是通過一系列改變證明狀態的策略來構建的。這種順序性可能導致錯誤累積，一個小的誤差就可能使證明偏離正確的路徑。具體來說，自回歸模型在生成長證明時可能會對中間策略狀態有錯誤的認識。

為了在不犧牲完整證明生成的簡便性和計算效率的同時，無縫地整合中間策略狀態，研究者在 DeepSeek-Prover-V1.5 中開發了一種統一方法。這種方法通過截斷和重新開始（truncate-and-resume）機制，結合了證明步驟生成和完整證明生成的優勢。

該過程從標準的完整證明生成開始，語言模型根據定理陳述前綴完成證明代碼，然后由 Lean 證明器進行驗證。如果證明正確無誤，流程就此結束。如果發現錯誤，就從第一個錯誤信息處截斷代碼，并丟棄后續代碼。然后，使用成功生成的證明代碼作為提示，生成下一個證明段。

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

核心貢獻

研究者提出了一個全面的框架，用于開發基于語言模型的形式化數學證明工具，他們整合了幾個關鍵組件：大規模數學預訓練、形式化數學語料庫的構建和增強、基于證明助手反饋的在線強化學習，以及用于定理證明長期規劃的樹搜索方法論。預訓練模型、監督微調模型、強化學習模型以及蒙特卡洛樹搜索算法的代碼都公開提供，以供進一步研究和應用。

1、預訓練

研究者通過進一步在高質量數學和代碼數據上預訓練，增強了基礎模型在形式化定理證明和數學推理方面的能力，重點關注 Lean、Isabelle 和 Metamath 等廣泛用于證明助手的形式語言。

2、監督微調

研究者通過實現兩種數據增強技術，改進了 Lean 4 代碼補全數據集。首先，他們使用 DeepSeek-Coder V2 236B 在 Lean 4 代碼旁注釋 CoT（chain-of-thought）評論，將形式化定理證明與自然語言推理對齊。其次，他們在 Lean 4 證明代碼中插入中間策略狀態信息，使他們的模型能夠更有效地利用編譯器反饋。然后，他們使用這個數據集對預訓練模型進行微調。

3、強化學習

研究者采用 GRPO 算法對監督微調模型進行 RLPAF（reinforcement learning from proof assistant feedback，基于證明助手反饋的強化學習）。Lean 證明器的驗證結果作為獎勵監督，增強了模型與驗證系統的形式規范的一致性。

4、蒙特卡洛樹搜索

研究者通過引入一種新的抽象和相應的搜索算法，推進了形式化定理證明中的樹搜索方法。他們的截斷和重新開始機制作為狀態 - 動作抽象，將樹搜索過程無縫集成到完整證明生成框架中。他們展示了 RMaxTS，這是一種創新的蒙特卡洛樹搜索算法，利用 RMax 策略來解決證明搜索問題中稀疏獎勵的探索挑戰。通過分配內在獎勵，這種算法鼓勵證明智能體生成多樣化的規劃路徑，從而促進對證明空間的廣泛探索。

評估和度量

1、高中水平 miniF2F 數據集

在單通道法完整證明生成設置中，DeepSeek-Prover-V1.5 在 miniF2F 的測試集上達到了 60.2% 的通過率，比 DeepSeek-Prover-V1 的 50.0% 提高了 10.2 個百分點。結合樹搜索技術后，通過率進一步提升，達到了 63.5% 的新 SOTA。

2、大學本科水平 ProofNet 數據集

DeepSeek-Prover-V1.5 在 ProofNet 的單通道法完整證明生成設置中也展現出強大的性能，在驗證集上通過率為 21.6%，在測試集上為 23.7%。結合樹搜索技術之后，這些結果被進一步增強，在驗證集上達到了 25.4% 的新 SOTA，在測試集上達到了 25.3%。

模型訓練

為了提高語言模型生成形式證明和通過數學語言進行推理的能力，研究者對基礎模型進行了進一步預訓練，并將這個改進的模型命名為 DeepSeek-ProverV1.5-Base。

接著文章探討了 DeepSeek-Prover-V1.5 的監督微調 (SFT) 所涉及的方法和流程。具體來說，研究者通過添加詳細的解釋性注釋來擴充 DeepSeekProver-V1 的證明數據集。此增強旨在改善自然語言描述與 Lean 4 代碼之間的一致性，從而促進更好的形式數學推理。此外，研究者將中間策略狀態信息作為輔助預測任務納入其中，以支持蒙特卡洛樹搜索過程中使用的截斷和重新開始機制，并將生成的模型稱為 DeepSeek-ProverV1.5-SFT。

基于證明助手反饋的強化學習

為了進一步提高 DeepSeek-Prover-V1.5-SFT 的性能，該研究引入了一個強化學習階段，從而得到了 DeepSeek-Prover-V1.5-RL 模型。這一階段利用強化學習（RL）根據 Lean 4 證明器的驗證反饋來提升性能。以下是該 RL 過程的具體細節。

訓練提示。在強化學習階段，該研究使用來自監督微調數據集的部分定理陳述作為訓練提示。經過篩選保留了大約 4,500 個獨特的定理陳述。每個定理都帶有 CoT 和非 CoT 引導提示，以增強模型在這兩種模式下的證明生成能力。 

獎勵。當通過 RL 訓練 LLM 時，訓練好的獎勵模型通常會提供反饋信號。相比之下，形式化定理證明受益于證明助手對生成的證明的嚴格驗證，從而提供了顯著的優勢。具體來說，如果驗證正確，則每個生成的證明將獲得 1 的獎勵，否則將獲得 0 的獎勵。雖然這種二元獎勵信號是準確的，但它也很稀疏，尤其是對于那些對監督微調模型具有挑戰性的定理而言。為了緩解這種稀疏性，研究者選擇了對監督微調模型具有挑戰性但可實現的訓練提示，如上所述。

強化學習算法。該研究采用組相對策略優化（GRPO）作為本文的 RL 算法，與 PPO 相比，該算法顯示出更高的有效性和效率。具體而言，GRPO 為每個定理提示抽取一組候選證明，并根據組內輸出的相對獎勵優化模型。

評估。圖 3 給出了 miniF2F 和 ProofNet 數據集上每個訓練階段的比較分析。在大多數設置中，CoT 模式始終優于非 CoT 模式。

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

為了在整體證明生成設置中實現樹搜索方法，該研究引入了證明樹抽象來定義定制的狀態和動作空間，并利用了截斷和重新開始機制。研究者首先將不完整的證明分解為與各個證明步驟相對應的樹節點序列，然后利用存儲在這些樹節點中的部分內容繼續證明生成過程。圖 4 說明了從整體證明生成構建證明搜索樹的過程。

截斷：該研究在策略級別構建證明搜索樹，其中每條樹邊代表策略狀態的單個轉換步驟。首先，該研究將模型生成的整個證明提交給 Lean 證明器，并將其解析為策略。然后在最早的驗證錯誤處截斷證明，確保所有后續策略代碼都可以成功應用，以將證明推進到所需的定理。策略代碼被分割成幾個代碼片段，每個代碼片段包含一個有效的策略代碼及其相關的思維鏈注釋，對應于代表策略狀態轉換的單個樹邊。通過這種抽象，每個策略代碼被轉換為一系列樹節點，形成從根到特定節點的路徑。

重新開始：在 Lean 4 中，不同的策略可以導致相同的策略狀態，這意味著證明樹中的每個節點可能對應多種能夠實現相同結果的策略代碼。為了解決這個問題，研究者在每個節點存儲一組這些等效的策略代碼。當樹搜索智能體展開一個節點時，它會隨機選擇一個策略作為語言模型的提示。

蒙特卡洛樹搜索的內在獎勵

接下來文章介紹了內在獎勵驅動的探索算法 —— 應用于樹搜索的 RMax（RMax applied to Tree Search，RMaxTS），將無獎勵探索納入證明搜索問題。

RMax 應用于 MCTS。該研究采用 RMax 這一經典探索機制來構建蒙特卡洛樹搜索的內在獎勵。在證明搜索的上下文中，證明完成之前不提供外部獎勵，此算法過程類似于 ZeroRMax ，其中智能體的探索僅由內在獎勵驅動，即設置。樹擴展步驟的內在獎勵取決于是否向搜索樹中添加新節點

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

實驗結果

在本節中，研究者使用 miniF2F 和 ProofNet 這兩個基準來評估 DeepSeek-Prover-V1.5 的定理證明能力。前者包括高中水平的練習和競賽問題，后者則涉及本科水平的定理。

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

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

• 通用模型

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

COPRA 促進了這些模型在形式定理證明中的評估，它是一個上下文學習智能體，利用這些大語言模型提出戰術應用。

此外，研究者還討論了 Llemma，這是一系列在廣泛的通用數學語料庫上訓練的語言模型，通常用作形式定理證明的基礎模型。

• 形式化數學的專用模型

GPT-f 是將 Transformers 應用于定理證明任務的證明步驟生成的初步嘗試，它利用最佳優先搜索模塊來構建完整的證明。后續的一些進展包括 ReProver、LLMStep 和 Lean-STaR。

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

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

miniF2F 上的結果

表 1 提供了各種定理證明方法在 miniF2F 測試數據集上的對比分析。

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

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

ProofNet 上的結果

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

重新審視訓練策略在大規模采樣中的效果

研究者重新審視了多個訓練模塊在大規模采樣環境中的效果，重點是單通道完整證明生成和蒙特卡洛樹搜索。

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

消融實驗

在消融實驗中，研究者檢驗了 RMaxTS 的算法設計。實驗是在 miniF2F 測試數據集上使用 DeepSeek-Prover-V1.5-RL 以 CoT 模式進行的。如圖 5 所示，左側顯示了 6400 個生成樣本內 Pass@K 準確率的曲線，右側顯示了樣本量更大時的結果。