DeepSeek开源新模型，数学推理能力大提升

五一假期前，DeepSeek发布惊喜——DeepSeek-Prover-V2在Hugging Face上线，同步提供模型卡与示例代码。该版本包括两个模型：DeepSeek-Prover-V2-7B（基于V1.5，支持32K上下文输入）和DeepSeek-Prover-V2-671B（以DeepSeek-V3-Base为基础，性能最强）。

训练采用“递归+强化学习”策略：DeepSeek-V3分解复杂定理，生成子目标和推理思路，再利用GRPO算法优选最佳方案。模型具备“快速模式”（non-CoT）和“逻辑模式”（CoT），分别注重速度与过程透明。

开发分两阶段：初期专注快速模式，用“专家迭代”法优化；后期培养逻辑推理，迁移知识并引入“冷启动”机制。GRPO算法通过对比候选答案质量，引导模型选择最优解。

最终，671B模型的能力被“蒸馏”至7B模型，实现小体积高性能。7B模型在MiniF2F测试中达88.9%通过率，解出PutnamBench中的49题。同时发布的ProverBench数据集含325道题，覆盖多领域，展现模型在不同数学推理中的能力。

经典问题测试显示，模型不仅解答正确，还能清晰解释抽象概念。DeepSeek-Prover-V2不仅提供答案，还指引语言模型未来发展方向：从生成内容到生成结构化逻辑，这是通向通用人工智能的重要一步。

模型现已通过Hugging Face免费下载，支持Transformers接口部署。相关地址已在文末列出。