近日，AI 開源社區(qū) Hugging Face 迎來了一項(xiàng)新成果，深度求索（DeepSeek）團(tuán)隊(duì)發(fā)布了名為 DeepSeek-Prover-V2-671B 的大型語言模型。與此同時(shí)，該團(tuán)隊(duì)還在 GitHub 等平臺(tái)分享了相關(guān)論文，詳細(xì)介紹了這一新模型的特性和成就。
DeepSeek-Prover-V2 是一款專注于形式化數(shù)學(xué)推理的開源模型，其基礎(chǔ)是 DeepSeek-V3-0324。為了生成訓(xùn)練所需的初始數(shù)據(jù)，團(tuán)隊(duì)采用了遞歸定理證明管道的方法。這一創(chuàng)新使得模型在處理復(fù)雜數(shù)學(xué)問題時(shí)，能夠展現(xiàn)出更高的精確度和效率。
DeepSeek 團(tuán)隊(duì)推出了兩個(gè)版本的模型：DeepSeek-Prover-V2-671B 和 DeepSeek-Prover-V2-7B。前者結(jié)合了 V3 基礎(chǔ)大模型的優(yōu)點(diǎn)，后者則是一個(gè)增強(qiáng)模型。團(tuán)隊(duì)還發(fā)布了 DeepSeek-ProverBench 數(shù)據(jù)集，為評(píng)估模型性能提供了有力工具。
DeepSeek-Prover-V2-671B 的架構(gòu)與 DeepSeek V3-0324 相同，但其應(yīng)用場景卻大相徑庭。這款模型并非用于常規(guī)對話或推理，而是專注于形式化定理證明，專門增強(qiáng)了數(shù)學(xué)能力。為了實(shí)現(xiàn)這一目標(biāo)，團(tuán)隊(duì)采用了復(fù)雜的策略。
首先，他們引導(dǎo) DeepSeek-V3 模型將復(fù)雜的數(shù)學(xué)定理分解為一系列子目標(biāo)。這一步驟整合了非形式化與形式化數(shù)學(xué)推理，使得模型能夠在 Lean 4 平臺(tái)上逐步完成形式化證明。接著，團(tuán)隊(duì)利用一個(gè)較小的 7B 參數(shù)模型來處理這些子目標(biāo)的證明搜索，從而大大減輕了計(jì)算負(fù)擔(dān)。
在訓(xùn)練過程中，團(tuán)隊(duì)精心篩選了一批難題，這些難題雖然 7B 模型無法直接解決，但其子目標(biāo)已被證明。通過整合這些子目標(biāo)的證明，團(tuán)隊(duì)形成了完整的形式化證明，并與 DeepSeek-V3 的推理過程對接，生成了豐富的合成數(shù)據(jù)。這些數(shù)據(jù)為模型的微調(diào)提供了堅(jiān)實(shí)的基礎(chǔ)。
隨后，團(tuán)隊(duì)利用強(qiáng)化學(xué)習(xí)進(jìn)一步提升模型的能力。他們以二元反饋（正確或錯(cuò)誤）作為獎(jiǎng)勵(lì)機(jī)制，通過不斷的試錯(cuò)和優(yōu)化，使得 DeepSeek-Prover-V2-671B 在神經(jīng)定理證明領(lǐng)域取得了顯著進(jìn)展。在 MiniF2F-test 數(shù)據(jù)集上，該模型的通過率達(dá)到了 88.9%，在 PutnamBench 數(shù)據(jù)集中也成功解決了 49 個(gè)問題。
為了推動(dòng)模型在多樣化場景下的測試與應(yīng)用，DeepSeek 團(tuán)隊(duì)還發(fā)布了 ProverBench 基準(zhǔn)數(shù)據(jù)集。該數(shù)據(jù)集包含了 325 個(gè)形式化數(shù)學(xué)問題，其中 15 個(gè)問題源自近期的 AIME 競賽，涉及數(shù)論與代數(shù)等高中競賽難度的內(nèi)容。其余 310 個(gè)問題則涵蓋了線性代數(shù)、微積分、概率等多個(gè)領(lǐng)域，為高中競賽和本科數(shù)學(xué)提供了全面的評(píng)估標(biāo)準(zhǔn)。
