機器之心報道

編輯：大盤雞、澤南

DeepSeek R2 的前奏？

五一勞動節到了，DeepSeek 的新消息可沒停下來。

前些天到處都在流傳著 DeepSeek-R2 即將發布的傳言，DeepSeek 確實有新動作，不過大家沒等來 R2，等來的是 DeepSeek-Prover-V2，它當然也是開源的。

Prover-V2 在定理證明賽道上實現了業內最佳性能，在 MiniF2F 測試中達到了 88.9% 的通過率，在 AIME 24、25 上也有不錯的分數。

在 4 月 30 日晚，機器學習協作平臺 HuggingFace 上就更新了 DeepSeek-Prover-V2 的一些技術細節。

這次 DeepSeek 團隊發布了兩個版本的 DeepSeek-Prover-V2 模型，參數規模分別為 7B 和 671B。

其中，DeepSeek-Prover-V2-671B 是在 DeepSeek-V3-Base 基礎上訓練而成，而 DeepSeek-Prover-V2-7B 則基于 DeepSeek-Prover-V1.5-Base 構建，并支持最長 32K tokens 的上下文長度擴展。

• DeepSeek-Prover-V2-7B 鏈接：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B
• DeepSeek-Prover-V2-671B 鏈接：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

要一句話總結 DeepSeek-Prover-V2 到底是什么？它是一款專為「數學 AI 編程語言」Lean 4 打造的開源大語言模型，專注于形式化定理證明。

它的初始化數據通過一個由 DeepSeek-V3 驅動的遞歸定理證明流程收集而來。在冷啟動訓練階段，首先通過提示 DeepSeek-V3 將復雜問題分解成一系列可以解決的子目標。每解決一個子目標就會將這些證明整合成「思維鏈」。 并融合 DeepSeek-V3 的逐步推理軌跡，共同構建出用于強化學習的初始訓練數據。

這一策略的精妙之處在于：它能夠將非形式化和形式化的數學推理融合到一個統一的模型中，讓模型既能像人一樣靈活思考，也能像機器一樣嚴謹論證，真正實現了數學推理的一體化融合。

具體是如何實現的呢？DeepSeek 也發布了 DeepSeek-Prover-V2 的技術報告，讓我們看看其中是怎么說的：

技術概述

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

為了構建冷啟動數據集，DeepSeek 團隊設計了一條簡潔高效的遞歸定理證明流程，使用 DeepSeek-V3 作為統一工具，既負責子目標的拆解，也負責推理步驟的形式化表達。其中具體的過程則是通過提示引導 DeepSeek-V3 將定理拆解為高層次的證明草圖，并在此過程中同時將這些推理步驟用 Lean 4 語言形式化，最終生成一系列結構清晰、邏輯嚴密的子目標。

DeepSeek-Prover-V2 使用冷啟動數據收集過程概覽。

降低計算開銷一直是 DeepSeek 團隊的強項，這次也不例外。他們使用一個更小的 7B 模型來完成每個子目標的證明搜索，從而降低計算負擔。當復雜問題被拆解的各個步驟都成功解決后，他們將完整的形式化逐步證明與 DeepSeek-V3 生成的思維鏈相對應，組合成冷啟動推理數據。

何將分解的子目標轉化為一系列引理陳述的一個示例。

基于合成冷啟動數據的強化學習

DeepSeek 團隊挑選了一部分具有挑戰性的定理問題。7B 證明模型沒法雖然沒法兒將它們端到端的解決，但是能夠拿捏拆解出來的一系列子目標。

整合所有子目標的證明就可以構建出原始問題的完整形式化證明。隨后，將該正式證明附加到 DeepSeek-V3 所生成的思維鏈，這條思維鏈展示了對應的引理拆解過程，從而形成了一份將非形式化推理與后續形式化過程緊密融合的訓練數據。

在對證明模型進行合成冷啟動數據的微調后，研究團隊進一步引入強化學習階段，進一步提升模型將非形式化推理轉化為形式化證明的能力。在訓練過程中，遵循推理模型的通用目標，采用「對 / 錯」二值反饋作為主要的獎勵信號。

最終得到的模型 DeepSeek-Prover-V2-671B 在神經定理證明任務中達到了當前最先進的性能，在 MiniF2F-test 上的通過率達到 88.9%，并成功解決了 PutnamBench 數據集中 658 道題中的 49 道。DeepSeek-Prover-V2 在 miniF2F 數據集上生成的所有證明已整理為 ZIP 文件，開放下載。

下載鏈接：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/minif2f-solutions.zip

訓練細節、實驗結果

DeepSeek-Prover-V2 經歷了兩階段訓練，這一過程建立了兩種互補的證明生成模式：

1. 高效非思維鏈（non-CoT）模式：此模式針對快速生成正式的 Lean 證明代碼進行優化，專注于生成簡潔的證明，沒有顯式的中間推理步驟。

2. 高精度思維鏈（CoT）模式：此模式系統地闡述中間推理步驟，強調透明度和邏輯進展，然后構建最終的正式證明。

與 DeepSeek-Prover-V1.5 一致，這兩種生成模式由兩個不同的引導提示控制。在第一階段采用專家迭代，在課程學習框架內訓練一個非 CoT 證明模型，同時通過基于子目標的遞歸證明合成難題的證明。選擇非 CoT 生成模式是為了加速迭代訓練和數據收集過程。

在此基礎上，第二階段利用了冷啟動鏈式思維（CoT）數據，通過將 DeepSeek-V3 復雜的數學推理模式與合成形式證明相結合而生成。CoT 模式通過進一步的強化學習階段得到增強，遵循了通常用于推理模型的標準訓練流程。

DeepSeek-Prover-V2 的非 CoT 模式訓練過程遵循專家迭代的范式，這是開發形式化定理證明器廣泛采用的框架。在每次訓練迭代中，當前最佳證明策略用于生成那些在先前迭代中未解決的難題的證明嘗試。這些成功的嘗試經由 Lean 證明助手驗證后，被納入 SFT 數據集以訓練改進的模型。這一迭代循環不僅確保模型能夠從初始演示數據集中學習，還能提煉出自己的成功推理軌跡，逐步提高其解決更難問題的能力。總體訓練過程與 DeepSeek-Prover-V1 的訓練過程大致一致，僅對訓練問題的分布進行了兩項修改。

首先，Prover-V2 引入了來自自動形式化和各種開源數據集的額外問題，擴大了訓練問題領域的覆蓋范圍。其次，新模型通過子目標分解生成的問題來擴充數據集，旨在解決 MiniF2F 基準測試有效劃分中的更多挑戰性實例。

研究人員在 DeepSeek-V3-Base-671B 上使用恒定的學習率 5e-6，在 16384 個 token 的上下文中進行監督微調。訓練語料庫由兩個互補來源組成：1）通過專家迭代收集的非 CoT 數據，生成無需中間推理步驟的 Lean 代碼；2）第 2.2 節中描述的冷啟動 CoT 數據，將 DeepSeek-V3 的高級數學推理過程提煉為結構化的證明路徑。非 CoT 組件強調精益定理證明器生態系統中的形式驗證技能，而 CoT 示例明確地建模了將數學直覺轉化為形式證明結構的認知過程。

Prover-V2 采用 GRPO 強化學習算法， 與 PPO 不同，GRPO 通過為每個定理提示采樣一組候選證明并根據它們的相對獎勵優化策略，消除了對單獨批評模型的需求。訓練使用二元獎勵，每個生成的 Lean 證明如果被驗證為正確則獲得 1 個獎勵，否則為 0。為了確保有效學習，研究人員精心挑選訓練提示，僅包括那些對監督微調模型具有足夠挑戰性但可解決的問題。模型在每次迭代中采樣 256 個不同的問題，為每個定理生成 32 個候選證明，最大序列長度為 32768 個 token。

最后是模型的蒸餾。研究人員把 DeepSeek-Prover-V1.5-Base-7B 的最大上下文長度從 4096 個 token 擴展到了 32768 個，并使用 DeepSeek-Prover-V2-671B 強化學習階段收集的 rollout 數據對這個擴展上下文模型進行微調。除了 CoT 推理模式外，研究人員還整合了專家迭代過程中收集的非 CoT 證明數據，以實現一種成本效益高的證明選項，該選項能夠生成簡潔的形式化輸出，并且模型規模較小。此外，7B 模型也采用了與 671B 模型訓練相同的強化學習階段以提升性能。

研究人員對 DeepSeek-Prover-V2 在形式定理證明的各種基準數據集上進行了系統評估，涵蓋了高中競賽題目和本科水平的數學問題。實驗表明，671B 版的模型實現了前所未有的準確率，且與業內其他先進模型相比效率也更高。

在 miniF2F 測試數據集上與最先進模型的比較。

DeepSeek-Prover-V2-671B 在 miniF2F 基準上解決的問題。

ProofNet - 測試和 PutnamBench 的實驗結果。

ProverBench：AIME 與教材題目的形式化基準數據集

這次，DeepSeek 還發布了 ProverBench，這是一個包含 325 道題目的基準數據集。其中，15 道題來自最近兩屆 AIME 數學競賽（AIME 24 和 25）中的數論與代數題目，經過形式化處理，具備真實的高中競賽難度。其余 310 道題則精選自教材示例和教學教程，覆蓋內容多樣，具有良好的教學基礎。

ProverBench 鏈接：https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench

該數據集旨在支持對模型在高中競賽題和本科數學題兩個層面的綜合評估。

ProverBench 數據集的構成情況

網友評價：太強大了

從新模型的受歡迎程度上來看，大家都在期待 DeepSeek 能夠再次改變世界。不少網友對 DeepSeek 新開源的這項工作表示十分欣賞。

還有鉆研數學奧林匹克的學生也發來印象深刻的驚呼（做過題的都知道這里面門道有多深）。

網友親測，效果真的神，把 o4-mini 和 Grok-3 都比下去了。

在社交網絡上有人表示，將復雜問題分解再處理的方式像極了人們教給初級工程師的技巧，DeepSeek-Prover-V2 處理數學問題的思路對于代碼等問題來說應該也是毫無問題。

不過，大家似乎對 DeepSeek-R2 有著更大的熱情！敲敲這頭小藍鯨，R2 到底什么時候發出啊！

更多詳細內容，請查看原鏈接～