北京
正当大家纷纷进入“五一”假期模式时，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.
