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