主要证据
- DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree SearchS1 · 主要研究来源 · 论文 · 2024-08-15
- DeepSeek-Prover-V1.5 repositoryS1 · 主要研究来源 · 代码仓库
DeepSeek-Prover-V1.5 结合证明助手反馈、强化学习与树搜索
该模型针对 Lean 4 形式数学进行专门训练，使用 Lean 反馈进行强化学习，并配合带内在奖励的蒙特卡洛树搜索变体探索多样证明路径。DeepSeek 公开了模型权重和复现实验的代码。
发生了什么？
DeepSeek-Prover-V1.5 通过证明助手反馈强化学习与 RMaxTS 证明搜索，在 miniF2F-test 上报告 63.5% 成功率，在 ProofNet 上报告 25.3%，较此前 DeepSeek-Prover 系列进一步提升。
为什么重要？
该系统清晰连接了静态证明生成与“面向形式验证器进行训练和搜索”的学习式 Agent，同时凭借较小规模与开放发布成为可广泛复用的研究基线。
重要性说明：DeepSeek-Prover-V1.5 将证明助手反馈直接用作强化学习训练信号，并与蒙特卡洛树搜索结合，同时公开 7B 模型和证明搜索实现。
历史脉络
证据与状态一览
- 重要性
- H2 · 领域里程碑
- 验证状态
- 论文已发布
- 证据等级
- E3 · 可检查工件
- AI 角色
- AI 主导、人类核验
- 形式保障
- 机器检查
贡献与验证
- 数学新颖性
- 基准结果
- 接口
- 形式化, 符号
- AI 贡献
- 语言模型生成 Lean 证明与树搜索动作，Lean 同时为训练和推理阶段提供正确性反馈与验证。
- 人类贡献
- 研究者构建形式训练数据，设计强化学习与 RMaxTS 流程，训练模型并选择评测协议。
- 验证状态
- 论文已发布 · E3 · 可检查工件 · 机器检查
- 最后审阅
- 2026-09-11
技术细节
- 系统
- deepseek-prover-v1-5, lean
- 机构
- deepseek-ai
- 数学问题
- minif2f, proofnet
- 方法
- reinforcement-learning-from-proof-feedback, monte-carlo-tree-search, formal-theorem-proving, proof-search
全部来源与工件
- DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree SearchS1 · 主要研究来源 · 论文 · 访问于 2026-09-10
- DeepSeek-Prover-V1.5 repositoryS1 · 主要研究来源 · 代码仓库 · 访问于 2026-09-10
验证历史
- 2024-08-15 · 论文已发布 · E2 · 研究记录
论文公开了训练方法与基准结果。
- 2024-08-15 · 论文已发布 · E3 · 可检查工件
模型权重、Lean 集成与证明搜索代码被公开发布。
更正
当前没有记录的更正。