DeepSeek-Prover-V1.5 - 70亿参数的开源数学大模型

DeepSeek-Prover-V1.5是什么

DeepSeek-Prover-V1.5是DeepSeek团队开发的开源数学大模型，参数量为70亿。它把强化学习（RLPAF）和蒙特卡洛树搜索（特别是RMaxTS变体）结合起来，数学定理证明的效率和准确率都有提升。高中和大学级别的数学题上，DeepSeek-Prover-V1.5在Lean 4平台的表现超过了其他开源模型，刷新了当时的SOTA。除了验证已有的证明，它也有潜力帮忙发现新的数学知识，把数学研究往“大数学”时代推一把。

DeepSeek-Prover-V1.5的主要功能

• 强化学习优化：模型用的是基于证明助手反馈的强化学习（RLPAF），把Lean证明器的验证结果当作奖励信号，用来优化证明生成的过程。
• 蒙特卡洛树搜索：引入RMaxTS算法——蒙特卡洛树搜索的一个变体，专门对付证明搜索里奖励稀疏的问题，让模型更愿意去探索。
• 证明生成能力：模型能生成高中和大学级别的数学定理证明，成功率比之前高了不少。
• 预训练与微调：先在高质量数学和代码数据上做预训练，再针对Lean 4代码补全数据集做监督微调，形式化证明的能力就是这么练出来的。
• 自然语言与形式化证明对齐：借助DeepSeek-Coder V2，在Lean 4代码旁边标注自然语言思维链，把自然语言推理和形式化定理证明连在一起。

DeepSeek-Prover-V1.5的技术原理

• 预训练（Pre-training）：DeepSeek-Prover-V1.5又在数学和代码数据上做了一轮预训练，重点放在Lean、Isabelle和Metamath这些形式化数学语言上，目的是加强形式化定理证明和数学推理的能力。
• 监督微调（Supervised Fine-tuning）：这里用了数据增强：在Lean 4代码旁边加上自然语言的思维链注释，同时在证明代码里插入中间策略状态信息，让模型更能对上自然语言和形式化证明之间的对应关系。
• 强化学习（Reinforcement Learning）：用GRPO算法做基于证明助手反馈的强化学习，Lean证明器的验证结果就是奖励信号，模型因此被进一步往形式化验证系统的要求上靠。
• 蒙特卡洛树搜索（Monte-Carlo Tree Search, MCTS）：这里引入了一种新的树搜索方法：靠截断和重新开始，把不完整的证明拆成树节点序列，再从这些节点接着往下生成证明。
• 内在奖励驱动的探索（Intrinsic Rewards for Exploration）：靠RMaxTS算法，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

• 环境配置：先把必要的软件和依赖装好，比如Lean证明助手，还有可能用到的编程语言环境。
• 获取模型：从DeepSeek-Prover-V1.5的GitHub仓库，克隆或下载模型的代码库到本地。
• 模型安装：照着安装指南装模型，可能涉及编译代码、装Python库或者其他依赖。
• 数据准备：准备好要证明的数学问题和定理描述，格式得按规范写，模型才读得懂。
• 交互界面：通过命令行界面，或者图形界面（如果有）跟模型交互，把数学问题或定理输进去。
• 证明生成：跑一下模型，让它处理刚才输入的问题，它会尝试给出完整证明，或者列出证明步骤。

DeepSeek-Prover-V1.5的应用场景

• 数学研究：数学家和研究人员探索新理论、新证明时，可以用它快速验证和生成复杂的数学证明。
• 教育领域：高等教育里，学生可以借它弄懂定理的证明过程，数学推理能力也能跟着练。当教学工具用，练习题的证明步骤能自动生成，学生拿去对照学习。
• 自动化定理证明：形式化验证领域，DeepSeek-Prover-V1.5可以用来自动证明数学软件和系统的正确性。
• 软件开发：接进软件开发流程里，帮开发人员弄清算法背后的数学依据，也能做验证。