机器之心报道
编辑：Panda、佳琪
对 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 可以帮助开发人员制定技术规范，包括自动生成规范文档、解释具体要求，以及帮助找出规范中的问题。