DeepSeek-Prover-V1.5：一个拥有70亿参数的开源数学大模型

DeepSeek-Prover-V1.5简介

DeepSeek-Prover-V1.5 是一个开源的数学大模型，拥有70亿参数。专为 Lean 4 中的定理证明而设计。它通过结合强化学习和蒙特卡洛树搜索，显著提升了证明生成的效率和准确性 。该模型在高中和本科级别的基准测试中取得了新的最优结果，分别为 63.5% 和 25.3% 。DeepSeek-Prover-V1.5 的核心贡献包括一个全面的框架，用于开发基于语言模型的形式化数学证明工具，整合了大规模数学预训练、形式化数学语料库的构建和增强、基于证明助手反馈的在线强化学习，以及用于定理证明长期规划的树搜索方法论 。此外，相关的代码和数据集已经开源，以供进一步研究和应用 。

DeepSeek-Prover-V1.5主要功能

1. 定理证明自动化：能够在Lean 4环境中自动完成数学定理的证明过程。
2. 预训练与微调：在DeepSeekMath-Base上进行预训练，并针对形式化数学语言进行专业化的微调。
3. 强化学习优化：通过证明助手反馈进行在线强化学习，进一步提升证明生成的准确性。
4. 蒙特卡洛树搜索：集成了RMaxTS算法，用于在证明搜索中进行有效的探索和决策。
5. 多策略生成：结合了证明步骤生成和完整证明生成技术，提高了证明过程的灵活性和准确性。

DeepSeek-Prover-V1.5技术原理

1. 预训练：在高质量数学和代码数据集上进行预训练，增强模型对形式化数学语言的理解。
2. 监督式微调：使用形式化定理证明数据集对模型进行微调，提高代码完成能力。
3. 截断和恢复机制：在证明过程中，如果检测到错误，模型将截断错误部分并重新生成，以此提高证明的准确性。
4. 内在奖励驱动探索：RMaxTS算法通过内在激励（好奇心）来驱动搜索代理探索不同的证明路径。
5. 蒙特卡洛树搜索：使用MCTS算法进行长期规划，通过选择、扩展、模拟和反向传播四个步骤来优化证明搜索。
6. 并行化处理：实现了MCTS的并行化，显著提高了证明搜索的效率。
7. 策略混合：结合了非CoT（Chain of Thought）模式和CoT模式的提示，以利用各自的优势解决不同的问题。

DeepSeek-Prover-V1.5应用场景

1. 数学教育辅助：帮助学生理解复杂的数学证明过程，提供自动生成的证明步骤作为学习参考。
2. 研究助理：为数学研究者提供自动化的证明支持，节省研究过程中的时间和精力。
3. 编程语言开发：在开发如Lean 4这样的形式化验证编程语言时，辅助验证算法和数学基础。
4. 逻辑和计算机科学：在逻辑推理和计算机科学领域，用于形式化验证和逻辑推导。
5. 人工智能研究：作为AI研究的一部分，探索和提升机器理解与生成数学证明的能力。
6. 竞赛数学训练：在数学竞赛准备中，为参赛者提供自动化的解题策略和证明方法。

DeepSeek-Prover-V1.5项目入口

• GitHub代码库：https://github.com/deepseek-ai/DeepSeek-Prover-V1.5
• arXiv技术论文：https://arxiv.org/pdf/2408.08152