DeepTheorem：腾讯突破性研究如何通过自然语言和强化学习提升大模型定理证明能力

在机器智能的历史长河中，数学定理证明一直是检验人工智能系统推理能力的终极试金石。2025年5月29日，来自腾讯和上海交通大学的研究团队在arXiv上发表了题为《DeepTheorem: 通过自然语言和强化学习推进大型语言模型的定理证明推理》的研究论文，为这一领域带来了重要突破。这项由张子寅、徐嘉浩（通讯作者）、何志伟等研究人员主导的工作，提出了一种全新的非形式化定理证明框架，该论文已发布在GitHub (https://github.com/Jiahao004/DeepTheorem) 和Hugging Face (https://huggingface.co/datasets/Jiahao004/DeepTheorem)上。

想象一下数学家如何证明定理：他们通常使用自然语言和数学符号，在草稿纸上勾画思路，逐步形成严谨的推理链。而传统的自动化定理证明系统却要求使用非常严格的形式化语言，如Lean、Coq或Isabelle这样的证明助手系统，这与大型语言模型（LLMs）在预训练阶段学到的知识类型存在巨大鸿沟。这就像强迫一个在中文环境长大的人突然用古希腊语写诗一样困难。

DeepTheorem项目就像是在搭建一座桥梁，让语言模型能够用它们最擅长的方式——自然语言——来进行数学定理证明。研究团队构建了一个包含12.1万个高质量非形式化定理和证明的大规模数据集，这些定理难度可媲美国际数学奥林匹克（IMO）水平。更令人兴奋的是，他们开发了一种创新的强化学习策略（RL-Zero），专门针对非形式化定理证明进行优化。

简单来说，这项研究就像是教会了AI用"人类数学家的思维方式"而非"计算机程序员的思维方式"来解决复杂的数学问题。接下来，让我们深入了解这项突破性工作的细节，看看它如何改变AI数学推理的未来。

一、为什么定理证明对大型语言模型如此重要？

想象你正在教一个孩子学习数学。一开始，你可能会教他简单的加减法；随着他的成长，你会引入更复杂的概念，如代数和几何。最终，当他能够证明复杂的数学定理时，你才会说他真正掌握了数学推理能力。类似地，定理证明已成为评估人工智能系统推理能力的"奥林匹克比赛"。

在人工智能领域，定理证明被视为检验复杂推理能力的最高标准之一。它要求AI同时掌握抽象思维、战略推理、模式识别和精确的逻辑推导能力。近年来，随着深度学习特别是大型语言模型（LLMs）的进步，自动化定理证明（ATP）领域发生了翻天覆地的变化。

然而，传统的ATP方法面临一个根本性问题：它们主要依赖Lean、Coq和Isabelle等形式化证明系统，或来自ProofWiki的特定领域语言。这些系统要求使用高度结构化、严格的形式语言，而这与大型语言模型在预训练过程中接触到的自然语言和LaTeX数学文本有着本质区别。

这种不匹配就像要求一个熟悉中餐烹饪的厨师突然制作精致的法式甜点，而且不允许他查看食谱——即使他有出色的烹饪天赋，也会因为工具和技巧的差异而表现不佳。同样，当语言模型被迫使用形式化语言进行定理证明时，它们的真实能力受到了严重限制。

腾讯和上交大的研究团队意识到，如果想要充分发挥大型语言模型在数学推理方面的潜力，必须创建一个与它们预训练知识相匹配的框架。这就是DeepTheorem项目的核心理念：不是强迫语言模型适应形式化证明系统，而是设计一个框架，让它们能够使用自然语言进行数学推理，就像人类数学家那样。

研究团队的方法包含三个关键要素：首先，构建一个大规模的非形式化定理证明数据集；其次，开发一种专门针对非形式化定理证明的强化学习策略；最后，设计全面的评估指标来衡量证明的正确性和推理过程的质量。

这种自然语言驱动的方法不仅更符合语言模型的预训练知识，还提供了更大的灵活性和可扩展性。它允许AI系统采用更接近人类数学家的启发式思维方式，而不是受限于严格的形式化规则。

二、DeepTheorem数据集：为何它如此与众不同？

想象你正在教一个学生学习烹饪。你可以给他一本只有几道简单菜谱的食谱书，或者提供一本包含成百上千种不同难度和风格菜肴的百科全书式烹饪指南。显然，后者能让学生接触到更广泛的技巧和知识。DeepTheorem数据集就像是这样一本全面的"数学烹饪指南"，涵盖了从基础数学"菜肴"到高级"大师级配方"的各种定理。

DeepTheorem数据集包含约12.1万个经过精心挑选的非形式化数学定理和高质量证明，其规模远超现有的类似数据集。如图1(a)所示，DeepTheorem的规模明显超过了Lean-Workbook、Deepseek-Prover-v1的训练语料库和OpenR1-Math中的定理。

但这个数据集的价值不仅仅在于它的规模。以下几个特点让它在数学推理训练资源中脱颖而出：

首先，DeepTheorem的每一条数据都像一幅完整的画卷，包含定理本身、相应的证明、正确性标签（真或假）、难度评分（例如，1到10分的精细难度评分）和主题分类（如数论、几何等）。这就像每道菜谱不仅告诉你材料和步骤，还标明了难度级别、烹饪风格和可能的变化。

其次，这些定理的难度水平非常高，大多集中在6-9级（满分10级），与国际数学奥林匹克（IMO）级别的挑战相当。如图3所示，DeepTheorem在高难度定理上的比例远高于其他数据集，这使它能够真正挑战和提升AI系统的数学推理能力。

第三，数据集的主题覆盖面非常广泛。如图4所示，DeepTheorem涵盖了代数、离散数学、应用数学、微积分、几何、数学分析、数论等众多数学领域。这种多样性确保了训练出的模型不会只擅长特定类型的数学问题，而是能够处理整个数学领域的各种挑战。

第四，DeepTheorem经过严格的除污处理，避免与广泛使用的基准测试集重叠。研究团队实施了一个严格的三步流程：首先使用嵌入模型生成所有定理语句的句子嵌入；然后计算训练样本与所有测试样本的嵌入余弦相似度；最后使用GPT-4o评估召回的测试样本是否在当前训练样本中被污染。这个过程移除了约19.9万个污染样本，有效识别了相同案例、泛化问题和逆定理。

最后，数据集中的证明由o3-mini生成，经过了精心调整，专为监督微调（SFT）量身定制。这些证明提供了完成证明所需逻辑步骤的简洁而完整的概述，以清晰和简洁为重点。这些用LaTeX表达的证明与LLM的非形式化性质相一致，使它们成为有效的学习信号。

构建这个庞大数据集的过程也十分复杂。如图5所示，研究团队从多个来源聚合原始数据，包括MMIQC、WebInstruct和NuminaMath-CoT。然后通过一系列处理步骤，包括除污、质量控制、证明生成、逻辑验证、难度标注和单一语句过滤，最终得到了121K高质量的挑战性定理。

三、通过强化学习进行定理证明：突破传统限制

传统上，非形式化定理证明数据集主要通过监督微调（SFT）来使用，AI模型通过模仿数据集中的例子来学习生成证明。然而，最近关于RL-Zero的研究表明，这种方法可以通过利用基础模型的预训练知识和探索能力在SFT之上取得更好的性能。

这就引出了一个自然的问题：我们能否利用基础模型的探索能力来进行非形式化定理证明？研究团队探索了将RL-Zero应用于非形式化定理证明的可能性，并取得了令人瞩目的成果。

整个过程可以分为三个关键步骤：1）数据增强，生成用于二元奖励的矛盾定理变体；2）使用GRPO算法进行RL-Zero训练；3）评估定理-证明生成。

**可验证奖励的定理变体**

为了构建适用于RL-Zero的带奖励的定理，研究团队做出了一个关键观察：定理陈述不必是正确的，也可以被证明是错误的，这使得可以构建一个与RL-Zero兼容的二元奖励结构。

这一发现允许他们将DeepTheorem的定理转化为真或假的变体，促进强化学习训练，鼓励稳健的推理。具体来说，研究团队使用LLM扩展原始定理为可以被反驳的矛盾变体。

例如，考虑下面三个定理变体（为简洁起见省略假设）： - 原始定理：x > 1 - 变体1：x > 0 - 变体2：x < 1

如果原始定理可以被证明，变体1也是正确的，可以用与原始定理相同的方式进行数学证明，而变体2必然是错误的，可以被反驳。

通过这种逻辑上蕴含或矛盾的转换，研究团队能够构建保证正确或错误的定理变体，而只需访问定理本身而不是证明过程。这使得这个转换任务比注释新的数学陈述要容易得多，从而允许相对较弱的LLM（如Qwen2.5-72B-Instruct）来执行它。经过这个扩展阶段，研究团队进一步注释了结果定理池的完整性，最终获得了一个包含24.2万个数学定理的训练集，这些定理可以被证明或反驳，每个都有完整的证明轨迹。

**二元奖励激活定理证明生成**

有了上述定理变体，研究团队现在可以将强化学习应用于自然语言定理证明。具体来说，他们采用了GRPO算法。

受到R1等推理专用模型成功的启发，研究团队在系统提示中鼓励模型在 标签中封闭其推理过程，以激励更详细的推理行为，然后要求模型以"\boxed{proved}"或"\boxed{disproved}"结束每个证明。在奖励函数中，他们提取这个答案并将其与真实情况进行比较，如果答案匹配则给予1的奖励，否则给予0。

他们还强制执行几项健全性检查以防止模型崩溃：如果模型解决方案中的空白比例低于0.05或平均字符重复计数大于300，则无论答案如何都会发出0的奖励。

**评估方法**

用于评估的定理证明问题来自两个具有挑战性的基准测试——FIMO和Putnam——以及新构建的HMMT定理证明子集。研究团队手动扩展了这三个数据源中的每个问题，生成多个蕴含或矛盾的变体，结果基准如表3所示。

对于结果评估，研究团队提出了一个新颖的评估框架，利用从每个定理派生的多个蕴含和矛盾变体。通过评估模型在这些变体上一致分配正确真值的能力，他们间接估计了其定理证明能力。当变体数量足够大时，这种方法为评估非形式化证明的正确性提供了一个稳健的代理。

对于过程评估，研究团队开发了一个框架，评估证明质量的四个维度： - 逻辑有效性：检查每一步是否从前一步逻辑上推导出来 - 完整性：验证是否包含证明定理所需的所有必要情况和步骤 - 正确性：确认最终结论是否正确 - 清晰度：评估证明是否清晰、明确和解释得当

四、实验结果：DeepTheorem如何改变游戏规则？

研究团队进行了一系列实验，以评估DeepTheorem数据集和RL-Zero训练方法的有效性。他们训练了两组模型，一组使用监督微调（SFT），另一组使用零强化学习（RL-Zero），两组都从Qwen2.5-Base开始。

对于SFT，他们在数据集中的完整证明解决方案上训练模型3个周期。对于RL-Zero，他们采用GRPO算法，批量大小为128，组大小为64，最大推出长度为8192。他们训练模型1000步，并在训练期间将每个模型分布在两台机器上。

作为基线，他们选择了OpenR1-Math的定理证明子集，这是现有的最高质量定理证明数据集，具有完整的问题和回答。他们对其应用与2.1节详述的相同处理流程，这产生了总共66K原始定理和130K变体。

**主要结果**

如表4所示，DeepTheorem在OpenR1-Math-Proof上展示了优越的性能，特别是对于7B骨干和过程评估方面。另一方面，RL-Zero训练范式始终优于SFT，验证了RL-Zero在推动模型的推理能力超越SFT限制方面的有效性。

特别令人印象深刻的是，在7B模型上使用DeepTheorem进行RL训练（称为DeepTheorem-RL-7B）在FIMO基准上达到了55.56%的准确率，在HMMT基准上达到了28.81%的准确率，在Putnam基准上达到了57.29%的准确率。这些结果显著优于使用相同架构但用OpenR1-Proof训练的模型。

**与最先进模型的比较**

在表5中，研究团队还提供了最先进LLM在三个基准上的评估结果。这些结果表明，定理证明，特别是他们新构建的HMMT基准，对LLM仍然是相当具有挑战性的。另一方面，他们的7B模型，用DeepTheorem上的RL-Zero训练，优于大得多的SOTA模型，包括那些专门用于数学和推理的模型，展示了DeepTheorem和他们创新的结果监督RL训练方法对定理证明的卓越质量。

**参数效率**

图7展示了DeepTheorem-RL策略如何实现强大的参数效率。与作为骨干模型的Qwen2.5系列相比，在1.5到7B模型上训练DeepTheorem显著提高了参数-性能空间中的非形式化定理证明边界。此外，DeepTheorem参数效率也超过了SOTA商业模型，如o1和o3-mini。

**分析：RL-Zero与DeepTheorem激活骨干模型的定理证明能力**

为了更深入地理解DeepTheorem-RL训练模型的能力，研究团队提供了一个案例研究，分析了由其模型生成的证明。他们选择了一个涉及多项式和固定点的复杂问题。模型成功地识别了问题的核心，正确地分析了Q(x)的性质（它是P应用k次的结果），并准确地推断出Q(x)不可能有超过n个整数固定点。

该证明展示了模型在处理复杂的多项式组合和理解迭代性质方面的能力，突显了它对这类问题的深刻理解。该模型正确地识别了关键观察点，即整数固定点的数量受到多项式预周期点数量的限制，并基于此得出正确的结论。

在图8中，研究团队还可视化了他们的7B模型在DeepTheorem上进行RL训练时使用的证明技术分布。直接证明最常用，其次是穷举证明和构造证明。这表明模型已经学会了应用多种证明策略，适应不同类型的数学问题。

五、结论：DeepTheorem如何改变AI数学推理的未来？

归根结底，DeepTheorem项目代表了AI数学推理领域的重要里程碑。通过创建一个利用自然语言进行数学推理的框架，研究团队成功解决了传统ATP方法与大型语言模型预训练知识之间的不匹配问题。

这项工作的核心贡献包括： - 一个包含12.1万个IMO级别非形式化数学定理和相应高质量证明的大规模自然语言数据集，这些定理经过系统标注，包括正确性、难度、主题多样性，并包含适用于高级强化学习的可验证定理变体。 - 一种专门为非形式化定理证明设计的新型RL-Zero训练方法，显著增强了LLM的推理能力，超越了传统SFT方法。 - 全面的评估框架，评估定理证明的正确性（结果评估）和生成的推理过程的完整性、逻辑有效性和正确性（过程评估）。

通过广泛的实验，研究团队确立了DeepTheorem范式的优越性，实现了最先进的性能，超越了现有的非形式化定理数据集和训练方法。

这项研究的意义远远超出了数学领域。通过改进AI系统进行复杂推理的能力，DeepTheorem为更广泛的问题解决应用铺平了道路。随着AI系统变得越来越擅长数学推理，我们可以期待它们在科学发现、工程优化和其他需要严格逻辑思维的领域做出更大贡献。

对于普通人来说，这项研究的意义在于，它使AI系统更接近于以人类可以理解和验证的方式解决复杂问题。通过使用自然语言而非形式化语言，DeepTheorem创建的AI系统将更容易与人类协作，可能成为从学生到研究人员等各类用户的强大工具。

未来的研究方向可能包括将DeepTheorem框架扩展到其他推理领域，开发更先进的非形式化证明验证技术，以及探索如何将自然语言证明与形式化证明系统结合起来，获得两者的优势。

对于那些想要深入了解这项研究的读者，完整论文可在arXiv上获取，代码和数据集可通过GitHub和Hugging Face访问。随着这些资源的公开，我们期待看到社区如何构建和扩展这项开创性工作。