DeepSeek 又在假期到來(lái)的時(shí)候有新動(dòng)作了。
剛剛，DeepSeek 在毫無(wú)預(yù)告的情況下，突然在 Hugging Face 平臺(tái)上開(kāi)源了最新數(shù)學(xué)定理證明專用模型 DeepSeek-Prover-V2-671B。
這個(gè)新模型并非通用的聊天機(jī)器人，而是專注于數(shù)學(xué)定理的形式化證明這一高度專業(yè)的領(lǐng)域。這類模型的目標(biāo)是利用像 Lean 4 這樣的證明助手軟件，來(lái)理解和生成嚴(yán)格的數(shù)學(xué)證明步驟。簡(jiǎn)單來(lái)說(shuō)，它們是幫助計(jì)算機(jī)驗(yàn)證數(shù)學(xué)定理正確性的 AI 工具，需要具備很強(qiáng)的邏輯推理能力。其主要應(yīng)用場(chǎng)景包括：自動(dòng)定理證明（從高中到大學(xué)水平的數(shù)學(xué)問(wèn)題）、發(fā)現(xiàn)證明中的錯(cuò)誤并提供修復(fù)建議、通過(guò)生成 Lean 4 代碼和解釋幫助教學(xué)，以及協(xié)助數(shù)學(xué)家探索新定理等。
實(shí)際上，DeepSeek 此前就已久發(fā)布過(guò)同類模型，2024 年 8 月時(shí)，他們?cè)l(fā)布了DeepSeek-Prover-V1.5，一個(gè)大約 7B 參數(shù)的模型。根據(jù) DeepSeek 當(dāng)時(shí)公布的信息，V1.5 在結(jié)合強(qiáng)化學(xué)習(xí)和蒙特卡洛樹搜索等技術(shù)后，在一些標(biāo)準(zhǔn)的數(shù)學(xué)證明測(cè)試（如miniF2F 和 ProofNet）中取得了不錯(cuò)的成果，能夠處理從高中到大學(xué)本科部分水平的數(shù)學(xué)問(wèn)題。
這次發(fā)布的 DeepSeek-Prover-V2-671B，在模型規(guī)模上有了巨大的飛躍，參數(shù)量達(dá)到了 671B ，比 V1.5 大了近百倍，比其他同類產(chǎn)品如 Llemma-7B/34B、InternLM2-StepProver 等也要大得多。
根據(jù)其公開(kāi)的配置文件，我們可以了解到更多關(guān)于模型結(jié)構(gòu)的信息。該模型建立在 DeepSeek-V3 架構(gòu)之上，因此許多配置與通用的 DeepSeek-V3 模型相似。它采用了混合專家（MoE，Mixture-of-Experts）的設(shè)計(jì)，具體來(lái)說(shuō)，每層包含 256 個(gè)路由專家（routed experts）和1個(gè)共享專家（shared expert），每個(gè)專家的中間層大?。╩oe_intermediate_size）為 2048，在處理每個(gè)輸入符號(hào)（token）時(shí)會(huì)激活其中的 8 個(gè)專家。此外，該模型支持的最大上下文長(zhǎng)度達(dá)到了 163,840 個(gè) token。
不過(guò)，截至發(fā)稿時(shí)，DeepSeek 官方尚未發(fā)布更多關(guān)于該模型的技術(shù)細(xì)節(jié)和性能數(shù)據(jù)。關(guān)于 DeepSeek-Prover-V2-671B 的訓(xùn)練方法、使用了哪些特定于數(shù)學(xué)證明的數(shù)據(jù)，以及它在基準(zhǔn)測(cè)試上的實(shí)際表現(xiàn)如何等關(guān)鍵信息，目前仍一無(wú)所知。
對(duì)于這個(gè)新模型的內(nèi)部構(gòu)造和具體能力，還有待官方提供更多信息?？紤]到參數(shù)量的巨大提升，我們可以期待 Prover-V2 能在各項(xiàng)數(shù)學(xué)證明基準(zhǔn)上取得更好的成績(jī)。
參考資料：
1.https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B/tree/main
2.https://arxiv.org/abs/2408.08152
排版：劉雅坤
熱門跟貼