2025年4月30日，深度求索在Hugging Face平臺(tái)低調(diào)的上傳了其數(shù)學(xué)定理證明專用模型DeepSeek-Prover-V2-671B，以驚人的6710億參數(shù)規(guī)模刷新了領(lǐng)域記錄。從前代7B參數(shù)的 DeepSeek-Prover-V1.5 到如今的671B，這一跨越式進(jìn)步展現(xiàn)了其在數(shù)學(xué)推理與定理證明領(lǐng)域的雄心與技術(shù)實(shí)力。

DeepSeek-Prover-V2-671B基于DeepSeek-V3架構(gòu)，采用混合專家系統(tǒng)（MoE）設(shè)計(jì)，包含256個(gè)路由專家，每個(gè)輸入token動(dòng)態(tài)分配至8個(gè)專家處理。其核心架構(gòu)包含61層Transformer與7168維隱藏層，顯著提升了復(fù)雜數(shù)學(xué)邏輯的解析能力。

關(guān)鍵技術(shù)突破

超長(zhǎng)上下文支持：通過YaRN縮放策略擴(kuò)展至163,840 tokens上下文窗口，完整覆蓋多步驟數(shù)學(xué)證明的全流程推導(dǎo)；

高效量化技術(shù)：采用FP8（e4m3格式）量化方案，在保持計(jì)算精度的同時(shí)降低顯存占用，推理效率較傳統(tǒng)方案提升超過40%；

領(lǐng)域?qū)＞珒?yōu)化：針對(duì)形式化數(shù)學(xué)語(yǔ)言（如Lean4）進(jìn)行強(qiáng)化訓(xùn)練，結(jié)合定理驗(yàn)證反饋機(jī)制，實(shí)現(xiàn)數(shù)學(xué)命題生成與驗(yàn)證的閉環(huán)協(xié)同。

相較前代7B參數(shù)的V1.5版本，V2模型通過三階段優(yōu)化實(shí)現(xiàn)性能飛躍

• 預(yù)訓(xùn)練基礎(chǔ)：基于DeepSeekMath-Base數(shù)據(jù)集完成初始訓(xùn)練；
• 監(jiān)督微調(diào)：采用增強(qiáng)型形式化定理證明數(shù)據(jù)集優(yōu)化領(lǐng)域適配性；
• 強(qiáng)化學(xué)習(xí)優(yōu)化：引入基于證明輔助反饋的強(qiáng)化學(xué)習(xí)（RLPAF）及群組相對(duì)策略優(yōu)化（GRPO），使輸出更貼合數(shù)學(xué)家思維模式。

創(chuàng)新性算法升級(jí)包括

• RMaxTS算法（蒙特卡洛樹搜索變體）：通過內(nèi)在獎(jiǎng)勵(lì)驅(qū)動(dòng)探索，生成多樣化證明路徑；
• 截?cái)嗖⒒謴?fù)（Truncate-and-Resume）機(jī)制：平衡全證明生成效率與逐步驗(yàn)證需求；
• 多頭潛注意力（MLA）架構(gòu)：壓縮鍵值緩存（KV Cache），降低推理資源消耗。

該模型的開源將加速多領(lǐng)域革新

• 學(xué)術(shù)研究：輔助數(shù)學(xué)家驗(yàn)證復(fù)雜猜想（如代數(shù)幾何、數(shù)論難題），縮短證明周期；
• 教育智能化：提供實(shí)時(shí)、可交互的數(shù)學(xué)證明輔導(dǎo)系統(tǒng)，支持從基礎(chǔ)代數(shù)到前沿?cái)?shù)學(xué)的個(gè)性化教學(xué)；
• 工業(yè)驗(yàn)證：應(yīng)用于芯片形式化驗(yàn)證、航空航天控制系統(tǒng)等高可靠性需求場(chǎng)景，降低人工驗(yàn)證成本。

模型已通過Hugging Face平臺(tái)開源，包含163個(gè)分片（每片約4.3GB），支持學(xué)術(shù)界與工業(yè)界直接調(diào)用及二次開發(fā)。

此次發(fā)布進(jìn)一步鞏固了 DeepSeek 在專業(yè)領(lǐng)域的技術(shù)領(lǐng)導(dǎo)地位。作為一家持續(xù)踐行開源戰(zhàn)略的企業(yè)，其此前推出的V3和R1模型已憑借“低成本-高性能”特性重塑行業(yè)格局。而新模型的推出不僅推動(dòng)了 AI 在形式化證明研究中的發(fā)展，為自動(dòng)推理與符號(hào)計(jì)算提供了基準(zhǔn)模型，還驗(yàn)證了超大規(guī)模模型在領(lǐng)域?qū)＞械臐摿Α?/p>

有分析指出，V2 采用的 GRPO 與 RMaxTS 等技術(shù)可能為即將發(fā)布的DeepSeek-R2提供核心模塊，預(yù)示著其在復(fù)雜推理能力上的進(jìn)一步突破，甚至可能將“證明型智能”融入更大規(guī)模的通用模型中，為“思維”與“證明”之間的探索鋪路。

學(xué)術(shù)界普遍認(rèn)為，這類超大規(guī)模領(lǐng)域?qū)＞Ｐ蛯⒅匦露x人工智能在基礎(chǔ)科學(xué)中的角色，從“計(jì)算加速器”逐步進(jìn)化為“創(chuàng)造性合作伙伴”。DeepSeek 的此次開源實(shí)踐，或?qū)⒊蔀檫@一轉(zhuǎn)型的關(guān)鍵里程碑，為全球AI研究與應(yīng)用注入新的活力。