DeepSeek推出了新模型DeepSeek-Prover-V2,，專注于數(shù)學(xué)定理證明,，并在多項(xiàng)高難度基準(zhǔn)測(cè)試中刷新了記錄。在普特南測(cè)試上,，Prover-V2解決了49道題,，遠(yuǎn)超當(dāng)前第一名的10道和未針對(duì)定理證明優(yōu)化的DeepSeek-R1的1道,。

論文中特別提到“通過強(qiáng)化學(xué)習(xí)發(fā)現(xiàn)新技能”的現(xiàn)象。例如，在普特南測(cè)試中,，參數(shù)量較小的DeepSeek-Prover-V2-7B用非CoT生成模式成功解決了13個(gè)671B模型未能解決的問題,。團(tuán)隊(duì)檢查后發(fā)現(xiàn)，7B模型處理涉及有限基數(shù)的問題時(shí),，經(jīng)常使用Cardinal.toNat和Cardinal.natCast_inj,，而671B模型沒有這些內(nèi)容。這表明7B模型學(xué)會(huì)了671B模型未學(xué)會(huì)的新技能,。

DeepSeek-Prover系列模型已推出三款：2024年3月的DeepSeek-Prover,、2024年8月的DeepSeek-Prover-V1.5以及2025年5月的DeepSeek-Prover-V2。Prover-V1主要通過大規(guī)模合成數(shù)據(jù)集微調(diào)DeepSeek-Math-7B來推進(jìn)定理證明,。Prover-V1.5增加了證明助手反饋的強(qiáng)化學(xué)習(xí)（RLPAF）和蒙特卡洛樹搜索方法,。Prover-V2進(jìn)一步提出“子目標(biāo)分解的強(qiáng)化學(xué)習(xí)”，基礎(chǔ)模型從DeepSeek-Math-7B升級(jí)到DeepSeek-V3,，整合了高上下文窗口和強(qiáng)大的自然語言推理能力,，統(tǒng)一了形式化和非形式化數(shù)學(xué)證明。

Prover-V2還繼承了Prover-V1.5提出的CoT和非CoT生成兩種模式,。通過遞歸證明搜索合成冷啟動(dòng)推理數(shù)據(jù),，利用DeepSeek-V3將定理分解為高級(jí)證明草圖并在Lean 4中形式化，從而產(chǎn)生一系列子目標(biāo),。使用70億參數(shù)模型處理每個(gè)子目標(biāo),，減輕計(jì)算負(fù)擔(dān)。一旦具有挑戰(zhàn)性的問題的分解步驟得到解決,，就將完整的逐步形式化證明與來自DeepSeek-V3的相應(yīng)思維鏈配對(duì),，創(chuàng)建冷啟動(dòng)推理數(shù)據(jù)。

Prover-V2分兩階段建立互補(bǔ)證明生成模式,。第一階段采用高效非思維鏈模式,，快速生成Lean證明代碼；第二階段基于第一階段成果,，采用高精度思維鏈模式,，闡述中間推理步驟，提升復(fù)雜問題推理能力,。非CoT模式訓(xùn)練遵循專家迭代范式,，用最佳證明策略為難題生成證明嘗試，經(jīng)Lean驗(yàn)證成功的納入監(jiān)督微調(diào)數(shù)據(jù)集,。監(jiān)督微調(diào)包括通過專家迭代收集的非CoT數(shù)據(jù)和冷啟動(dòng)CoT數(shù)據(jù),。強(qiáng)化學(xué)習(xí)階段采用GRPO算法，根據(jù)二元獎(jiǎng)勵(lì)機(jī)制優(yōu)化策略,。

此外,，DeepSeek-Prover-V2-7B擴(kuò)展了上下文窗口并用Prover-V2-671B數(shù)據(jù)微調(diào),，融入非CoT證明數(shù)據(jù)，提供經(jīng)濟(jì)高效的證明選項(xiàng),。Prover-V2-671B在miniF2F測(cè)試中的通過率達(dá)到88.9%,，并解決了普特南測(cè)試中的49道題。ProverBench是一個(gè)包含325個(gè)問題的基準(zhǔn)數(shù)據(jù)集,，其中15個(gè)問題來自AIME競(jìng)賽,，其余310個(gè)問題取自教科書示例和教學(xué)教程。

Prover-V2發(fā)布后迅速引發(fā)社區(qū)關(guān)注,，GitHub倉庫短時(shí)間內(nèi)獲得大量星標(biāo),。研究者們?cè)赬、抱抱臉等平臺(tái)展開熱烈討論,，稱贊這項(xiàng)工作標(biāo)志著能力上的重大飛躍,。網(wǎng)友們最關(guān)心的問題是R2何時(shí)發(fā)布。