DeepSeek-Prover-V1.5 透過結合強化學習和蒙特卡洛樹搜索，顯著提升了證明生成的效率和準確性。
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）探索演算法，用於解決證明搜尋中的獎勵稀疏問題。他們賦予樹搜尋智慧體內在的驅動力，也就是好奇心，以廣泛探索策略狀態空間。這些演算法模組擴展了他們的完整證明生成模型，使其成為一個靈活的互動式定理證明工具，能夠有效利用證明助手的回饋，產生多樣化的解決方案。 研究者提出了一個全面的框架，用於開發基於語言模型的形式化數學證明工具，他們整合了幾個關鍵組件：大規模數學預訓練、形式化數學語料庫的構建和增強、基於證明助手反饋的在線強化學習，以及用於定理證明長期規劃的樹搜尋方法論。預訓練模型、監督微調模型、強化學習模型以及蒙特卡洛樹搜尋演算法的程式碼都公開提供，以便進一步研究和應用。 研究者透過進一步在高品質數學和程式碼資料上預先訓練，增強了基礎模型在形式化定理證明和數學推理方面的能力，重點關注Lean、Isabelle 和Metamath 等廣泛用於證明助手的形式語言。 研究者透過實現兩種資料增強技術，改進了Lean 4 程式碼補全數據集。首先，他們使用 DeepSeek-Coder V2 236B 在 Lean 4 程式碼旁註釋 CoT（chain-of-thought）評論，將形式化定理證明與自然語言推理對齊。其次，他們在 Lean 4 證明程式碼中插入中間策略狀態訊息，使他們的模型更有效地利用編譯器回饋。然後，他們使用這個資料集對預訓練模型進行微調。 研究者採用GRPO 演算法對監督微調模型進行RLPAF（inforcement learning proreinforcement learning pro assistant feedback，基於證明助手回饋的強化學習）。 Lean 證明器的驗證結果作為獎勵監督，增強了模型與驗證系統的形式規範的一致性。 研究者透過引入一種新的抽象和相應的搜尋演算法，推進了形式化定理證明中的樹搜尋方法。他們的截斷和重新開始機製作為狀態 - 動作抽象，將樹搜尋過程無縫整合到完整證明生成框架中。他們展示了 RMaxTS，這是一種創新的蒙特卡羅樹搜尋演算法，利用 RMax 策略來解決證明搜尋問題中稀疏獎勵的探索挑戰。透過分配內在獎勵，這種演算法鼓勵證明智能體產生多樣化的規劃路徑，從而促進對證明空間的廣泛探索。
在單通道法完整證明生成設定中，DeepSeek-Prover-V1.5 在miniF2F 的測試集上達到了60.2% 的通過率，比DeepSeek-Prover-V1 的50.0 % 提高了10.2 個百分點。結合樹搜尋技術後，通過率進一步提升，達到了 63.5% 的新 SOTA。
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。 為了進一步提高DeepDeep 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 ，其中智能體的探索僅由內在獎勵驅動，即設定
。樹擴展步驟的內在獎勵取決於是否向搜尋樹中添加新節點這種啟發式方法可以潛在地減少冗餘生成並提高樣本效率。 在本節中，研究者使用他們使用兩個基準來評估DeepSeek-Prover-V1.5 的定理證明能力。前者包括高中程度的練習和競賽問題，後者則涉及本科程度的定理。 為了確保一致性，研究者使用了與評估中相同的訓練模型和推理配置，展示了完整證明生成和蒙特卡洛樹搜尋方法的結果。 首先，論文介紹了 DeepSeek-Prover-V1.5 與之前的一些 SOTA 模型的對比分析，重點展示了其性能和進步。
COPRA 促進了這些模型在形式定理證明中的評估，它是一個上下文學習智能體，利用這些大語言模型提出戰術應用。
此外，研究者還討論了 Llemma，這是一系列在廣泛的通用數學語料庫上訓練的語言模型，通常用作形式定理證明的基礎模型。
Hypertree Proof Search 利用 Lean 探討了蒙特卡羅樹搜尋在形式定理證明中的應用。同期的 InternLM2-Math 和 InternLM2-StepProver 也表現出卓越的性能。
然後，研究者將這些模型與 DeepSeek-Prover-V1.5 進行了比較。
各種定理證明方法在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% 的通過率。
表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 模式的優勢被放大。 在消融實驗中，研究者檢驗了RMaxRTS 的演算法設計。實驗是在 miniF2F 測試資料集上使用 DeepSeek-Prover-V1.5-RL 以 CoT 模式進行的。如圖 5 所示，左側顯示了 6400 個生成樣本內 Pass@K 準確率的曲線，右側顯示了樣本量更大時的結果。 以上是DeepSeek開源數學大模型，高中、大學定理證明新SOTA的詳細內容。更多資訊請關注PHP中文網其他相關文章！
