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