太低调了！就在刚刚，DeepSeek悄咪咪发布新模型！ 就在刚刚（2025.4.30）， DeepSeek 在官方 HuggingFace 仓库更新了他们最新版本的数学领域垂类模型：deepseek-ai/DeepSeek-Prover-V2-671B 从公开信息来看，这个模型是在 DeepSeek-V3-671B 基座上研发得到的，面向数学领域，有望在定理证明等领域为数学家和研究人员提供辅助！ 在这之前，DeepSeek 就已经开源发布了基于 Llama 的 DeepSeek-Prover-V1.5 模型，推测 V2 是在 1.5 基础上的最新工作。 DeepSeek-Prover-V1.5 的模型大小为 70 亿参数 。它在 DeepSeekMath-Base 上进行了预训练，该基础模型专注于通用数学知识和形式化数学语言的专业化 。 V1.5 经历了监督微调（SFT）过程，使用了从 DeepSeek-Prover-V1 衍生出的增强型形式化定理证明数据集 。此外，模型还采用了来自证明助手反馈的强化学习（RLPAF）技术进行进一步的优化 。 V1.5 的一个重要特点是引入了 RMaxTS，一种蒙特卡洛树搜索的变体，用于增强推理 。RMaxTS 采用内在奖励驱动的探索策略，以生成多样化的证明路径。V1.5 还结合了“截断并恢复”（truncate-and-resume）机制与 MCTS ，该机制结合了全证明生成和证明步骤生成的方法。 链接：https://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B/tree/main