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