夢晨 西風 發(fā)自 凹非寺
量子位 | 公眾號 QbitAI

DeepSeek放大招！新模型專注數(shù)學定理證明，大幅刷新多項高難基準測試。

在普特南測試上，新模型DeepSeek-Prover-V2直接把記錄刷新到49道。

目前的第一名在657道題中只做出10道題，為Kimi與AIME2024冠軍團隊Numina合作成果Kimina-Prover。

而未針對定理證明優(yōu)化的DeepSeek-R1只做出1道。

讓還沒發(fā)布的R2更令人期待了。

除測評結果之外，論文中特別報告了“通過強化學習發(fā)現(xiàn)新技能”現(xiàn)象。

正如R1帶來了“啊哈時刻”，Prover-V2也有令人意想不到的能力。

具體來說，在普特南測試中，參數(shù)量較小的DeepSeek-Prover-V2-7B用非CoT生成模式成功解決了13個671B模型未能解決的問題。

團隊仔細檢查該模型的輸出后發(fā)現(xiàn)，其推理方法存在一個獨特模式：7B模型處理涉及有限基數(shù)的問題時，經(jīng)常使用Cardinal.toNat和Cardinal.natCast_inj，而671B模型生成的輸出中明顯沒有這些內(nèi)容。

要注意，7B模型是在DeepSeek-Prover-V1.5-Base模型基礎上，先使用671B模型在強化學習階段收集的數(shù)據(jù)微調，再執(zhí)行強化學習得來的。

也就是說，7B模型學會了671B模型沒有學會的新技能。

那么，DeepSeeK-Prover-V2如何煉成的呢？與前代相比又有哪些改進？

形式化和非形式化數(shù)學證明統(tǒng)一模型

DeepSeek數(shù)學定理證明DeepSeek-Prover系列模型已推出3款：

• 2024年3月的DeepSeek-Prover（后簡稱為Prover-V1）
• 2024年8月的DeepSeek-Prover-V1.5（后簡稱為Prover-V1.5）
• 2025年5月的DeepSeek-Prover-V2（后簡稱為Prover-V2）

Prover-V1主要探索了通過大規(guī)模合成數(shù)據(jù)集微調DeepSeek-Math-7B，來推進定理證明。

Prover-V1.5在此基礎上增加了證明助手反饋的強化學習（RLPAF）和蒙特卡洛樹搜索方法。

Prover-V2進一步提出“子目標分解的強化學習”，并且基礎模型從DeepSeek-Math-7B升級到DeepSeek-V3。

整合DeepSeek-V3的高上下文窗口和強大的自然語言推理能力，把形式化和非形式化數(shù)學證明統(tǒng)一到一個模型中。

Prover-V2還繼承了Prover-V1.5提出的CoT和非CoT生成兩種模式。

接下來，詳細介紹Prover-V2的各主要環(huán)節(jié)。

通過遞歸證明搜索合成冷啟動推理數(shù)據(jù)

利用DeepSeek-V3作為子目標分解和形式化的統(tǒng)一工具構建冷啟動數(shù)據(jù)集，提示DeepSeek-V3將定理分解為高級證明草圖，同時在Lean 4中將這些證明步驟形式化，從而產(chǎn)生一系列子目標。

使用一個較小的70億參數(shù)模型來處理每個子目標的證明搜索，從而減輕相關的計算負擔。一旦一個具有挑戰(zhàn)性的問題的分解步驟得到解決，就將完整的逐步形式化證明與來自DeepSeek-V3的相應思維鏈進行配對，以創(chuàng)建冷啟動推理數(shù)據(jù)。

使用合成冷啟動數(shù)據(jù)進行子目標分解的強化學習

團隊精心挑選了一組具有挑戰(zhàn)性的問題，這些問題無法由70億參數(shù)量的證明器模型以端到端的方式解決，但所有分解后的子目標都已成功解決。

通過組合所有子目標的證明，為原始問題構建了一個完整的形式化證明。

然后，將此證明附加到DeepSeek-V3的思維鏈中，該思維鏈概述了相應的引理分解，從而實現(xiàn)了非形式化推理與后續(xù)形式化的有機結合。

在合成冷啟動數(shù)據(jù)上對證明器模型進行微調后進行強化學習階段，進一步增強其將非正式推理與形式化證明構建相銜接的能力。遵循推理模型的標準訓練目標，使用二元的正確或錯誤反饋作為獎勵監(jiān)督的主要形式。

具體訓練細節(jié)

兩階段訓練：

DeepSeek-Prover-V2分兩階段建立互補證明生成模式。

第一階段用高效非思維鏈（non-CoT）模式，聚焦快速生成Lean證明代碼，加快迭代和數(shù)據(jù)收集。

第二階段基于第一階段成果，采用高精度思維鏈（CoT）模式，闡述中間推理步驟，用冷啟動思維鏈數(shù)據(jù)強化學習，提升復雜問題推理能力。

專家迭代：

其中非CoT模式訓練遵循專家迭代范式，用最佳證明策略為難題生成證明嘗試，經(jīng)Lean驗證，成功的納入監(jiān)督微調（SFT）數(shù)據(jù)集。與之前版本相比，訓練問題分布有調整，引入了額外問題和子目標分解生成的問題。

監(jiān)督微調：

對DeepSeek-V3-Base-671B做監(jiān)督微調，訓練語料庫包含兩個互補來源的數(shù)據(jù)：

一是通過專家迭代收集的非CoT數(shù)據(jù)，這些數(shù)據(jù)生成的Lean代碼不包含中間推理步驟，主要用于強化模型在 Lean 定理證明生態(tài)系統(tǒng)中的形式驗證技能。

二是冷啟動CoT數(shù)據(jù)，這些數(shù)據(jù)將DeepSeek-V3的先進數(shù)學推理過程提煉為結構化的證明路徑，明確地模擬了將數(shù)學直覺轉化為形式證明結構的認知過程。

強化學習：

采用GRPO算法，與傳統(tǒng)的PPO不同，GRPO無需單獨的裁判模型，它通過為每個定理提示采樣一組候選證明，并根據(jù)它們的相對獎勵來優(yōu)化策略。

訓練過程中使用二元獎勵機制，即生成的Lean證明若被驗證正確則獲得獎勵1，否則為0。

為確保學習效果，精心挑選訓練提示，僅包含那些有足夠挑戰(zhàn)性但又能被監(jiān)督微調后的模型解決的問題。

蒸餾DeepSeek-Prover-V2 7B

將DeepSeek-Prover-V1.5-Base-7B上下文窗口擴展到32768個token，用DeepSeek-Prover-V2-671B數(shù)據(jù)微調，融入非CoT證明數(shù)據(jù)，以便利用小模型生成簡潔的形式化輸出，提供一種經(jīng)濟高效的證明選項。

此外，對DeepSeek-Prover-V2-7B執(zhí)行與671B模型訓練中相同的強化學習階段，以進一步提升其性能。

由此得到的模型Prover-V2 671B在神經(jīng)定理證明方面達到了最先進的性能，在miniF2F測試中的通過率達到 88.9%，并解決了普特南測試中的49道。Prover-V2為miniF2F數(shù)據(jù)集生成的證明可單獨下載。

ProverBench：AIME和教科書問題的形式化

與Prover-V2一起推出ProverBench，這是一個包含325個問題的基準數(shù)據(jù)集。其中，有15個問題是從近期美國數(shù)學邀請賽（AIME 24和25）的數(shù)論與代數(shù)題目中形式化而來，提供了真實的高中競賽水平挑戰(zhàn)。其余310個問題則取自精心挑選的教科書示例和教學教程，構成了一套多樣化且基于教學需求的形式化數(shù)學問題集合。該基準旨在能夠對高中競賽問題和本科階段數(shù)學問題進行更全面的評估。

DeepSeek-Prover-V2系列在三個數(shù)據(jù)集上評測的最后總成績?nèi)缦拢?/p>

DeepSeek全明星陣容

Prover-V2的作者共18人，共同一作Z.Z. Ren, 邵智宏、辛華劍都是參與過V3、R1以及Prover系列前作的主力成員。

作者名單中出現(xiàn)了幾位未參與前兩代版本（Prover-V1、Prover-V1.5）的研究者。

比如Shirong Ma，清華本碩。公開資料顯示，他于去年畢業(yè)后即加入DeepSeek，現(xiàn)為DeepSeek研究員，此前參與了從DeepSeek LLM v1到R1以及DeepSeek-Coder等工作。

還有Zhe Fu、Yuxuan Liu。

雖然他們都沒出現(xiàn)在Prover-V1、Prover-V1.5的作者名單中，但均為DeepSeek資深成員。

在Prover-V1/V1.5同一期發(fā)布的《Fire-Flyer AI-HPC》研究中可見其署名。

該研究提出的Fire-Flyer AI-HPC架構，通過軟硬件協(xié)同設計降低訓練成本，解決傳統(tǒng)超算架構在AI訓練需求上的不足。

不過這次Prover-V2的論文中并未提及在訓練或推理基礎設施具體有哪些優(yōu)化策略。

最后還有一位新面孔Hongxuan Tang，暫未了解到具體信息。

Prover-V2發(fā)布后迅速引發(fā)社區(qū)關注，GitHub倉庫12小時內(nèi)即獲得350+星標。

在X（原Twitter）、抱抱臉等平臺，網(wǎng)友們展開熱烈討論。

Prover-V2核心貢獻者邵智宏在個人賬號主動推介研究成果。

X工程師@kache特別贊賞道：

感謝你們對開放科學研究的奉獻。

普林斯頓大學助理教授Chi Jin表示：

恭喜這項驚人的工作！在miniF2F上攻克最后10%-20%的問題標志著能力上的重大飛躍。當前形式化數(shù)學領域的競爭態(tài)勢堪稱激烈，難以置信Kimina僅保持了兩周SOTA就被DeepSeek超越。

就連Kimina-Prover核心貢獻者@Marco Dos Santos都來送上了祝賀：

祝賀DeepSeek AI團隊將miniF2F任務的SOTA提升到了89%！
很高興看到長思維鏈方法正在被其他團隊獨立探索且呈現(xiàn)出一些有趣的差異。形式數(shù)學如今比以往任何時候都更受歡迎！

另外，網(wǎng)友們最關注的問題仍然是：R2什么時候發(fā)布啊～

論文：
https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/DeepSeek_Prover_V2.pdf
模型：
https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B

DeepSeek-Prover
https://arxiv.org/abs/2405.14333
DeepSeek-Prover-V1.5
https://arxiv.org/abs/2408.08152