廣告
快訊
KNEWS
⚡
DeepSeek再推出新模型 專注數學推理開源大語言模型
【財經中心／台北報導】中國AI新創公司DeepSeek昨在AI開源社區Hugging Face上，發布名為DeepSeek-Prover-V2-671B的新模型，隨後在GitHub等平台上公開相關論文資訊。
專注數學推理開源大型語言模型
論文介紹，DeepSeek-Prover-V2是一款專注於形式化數學推理的開源大型語言模型，基於DeepSeek-V3-0324，透過遞歸定理證明管線生成初始數據。
DeepSeek推出DeepSeek-Prover-V2-671B（結合V3基礎大模型）、DeepSeek-Prover-V2-7B（增強模型）兩款模型，以及 DeepSeek-ProverBench 數據集。
DeepSeek-Prover-V2-671B採用與DeepSeek V3-0324相同的架構，並非用於正常對話或推理，而是專門用於形式化定理證明、強化數學能力的模型。
IT之家報導，DeepSeek團隊首先引導DeepSeek-V3模型將複雜定理拆解為一系列子目標（subgoals），整合非形式與形式化數學推理，在Lean 4平台上進行形式化證明步驟。
以二元反饋作為獎勵機制
接著，利用一個較小的7B參數模型處理子目標的證明搜尋，以減輕計算負擔。最終，結合完整的逐步證明與DeepSeek-V3的思維鏈（chain-of-thought），形成強化學習的「冷啟動」數據。
在訓練過程中，團隊篩選出一批7B模型無法直接解決但其子目標已被證明的難題，透過整合子目標證明，形成完整的形式化證明，並與DeepSeek-V3的推理過程對接，生成合成數據。
隨後，模型對這些數據進行微調，並透過強化學習進一步提升能力，以二元反饋（正確或錯誤）作為獎勵機制。
MiniF2F-test數據集通過率達88.9%
最終，DeepSeek-Prover-V2-671B在神經定理證明領域創下新高，在MiniF2F-test數據集上的通過率達到88.9%，在PutnamBench數據集中成功解決658個問題中的49個。
團隊同時發表ProverBench基準數據集，包含325個形式化數學問題。其中15個問題來自近期的AIME競賽（AIME 24 和 25），涵蓋數論與代數，代表高中競賽難度。
其餘310個問題則選自精選教材與教學內容，涵蓋線性代數、微積分、機率等多個領域。該數據集主要在為高中競賽與大學數學提供全面評估標準，推動模型在多樣化場景下的測試與應用。
