量子位
·
DeepSeek新数学模型刷爆记录！7B小模型自主发现671B模型不会的新技能
内容提要
DeepSeek推出的Prover-V2模型专注于数学定理证明，刷新多项基准测试记录。该7B模型成功解决了671B模型未能解决的问题，展现出独特的推理模式。Prover-V2结合强化学习与子目标分解，提升了形式化与非形式化证明的能力，标志着数学领域的重要进展。
关键要点
-
DeepSeek推出的Prover-V2模型专注于数学定理证明，刷新多项基准测试记录。
-
Prover-V2模型成功解决了671B模型未能解决的问题，展现出独特的推理模式。
-
该模型结合强化学习与子目标分解，提升了形式化与非形式化证明的能力。
-
Prover-V2在普特南测试中解决了13个671B模型未能解决的问题。
-
DeepSeek-Prover系列模型已推出3款，分别为Prover-V1、Prover-V1.5和Prover-V2。
-
Prover-V2提出了“子目标分解的强化学习”，并整合了DeepSeek-V3的高上下文窗口和自然语言推理能力。
-
模型通过递归证明搜索合成冷启动推理数据，减轻计算负担。
-
使用合成冷启动数据进行子目标分解的强化学习，构建完整的形式化证明。
-
DeepSeek-Prover-V2采用两阶段训练，第一阶段聚焦快速生成Lean证明代码，第二阶段提升复杂问题推理能力。
-
Prover-V2在miniF2F测试中的通过率达到88.9%，并解决了普特南测试中的49道问题。
-
与Prover-V2一起推出的ProverBench包含325个问题，旨在评估高中竞赛和本科阶段数学问题。
-
Prover-V2的作者团队包括多位参与过前作的研究者，论文发布后引发社区关注。
延伸问答
DeepSeek-Prover-V2模型的主要功能是什么？
DeepSeek-Prover-V2模型专注于数学定理证明，刷新了多项基准测试记录。
Prover-V2与671B模型相比有什么优势？
Prover-V2成功解决了671B模型未能解决的13个问题，展现出独特的推理模式。
DeepSeek-Prover-V2是如何提升证明能力的？
该模型结合了强化学习与子目标分解，提升了形式化与非形式化证明的能力。
Prover-V2的训练过程是怎样的？
Prover-V2采用两阶段训练，第一阶段聚焦快速生成Lean证明代码，第二阶段提升复杂问题推理能力。
ProverBench包含哪些类型的问题？
ProverBench包含325个问题，其中包括高中竞赛和本科阶段的数学问题。
DeepSeek-Prover-V2的作者团队有哪些背景？
Prover-V2的作者团队包括多位参与过前作的研究者，且有新成员加入，背景多样。
