近日，AI 開源社區(qū) Hugging Face 迎來了一項新成果，深度求索（DeepSeek）團隊發(fā)布了名為 DeepSeek-Prover-V2-671B 的大型語言模型。與此同時，該團隊還在 GitHub 等平臺分享了相關論文，詳細介紹了這一新模型的特性和成就。

DeepSeek-Prover-V2 是一款專注于形式化數(shù)學推理的開源模型，其基礎是 DeepSeek-V3-0324。為了生成訓練所需的初始數(shù)據(jù)，團隊采用了遞歸定理證明管道的方法。這一創(chuàng)新使得模型在處理復雜數(shù)學問題時，能夠展現(xiàn)出更高的精確度和效率。

DeepSeek 團隊推出了兩個版本的模型：DeepSeek-Prover-V2-671B 和 DeepSeek-Prover-V2-7B。前者結合了 V3 基礎大模型的優(yōu)點，后者則是一個增強模型。團隊還發(fā)布了 DeepSeek-ProverBench 數(shù)據(jù)集，為評估模型性能提供了有力工具。

DeepSeek-Prover-V2-671B 的架構與 DeepSeek V3-0324 相同，但其應用場景卻大相徑庭。這款模型并非用于常規(guī)對話或推理，而是專注于形式化定理證明，專門增強了數(shù)學能力。為了實現(xiàn)這一目標，團隊采用了復雜的策略。

首先，他們引導 DeepSeek-V3 模型將復雜的數(shù)學定理分解為一系列子目標。這一步驟整合了非形式化與形式化數(shù)學推理，使得模型能夠在 Lean 4 平臺上逐步完成形式化證明。接著，團隊利用一個較小的 7B 參數(shù)模型來處理這些子目標的證明搜索，從而大大減輕了計算負擔。

在訓練過程中，團隊精心篩選了一批難題，這些難題雖然 7B 模型無法直接解決，但其子目標已被證明。通過整合這些子目標的證明，團隊形成了完整的形式化證明，并與 DeepSeek-V3 的推理過程對接，生成了豐富的合成數(shù)據(jù)。這些數(shù)據(jù)為模型的微調(diào)提供了堅實的基礎。

隨后，團隊利用強化學習進一步提升模型的能力。他們以二元反饋（正確或錯誤）作為獎勵機制，通過不斷的試錯和優(yōu)化，使得 DeepSeek-Prover-V2-671B 在神經(jīng)定理證明領域取得了顯著進展。在 MiniF2F-test 數(shù)據(jù)集上，該模型的通過率達到了 88.9%，在 PutnamBench 數(shù)據(jù)集中也成功解決了 49 個問題。

為了推動模型在多樣化場景下的測試與應用，DeepSeek 團隊還發(fā)布了 ProverBench 基準數(shù)據(jù)集。該數(shù)據(jù)集包含了 325 個形式化數(shù)學問題，其中 15 個問題源自近期的 AIME 競賽，涉及數(shù)論與代數(shù)等高中競賽難度的內(nèi)容。其余 310 個問題則涵蓋了線性代數(shù)、微積分、概率等多個領域，為高中競賽和本科數(shù)學提供了全面的評估標準。