機(jī)器之心報(bào)道
編輯：大盤(pán)雞、澤南
DeepSeek R2 的前奏？
五一勞動(dòng)節(jié)到了，DeepSeek 的新消息可沒(méi)停下來(lái)。
前些天到處都在流傳著 DeepSeek-R2 即將發(fā)布的傳言，DeepSeek 確實(shí)有新動(dòng)作，不過(guò)大家沒(méi)等來(lái) R2，等來(lái)的是 DeepSeek-Prover-V2，它當(dāng)然也是開(kāi)源的。
Prover-V2 在定理證明賽道上實(shí)現(xiàn)了業(yè)內(nèi)最佳性能，在 MiniF2F 測(cè)試中達(dá)到了 88.9% 的通過(guò)率，在 AIME 24、25 上也有不錯(cuò)的分?jǐn)?shù)。
在 4 月 30 日晚，機(jī)器學(xué)習(xí)協(xié)作平臺(tái) HuggingFace 上就更新了 DeepSeek-Prover-V2 的一些技術(shù)細(xì)節(jié)。
這次 DeepSeek 團(tuán)隊(duì)發(fā)布了兩個(gè)版本的 DeepSeek-Prover-V2 模型，參數(shù)規(guī)模分別為 7B 和 671B。
其中，DeepSeek-Prover-V2-671B 是在 DeepSeek-V3-Base 基礎(chǔ)上訓(xùn)練而成，而 DeepSeek-Prover-V2-7B 則基于 DeepSeek-Prover-V1.5-Base 構(gòu)建，并支持最長(zhǎng) 32K tokens 的上下文長(zhǎng)度擴(kuò)展。
- DeepSeek-Prover-V2-7B 鏈接：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B
- DeepSeek-Prover-V2-671B 鏈接：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
要一句話總結(jié) DeepSeek-Prover-V2 到底是什么？它是一款專(zhuān)為「數(shù)學(xué) AI 編程語(yǔ)言」Lean 4 打造的開(kāi)源大語(yǔ)言模型，專(zhuān)注于形式化定理證明。
它的初始化數(shù)據(jù)通過(guò)一個(gè)由 DeepSeek-V3 驅(qū)動(dòng)的遞歸定理證明流程收集而來(lái)。在冷啟動(dòng)訓(xùn)練階段，首先通過(guò)提示 DeepSeek-V3 將復(fù)雜問(wèn)題分解成一系列可以解決的子目標(biāo)。每解決一個(gè)子目標(biāo)就會(huì)將這些證明整合成「思維鏈」。 并融合 DeepSeek-V3 的逐步推理軌跡，共同構(gòu)建出用于強(qiáng)化學(xué)習(xí)的初始訓(xùn)練數(shù)據(jù)。
這一策略的精妙之處在于：它能夠?qū)⒎切问交托问交臄?shù)學(xué)推理融合到一個(gè)統(tǒng)一的模型中，讓模型既能像人一樣靈活思考，也能像機(jī)器一樣嚴(yán)謹(jǐn)論證，真正實(shí)現(xiàn)了數(shù)學(xué)推理的一體化融合。
具體是如何實(shí)現(xiàn)的呢？DeepSeek 也發(fā)布了 DeepSeek-Prover-V2 的技術(shù)報(bào)告，讓我們看看其中是怎么說(shuō)的：
技術(shù)概述
通過(guò)遞歸式證明搜索生成冷啟動(dòng)推理數(shù)據(jù)
為了構(gòu)建冷啟動(dòng)數(shù)據(jù)集，DeepSeek 團(tuán)隊(duì)設(shè)計(jì)了一條簡(jiǎn)潔高效的遞歸定理證明流程，使用 DeepSeek-V3 作為統(tǒng)一工具，既負(fù)責(zé)子目標(biāo)的拆解，也負(fù)責(zé)推理步驟的形式化表達(dá)。其中具體的過(guò)程則是通過(guò)提示引導(dǎo) DeepSeek-V3 將定理拆解為高層次的證明草圖，并在此過(guò)程中同時(shí)將這些推理步驟用 Lean 4 語(yǔ)言形式化，最終生成一系列結(jié)構(gòu)清晰、邏輯嚴(yán)密的子目標(biāo)。
DeepSeek-Prover-V2 使用冷啟動(dòng)數(shù)據(jù)收集過(guò)程概覽。
降低計(jì)算開(kāi)銷(xiāo)一直是 DeepSeek 團(tuán)隊(duì)的強(qiáng)項(xiàng)，這次也不例外。他們使用一個(gè)更小的 7B 模型來(lái)完成每個(gè)子目標(biāo)的證明搜索，從而降低計(jì)算負(fù)擔(dān)。當(dāng)復(fù)雜問(wèn)題被拆解的各個(gè)步驟都成功解決后，他們將完整的形式化逐步證明與 DeepSeek-V3 生成的思維鏈相對(duì)應(yīng)，組合成冷啟動(dòng)推理數(shù)據(jù)。
何將分解的子目標(biāo)轉(zhuǎn)化為一系列引理陳述的一個(gè)示例。
基于合成冷啟動(dòng)數(shù)據(jù)的強(qiáng)化學(xué)習(xí)
DeepSeek 團(tuán)隊(duì)挑選了一部分具有挑戰(zhàn)性的定理問(wèn)題。7B 證明模型沒(méi)法雖然沒(méi)法兒將它們端到端的解決，但是能夠拿捏拆解出來(lái)的一系列子目標(biāo)。
整合所有子目標(biāo)的證明就可以構(gòu)建出原始問(wèn)題的完整形式化證明。隨后，將該正式證明附加到 DeepSeek-V3 所生成的思維鏈，這條思維鏈展示了對(duì)應(yīng)的引理拆解過(guò)程，從而形成了一份將非形式化推理與后續(xù)形式化過(guò)程緊密融合的訓(xùn)練數(shù)據(jù)。
在對(duì)證明模型進(jìn)行合成冷啟動(dòng)數(shù)據(jù)的微調(diào)后，研究團(tuán)隊(duì)進(jìn)一步引入強(qiáng)化學(xué)習(xí)階段，進(jìn)一步提升模型將非形式化推理轉(zhuǎn)化為形式化證明的能力。在訓(xùn)練過(guò)程中，遵循推理模型的通用目標(biāo)，采用「對(duì) / 錯(cuò)」二值反饋?zhàn)鳛橹饕莫?jiǎng)勵(lì)信號(hào)。
最終得到的模型 DeepSeek-Prover-V2-671B 在神經(jīng)定理證明任務(wù)中達(dá)到了當(dāng)前最先進(jìn)的性能，在 MiniF2F-test 上的通過(guò)率達(dá)到 88.9%，并成功解決了 PutnamBench 數(shù)據(jù)集中 658 道題中的 49 道。DeepSeek-Prover-V2 在 miniF2F 數(shù)據(jù)集上生成的所有證明已整理為 ZIP 文件，開(kāi)放下載。
下載鏈接：https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/minif2f-solutions.zip
訓(xùn)練細(xì)節(jié)、實(shí)驗(yàn)結(jié)果
DeepSeek-Prover-V2 經(jīng)歷了兩階段訓(xùn)練，這一過(guò)程建立了兩種互補(bǔ)的證明生成模式：
1. 高效非思維鏈（non-CoT）模式：此模式針對(duì)快速生成正式的 Lean 證明代碼進(jìn)行優(yōu)化，專(zhuān)注于生成簡(jiǎn)潔的證明，沒(méi)有顯式的中間推理步驟。
2. 高精度思維鏈（CoT）模式：此模式系統(tǒng)地闡述中間推理步驟，強(qiáng)調(diào)透明度和邏輯進(jìn)展，然后構(gòu)建最終的正式證明。
與 DeepSeek-Prover-V1.5 一致，這兩種生成模式由兩個(gè)不同的引導(dǎo)提示控制。在第一階段采用專(zhuān)家迭代，在課程學(xué)習(xí)框架內(nèi)訓(xùn)練一個(gè)非 CoT 證明模型，同時(shí)通過(guò)基于子目標(biāo)的遞歸證明合成難題的證明。選擇非 CoT 生成模式是為了加速迭代訓(xùn)練和數(shù)據(jù)收集過(guò)程。
在此基礎(chǔ)上，第二階段利用了冷啟動(dòng)鏈?zhǔn)剿季S（CoT）數(shù)據(jù)，通過(guò)將 DeepSeek-V3 復(fù)雜的數(shù)學(xué)推理模式與合成形式證明相結(jié)合而生成。CoT 模式通過(guò)進(jìn)一步的強(qiáng)化學(xué)習(xí)階段得到增強(qiáng)，遵循了通常用于推理模型的標(biāo)準(zhǔn)訓(xùn)練流程。
DeepSeek-Prover-V2 的非 CoT 模式訓(xùn)練過(guò)程遵循專(zhuān)家迭代的范式，這是開(kāi)發(fā)形式化定理證明器廣泛采用的框架。在每次訓(xùn)練迭代中，當(dāng)前最佳證明策略用于生成那些在先前迭代中未解決的難題的證明嘗試。這些成功的嘗試經(jīng)由 Lean 證明助手驗(yàn)證后，被納入 SFT 數(shù)據(jù)集以訓(xùn)練改進(jìn)的模型。這一迭代循環(huán)不僅確保模型能夠從初始演示數(shù)據(jù)集中學(xué)習(xí)，還能提煉出自己的成功推理軌跡，逐步提高其解決更難問(wèn)題的能力。總體訓(xùn)練過(guò)程與 DeepSeek-Prover-V1 的訓(xùn)練過(guò)程大致一致，僅對(duì)訓(xùn)練問(wèn)題的分布進(jìn)行了兩項(xiàng)修改。
首先，Prover-V2 引入了來(lái)自自動(dòng)形式化和各種開(kāi)源數(shù)據(jù)集的額外問(wèn)題，擴(kuò)大了訓(xùn)練問(wèn)題領(lǐng)域的覆蓋范圍。其次，新模型通過(guò)子目標(biāo)分解生成的問(wèn)題來(lái)擴(kuò)充數(shù)據(jù)集，旨在解決 MiniF2F 基準(zhǔn)測(cè)試有效劃分中的更多挑戰(zhàn)性實(shí)例。
研究人員在 DeepSeek-V3-Base-671B 上使用恒定的學(xué)習(xí)率 5e-6，在 16384 個(gè) token 的上下文中進(jìn)行監(jiān)督微調(diào)。訓(xùn)練語(yǔ)料庫(kù)由兩個(gè)互補(bǔ)來(lái)源組成：1）通過(guò)專(zhuān)家迭代收集的非 CoT 數(shù)據(jù)，生成無(wú)需中間推理步驟的 Lean 代碼；2）第 2.2 節(jié)中描述的冷啟動(dòng) CoT 數(shù)據(jù)，將 DeepSeek-V3 的高級(jí)數(shù)學(xué)推理過(guò)程提煉為結(jié)構(gòu)化的證明路徑。非 CoT 組件強(qiáng)調(diào)精益定理證明器生態(tài)系統(tǒng)中的形式驗(yàn)證技能，而 CoT 示例明確地建模了將數(shù)學(xué)直覺(jué)轉(zhuǎn)化為形式證明結(jié)構(gòu)的認(rèn)知過(guò)程。
Prover-V2 采用 GRPO 強(qiáng)化學(xué)習(xí)算法， 與 PPO 不同，GRPO 通過(guò)為每個(gè)定理提示采樣一組候選證明并根據(jù)它們的相對(duì)獎(jiǎng)勵(lì)優(yōu)化策略，消除了對(duì)單獨(dú)批評(píng)模型的需求。訓(xùn)練使用二元獎(jiǎng)勵(lì)，每個(gè)生成的 Lean 證明如果被驗(yàn)證為正確則獲得 1 個(gè)獎(jiǎng)勵(lì)，否則為 0。為了確保有效學(xué)習(xí)，研究人員精心挑選訓(xùn)練提示，僅包括那些對(duì)監(jiān)督微調(diào)模型具有足夠挑戰(zhàn)性但可解決的問(wèn)題。模型在每次迭代中采樣 256 個(gè)不同的問(wèn)題，為每個(gè)定理生成 32 個(gè)候選證明，最大序列長(zhǎng)度為 32768 個(gè) token。
最后是模型的蒸餾。研究人員把 DeepSeek-Prover-V1.5-Base-7B 的最大上下文長(zhǎng)度從 4096 個(gè) token 擴(kuò)展到了 32768 個(gè)，并使用 DeepSeek-Prover-V2-671B 強(qiáng)化學(xué)習(xí)階段收集的 rollout 數(shù)據(jù)對(duì)這個(gè)擴(kuò)展上下文模型進(jìn)行微調(diào)。除了 CoT 推理模式外，研究人員還整合了專(zhuān)家迭代過(guò)程中收集的非 CoT 證明數(shù)據(jù)，以實(shí)現(xiàn)一種成本效益高的證明選項(xiàng)，該選項(xiàng)能夠生成簡(jiǎn)潔的形式化輸出，并且模型規(guī)模較小。此外，7B 模型也采用了與 671B 模型訓(xùn)練相同的強(qiáng)化學(xué)習(xí)階段以提升性能。
研究人員對(duì) DeepSeek-Prover-V2 在形式定理證明的各種基準(zhǔn)數(shù)據(jù)集上進(jìn)行了系統(tǒng)評(píng)估，涵蓋了高中競(jìng)賽題目和本科水平的數(shù)學(xué)問(wèn)題。實(shí)驗(yàn)表明，671B 版的模型實(shí)現(xiàn)了前所未有的準(zhǔn)確率，且與業(yè)內(nèi)其他先進(jìn)模型相比效率也更高。
在 miniF2F 測(cè)試數(shù)據(jù)集上與最先進(jìn)模型的比較。
DeepSeek-Prover-V2-671B 在 miniF2F 基準(zhǔn)上解決的問(wèn)題。
ProofNet - 測(cè)試和 PutnamBench 的實(shí)驗(yàn)結(jié)果。
ProverBench：AIME 與教材題目的形式化基準(zhǔn)數(shù)據(jù)集
這次，DeepSeek 還發(fā)布了 ProverBench，這是一個(gè)包含 325 道題目的基準(zhǔn)數(shù)據(jù)集。其中，15 道題來(lái)自最近兩屆 AIME 數(shù)學(xué)競(jìng)賽（AIME 24 和 25）中的數(shù)論與代數(shù)題目，經(jīng)過(guò)形式化處理，具備真實(shí)的高中競(jìng)賽難度。其余 310 道題則精選自教材示例和教學(xué)教程，覆蓋內(nèi)容多樣，具有良好的教學(xué)基礎(chǔ)。
ProverBench 鏈接：https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench
該數(shù)據(jù)集旨在支持對(duì)模型在高中競(jìng)賽題和本科數(shù)學(xué)題兩個(gè)層面的綜合評(píng)估。
ProverBench 數(shù)據(jù)集的構(gòu)成情況
網(wǎng)友評(píng)價(jià)：太強(qiáng)大了
從新模型的受歡迎程度上來(lái)看，大家都在期待 DeepSeek 能夠再次改變世界。不少網(wǎng)友對(duì) DeepSeek 新開(kāi)源的這項(xiàng)工作表示十分欣賞。
還有鉆研數(shù)學(xué)奧林匹克的學(xué)生也發(fā)來(lái)印象深刻的驚呼（做過(guò)題的都知道這里面門(mén)道有多深）。
網(wǎng)友親測(cè)，效果真的神，把 o4-mini 和 Grok-3 都比下去了。
在社交網(wǎng)絡(luò)上有人表示，將復(fù)雜問(wèn)題分解再處理的方式像極了人們教給初級(jí)工程師的技巧，DeepSeek-Prover-V2 處理數(shù)學(xué)問(wèn)題的思路對(duì)于代碼等問(wèn)題來(lái)說(shuō)應(yīng)該也是毫無(wú)問(wèn)題。
不過(guò)，大家似乎對(duì) DeepSeek-R2 有著更大的熱情！敲敲這頭小藍(lán)鯨，R2 到底什么時(shí)候發(fā)出??！
更多詳細(xì)內(nèi)容，請(qǐng)查看原鏈接～
熱門(mén)跟貼