⏶15
DeepTheorem：通过自然语言和强化学习提升LLM用于定理证明的推理能力
发表
由 
Jiahao Xu 提交
Jiahao Xu 提交作者: 
Ziyin Zhang, Jiahao Xu, Zhiwei He, Tian Liang, Qiuzhi Liu, Yansi Li, Linfeng Song, 
Zhengwen Liang, Zhuosheng Zhang, Rui Wang, Zhaopeng Tu, Haitao Mi, Dong Yu
Ziyin Zhang, Jiahao Xu, Zhiwei He, Tian Liang, Qiuzhi Liu, Yansi Li, Linfeng Song, Zhengwen Liang, Zhuosheng Zhang, Rui Wang, Zhaopeng Tu, Haitao Mi, Dong Yu摘要
定理证明是评估大型语言模型 (LLM) 复杂推理能力的重要测试平台。然而，传统的自动化定理证明 (ATP) 方法严重依赖形式化证明系统，这与 LLM 在预训练期间从非正式、自然语言知识中获得的优势不符。在这项工作中，我们提出了 DeepTheorem，这是一个利用自然语言增强 LLM 数学推理的综合性非正式定理证明框架。DeepTheorem 包含一个大规模基准数据集，由 12.1 万个高质量 IMO 级别的非正式定理和证明组成，涵盖不同的数学领域，并经过严格的正确性、难度和主题类别标注，同时附带系统构建的可验证定理变体。我们设计了一种专门针对非正式定理证明的新型强化学习策略 (RL-Zero)，利用可验证定理变体来激励鲁棒的数学推理。此外，我们提出了全面的结果和过程评估指标，用于检查证明的正确性和推理步骤的质量。广泛的实验分析表明，与现有数据集和有监督微调协议相比，DeepTheorem 显著提高了 LLM 的定理证明性能，达到了最先进的准确性和推理质量。我们的研究结果强调了 DeepTheorem 在从根本上推进自动化非正式定理证明和数学探索方面的潜力。
🚨 隆重推出 DeepTheorem：革新 LLM 数学推理！🚀
要点速览：
🌟 通过探索学习是近期零训练强化学习（RL-zero training）教给我们的最重要的理念，因为自我探索显著提高了 LLM 预训练知识的利用率；
🧐 既然 LLM 预训练中包含了大量的数学定理知识，那么 LLM 能否通过自我探索学习定理证明呢？
🤯 我们展示了，使用我们的高质量深度定理数据集进行在线强化学习（RL learning）足以激活 LLM 的定理证明能力。我们的 7B 模型甚至可以超越 Gemini 和 Claude 3.5 等先进模型！更重要的是，我们不需要任何定理证明标注，您只需要定理本身的真值即可。