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

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

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增加了證明助手反饋的強化學(xué)習(xí)（RLPAF）和蒙特卡洛樹搜索方法。Prover-V2進(jìn)一步提出“子目標(biāo)分解的強化學(xué)習(xí)”，基礎(chǔ)模型從DeepSeek-Math-7B升級到DeepSeek-V3，整合了高上下文窗口和強大的自然語言推理能力，統(tǒng)一了形式化和非形式化數(shù)學(xué)證明。

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

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

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

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