主要证据
- DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal DecompositionS1 · 主要研究来源 · 论文 · 2025-04-30
- DeepSeek-Prover-V2 models, benchmark and solution artifactsS1 · 主要研究来源 · 代码仓库
DeepSeek-Prover-V2 将非形式子目标分解与 Lean 强化学习结合
DeepSeek-V3 先把问题分解为子目标，成功的子目标证明被整理为强化学习的冷启动推理轨迹。
发生了什么？
DeepSeek-Prover-V2-671B 报告 miniF2F-test 88.9%，并解出 PutnamBench 658 题中的 49 题。
为什么重要？
该设计把非形式规划显式变成高容量形式定理证明器的训练脚手架。
重要性说明：DeepSeek-Prover-V2 在更大规模上连接自然语言推理与形式证明生成，缩小两者能力差距。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 非形式化, 形式化, 混合
- AI 贡献
- 模型分解问题、生成 Lean 证明，并通过验证器反馈强化学习提升能力。
- 人类贡献
- 研究者设计递归数据生成、子目标分解与强化学习训练。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- deepseek-prover-v2, lean
- 机构
- deepseek
- 数学问题
- minif2f, putnambench, proverbench
- 方法
- subgoal-decomposition, reinforcement-learning, formal-proof
全部来源与工件
- DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal DecompositionS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- DeepSeek-Prover-V2 models, benchmark and solution artifactsS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-11
验证历史
- 2025-04-30 · 论文已发布 · E2 · 研究记录
Chronicle 依据所引 primary / official source 记录该事件；该状态不表示 Chronicle 已完成独立验证。
- 2026-09-11 · 论文已发布 · E3 · 可检查工件
本轮 corpus 刷新增补了由作者或发布机构维护、可直接检查的公开产物。E3 表示证据已达到可检查 artifact 层级，并不等同于底层科学或数学主张已获得独立验证。
更正
当前没有记录的更正。