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

論文中特別提到“通過(guò)強(qiáng)化學(xué)習(xí)發(fā)現(xiàn)新技能”的現(xiàn)象,。例如,，在普特南測(cè)試中，參數(shù)量較小的DeepSeek-Prover-V2-7B用非CoT生成模式成功解決了13個(gè)671B模型未能解決的問(wèn)題,。團(tuán)隊(duì)檢查后發(fā)現(xiàn),，7B模型處理涉及有限基數(shù)的問(wèn)題時(shí)，經(jīng)常使用Cardinal.toNat和Cardinal.natCast_inj,，而671B模型沒(méi)有這些內(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ò)大規(guī)模合成數(shù)據(jù)集微調(diào)DeepSeek-Math-7B來(lái)推進(jìn)定理證明。Prover-V1.5增加了證明助手反饋的強(qiáng)化學(xué)習(xí)（RLPAF）和蒙特卡洛樹(shù)搜索方法,。Prover-V2進(jìn)一步提出“子目標(biāo)分解的強(qiáng)化學(xué)習(xí)”,，基礎(chǔ)模型從DeepSeek-Math-7B升級(jí)到DeepSeek-V3，整合了高上下文窗口和強(qiáng)大的自然語(yǔ)言推理能力,，統(tǒng)一了形式化和非形式化數(shù)學(xué)證明,。

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

Prover-V2分兩階段建立互補(bǔ)證明生成模式。第一階段采用高效非思維鏈模式,，快速生成Lean證明代碼,；第二階段基于第一階段成果，采用高精度思維鏈模式,，闡述中間推理步驟,，提升復(fù)雜問(wèn)題推理能力。非CoT模式訓(xùn)練遵循專(zhuān)家迭代范式,，用最佳證明策略為難題生成證明嘗試,，經(jīng)Lean驗(yàn)證成功的納入監(jiān)督微調(diào)數(shù)據(jù)集。監(jiān)督微調(diào)包括通過(guò)專(zhuān)家迭代收集的非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è)試中的通過(guò)率達(dá)到88.9%,，并解決了普特南測(cè)試中的49道題。ProverBench是一個(gè)包含325個(gè)問(wèn)題的基準(zhǔn)數(shù)據(jù)集,，其中15個(gè)問(wèn)題來(lái)自AIME競(jìng)賽,，其余310個(gè)問(wèn)題取自教科書(shū)示例和教學(xué)教程。

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