DeepSeek开源DeepSeek-Prover-V2

素材来源官方媒体/网络新闻

,

,

,

deepseek-ai/DeepSeek-Prover-V2-671B deepseek发了新模型\x0a\x0ahttps://huggingface.co/deepseek-ai/DeepSeek-Prover-V2-671B\x0a\x0aDeepSeek-Prover-V1.5：利用证明助手反馈进行强化学习和蒙特卡洛树搜索\x0ahttps://zhuanlan.zhihu.com/p/28837730298\x0a\x0aDeepSeek-Prover-V1.5通过预训练、监督微调和强化学习进行训练。在监督微调阶段，预训练模型接收一个以策略状态注释关键字结尾的不完整定理证明。模型被训练以预测该策略状态的内容（辅助目标）并补全后续的证明步骤（主要目标）。在强化学习阶段，给定一个不完整的定理证明和来自 Lean 验证器的真实策略状态，我们通过微调模型生成多个证明候选，然后由 Lean 验证器进行验证。这些候选的验证结果被用作二元（0-1）奖励，以进一步优化模型并增强其与验证系统形式化规范的对齐。在模型推理阶段，我们提供了两种选择：单遍采样和蒙特卡洛树搜索。