夢晨 西風 發自 凹非寺
量子位 | 公眾號 QbitAI

DeepSeek放大招！新模型專注數學定理證明，大幅刷新多項高難基準測試。

在普特南測試上，新模型DeepSeek-Prover-V2直接把記錄刷新到49道。

目前的第一名在657道題中只做出10道題，為Kimi與AIME2024冠軍團隊Numina合作成果Kimina-Prover。

而未針對定理證明優化的DeepSeek-R1只做出1道。

讓還沒發布的R2更令人期待了。

除測評結果之外，論文中特別報告了“通過強化學習發現新技能”現象。

正如R1帶來了“啊哈時刻”，Prover-V2也有令人意想不到的能力。

具體來說，在普特南測試中，參數量較小的DeepSeek-Prover-V2-7B用非CoT生成模式成功解決了13個671B模型未能解決的問題。

團隊仔細檢查該模型的輸出后發現，其推理方法存在一個獨特模式：7B模型處理涉及有限基數的問題時，經常使用Cardinal.toNat和Cardinal.natCast_inj，而671B模型生成的輸出中明顯沒有這些內容。

要注意，7B模型是在DeepSeek-Prover-V1.5-Base模型基礎上，先使用671B模型在強化學習階段收集的數據微調，再執行強化學習得來的。

也就是說，7B模型學會了671B模型沒有學會的新技能。

那么，DeepSeeK-Prover-V2如何煉成的呢？與前代相比又有哪些改進？

形式化和非形式化數學證明統一模型

DeepSeek數學定理證明DeepSeek-Prover系列模型已推出3款：

• 2024年3月的DeepSeek-Prover（后簡稱為Prover-V1）
• 2024年8月的DeepSeek-Prover-V1.5（后簡稱為Prover-V1.5）
• 2025年5月的DeepSeek-Prover-V2（后簡稱為Prover-V2）

Prover-V1主要探索了通過大規模合成數據集微調DeepSeek-Math-7B，來推進定理證明。

Prover-V1.5在此基礎上增加了證明助手反饋的強化學習（RLPAF）和蒙特卡洛樹搜索方法。

Prover-V2進一步提出“子目標分解的強化學習”，并且基礎模型從DeepSeek-Math-7B升級到DeepSeek-V3。

整合DeepSeek-V3的高上下文窗口和強大的自然語言推理能力，把形式化和非形式化數學證明統一到一個模型中。

Prover-V2還繼承了Prover-V1.5提出的CoT和非CoT生成兩種模式。

接下來，詳細介紹Prover-V2的各主要環節。

通過遞歸證明搜索合成冷啟動推理數據

利用DeepSeek-V3作為子目標分解和形式化的統一工具構建冷啟動數據集，提示DeepSeek-V3將定理分解為高級證明草圖，同時在Lean 4中將這些證明步驟形式化，從而產生一系列子目標。

使用一個較小的70億參數模型來處理每個子目標的證明搜索，從而減輕相關的計算負擔。一旦一個具有挑戰性的問題的分解步驟得到解決，就將完整的逐步形式化證明與來自DeepSeek-V3的相應思維鏈進行配對，以創建冷啟動推理數據。

使用合成冷啟動數據進行子目標分解的強化學習

團隊精心挑選了一組具有挑戰性的問題，這些問題無法由70億參數量的證明器模型以端到端的方式解決，但所有分解后的子目標都已成功解決。

通過組合所有子目標的證明，為原始問題構建了一個完整的形式化證明。

然后，將此證明附加到DeepSeek-V3的思維鏈中，該思維鏈概述了相應的引理分解，從而實現了非形式化推理與后續形式化的有機結合。

在合成冷啟動數據上對證明器模型進行微調后進行強化學習階段，進一步增強其將非正式推理與形式化證明構建相銜接的能力。遵循推理模型的標準訓練目標，使用二元的正確或錯誤反饋作為獎勵監督的主要形式。

具體訓練細節

兩階段訓練：

DeepSeek-Prover-V2分兩階段建立互補證明生成模式。

第一階段用高效非思維鏈（non-CoT）模式，聚焦快速生成Lean證明代碼，加快迭代和數據收集。

第二階段基于第一階段成果，采用高精度思維鏈（CoT）模式，闡述中間推理步驟，用冷啟動思維鏈數據強化學習，提升復雜問題推理能力。

專家迭代：

其中非CoT模式訓練遵循專家迭代范式，用最佳證明策略為難題生成證明嘗試，經Lean驗證，成功的納入監督微調（SFT）數據集。與之前版本相比，訓練問題分布有調整，引入了額外問題和子目標分解生成的問題。

監督微調：

對DeepSeek-V3-Base-671B做監督微調，訓練語料庫包含兩個互補來源的數據：

一是通過專家迭代收集的非CoT數據，這些數據生成的Lean代碼不包含中間推理步驟，主要用于強化模型在 Lean 定理證明生態系統中的形式驗證技能。

二是冷啟動CoT數據，這些數據將DeepSeek-V3的先進數學推理過程提煉為結構化的證明路徑，明確地模擬了將數學直覺轉化為形式證明結構的認知過程。

強化學習：

采用GRPO算法，與傳統的PPO不同，GRPO無需單獨的裁判模型，它通過為每個定理提示采樣一組候選證明，并根據它們的相對獎勵來優化策略。

訓練過程中使用二元獎勵機制，即生成的Lean證明若被驗證正確則獲得獎勵1，否則為0。

為確保學習效果，精心挑選訓練提示，僅包含那些有足夠挑戰性但又能被監督微調后的模型解決的問題。

蒸餾DeepSeek-Prover-V2 7B

將DeepSeek-Prover-V1.5-Base-7B上下文窗口擴展到32768個token，用DeepSeek-Prover-V2-671B數據微調，融入非CoT證明數據，以便利用小模型生成簡潔的形式化輸出，提供一種經濟高效的證明選項。

此外，對DeepSeek-Prover-V2-7B執行與671B模型訓練中相同的強化學習階段，以進一步提升其性能。

由此得到的模型Prover-V2 671B在神經定理證明方面達到了最先進的性能，在miniF2F測試中的通過率達到 88.9%，并解決了普特南測試中的49道。Prover-V2為miniF2F數據集生成的證明可單獨下載。

ProverBench：AIME和教科書問題的形式化

與Prover-V2一起推出ProverBench，這是一個包含325個問題的基準數據集。其中，有15個問題是從近期美國數學邀請賽（AIME 24和25）的數論與代數題目中形式化而來，提供了真實的高中競賽水平挑戰。其余310個問題則取自精心挑選的教科書示例和教學教程，構成了一套多樣化且基于教學需求的形式化數學問題集合。該基準旨在能夠對高中競賽問題和本科階段數學問題進行更全面的評估。

DeepSeek-Prover-V2系列在三個數據集上評測的最后總成績如下：

DeepSeek全明星陣容

Prover-V2的作者共18人，共同一作Z.Z. Ren, 邵智宏、辛華劍都是參與過V3、R1以及Prover系列前作的主力成員。

作者名單中出現了幾位未參與前兩代版本（Prover-V1、Prover-V1.5）的研究者。

比如Shirong Ma，清華本碩。公開資料顯示，他于去年畢業后即加入DeepSeek，現為DeepSeek研究員，此前參與了從DeepSeek LLM v1到R1以及DeepSeek-Coder等工作。

還有Zhe Fu、Yuxuan Liu。

雖然他們都沒出現在Prover-V1、Prover-V1.5的作者名單中，但均為DeepSeek資深成員。

在Prover-V1/V1.5同一期發布的《Fire-Flyer AI-HPC》研究中可見其署名。

該研究提出的Fire-Flyer AI-HPC架構，通過軟硬件協同設計降低訓練成本，解決傳統超算架構在AI訓練需求上的不足。

不過這次Prover-V2的論文中并未提及在訓練或推理基礎設施具體有哪些優化策略。

最后還有一位新面孔Hongxuan Tang，暫未了解到具體信息。

Prover-V2發布后迅速引發社區關注，GitHub倉庫12小時內即獲得350+星標。

在X（原Twitter）、抱抱臉等平臺，網友們展開熱烈討論。

Prover-V2核心貢獻者邵智宏在個人賬號主動推介研究成果。

X工程師@kache特別贊賞道：

感謝你們對開放科學研究的奉獻。

普林斯頓大學助理教授Chi Jin表示：

恭喜這項驚人的工作！在miniF2F上攻克最后10%-20%的問題標志著能力上的重大飛躍。當前形式化數學領域的競爭態勢堪稱激烈，難以置信Kimina僅保持了兩周SOTA就被DeepSeek超越。

就連Kimina-Prover核心貢獻者@Marco Dos Santos都來送上了祝賀：

祝賀DeepSeek AI團隊將miniF2F任務的SOTA提升到了89%！
很高興看到長思維鏈方法正在被其他團隊獨立探索且呈現出一些有趣的差異。形式數學如今比以往任何時候都更受歡迎！

另外，網友們最關注的問題仍然是：R2什么時候發布啊～

論文：
https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/DeepSeek_Prover_V2.pdf
模型：
https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

DeepSeek-Prover
https://arxiv.org/abs/2405.14333
DeepSeek-Prover-V1.5
https://arxiv.org/abs/2408.08152