2025年4月30日， —— 中国AI公司DeepSeek在Hugging Face平台低调上线全新模型DeepSeek-Prover-V2-671B，这是其专为数学定理证明设计的垂类大模型，基于此前发布的DeepSeek-V3-671B架构打造。这一发布标志着DeepSeek在数学AI领域的又一重大突破，为数学家、研究人员和开发者提供了强大的辅助工具。
模型亮点：超大规模与数学专精
DeepSeek-Prover-V2-671B拥有6710亿参数，采用Mixture-of-Experts（MoE）架构，每层包含256个专家网络，每个token动态激活8个专家，兼顾计算效率与推理能力。 该模型在DeepSeek-V3-671B的基础上，进一步优化了形式化数学证明能力，特别适用于使用Lean 4框架进行自动化定理证明，目标是提升复杂逻辑推理和数学研究的效率。
与2024年8月发布的DeepSeek-Prover-V1.5（70亿参数）相比，V2版本实现了参数规模的飞跃。V1.5基于DeepSeekMath-Base预训练，专注于数学知识和形式化语言，通过监督微调（SFT）和证明助手反馈强化学习（RLPAF）优化，展现了出色的定理证明能力。V2则继承并升级了这些技术，预计在性能和应用范围上进一步突破。
技术创新：多样化证明路径与高效推理
DeepSeek-Prover-V2-671B延续了V1.5的创新技术，并引入了更强大的功能：
-
RMaxTS算法：一种基于蒙特卡洛树搜索（MCTS）的变体，通过内在奖励驱动的探索策略生成多样化的证明路径，提升模型解决复杂数学问题的能力。
-
截断并恢复机制：结合全证明生成与单步证明生成，优化证明过程的灵活性和准确性。
-
高效架构：沿用DeepSeek-V3的多头潜在注意力（MLA）和DeepSeekMoE架构，通过低秩键值压缩和FP8混合精度训练，大幅降低推理成本，同时保持高性能。
这些技术使模型在处理高难度数学问题时，不仅能提供更快、更准确的证明，还能生成多样化的推理路径，为研究人员提供更多灵感。
应用场景：助力数学与逻辑研究
DeepSeek-Prover-V2-671B专为数学定理证明和复杂逻辑推理设计，应用场景包括：
-
学术研究：辅助数学家验证和生成形式化证明，加速高水平数学问题的解决；
-
教育支持：为学生和教师提供逻辑推理和证明的教学工具；
-
自动化推理：在计算机科学、密码学等领域支持复杂算法验证。
V1.5已在miniF2F（高中数学竞赛级别，63.5%准确率）和ProofNet（本科数学级别，25.3%准确率）等基准测试中取得领先成绩，V2的超大规模架构有望进一步提升这些指标。
开源与社区支持
DeepSeek一贯致力于开源AI研究，Prover-V2-671B模型已在Hugging Face上提供，采用safetensors文件格式，支持多种计算精度（如FP8、BF16），便于开发者在不同硬件上训练和部署。 模型支持通过Hugging Face的Transformers库进行推理，社区开发者可参考官方文档在NVIDIA或AMD GPU上运行。
尽管完整数据集和训练代码尚未公开，DeepSeek鼓励社区贡献反馈，并通过其Discord和GitHub平台提供技术支持。模型的发布引发了热烈讨论，Reddit社区LocalLLLaMA上已有用户称其为“数学证明领域的游戏规则改变者”。
未来展望
DeepSeek-Prover-V2-671B的发布进一步巩固了DeepSeek在数学AI领域的领先地位。此前，DeepSeek的R1和V3模型已因在数学、代码和推理任务中媲美GPT-4o而备受关注。 V2的超大规模设计和高效推理能力，预示着未来在更广泛的学术和工业场景中的应用潜力。
DeepSeek表示，将继续优化Prover系列，探索在医学、物理等其他科学领域的推理应用，并计划开源更多推理引擎组件，以推动全球AI研究的发展。
结语
DeepSeek-Prover-V2-671B的悄然发布，不仅展示了DeepSeek在超大规模AI模型上的技术实力，也为数学定理证明领域注入了新的活力。作为一款开源模型，它为全球研究人员提供了探索复杂逻辑推理的机会。未来，随着社区的深入参与和模型的进一步迭代，DeepSeek-Prover系列有望成为数学与AI交叉领域的标杆。
相关链接：
-
模型仓库：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B
-
DeepSeek官网：https://www.deepseek.com
