北京
正當大家紛紛進入“五一”假期模式時，AI 界的 “勞模” DeepSeek 再次證明：放假？不存在的。他們就在這個節骨眼上，悄然向開源社區投喂了一款重量級新模型——DeepSeek-Prover-V2-671B。
模型現已登陸 Hugging Face (鏈接: https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B)，光看這 6710 億（671B）的參數量，就足以讓不少機器瑟瑟發抖。
這并非一款通用大模型，而是 DeepSeek 專為高難度數學領域，特別是使用 Lean 4 進行形式化定理證明而打造的“專業選手”。
作為 DeepSeek-Prover 系列的第二代產品，大家自然對其能力充滿期待。要知道，其前身 V1.5（雖然只有 7B 參數）在去年的高中數學測試 (miniF2F) 中已能達到 63.5% 的成功率，在大學級別測試 (ProofNet) 中也有 25.3% 的準確率。如今參數量暴漲近百倍的 V2，潛力顯然不可同日而語，但具體實力如何，還有待驗證。
然而，DeepSeek 這次的操作頗有“先把孩子生下來，名字和體檢報告稍后補上”的風格。模型權重已經大方開源，但至關重要的 Model Card (模型詳細說明書) 和 Benchmark (官方性能成績單) 卻暫時缺席。
這不禁讓人猜測，是團隊為了趕在假期前“交卷”過于匆忙，還是有意讓社區進行一輪“盲測”和探索？
總之，勞動節是得繼續勞動了。
特別聲明：以上內容(如有圖片或視頻亦包括在內)為自媒體平臺“網易號”用戶上傳并發布，本平臺僅提供信息存儲服務。
Notice: The content above (including the pictures and videos if any) is uploaded and posted by a user of NetEase Hao, which is a social media platform and only provides information storage services.
