开源数学大模型DeepSeek-Prover-V1.5问世，或将推动数学研究进入“大数学”时代
北京时间2024年8月28日 – DeepSeek团队近日发布了其最新研发的开源数学大模型DeepSeek-Prover-V1.5，该模型拥有70亿参数，在数学定理证明方面取得了显著的效率和准确性提升。DeepSeek-Prover-V1.5在Lean 4平台上的表现超越了其他所有开源模型，创造了新的最先进水平（SOTA）。
DeepSeek-Prover-V1.5的突破性进展在于其融合了强化学习（RLPAF）和蒙特卡洛树搜索（RMaxTS变体）技术。通过结合这两种技术，模型能够有效地解决证明搜索中的奖励稀疏问题，并增强模型的探索行为。
DeepSeek-Prover-V1.5的主要功能包括：
- 强化学习优化：模型采用基于证明助手反馈的强化学习（RLPAF），通过Lean证明器的验证结果作为奖励信号，优化证明生成过程。
- 蒙特卡洛树搜索：引入RMaxTS算法，一种蒙特卡洛树搜索的变体，用于解决证明搜索中的奖励稀疏问题，增强模型探索行为。
- 证明生成能力：模型能生成高中和大学级别的数学定理证明，显著提高了证明的成功率。
- 预训练与微调：在高质量数学和代码数据上进行预训练，并针对Lean 4代码补全数据集进行监督微调，提升了模型的形式化证明能力。
- 自然语言与形式化证明对齐：用DeepSeek-Coder V2在Lean 4代码旁注释自然语言思维链，将自然语言推理与形式化定理证明相结合。
DeepSeek-Prover-V1.5的技术原理主要基于以下几个方面：
- 预训练：在数学和代码数据上进行进一步的预训练，专注于Lean、Isabelle和Metamath等形式化数学语言，以增强模型在形式化定理证明和数学推理方面的能力。
- 监督微调：使用特定的数据增强技术，包括在Lean 4代码旁边添加自然语言的思维链注释，以及在证明代码中插入中间策略状态信息，以此来提高模型对自然语言和形式化证明之间一致性的理解。
- 强化学习：采用GRPO算法进行基于证明助手反馈的强化学习，利用Lean证明器的验证结果作为奖励信号，进一步优化模型，使其与形式化验证系统的要求更加一致。
- 蒙特卡洛树搜索：引入了一种新的树搜索方法，通过截断和重新开始机制，将不完整的证明分解为树节点序列，并利用这些节点继续证明生成过程。
- 内在奖励驱动的探索：通过RMaxTS算法，DeepSeek-Prover-V1.5使用内在奖励来驱动探索行为，鼓励模型生成多样化的证明路径，解决证明搜索中的奖励稀疏问题。
DeepSeek-Prover-V1.5的应用场景十分广泛，包括：
- 数学研究：辅助数学家和研究人员在探索新的数学理论和证明时，快速验证和生成复杂的数学证明。
- 教育领域：在高等教育中，帮助学生学习和理解数学定理的证明过程，提高他们的数学推理能力。作为教学工具，自动生成练习题的证明步骤，提供给学生作为学习参考。
- 自动化定理证明：在形式化验证领域，DeepSeek-Prover-V1.5可以用于自动化地证明数学软件和系统的正确性。
- 软件开发：集成到软件开发流程中，帮助开发人员理解和验证算法的数学基础。
DeepSeek-Prover-V1.5的开源发布，将为数学研究和教育领域带来巨大的变革。它不仅能够验证现有证明，还有潜力帮助创造新的数学知识，推动数学研究进入“大数学”时代。
DeepSeek-Prover-V1.5的项目地址：
- 产品官网：deepseek.com
- GitHub仓库：https://github.com/deepseek-ai/DeepSeek-Prover-V1.5
- arXiv技术论文：https://arxiv.org/pdf/2408.08152
DeepSeek-Prover-V1.5的出现，标志着人工智能在数学领域应用的又一重大突破，也为未来数学研究的发展方向指明了新的路径。
Views: 0