对 AI 研究者来说，数学既是一类难题，也是一个标杆，能够成为衡量 AI 技术的发展重要尺度。近段时间，随着 AI 推理能力的提升，使用 AI 来证明数学问题已经成为一个重要的研究探索方向。著名数学家陶哲轩就是这一方向的推动者，他曾表示：未来数学家可以通过向类似 GPT 的 AI 解释证明，AI 会将其形式化为 Lean 证明。这种助手型 AI 不仅能生成 LaTeX 文件，还能帮助提交论文，从而大幅提高数学家的工作效率和便利性。 

如今，已经诞生了 Gemini 2.0 Flash Thinking 和 o1/o3 等强大推理模型，那么用 AI 来进行形式化数学推理又已经走到了哪一步呢？ 

Meta FAIR 和斯坦福大学等多所机构的一篇新的立场论文（position paper）或许能为你给出这个问题的答案。 

论文标题：Formal Mathematical Reasoning: A New Frontier in AI

论文地址：https://arxiv.org/pdf/2412.16075

本文一作杨凯峪在 X 上表示，AI4Math 的下一步是使用证明助手等形式化系统来实现形式化数学推理。他也在推文以及论文中感谢了陶哲轩等数学家提供的反馈。 

Meta 研究科学家田渊栋也分享转发了这篇立场论文，并表示很期待看到 AI 能基于现有的互联网数据在数学阶梯上能到达何种高度。 

这篇论文的内容相当丰富，机器之心将在此介绍该论文的主要内容结构，尤其是该团队对多个相关研究方向的分级策略。这些分级可以帮助我们更好地界定 AI 在形式化数学推理方面的进展。下图为该综述的目录截图。 

自 AI 诞生之初，研究者就梦想着构建能够自动进行数学推理的 AI 系统。历史上，首个此类 AI 程序是 Newell 和 Simon 打造的 Logic Theorist（逻辑理论家），这个定理证明系统能够证明《数学原理》中的 38 条定理。 

自那之后已过去数十年，AI 的中心已经从符号方法转移到了机器学习，并出现了一个新领域：用于数学的统计式人工智能（AI4Math）。 

这是一个非常吸引人的领域。原因不难理解，很多推理和规划任务本质上都是数学问题。另外，数学在定量学科中起着基础性作用，因此 AI4Math 有可能给科学、工程和其他领域的人工智能带来革新。也正因为这些原因，LLM 开发者通常会把数学问题求解能力作为一个核心衡量指标，人们也在努力创造能在数学问题上比肩甚至超越人类的 AI 系统。 

AI4Math 的重要性吸引了大量研究者，他们开始使用来自自然语言处理（NLP）领域的技术来开发数学 LLM。 

一种常用方法是使用数学数据来对 LLM 进行持续预训练，比如可以使用来自 arXiv 论文和 MathOverflow 网页的数据，然后在精心选择的数学问题数据集（其中会提供详细的分步解决方案）上对模型进行微调。该团队称之为非形式化（informal）方法。 

类似于通用 LLM，数学 LLM 的配方也很简单，秘诀往往在于数据的整编。在 GSM8K、MATH、AIMO Progress Prize 等常用基准上取得进展的数学 LLM 通常包含精心整编的训练数据集、思维链等推理时间技术、自我一致性和工具使用能力。 

然而，直到本文写作时，非形式化方法得到的 AI 的数学能力基本都不超过 AIME 的高中数学水平。 

那么，问题就来了：非形式化方法的规模扩展之路还能走多远？它能让数学 LLM 解决更具挑战性的竞赛问题（例如，IMO、国际数学奥林匹克）甚至还在研究中的数学问题吗？ 

从高中到更高级的数学，非形式方法面临的难题无法仅仅通过规模扩展解决。 

首先，训练数学 LLM 需要高质量的数据，而高质量高等数学数据很稀缺。对于新的研究数学问题，不可能在互联网上找到类似问题的解答或大规模手动标注数据。如果没法扩大数据规模，就不可能充分享受到 LLM 的 Scaling Law。 

第二，很多高等数学的解并不是数值，因此难以通过比较 ground truth 来进行评估。例如证明问题需要一系列复杂的推理步骤。 

LLM 还有个臭名昭著的幻觉问题，会生成看起来可行的推理步骤，因此评估模型输出或收集有用反馈的难度非常大。 

这些问题都难以通过扩大非形式化方法的规模来解决。 

如果训练时间扩展不够用，那我们还需要什么呢？OpenAI o1 展示了一个可能方向：在推理时间扩展非形式化方法，比如将搜索与神经验证器组合起来缓解推理幻觉。 

虽然这种方法吸引了很多人的眼球，但它究竟能不能有效解决高等数学问题还有待解答。 

而本篇立场论文关注的则是一个较少被探索的补充方法：形式化数学推理（formal mathematical reasoning。 

该团队表示，形式化数学推理是指立足于形式化系统的数学推理，而形式化系统包括但不限于一阶 / 高阶逻辑、依赖类型理论和带有形式规范注释的计算机程序。 

这种形式化系统可提供验证模型推理并提供自动反馈的环境。它们不同于现代 LLM 使用的「工具」，因为它们可以建模广泛命题的真与假，并且还是可证明的。此类系统提供的反馈可以缓解数据稀缺问题；此外，此类系统还可以进行严格的测试时间检查，以抵抗幻觉。 

相比之下，非形式化数学是指教科书、研究论文和在线数学论坛中常见的数学文本。非形式化数学会将自然语言与符号（例如 LATEX）交织在一起，但这些符号没有自我包含的形式语义，而是依靠非形式文本来传达其含义的重要部分。 

AlphaProof 和 AlphaGeometry 是这一想法成功的两个突出例子。在此之前，很多研究者尝试过使用 LLM 来解决奥数级数学问题，但都失败了。上述系统的关键区别在于原则性地使用了符号表示和证明检查框架。其中，符号组件（AlphaProof 的 Lean、AlphaGeometry 的特定领域几何系统）的作用是执行神经网络的推理步骤并生成高质量的合成数据，从而实现前所未有的数学推理能力。 

AlphaProof 和 AlphaGeometry 之前，已经有许多文献做好了铺垫 —— 它们探讨了形式化方法和机器学习在数学任务中的协同使用。具体涉及的主题包括神经定理证明、自动形式化（autoformalization）等。 

LLM 的出现大大加速了这一领域的研究。例如，由于缺乏用于微调的已对齐非形式化 - 形式化对，自动形式化长期以来一直都进展缓慢。LLM 可以通过合成数据或执行无微调自动形式化来缓解此问题。因此，人们开始认识到自动形式化在引导神经定理证明器方面的潜力。LLM 也是定理证明的强大工具；事实上，最近已有方法利用 LLM 来预测证明步骤并修复有缺陷的证明，同时还无需基于形式化证明数据进行明确训练。 

围绕 LLM 和形式化推理的研究基础设施正在迅速成熟。Lean 这种用于编写形式化证明的语言在数学家中越来越受欢迎，并催生了形式化研究数学和通用数学库。现在已有多个框架可支持 LLM 和 Lean 之间的交互。这些框架支持基于人工编写的形式化证明提取训练数据，以及通过与形式化环境的交互进行定理证明。 

除了 Lean 之外，Coq 和 Isabelle 等证明语言的多语言基础设施也已在构建中 。 

最后，LLM 已被用于协助人类数学家编写形式化证明 ，这可能会启动一个数据飞轮，其中不断增长的人类编写的形式化数学数据会产生更强大的 LLM，从而让人可以更轻松地创建更多数据。 

AI 在形式化数学推理方面大有机会，因而研究繁盛。AI 在形式化数学推理方面的新兴机会导致了研究活动的蓬勃发展。正如最近的一项调查给出的那样，该领域的发表文献数量在 2023 年几乎翻了一番，并且很可能在 2024 年再翻一番。通过将自动形式化与强化学习相结合，AlphaProof 成为第一个在 IMO 中获得银牌的人工智能。 

该领域的进展也可直接应用于形式化验证（formal verification） ，这是一个核心的计算机科学问题，传统上一直是形式化数学最重要的应用之一。虽然形式化验证可以得到极其稳健和安全的软件和硬件系统，但从历史上看，除了安全性至关重要的应用之外，形式化验证其实很少用，因为其部署成本太高。AI 可以通过自动化形式化和证明工作来大幅降低这一成本。这可能导致未来大规模生产的软件和硬件系统比现在更加稳健。 

该团队表示：「出于所有这些原因，我们相信基于 AI 的形式化数学推理已经到达了一个转折点，未来几年将取得重大进展。然而，仍有大量工作要做。」 

本立场论文概述了该领域在数据和算法方面面临的难题，以及未来进步的可能路线。 

AI4Math 与形式化数学推理

数学推理是 AI 领域的前沿研究方向。本节首先将介绍 AI4Math 的非形式化方法及其局限性。然后将介绍在推进 AI4Math 方面，形式化数学推理是一条有希望的道路。这一节涵盖的内容包括： 

当前最佳的数学 LLM 以及它们的局限性，目前的难题包括数据稀缺、缺乏验证正确性的手段。 

用于形式化数学推理的 AI：这一节将介绍从非形式化到形式化的转向、证明助理和 Lean 等。 

数学 AI 的其它方向：AI4Math 范围很广，还包含其它许多研究方向，比如使用神经网络来近似函数等等。 

用于形式化数学推理的 AI 的最新进展

AI 已在形式数学推理方面取得了实质性进展。本节首先将讨论两个关键任务的进展：自动形式化和定理证明。然后将抽样两个相邻领域 —— 自然语言和代码生成 —— 它们可受益于形式化方法实现的可验证推理。 

在自动形式化方面，本文介绍了基于规则的自动形式化、基于神经和 LLM 的自动形式化、自动形式化的应用。 

在神经定理证明方面，本文介绍了专家迭代、从错误中学习、非正式证明草图、库学习、前提选择和检索等主题。 

此外，这一节还介绍了自然语言中的验证推理、形式系统验证和验证生成。 

挑战与未来的方向

这一节，该团队分享了几个仍待解决的挑战和有希望的研究方向，包括形式化数学推理的数据和算法、协助人类数学家和证明工程师的 AI 工具，以及集成 AI 和形式化方法来生成可验证代码。 

数据

数据稀缺是首要问题。潜在的解决方案包括: 

从教科书、论文和讲义中自动形式化非形式化数学内容

基于数学公理生成合成的猜想和证明

从不同的证明框架和代码等数据丰富的领域迁移知识

算法

在这个方面，又有许多亟待解决的问题，该团队也提出了一些解决的设想： 

问题 1：如何让 AI 能够自动地将非形式化的内容转换成形式化的数学语言？ 

建立自动形式化语句的评估指标

将形式化过程分解为小步骤

加强与形式系统的交互

问题 2：如何改进数学推理的模型架构？ 

增强多步推理、长文本处理、抽象和分层规划能力

通过合成基准诊断推理失败之处

利用检索和搜索等推理技术辅助模型

问题 3：如何有效地搜索证明？ 

对搜索进行扩展以利用更多的测试时间计算；

对模型、搜索算法和超参数进行系统性评估；

用于评估证明目标并为其设定优先级的价值模型。

问题 4：如何利用定理证明中的层次结构？ 

将大型、高级证明目标逐步分解为较小的目标。

问题 5：如何学习数学抽象？ 

学习在成熟的证明助手中构建新的定义、引理和策略。

问题 6：如何利用现有的数学知识？ 

为形式数学推理量身定制的检索器；

处理动态增长的知识库。

问题 7：如何协调专家方法和通用方法？ 

识别跨领域联系的通用方法；

针对各个领域的有效性的专家方法以及与数学家合作的专家方法；

将通用方法和专家方法结合起来，例如为 LLM 配备特定领域的工具。

用于辅助人类数学家的工具

这方面的主要问题是：AI 如何更好地协助人类研究形式化数学？ 

这个方面的难题和潜在研究方向包括： 

资源、激励措施和工程开发，以提高可用性和用户友好性；

研究数学家如何使用形式化工具的行为；

支持大规模分布式协作的工具。

形式验证和已验证生成

这方面的主要问题是：AI 如何辅助人类开发正确和安全的软件？ 

这个方面的难题和潜在研究方向包括： 

将形式化方法纳入 AI 辅助的系统设计和实现中；

增强 AI 进行形式化软件和硬件验证的能力；

将基于 AI 的生成与形式化验证结合起来。

评估标准

在解决问题的过程中，一个关键问题逐渐浮现：如何有效衡量进展？ 

受自动驾驶汽车自动化等级的启发，该团队提出了一个评估 AI 数学推理能力的分级框架。他们强调，在这个新兴领域还需要建立更多新的基准和评估方法。 

定理证明能力

目前，AI 在形式数学领域的主要工作集中在自动定理证明上。像 Lean 这样的形式系统提供了巨大优势 - 一旦找到证明，即使人可能没完全理解，就能保证其正确性。 

研究团队根据表 1 给出了 AI 形式定理证明的分级基准。 

在最基础的 0 级水平，AI 能够识别正确的形式证明。 

到了 1 级，AI 系统可以提供潜在有用的数据，但还不能写出证明。 

2 级及以上的系统可以生成完整或部分证明。人类专家设计和编写的固定证明策略和规则，AI 按照这些预设的策略执行证明过程。 

在 3 级水平，AI 系统能够在一般领域自动证明定理，但仍局限于简单定理。 

4 级系统应该能够自主规划和执行形式化项目，分解大型结果，提出新的定义和定理，并在探索的过程中尝试不同的解决方案。 

5 级则意味着系统能够解决超出人类水平的问题。 

自然语言推理验证能力

研究团队首先提出了一个问题：如何在不完全形式化的情况下实现严谨的推理？ 

他们发现，让 AI 在形式系统和自然语言之间切换是一个很有前景的方向。这样的 AI 系统应该能够进行逻辑推理、数值计算，并以严谨且易懂的方式生成答案。 

虽然推理过程可能不是严格的形式化证明，但其中的部分内容仍可以在人工的监督下以半自动化的形式验证。该团队将这种能力称为「自然语言验证推理」，并提出了一个分级框架 (表 2)。 

在 0 级水平，AI 能够用自然语言生成逐步推理过程，但不涉及验证。 

到了 1 级，AI 系统在生成推理的同时具备了验证能力，可以评估每个推理步骤的正确性。 

在 2 级，AI 系统能够利用外部工具，执行单靠神经网络难以学会的计算任务。 

第 3 级的 AI 系统将可以使用外部工具进行严格的逻辑推理。 

在第 4 级，AI 系统能够识别日常任务中的数学问题并使用严谨的方法。对其进行推理 

自动形式化的能力

该团队提出了一个自动形式化能力评估体系，评估 AI 如何在数学知识的非形式化表述和形式化表述之间自动转换。 

根据表 3，在最基础的 0 级水平，AI 系统能够存储和检验形式化知识，方便人工形式化。 

在第 1 级，AI 将可以为自动生成形式化的几种草稿，并通过持续收集和存储人类反馈来不断改进系统性能。 

到了第 2 级，AI 应能够在两者之间进行稳定且准确的转换，准确度接近人类水平。 

第 3 级的 AI 系统能够在形式化的过程中推断出缺失饿信息，并标记出它无法补全的部分。 

在第 4 级，AI 将具备遇到错误或对不上的输入时自我纠正的能力。 

最后在第 5 级，该团队预计 AI 将能够创造新的数学定义，有望降低证明的复杂度。 

猜想能力

研究团队发现，在数学研究中，提出定理证明之前的猜想阶段同样重要。该团队认为，AI 有望自主提出数学猜想。 

根据表 4 的分级标准，0 级水平是指 AI 能够针对特定问题或目标结果提出相关猜想。更进一步，在 1 级水平上，AI 就预计可以在给定研究领域内自主提出猜想，而不必局限于某个具体定理了。 

形式化验证与验证生成的结果

研究团队最新发现，把 AI 应用到程序验证和系统开发时，面临的挑战与数学研究有很大不同。为了更好地理解这个领域，该团队设计了一个 4 级能力评估体系 (表 5)。 

在最基础的第 1 级，AI 已经能够完成一些简单的验证工作，比如检查小段代码是否正确，或者自动生成一些简单的可验证代码。 

到了第 2 级，AI 的能力提升到可以帮助开发团队验证整个项目，并且能处理更复杂的问题。 

第 3 级是一个重要突破，AI 不仅能生成代码，还能提供证明并帮助维护系统。 

在最高的第 4 级，AI 可以帮助开发人员制定技术规范，包括自动生成规范文档、解释具体要求，以及帮助找出规范中的问题。