4 月 30 日發布 DeepSeek-Prover-V2 模型，再次推動熱度

深度求索（DeepSeek）于 2025 年 4 月 30 日發布的新一代數學推理大模型 DeepSeek-Prover-V2，在數學定理證明領域實現了技術范式的突破。該模型基于 DeepSeek-V3 架構，通過遞歸子目標分解與強化學習的結合，將復雜數學問題拆解為可驗證的子目標鏈，并生成對應的 Lean 4 形式化代碼框架，實現了自然語言推理與形式化證明的深度融合。其核心技術突破包括采用遞歸子目標分解架構，將費馬大定理等復雜定理分解為橢圓曲線模性定理等子目標，由 7B 輕量模型遞歸解決后拼接成完整證明；雙模式推理機制則通過快速模式（non-CoT）直接生成精煉的 Lean 4 代碼，30 秒內解決 AIME 競賽題，邏輯模式（CoT）則逐步闡述推理過程，確保邏輯透明。模型采用 GRPO 強化學習算法，從 32 種候選方案中自主選擇最優解，訓練數據通過 “失敗回撤 - 路徑重組” 機制自動生成，擺脫對人工標注的依賴。

在性能表現上，Prover-V2 的 671B 版本在 MiniF2F-test 中通過率達 88.9%，較前代提升 47%，解決 PutnamBench 數據集 658 題中的 49 道，遠超競品的 23 題。7B 版本在 PutnamBench 中解決 13 個 671B 模型未解決的問題，支持本地設備運行，推理速度達 60 tokens / 秒，且通過 FP8 量化技術節省 35% 顯存。跨領域泛化能力方面，模型在 ProofNet（本科數學問題）和 CombiBench（組合數學）測試中表現優異，尤其在有限基數問題中使用特定數學工具 Cardinal.toNat 等，展現差異化推理能力。

應用場景上，Prover-V2 已在教育、科研、工業等領域落地。新東方、猿輔導等機構利用其 7B 版本實時解析 3.2 萬字符的數學證明，輔助智能教輔系統；MIT 團隊用其輔助完成代數幾何領域頂刊論文，驗證猜想并生成形式化證明。工業領域中，華為將其應用于 5G 協議棧的自動化審計，解決形式化驗證中的 “組合爆炸” 難題；Fermat-1 量化平臺基于 Prover-V2 的算法實現年化 36% 的超額收益。模型已在 Hugging Face 開源，提供 7B 和 671B 版本，并配套發布 ProverBench 測試集，吸引超 10 萬開發者參與，形成 “模型 - 工具 - 社區” 閉環。

行業評價認為，Prover-V2 的發布標志著 AI 從解題工具向探索伙伴轉型，其 “神經符號結合” 架構為通用人工智能（AGI）發展提供關鍵支撐。技術報告詳細披露訓練流程與性能數據，被 MLCommons 列為基準測試參考模型。下一代旗艦模型 R2 計劃擴展至 1.2 萬億參數，支持 “文本 + 視覺” 跨模態推理，目標覆蓋科研輔助、金融建模等場景。