5 月 1 日消息，深度求索（DeepSeek）昨日（4 月 30 日）在 AI 開源社區 Hugging Face 上，發布名為 DeepSeek-Prover-V2-671B 的新模型，隨后在 GitHub 等平臺上公布了論文信息。

援引論文介紹，DeepSeek-Prover-V2 是一款專注于形式化數學推理的開源大型語言模型，基于 DeepSeek-V3-0324，通過遞歸定理證明管道生成初始數據。

Deepseek 推出了 DeepSeek-Prover-V2-671B（結合 V3 基礎大模型）、DeepSeek-Prover-V2-7B（增強模型）兩個模型，以及DeepSeek-ProverBench 數據集。

DeepSeek-Prover-V2-671B 采用和 DeepSeek V3-0324 相同的架構，并非用于常規對話或者推理，而是用于形式化定理證明、專門增強數學能力的模型。

DeepSeek 團隊首先引導 DeepSeek-V3 模型將復雜定理分解為一系列子目標（subgoals），整合非形式與形式化數學推理，在 Lean 4 平臺上形式化證明步驟。

接著，利用一個較小的 7B 參數模型處理子目標的證明搜索，減輕計算負擔。最終，結合完整的逐步證明與 DeepSeek-V3 的思維鏈（chain-of-thought），形成強化學習的“冷啟動”數據。

在訓練中，團隊篩選出一批 7B 模型無法直接解決但子目標已被證明的難題。通過整合子目標證明，形成完整的形式化證明，并與 DeepSeek-V3 的推理過程對接，生成合成數據。

隨后，模型微調這些數據，并通過強化學習進一步提升能力，以二元反饋（正確或錯誤）作為獎勵機制。最終，DeepSeek-Prover-V2-671B 在神經定理證明領域創下新高，在 MiniF2F-test 數據集上通過率達 88.9%，在 PutnamBench 數據集中解決 658 個問題中的 49 個。

團隊還發布了 ProverBench 基準數據集，包含 325 個形式化數學問題。其中，15 個問題源自近期 AIME 競賽（AIME 24 和 25），涉及數論與代數，代表高中競賽難度。

其余 310 個問題則來自精選教材和教學內容，涵蓋線性代數、微積分、概率等多個領域。這一數據集旨在為高中競賽和本科數學提供全面評估標準，推動模型在多樣化場景下的測試與應用。