DeepSeek發佈開源數學定理證明模型

DeepSeek2024年8月16日
DeepSeek-Prover-V1 展示了大模型在數學定理證明領域的潛力，通過將數學問題轉換爲 Lean 編程語言，幫助數學家嚴格驗證證明正確性。
今天，DeepSeek 開源 Prover-V1.5 版本，引入了類似 AlphaGo 的強化學習系統，模型通過自我迭代和 Lean 證明器監督，構建了一個“圍棋”式的學習環境。
最終，僅 7B 參數規模的 Prover-V1.5，在高中（miniF2F）和大學（ProofNet）數學定理證明測試中分別達到了 63.5% 和 25.3% 的成功率，超越了多款開源模型（InternLM2-StepProver、Llemma）。

Highlights

  • 數據 ：使用 DeepSeek-Coder-V2 合成自然語言思維鏈標註數據，結合 Lean 證明器標註的中間狀態信息，將模型的形式化證明能力與自然語言推理對齊，同時滿足程序驗證的要求。
  • 訓練 ：以 Lean 證明器的驗證結果直接作爲獎勵信號，使用 GRPO 算法對模型進行強化學習訓練。
  • 蒙特卡洛樹搜索 ：引入 RMaxTS 算法，激勵探索行爲以解決證明搜索中的獎勵稀疏問題，增強模型靈活生成多樣化證明的能力。
  • 實驗結果 ：在高中水平的 miniF2F 和大學本科水平的 ProofNet 基準測試中取得了新的 SOTA，顯著超越了主流數學模型。
論文和模型均已開源：
論文地址： https://arxiv.org/abs/2408.08152
模型下載： https://huggingface.co/deepseek-ai

GitHub 主頁： https://github.com/deepseek-ai/DeepSeek-Prover-V1.5

模型訓練

  • 預訓練

在高質量的數學和代碼數據上進行進一步的預訓練，特別關注 Lean、Isabelle 和 Metamath 等定理證明語言，以提高模型在形式化數學領域的通用能力。

  • 有監督微調

已有工作大多聚焦於僅僅生成下一個證明步驟，而 DeepSeek-Prover-V1.5 則選擇了更爲困難的完整證明生成的訓練目標。此外，在 DeepSeek-Prover-V1 合成的大規模定理證明數據的基礎上，利用 DeepSeek-Coder-V2 合成自然語言的思維鏈數據標註，促使模型兼顧自然語言推理與形式化定理證明。

  • 強化學習

抽取微調數據中的定理內容作爲輸入，使用微調後的模型生成多個完整的證明候選項，然後利用 Lean 證明器對其正確性進行檢驗。將驗證結果作爲二元獎勵信號，強化學習訓練進一步增強了模型與驗證系統形式規範的一致性。

三階段模型權重均已開源。

蒙特卡洛樹搜索

DeepSeek-Prover-V1.5 將定理證明中的蒙特卡洛樹搜索從單一證明預測推廣至完整證明生成，爲此特別引入了“截斷-恢復”的機制來進行樹節點的擴展：
（a） 選擇一個節點進行擴展，追蹤其對應的證明代碼前綴，其中包括文件頭、初始聲明以及所有祖先節點中已經成功應用的 tactics。
（b） 模型基於這個代碼前綴和 Lean 證明器返回的 tactic state 生成後續完整證明。
（c） Lean 4 證明器驗證組合後的證明代碼（前綴和新生成的代碼）。如果沒有發現錯誤，樹搜索過程終止。如果檢測到錯誤，我們在第一個錯誤消息處截斷新生成的代碼，丟棄後續代碼，並將成功部分解析爲 tactics。
（d） 每個 tactic 作爲新節點添加到搜索樹中，在選定的節點之後擴展出一串後繼節點。
（e） 完成樹節點擴展後，選擇另一個候選節點並進行下一輪擴展。
這個過程重複進行，直到找到正確的證明或達到採樣數上限。

此外，DeepSeek-Prover-V1.5 結合了一種新的蒙特卡洛樹搜索算法——RMaxTS，建立了內在獎勵機制以引導搜索流程中生成的證明產生多樣化的 tactic state，利用 Lean 證明器的反饋來幫助減少冗餘生成，提高採樣效率。

模型表現

下表展示了各模型在 miniF2F-test 基準測試中的表現。該基準由高中水平的數學習題和競賽題（如 AMC、AIME 和 IMO）在 Lean 定理證明語言中形式化而成。在直接生成完整證明的任務中，DeepSeek-Prover-V1.5 以 60.2% 的證明通過率顯著領先其他方法。當結合 RMaxTS 樹搜索技術時，其性能更是提升至 63.5% 的通過率。

下表呈現了各模型在 ProofNet 基準測試上的成績。該基準精選了數學本科主流教材中的習題，涵蓋實分析、複分析、線性代數、抽象代數和拓撲學等核心分支。在直接生成證明的任務中，DeepSeek-Prover-V1.5 再次以 22.6% 的通過率顯著超越其他方法。運用 RMaxTS 樹搜索後，其表現進一步提升至 25.3% 的通過率。

更多方法細節和分析實驗見論文，閱讀原文即可獲取。

About Future

隨着人工智能技術的不斷進步，數學定理證明領域正迎來一場革命。DeepSeek-Prover-V1.5的最新成果表明，AI能夠憑藉其強大的邏輯推理能力獨立解決多步驟的複雜證明問題。這一突破不僅展示了AI在數學定理證明中的巨大潛力，還爲未來開發能夠自主提出並證明完整數學理論的AI系統奠定了堅實基礎。這些系統將有助於人類數學家更深入地探索數學真理，推動數學研究的前沿發展。

閱讀原文