量子位
·
DeepSeek新数学模型刷爆记录！7B小模型自主发现671B模型不会的新技能
💡
原文中文，约4200字，阅读约需10分钟。
📝
内容提要
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的作者团队包括多位参与过前作的研究者，论文发布后引发社区关注。
➡️
