DeepSeek新數(shù)學(xué)模型刷爆記錄！7B小模型自主發(fā)現(xiàn)671B模型不會(huì)的新技能

夢(mèng)晨 西風(fēng) 發(fā)自 凹非寺
量子位 | 公眾號(hào) QbitAI

DeepSeek放大招！新模型專注數(shù)學(xué)定理證明，大幅刷新多項(xiàng)高難基準(zhǔn)測(cè)試。

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

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

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

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

除測(cè)評(píng)結(jié)果之外，論文中特別報(bào)告了“通過強(qiáng)化學(xué)習(xí)發(fā)現(xiàn)新技能”現(xiàn)象。

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

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

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

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

也就是說，7B模型學(xué)會(huì)了671B模型沒有學(xué)會(huì)的新技能。

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

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

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

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

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

Prover-V1.5在此基礎(chǔ)上增加了證明助手反饋的強(qiáng)化學(xué)習(xí)（RLPAF）和蒙特卡洛樹搜索方法。

Prover-V2進(jìn)一步提出“子目標(biāo)分解的強(qiáng)化學(xué)習(xí)”，并且基礎(chǔ)模型從DeepSeek-Math-7B升級(jí)到DeepSeek-V3。

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

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

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

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

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

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

使用合成冷啟動(dòng)數(shù)據(jù)進(jìn)行子目標(biāo)分解的強(qiáng)化學(xué)習(xí)

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

通過組合所有子目標(biāo)的證明，為原始問題構(gòu)建了一個(gè)完整的形式化證明。

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

在合成冷啟動(dòng)數(shù)據(jù)上對(duì)證明器模型進(jìn)行微調(diào)后進(jìn)行強(qiáng)化學(xué)習(xí)階段，進(jìn)一步增強(qiáng)其將非正式推理與形式化證明構(gòu)建相銜接的能力。遵循推理模型的標(biāo)準(zhǔn)訓(xùn)練目標(biāo)，使用二元的正確或錯(cuò)誤反饋?zhàn)鳛楠?jiǎng)勵(lì)監(jiān)督的主要形式。

具體訓(xùn)練細(xì)節(jié)

兩階段訓(xùn)練：

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

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

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

專家迭代：

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

監(jiān)督微調(diào)：

對(duì)DeepSeek-V3-Base-671B做監(jiān)督微調(diào)，訓(xùn)練語料庫(kù)包含兩個(gè)互補(bǔ)來源的數(shù)據(jù)：

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

二是冷啟動(dòng)CoT數(shù)據(jù)，這些數(shù)據(jù)將DeepSeek-V3的先進(jìn)數(shù)學(xué)推理過程提煉為結(jié)構(gòu)化的證明路徑，明確地模擬了將數(shù)學(xué)直覺轉(zhuǎn)化為形式證明結(jié)構(gòu)的認(rèn)知過程。

強(qiáng)化學(xué)習(xí)：

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

訓(xùn)練過程中使用二元獎(jiǎng)勵(lì)機(jī)制，即生成的Lean證明若被驗(yàn)證正確則獲得獎(jiǎng)勵(lì)1，否則為0。

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

蒸餾DeepSeek-Prover-V2 7B

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

此外，對(duì)DeepSeek-Prover-V2-7B執(zhí)行與671B模型訓(xùn)練中相同的強(qiáng)化學(xué)習(xí)階段，以進(jìn)一步提升其性能。

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

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

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

DeepSeek-Prover-V2系列在三個(gè)數(shù)據(jù)集上評(píng)測(cè)的最后總成績(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架構(gòu)，通過軟硬件協(xié)同設(shè)計(jì)降低訓(xùn)練成本，解決傳統(tǒng)超算架構(gòu)在AI訓(xùn)練需求上的不足。

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

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

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

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

Prover-V2核心貢獻(xiàn)者邵智宏在個(gè)人賬號(hào)主動(dòng)推介研究成果。

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

感謝你們對(duì)開放科學(xué)研究的奉獻(xiàn)。

普林斯頓大學(xué)助理教授Chi Jin表示：

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

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

祝賀DeepSeek AI團(tuán)隊(duì)將miniF2F任務(wù)的SOTA提升到了89%！

很高興看到長(zhǎng)思維鏈方法正在被其他團(tuán)隊(duì)獨(dú)立探索且呈現(xiàn)出一些有趣的差異。形式數(shù)學(xué)如今比以往任何時(shí)候都更受歡迎！

另外，網(wǎng)友們最關(guān)注的問題仍然是：R2什么時(shí)候發(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