万人瞩目的DeepSeek R2没有出来，昨天（4月30日）凌晨却以迅雷不及掩耳盗铃之势偷梁换柱，发布了一款名为DeepSeek Prover V2的最新模型。与其他众多大模型不同，延续了梁文锋大才子一向的低调，这次DeepSeek 选择了一种极其静悄悄的方式进行发布：将其直接放到了 GitHub 上，没有任何正式的新闻稿或白皮书。但是人家想低调也不可能，一下子就被业界纷纷报道并立马投入测试，拿着放大镜显微镜仔细看。结果呢？虽然这只是一款专用模型，但其结果并没有让人失望：出道即巅峰，标志着形式化数学推理领域的又一项里程碑进展！
模型类型与核心目标
DeepSeek Prover V2 是一款开源的大语言模型，专门设计用于数学推理和形式定理证明 (formal theorem proving)。它与一般的聊天机器人不同，而是一个更基于逻辑、专门针对数学的模型。模型旨在通过强化学习推进子目标分解形式的数学推理，并将非形式化和形式化的数学推理整合到一个统一的模型中。它是一个证明者，而不是一个聊天者。模型的主要目标是帮助数学家和研究人员创建数学证明，专注于数学证明的验证并能输出数学证明。不同于只能给出答案而无法解释过程的模型，Prover V2 设计为提供带有证明的可靠数学解答。
模型规模与可用性
DeepSeek Prover V2 模型具有巨大的规模，其中一个版本是671B 参数的模型。资料也提到还有一个7B 参数版本可用。
模型是完全免费的。用户可以在GitHub和Hugging Face上获取模型文件。此外，也可以通过OpenRouter API直接访问和使用其聊天界面，或者通过 Python 使用。但有用户提到，免费 API 可能因为新发布且使用量大而较慢或出现错误。
技术特点与训练方法
DeepSeek Prover V2 的技术架构包括一个163K token 或 32K tokens 的上下文窗口和递归搜索 transformer 基础架构。模型擅长问题分解和双重推理。基于分词器和隐藏层大小与 DeepSeek V3 的相似性，可以推测 Prover V2可能基于 DeepSeek V3 模型或与其相关。模型支持FP8 计算精度优化。
模型的训练方法非常关键且独特：
- 模型的初始化利用了DeepSeek V3 驱动的递归定理证明流程。
- 冷启动训练首先将复杂问题分解为子目标，合成思维链，并结合 DeepSeek V3 逐步推理，为强化学习创建初始训练数据。
- 利用 DeepSeek 作为子目标分解和形式化的统一工具，可以将问题分解成高级证明草图。
- 在 Lean 4 中将证明步骤形式化，生成一系列子目标。Lean 4 是一种用于证明数学理论的编程语言。Prover V2 能够生成 Lean 4 代码。
- 使用一个较小的7B 参数模型来处理子目标和目标证明搜索，以减轻计算负担。
- 一旦解决了具有挑战性问题的分解步骤，就分发证明及其匹配，以创建冷启动推理数据。
- 随后，根据合成的冷启动数据进行强化学习 (reinforcement learning)和蒙特卡洛搜索 (Monte Carlo research)（通过尝试不同解决方法，选择最有希望的路径进一步探索）。
- 模型采用端到端的方式来组织尚未证明解决的问题集。
- 所有子目标成功解决后，根据思维链和理解在合成冷启动数据上对模型进行微调。
- 然后模型进入强化学习阶段，构建非形式化推理和形式证明构造的能力。
- 使用二元正确性或侧反馈作为奖励监督的主要形式。
- 这种训练方法解决了大语言模型在形式定理证明中的数据不足问题通过生成大量高质量的证明数据来训练模型。
性能表现
DeepSeek Prover V2 在数学问题上表现出色，甚至被称为“碾压”其他模型。它在各种数学基准测试上取得了最先进的 (state-of-the-art)成果。
- 在mini F2F 测试集上，DeepSeek Prover V2 达到了惊人的88.9% 的通过率，这显著优于 GPT-4 (75.2%)、Claude (71%) 和 Gemini (68%)，以及之前的最佳水平 (63%)。
- 在正式定理证明的 658 个挑战性问题中，它解决了其中的49 个，准确率达到 49.8%。
- 它在 Putnham bench 和 Amy 24、25 问题的形式化版本上表现出色。
- 有博主进行数学能力测评，使用了15 道具有难度并涵盖不同领域的数学题，包括代数、几何、微积分、数论、线性代数、组合博弈论等。输入部分复杂公式时使用了 LaTeX 语法。在这次测试中，DeepSeek Prover V2只错了 3 个。对于大多数题目，模型都能给出详细的解题步骤，例如在弹珠比例、两整数乘积与差、阶乘倍数、巧克力工厂打包、画框面积、代币游戏、丢番图方程求值、对数方程求值、定积分计算等问题上给出了正确答案和详细分析。虽然在矩形网格染色、全一矩阵平方、围成一圈的孩子与数字牌问题上出现了错误，但在丢番图方程等问题上展示了类似思维链的推理方式。总的来说，通过测试发现，DeepSeek Prover V2 在数学方面的能力确实有了非常大的提升。
- 它能生成 LaTeX 格式的证明。有作者检查了生成的 LaTeX 证明并认为它是正确的。有时模型生成的内容感觉像是在交流，但最终仍能生成正确的 LaTeX 证明代码。
此外，还测试了PCH（Proof Collection from Highschool）数据集，包含 325 个问题，其中包括 15 个高中竞赛水平的挑战以及 310 个多样的教学数学问题集。
应用领域与未来潜力
DeepSeek Prover V2 的用途广泛且重要。
- 学术研究：帮助数学家探索新理论、自动生成和验证形式证明、加速数学发现、提高研究效率。
- 软件验证：增强关键软件系统的形式验证。
- 错误检测和修正：在数学证明中识别和纠正逻辑错误。
- 教育学习：为学生和数学家提供详细的分步解释，帮助他们学习和提高。由于模型能提供完整的解题步骤，使用 DeepSeek Prover V2 来辅助学习数学非常有帮助。
- 更广泛的用途：可作为问题解决助手/导师，帮助解决各种难题，甚至对编程/编码有帮助，适用于更广泛的思维和推理任务。AI 进行数学工作可能会帮助 AI 自身改进。模型在生成数学合成数据方面也有很大潜力。
结语
总之，DeepSeek Prover V2 是一款强大的、开源的、免费的数学推理和形式定理证明模型。它在相关基准测试中取得了显著超越现有模型的优秀成绩，并具有广泛的学术和潜在的日常应用价值。DeepSeek 专注于工作成果而非市场宣传的方式也为其赢得了赞赏。社区对 DeepSeek 未来的模型（如 R2 或 V4）以及相关的研究论文充满期待。
Let's Make AGI Real 
留下评论