文章圖片
前天晚上 ， DeepSeek發布了最新的數學專用大模型V2 。該模型有兩個版本 ， 分別是671億參數和7億參數 。 在極具挑戰性的數學評測MiniF2F中 ， 671B版本的通過率高達88.9% 。 此外 ， 在PutnamBench包含的658道題目中 ， 該模型成功解決了49道 ， 展現出卓越的數學推理和解題能力 。同時 ， DeepSeek還公開了一個高質量的數學評測數據集ProverBench ， 為數學能力測試提供了有力支持 。
開源地址：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
評估數據集：https://huggingface.co/datasets/deepseek-ai/DeepSeek-ProverBench
在架構方面 ， V2-671B是在DeepSeek-V3-Base模型的基礎上進一步訓練得到的 ， 而V2-7B則基于DeepSeek-Prover-V1.5-Base構建 ， 同時擴展了上下文長度 ， 最大支持32K標記 。
V2搭建了一個統一的數學推理框架 ， 將非形式化推理與形式化證明相結合 。 它通過將復雜數學問題拆解為多個子目標 ， 利用V3的逐步推理能力 ， 實現了從問題拆解到最終證明生成的無縫連接 。
在冷啟動數據生成階段 ， V2采用遞歸的定理證明流程 。 首先 ， V3被用來將定理拆分成高層次的證明草圖 ， 并在Lean4環境中對這些證明步驟進行形式化 ， 形成多個子目標 。 隨后 ， 較小的7B模型專注于每個子目標的證明搜索 ， 這極大地減輕了整體計算壓力 。 當所有拆分步驟完成后 ， 結合DeepSeek-V3的鏈式思考技術 ， 系統生成了用于初始訓練的推理數據 。
基于這些冷啟動數據 ， V2進入強化學習階段 。 在此階段 ， 重點挑選出那些7B模型無法端到端解決的問題 ， 但其所有子目標均已成功證明 。 通過整合這些子目標的證明 ， 構建出完整形式化的原始問題證明 ， 并將其融合進V3的鏈式思考流程 ， 實現了非形式推理與形式證明的連貫結合 。
在強化學習階段 ， 模型主要依靠二元的正誤反饋作為獎勵信號 ， 進一步提升了將非形式推理與形式證明相結合的能力 。 為了更全面地評估模型表現 ， DeepSeek推出了ProverBench測試集 。 該數據集涵蓋了325道問題 ， 其中15道題目取自近期AIME（第24屆和第25屆）競賽中的數論和代數題 ， 體現了真實高中競賽的難度水平 。
其余的310道題目來源于精心挑選的教科書案例和教學資料 ， 內容涵蓋高中至大學階段的多個數學領域 ， 如數論、基礎代數、線性代數、抽象代數、微積分、實分析、復分析、泛函分析以及概率論等 ， 為對模型能力的評估提供了廣泛且多樣化的測試內容 。
·
我們相信人工智能為普通人提供了一種“增強工具” ， 并致力于分享全方位的AI知識 。 在這里 ， 您可以找到最新的AI科普文章、工具評測、提升效率的秘籍以及行業洞察 。【DeepSeek發布了全新開源大模型，實現了數學能力的重大提升！】·
歡迎關注“福大大架構師每日一題” ， 讓AI助力您的未來發展 。
推薦閱讀
- 聯想moto edge 60/razr 60系列預熱，5 月 8 日發布
- 有必要買相機嗎？手機拍照真的可以媲美甚至超越相機拍照了嗎？
- 徹底告別Windows！華為鴻蒙PC版本月發布：自主可控、統一生態
- Zen3+突然出現！AMD低調發布銳龍5 7533HS：第一款3字尾型號
- 我靠！一加13T首發當天直接賣爆了
- 真我GT8 Pro狂堆料，性能影像全面升級，這是要奔頂級旗艦去了？
- 首發天璣旗艦芯！一加Ace5系列兩員大將即將登場，千元天花板穩了
- 1.93GB大更新！鴻蒙5.0.1新版本來了，哪些老機型被淘汰？
- 存儲芯片崛起！8家公司一季報大增超50%，這下瑞銀、北向全來了
- iOS18.5新代碼暗示了即將發布的新品！