繼昨日放出新開源模型 Prover V2 之后，DeepSeek 在今天又公布了它的技術(shù)報(bào)告。
這份報(bào)告長(zhǎng)達(dá) 34 頁(yè)，披露了更多該模型的重要技術(shù)細(xì)節(jié)和基準(zhǔn)測(cè)試表現(xiàn)，讓我們有機(jī)會(huì)進(jìn)一步了解它的創(chuàng)新之處。
DeepSeek Prover V2 系列模型有兩個(gè)尺寸：7B 和 671B 參數(shù)。
DeepSeek-Prover-V2-671B 在 DeepSeek-V3-Base 基礎(chǔ)上進(jìn)行訓(xùn)練，推理性能更強(qiáng)。
DeepSeek-Prover-V2-7B 則基于 DeepSeek-Prover-V1.5-Base 構(gòu)建，上下文長(zhǎng)度得到了擴(kuò)展，最高可達(dá) 32K token。
其中，DeepSeek-Prover-V2-671B 在神經(jīng)定理證明（neural theorem proving）領(lǐng)域超越了之前的模型：MiniF2F 測(cè)試集在 Pass@32 下達(dá)到了 82.4% 的準(zhǔn)確率。
兩個(gè)模型都已經(jīng)開源，可以在開源社區(qū) Hugging Face 上找到。技術(shù)論文則是在 GitHub 上（模型和論文鏈接在文末）。
據(jù)論文介紹，DeepSeek Prover V2 是一個(gè)專為 Lean 4 形式定理證明設(shè)計(jì)的開源大型語言模型。其最大創(chuàng)新點(diǎn)在于，能將非形式化的數(shù)學(xué)推理能力與嚴(yán)格的形式化證明過程結(jié)合在一起，實(shí)現(xiàn)了兩種思維模式的有效融合。
你可以想象一下，當(dāng)我們要解決一道數(shù)學(xué)題時(shí)，腦海中往往先有一個(gè)大致的思路，然后再一步步填充細(xì)節(jié)。這種從整體到局部、從思路到步驟的過程，對(duì)人類來說很自然，但對(duì)AI卻是一項(xiàng)艱巨的挑戰(zhàn)。
在 AI 發(fā)展歷程中，GPT 和 Claude 等大語言模型（LLM，Large Language Model）已經(jīng)展示出令人印象深刻的數(shù)學(xué)問題求解能力。它們能夠通過“思維鏈”（CoT，Chain-of-Thought）方法，像人類一樣逐步思考問題，甚至能解決一些競(jìng)賽級(jí)別的難題。
然而，在更為嚴(yán)格的數(shù)學(xué)領(lǐng)域——形式化定理證明方面，AI 的表現(xiàn)卻相對(duì)遜色。
原因在于兩種思維模式的本質(zhì)差異：自然語言推理是靈活的、啟發(fā)式的，允許一定程度的模糊性和跳躍性思維；而形式化證明則要求百分百的精確性和嚴(yán)謹(jǐn)性，每一個(gè)推理步驟都必須經(jīng)過嚴(yán)格驗(yàn)證，不允許任何隱含假設(shè)和細(xì)節(jié)省略。
就像兩種不同的語言，雖然表達(dá)的是同一個(gè)數(shù)學(xué)世界，但規(guī)則和要求卻大相徑庭。
為了解決這一挑戰(zhàn)，DeepSeek-Prover-V2 采用了一種創(chuàng)新的“遞歸定理證明流程”，這一流程的靈感源自人類數(shù)學(xué)家解決復(fù)雜問題的方法——將困難問題分解為一系列更容易解決的子問題。
首先，研究團(tuán)隊(duì)利用 DeepSeek-V3 模型擔(dān)任“分解專家”的角色，構(gòu)建定理證明系統(tǒng)的基礎(chǔ)框架。
當(dāng)面對(duì)一個(gè)復(fù)雜的數(shù)學(xué)定理時(shí)，DeepSeek-V3 會(huì)用自然語言分析和理解問題，提出高層次的證明思路，將整個(gè)證明分解為一系列較小的子目標(biāo)，最后將每個(gè)子目標(biāo)翻譯成嚴(yán)格的 Lean 4 形式語言表達(dá)，由 have…sorry 語句組成，也就是需要解決的子目標(biāo)。
這種方法也是人類所用的證明構(gòu)建方式，即將復(fù)雜定理逐步簡(jiǎn)化為一系列更易管理的引理。
一旦復(fù)雜問題被分解為多個(gè)子目標(biāo)，研究團(tuán)隊(duì)就會(huì)使用更小的 7B 參數(shù)模型作為解題專家，逐一攻克這些子目標(biāo)。這種方法不僅提高了效率，還大幅降低了計(jì)算資源的消耗。
DeepSeek 采用遞歸求解策略系統(tǒng)地解決每個(gè)中間證明步驟。他們從 have 語句中提取子目標(biāo)表達(dá)式，用它們替代原始問題中的目標(biāo)，并將前面的子目標(biāo)作為前提條件。
這種構(gòu)建使后續(xù)子目標(biāo)能夠利用早期步驟的中間結(jié)果，從而促進(jìn)更局部化的依賴結(jié)構(gòu)，有助于開發(fā)更簡(jiǎn)單的引理。
為了減少大量證明搜索的計(jì)算開銷，使用專門優(yōu)化的小型 7B 證明模型處理分解后的引理。成功解決所有分解步驟后，原始定理的完整證明就可以自動(dòng)推導(dǎo)出來。
在這個(gè)過程中，證明模型的訓(xùn)練需要大型形式語言問題集，但從人類編寫文本形式化獲得的訓(xùn)練信號(hào)通常較為稀疏，因?yàn)榇蟛糠钟?jì)算嘗試都不會(huì)產(chǎn)生成功的證明，因此不提供積極的獎(jiǎng)勵(lì)信號(hào)。
為了產(chǎn)生更密集的訓(xùn)練信號(hào)，DeepSeek 利用子目標(biāo)擴(kuò)展用于模型訓(xùn)練的形式語句范圍，生成兩類子目標(biāo)定理：一類將前面的子目標(biāo)作為前提條件，另一類則不包含前提條件。
這兩類子目標(biāo)被整合到專家迭代階段，建立一個(gè)課程（curriculum），逐步引導(dǎo)證明模型系統(tǒng)地解決精心策劃的一系列挑戰(zhàn)性問題。
隨后，研究團(tuán)隊(duì)挑選了一些 7B 證明模型無法“端到端（完全）解決”，但“所有子目標(biāo)均已成功解決”的挑戰(zhàn)性問題。通過組合所有子目標(biāo)的證明，他們構(gòu)建了原始問題的完整形式證明。這個(gè)證明再與 DeepSeek-V3 的自然語言推理過程配對(duì)，創(chuàng)建了“冷啟動(dòng)推理數(shù)據(jù)”。
“這使我們能夠收集數(shù)百個(gè)高質(zhì)量的合成冷啟動(dòng)數(shù)據(jù)，作為訓(xùn)練 DeepSeek-Prover-V2 的基礎(chǔ)?！闭撐膶懙馈?/p>
這些冷啟動(dòng)數(shù)據(jù)之所以珍貴，是因?yàn)樗鼈兺瑫r(shí)包含了兩種形式的數(shù)學(xué)推理：直觀的自然語言思考鏈和嚴(yán)格的形式化證明步驟。就像是給 AI 提供了一本內(nèi)容豐富的“雙語教材”，幫助它學(xué)習(xí)如何在兩種表達(dá)方式之間自如轉(zhuǎn)換。
有了冷啟動(dòng)數(shù)據(jù)后，研究團(tuán)隊(duì)通過面向推理的強(qiáng)化學(xué)習(xí)（Reasoning-oriented Reinforcement Learning）進(jìn)一步優(yōu)化模型性能。在這個(gè)階段，DeepSeek-Prover-V2 會(huì)學(xué)習(xí)如何更好地連接非形式推理與形式證明構(gòu)建，特別注重保持證明結(jié)構(gòu)與初始分解思路的一致性。
這個(gè)過程類似于學(xué)生在掌握基本思路后，通過不斷練習(xí)和反饋來提升解題能力，逐漸形成自己的解題風(fēng)格和策略。
在訓(xùn)練階段，DeepSeek-Prover-V2 采用了兩階段訓(xùn)練策略，建立了兩種互補(bǔ)的證明生成模式：
- 高效非鏈?zhǔn)剿季S（non-CoT）模式：快速生成簡(jiǎn)潔的形式 Lean 證明代碼，不包含明確的中間推理步驟。
- 高精度鏈?zhǔn)剿季S（CoT）模式：系統(tǒng)地闡述中間推理步驟，強(qiáng)調(diào)透明度和邏輯進(jìn)展，構(gòu)建最終形式證明。
訓(xùn)練過程中，研究團(tuán)隊(duì)使用“專家迭代”方法不斷提升模型能力。每次迭代中，用當(dāng)前最佳模型（策略）嘗試解決之前未能解決的問題，成功的證明被添加到訓(xùn)練數(shù)據(jù)中，用于改進(jìn)模型。
這個(gè)迭代循環(huán)持續(xù)進(jìn)行，使模型能夠逐步提高解決難題的能力。
此外，在強(qiáng)化學(xué)習(xí)階段，DeepSeek 使用了“群體相對(duì)策略優(yōu)化”的算法，相比傳統(tǒng) PPO 效果更好、效率更高。
性能方面，DeepSeek-Prover-V2 在多個(gè)主流基準(zhǔn)測(cè)試中都取得了不錯(cuò)的成績(jī)。
在評(píng)估 AI 形式證明能力的標(biāo)準(zhǔn)測(cè)試集 MiniF2F 中，DeepSeek-Prover-V2-671B 創(chuàng)造了新記錄。在嘗試 32 次（Pass@32）的情況下達(dá)到了 82.4% 的準(zhǔn)確率，當(dāng)增加到 8192 次（Pass@8192）時(shí)，表現(xiàn)提高到了 88.9%。
即使是參數(shù)較少的 DeepSeek-Prover-V2-7B 也超越了以往所有開源定理證明模型。
在評(píng)估大學(xué)水平數(shù)學(xué)能力的 ProofNet 和 PutnamBench 測(cè)試中，DeepSeek-Prover-V2-671B 同樣表現(xiàn)出色。在 ProofNet 測(cè)試集上，它以 Pass@1024 指標(biāo)達(dá)到了 37.1% 的解題率。在極具挑戰(zhàn)性的 PutnamBench 上成功解決了 658 個(gè)問題中的 49 個(gè)。
更加令人驚訝的是，研究團(tuán)隊(duì)發(fā)現(xiàn)較小的 7B 模型在某些特定問題上甚至超越了 671B 的大模型，成功解決了 13 個(gè)大模型未能攻克的問題，將總解題數(shù)提升至 62 題。
在更全面的 CombiBench 測(cè)試中，DeepSeek-Prover-V2 在 77 個(gè)問題中解決了 12 個(gè)。雖然這一數(shù)字看似不高，但考慮到模型主要在數(shù)論和代數(shù)領(lǐng)域訓(xùn)練，這一表現(xiàn)已經(jīng)展示了其良好的跨領(lǐng)域泛化能力。
在 15 個(gè)來自 AIME 24 和 25 競(jìng)賽的數(shù)學(xué)問題上，DeepSeek-Prover-V2-671B 成功解決了 6 個(gè)，而其通用語言模型 DeepSeek-V3 則解決了 8 個(gè)。
研究團(tuán)隊(duì)認(rèn)為這一對(duì)比結(jié)果很有趣，因?yàn)樗砻餍问綌?shù)學(xué)證明與非形式數(shù)學(xué)推理之間的能力差距正在顯著縮小。
最后，DeepSeek 團(tuán)隊(duì)計(jì)劃將創(chuàng)造 DeepSeek-Prover-V2-671B 的經(jīng)驗(yàn)擴(kuò)展稱一個(gè)類似 AlphaProof 的系統(tǒng)，最終目標(biāo)是挑戰(zhàn)國(guó)際數(shù)學(xué)奧林匹克級(jí)別的數(shù)學(xué)問題。
至于傳聞中的下一代 V4/R2 模型，說不定也會(huì)用上相關(guān)的技術(shù)進(jìn)展。
參考資料：
https://github.com/deepseek-ai/DeepSeek-Prover-V2/tree/main
論文鏈接：
https://github.com/deepseek-ai/DeepSeek-Prover-V2/blob/main/DeepSeek_Prover_V2.pdf
模型鏈接：
https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-7B
排版：劉雅坤
熱門跟貼