DeepSeek开源数学大模型，高中、大学定理证明新SOTA

AIGC动态4个月前发布 almosthuman2014

795 0 0

文章摘要

【关键词】 AI数学、形式化证明、DeepSeek-Prover、强化学习、模型优化

数学家陶哲轩在牛津数学公开讲座中提出，人工智能（AI）与数学的结合将推动形式化证明的编写超越人类，这不仅将验证现有证明，还将创造新的数学知识。AI在形式化定理证明中的应用已成为数学家的日常操作，而AI科学家们正在努力提高AI在这一领域的性能和效率。DeepSeek-Prover-V1.5模型的推出正是这一努力的体现。

DeepSeek-Prover-V1.5是一个70亿参数的开源模型，它结合了强化学习（RLPAF）和蒙特卡洛树搜索（RMaxTS），在Lean 4的形式定理证明方面优于所有开源模型。技术报告详细介绍了该模型的架构和性能，指出其在处理复杂形式证明时的高效性和准确性。

报告概述了大型语言模型在数学推理和定理证明方面的发展，同时指出了现有模型在形式化定理证明方面的挑战。DeepSeek-Prover-V1.5通过截断和重新开始机制，结合了证明步骤生成和完整证明生成的优势，提高了模型的准确性和效率。

研究者提出了一个全面的框架，整合了大规模数学预训练、形式化数学语料库的构建和增强、基于证明助手反馈的在线强化学习，以及用于定理证明长期规划的树搜索方法论。这些组件的代码都已公开提供，以供进一步研究和应用。

在评估和度量方面，DeepSeek-Prover-V1.5在高中水平的miniF2F数据集和大学本科水平的ProofNet数据集上均展现出强大的性能。模型训练方面，研究者对基础模型进行了进一步预训练，并进行了监督微调，以提高生成形式证明和通过数学语言进行推理的能力。

基于证明助手反馈的强化学习阶段进一步增强了模型性能。研究者使用组相对策略优化（GRPO）算法，根据Lean 4证明器的验证反馈来优化模型。此外，研究者还引入了面向探索的蒙特卡洛树搜索，通过截断和重新开始机制，以及RMaxTS算法，解决了证明搜索中的奖励稀疏问题。

实验结果表明，DeepSeek-Prover-V1.5在定理证明能力上优于其他现有模型。在miniF2F和ProofNet基准测试中，该模型均达到了新的最佳水平。研究者还重新审视了训练策略在大规模采样中的效果，并通过消融实验检验了RMaxTS算法设计的有效性。

总体而言，DeepSeek-Prover-V1.5的推出标志着AI在形式化定理证明领域的重要进展，其结合了多种先进技术，提高了证明生成的效率和准确性，为数学家提供了一个强大的工具，有望推动数学知识的创造和发展。