DeepSeek开源数学大模型，高中、大学定理证明新SOTA
内容提要
DeepSeek-Prover-V1.5是一个结合了强化学习和蒙特卡洛树搜索的证明生成模型，提高了证明生成的效率和准确性。该模型在Lean 4的形式定理证明中表现优于其他开源模型。它采用了统一的方法，结合了证明步骤生成和整体证明生成，并且通过截断和恢复机制无缝地集成了中间策略状态。该模型还利用了无奖励探索算法和新的蒙特卡洛树搜索算法来提高证明搜索效率。评估结果显示，DeepSeek-Prover-V1.5在miniF2F和ProofNet数据集上相比之前的模型实现了更高的通过率。
延伸解读
统一证明生成与步骤生成的优势
DeepSeek-Prover-V1.5通过截断和重新开始机制，将完整证明生成的高效性与证明步骤生成的精确性相结合。当完整证明出现错误时，模型从首个错误处截断，并利用Lean证明器的状态作为提示继续生成，从而减少错误累积。这种方法在保持计算效率的同时，提升了证明的准确性，为形式化定理证明提供了新思路。
强化学习与树搜索的协同创新
模型采用基于证明助手反馈的强化学习（RLPAF）和RMaxTS算法，解决了奖励稀疏问题。RLPAF利用Lean验证器的二元奖励信号，而RMaxTS通过内在奖励鼓励探索多样化的证明路径。这种协同作用使模型在miniF2F和ProofNet数据集上实现了更高的通过率，展示了结合外部验证与内在探索的有效性。
性能突破与效率提升
DeepSeek-Prover-V1.5在miniF2F测试集上达到60.2%的通过率，结合树搜索后提升至63.5%；在ProofNet测试集上达到25.3%。值得注意的是，它仅需3200次完整证明采样就能达到54.9%的通过率，超过了之前需要大量树搜索的模型。这表明该模型在效率和准确性上均取得了显著进步，为形式化数学证明设定了新标杆。
对数学AI发展的意义
陶哲轩指出，AI将加速形式化证明的编写，开启“大数学”时代。DeepSeek-Prover-V1.5作为开源模型，在高中和大学水平的定理证明中达到新SOTA，降低了形式化证明的门槛。其公开的代码和模型有望促进更多研究，推动AI与数学的深度协作，但实际应用仍需进一步验证其泛化能力。
Q&A
DeepSeek-Prover-V1.5的主要创新是什么？
DeepSeek-Prover-V1.5结合了强化学习和蒙特卡洛树搜索，显著提升了证明生成的效率和准确性。
DeepSeek-Prover-V1.5在形式定理证明中表现如何？
DeepSeek-Prover-V1.5在Lean 4的形式定理证明中优于其他开源模型，达到了新的SOTA水平。
陶哲轩对AI在数学中的看法是什么？
陶哲轩认为AI将加速形式化证明的编写，开启一个大数学时代。
DeepSeek-Prover-V1.5如何提高证明生成的准确性？
该模型通过截断和恢复机制整合了证明步骤生成和完整证明生成的优势，并利用Lean证明器的反馈进行强化学习。
DeepSeek-Prover-V1.5在miniF2F和ProofNet数据集上的通过率是多少？
在miniF2F测试集上，DeepSeek-Prover-V1.5达到了60.2%的通过率；在ProofNet测试集上达到了25.3%。
DeepSeek-Prover-V1.5的参数规模是多少？
DeepSeek-Prover-V1.5是一个70亿参数的开源模型。
