华为诺亚方舟实验室新突破：让AI像数学家一样思考，自己设定小目标来证明定理

这项由华为诺亚方舟实验室的Matthieu Zimmer、Xiaotong Ji、Rasul Tutunov等研究人员联合帝国理工学院、UCL人工智能中心、华为拉格朗日中心共同完成的研究发表于2025年7月的arXiv预印本平台。有兴趣深入了解的读者可以通过arXiv:2507.02726v1访问完整论文。

当我们解决一道复杂的数学题时，很少会一步到位直接找到答案。更常见的做法是将大问题分解成几个小问题，一步步解决，最终达成目标。这正是人类数学家证明定理时的自然思路。然而，当前的人工智能在自动定理证明方面却往往采用"蛮力"搜索，就像无头苍蝇一样盲目尝试，效率极低。

研究团队意识到了这个问题的关键所在。在自动定理证明这个领域，AI面临着一个被称为"奖励稀疏"的挑战。这就好比在黑暗的迷宫中寻找出口，只有当你真正找到出口时才会有光亮指引，在此之前的所有探索都得不到任何反馈。对于AI来说，只有当它完整地证明了一个定理时才会获得"成功"的信号，而在漫长的证明过程中，它完全不知道自己是在朝着正确方向前进还是越走越远。

为了解决这个问题，研究团队开发了一个名为"自生成目标条件马尔科夫决策过程"的新框架，简称sG-MDP。这个拗口的名字背后其实是一个很直观的想法：让AI学会像人类数学家一样，在证明过程中自己设定中间目标，然后逐步实现这些小目标，最终完成整个证明。

传统的目标条件方法就像给学生一份详细的学习计划，告诉他每一步应该做什么。而这个新方法则更像是培养学生的自主学习能力，让AI自己判断在证明过程的每个阶段应该设定什么样的中间目标。当AI在证明一个复杂定理时，它会根据当前的证明状态动态地提出一些有用的子命题或引理，然后专注于证明这些中间步骤，从而获得更密集的反馈信号。

研究团队将这个理论框架具体应用到了Lean4这个形式化数学证明系统中。Lean4就像是数学界的"代码检查器"，它能够严格验证每一步推理是否正确，确保证明的绝对可靠性。在这个系统中，AI的"状态"就是当前的证明进度，"动作"包括两类：一类是执行具体的数学推理步骤（比如应用某个定理或公式），另一类是提出新的中间目标（比如"我先证明这个不等式成立"）。

为了在这个复杂的证明空间中高效搜索，研究团队采用了蒙特卡洛树搜索算法。这种算法就像是一个经验丰富的探险家，它会根据之前的探索经验来决定接下来应该往哪个方向深入探索。与传统方法不同的是，他们的搜索算法不仅仅以最终证明成功作为奖励，还会对每个被验证的中间命题给予奖励，这样AI就能得到更丰富的学习信号。

基于这个框架，研究团队开发了一个名为Bourbaki的具体系统。这个名字来源于20世纪法国的一个数学家团体，他们以严谨的公理化方法重构现代数学而闻名。Bourbaki系统的一个重要特点是它可以集成多个不同的大语言模型，让它们各自发挥优势。在实际实现中，研究团队将DeepSeek-Prover-v2-7B和Kimina-7B两个模型进行了组合，形成了Bourbaki 7B版本。

这种集成策略类似于组建一个专家团队来解决复杂问题。不同的模型可能在不同类型的推理上有各自的强项，通过协作可以弥补单个模型的不足。比如，一个模型可能擅长代数操作，另一个模型可能在几何推理方面更强，通过合理的任务分工可以显著提升整体性能。

研究团队在PutnamBench这个极具挑战性的数学竞赛数据集上测试了Bourbaki系统。Putnam数学竞赛被誉为北美最难的大学数学竞赛之一，其题目需要高度的创造性和复杂的多步推理。这个数据集包含了658个历年竞赛题目，每一个都是大学水平的高难度证明题，远超普通教科书练习的复杂程度。

实验结果令人振奋。Bourbaki 7B成功证明了26个定理，大幅超越了之前7B参数规模模型的最佳成绩。相比之下，此前的最强7B模型Kimina-7B只能解决10个问题，而DeepSeek-Prover-v2-7B在最好情况下也只能解决23个问题，而且需要更多的计算资源。这个结果不仅在数量上有显著提升，更重要的是展现了方法论上的优越性。

为了验证方法的普适性，研究团队还在其他基础模型上测试了sG-MDP框架。结果显示，无论是应用到STP模型还是DeepSeek-Prover-v2模型上，这个框架都能带来一致的性能提升。比如，在STP模型上，使用64次采样时原本只能解决6个问题，加入Bourbaki框架后能解决7个问题；使用128次采样时，从7个问题提升到8个问题。在DeepSeek-Prover-v2模型上，使用128次采样时从15个问题大幅提升到23个问题。

这种一致性的提升说明了sG-MDP框架的通用价值。它不是针对特定模型的定制化改进，而是一种可以广泛应用的方法论创新。这就像是发明了一种新的学习方法，不管是哪个学生使用都能提高学习效率。

除了解题数量的提升，Bourbaki系统还展现出了更好的证明多样性。对于同一个问题，它能够生成更多不同的正确证明路径。例如，在求解putnam_1990_a1这个问题时，DeepSeek-V2-7B只能生成1种正确证明，而Bourbaki能生成4种不同的证明；在putnam_2001_a1问题上，DeepSeek-V2-7B生成36种正确证明，Bourbaki则能生成105种。这种多样性不仅体现了系统的鲁棒性，也为数学教育和研究提供了更丰富的参考。

研究团队在实现过程中还遇到了一些有趣的技术挑战。他们发现有些模型会生成"启发式"策略，比如Lean4中的apply?命令，这个命令会自动尝试多种可能的证明步骤。这就像是一个"万能钥匙"，但它的结果具有一定的随机性。为了处理这种情况，研究团队采用了混合策略，在遇到这类命令时会调用基础模型来完成剩余的证明步骤。

在奖励函数的设计上，研究团队也进行了精心考虑。他们不仅奖励最终的证明成功，还对证明深度、解决的子命题数量等中间指标给予奖励。这种设计就像是在马拉松比赛中不仅关注最终成绩，还对通过每个检查点给予鼓励，这样能够更好地指导AI的探索方向。

从技术架构角度来看，Bourbaki系统使用了Pantograph作为与Lean4的交互接口。Pantograph提供了执行策略、跟踪依赖关系、管理目标状态等功能，同时解决了Lean特有的一些技术难题，比如元变量耦合问题。这个接口的设计支持子目标的独立执行和状态回溯，这对于实现蒙特卡洛树搜索算法至关重要。

在搜索算法的实现上，研究团队对传统的蒙特卡洛树搜索进行了专门的改进。他们的选择策略基于上置信界算法，平衡探索和利用；扩展策略会查询策略模型来建议候选动作，一旦验证有效就添加到搜索树中；估值策略会根据当前状态设置初始值；反向传播策略会更新从扩展节点到根节点路径上所有节点的访问计数和累积值。

这项研究的意义远不止于在一个特定数据集上取得好成绩。它代表了自动定理证明领域的一个重要方向转变：从盲目搜索转向结构化推理。传统的方法往往依赖大量的计算资源进行暴力搜索，而这种新方法通过模拟人类数学家的思维模式，能够更加高效和优雅地解决复杂问题。

从更广阔的视角来看，这种自生成目标的思想也可能对其他需要复杂推理的AI任务产生启发。无论是科学发现、工程设计还是战略规划，很多复杂任务都可以受益于这种将大目标分解为小目标的方法。

当然，这项研究也存在一些局限性和未来的改进方向。目前的系统主要在数学定理证明领域进行了验证，在其他形式推理任务上的表现还有待进一步探索。此外，如何更好地设计奖励函数、如何处理更复杂的子目标依赖关系、如何进一步提升搜索效率等问题都值得继续研究。

研究团队在论文中还提到了一些技术细节的处理。比如，他们使用vLLM来实现基础模型的高效批量生成，每个节点最多允许10个策略候选，最大迭代次数设为512。这些参数的设置都是通过实验优化得出的，体现了工程实现中的精细考量。

值得一提的是，这项研究采用了开放的实验设置，使用的基础模型和数据集都是公开可获得的，这为其他研究者复现和扩展这项工作提供了便利。这种开放性对于推动整个领域的发展具有重要意义。

说到底，这项研究最引人注目的地方在于它成功地将人类数学家的直觉思维模式转化为了可操作的AI算法。通过让AI学会自主设定中间目标，研究团队不仅解决了奖励稀疏的技术难题，更重要的是为AI推理能力的提升开辟了一条新的道路。这种方法论上的创新可能会对未来的AI系统设计产生深远影响，让机器能够更像人类一样进行复杂的逻辑推理和问题解决。

对于普通人来说，这项研究虽然看起来很技术化，但它实际上关系到AI能否在需要深度思考的任务上真正帮助人类。从自动化的数学证明到科学发现，从复杂系统的验证到教育辅导，这种能够进行结构化推理的AI系统将在越来越多的领域发挥重要作用。未来，当我们面对复杂问题时，也许真的可以依靠AI助手来帮我们分解问题、制定策略、逐步解决，就像有了一个永不疲倦的智能伙伴。

有兴趣深入了解这项研究技术细节的读者，可以通过arXiv平台访问完整论文，论文编号为arXiv:2507.02726v1。

Q&A

Q1：Bourbaki是什么？它能做什么？ A：Bourbaki是华为诺亚方舟实验室开发的AI数学定理证明系统。它的核心能力是像人类数学家一样，在证明复杂定理时自己设定中间小目标，然后逐步解决这些子问题，最终完成整个证明。它在PutnamBench数学竞赛数据集上成功证明了26个定理。

Q2：这项技术会不会让数学家失业？ A：目前不会。Bourbaki主要是在帮助验证和寻找数学证明，就像一个强大的计算工具。数学家的创造性思维、问题发现能力和数学直觉仍然是不可替代的。这项技术更可能成为数学家的得力助手，帮助处理繁琐的证明验证工作。

Q3：普通人能使用这个系统吗？ A：目前这还是一个研究阶段的系统，主要在学术环境中使用。不过随着技术发展，未来可能会出现基于类似原理的数学学习辅助工具，帮助学生理解复杂的数学证明过程或验证作业答案。