基本信息

文件基本信息

名称

DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decomposition

首页

https://yiyibooks.cn/arxiv/2504.21801v2/index.html

原始地址

https://arxiv.org/pdf/2504.21801

描述

我们介绍了DeepSeek-Prover-V2，这是一种旨在正式定理的开源大语言模型，该模型在LEAN 4中证明，通过递归定理收集的初始化数据证明了由DeepSeek-V3供电的管道。冷启动训练程序首先促使DeepSeek-V3将复杂的问题分解为一系列子目标。解决的子目标的证明被合成为一个经过思考的过程，并结合了DeepSeek-V3的逐步推理，为增强学习创造了最初的冷启动 ...