前些天到處都在流傳著 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 鏈接：DeepSeek-Prover-V2-7B
- DeepSeek-Prover-V2-671B 鏈接：DeepSeek-Prover-V2-671B
要一句話總結 DeepSeek-Prover-V2 到底是什麼？它是一款專為「數學 AI 編程語言」Lean 4 打造的開源大語言模型，專注於形式化定理證明。
它的初始化數據通過一個由 DeepSeek-V3 驅動的遞歸定理證明流程收集而來。在冷啟動訓練階段，首先通過提示 DeepSeek-V3 將複雜問題分解成一系列可以解決的子目標。每解決一個子目標就會將這些證明整合成「思維鏈」。並融合 DeepSeek-V3 的逐步推理軌跡，共同構建出用於強化學習的初始訓練數據。
這一策略的精妙之處在於：它能夠將非形式化和形式化的數學推理融合到一個統一的模型中，讓模型既能像人一樣靈活思考，也能像機器一樣嚴謹論證，真正實現了數學推理的一體化融合。
技術概述#
通過遞歸式證明搜索生成冷啟動推理數據#
為了構建冷啟動數據集，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 文件，開放下載。
- 下載鏈接：miniF2F 解決方案