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

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

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

行業(yè)評價認(rèn)為，Prover-V2 的發(fā)布標(biāo)志著 AI 從解題工具向探索伙伴轉(zhuǎn)型，其 “神經(jīng)符號結(jié)合” 架構(gòu)為通用人工智能（AGI）發(fā)展提供關(guān)鍵支撐。技術(shù)報告詳細(xì)披露訓(xùn)練流程與性能數(shù)據(jù)，被 MLCommons 列為基準(zhǔn)測試參考模型。下一代旗艦?zāi)Ｐ?R2 計劃擴展至 1.2 萬億參數(shù)，支持 “文本 + 視覺” 跨模態(tài)推理，目標(biāo)覆蓋科研輔助、金融建模等場景。