Meta FAIR揭秘：智能技术如何革新数学前沿？

Meta FAIR揭秘：智能技术如何革新数学前沿？

对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之间的交互。这些框架支持基于人工编写的形式化证明提取训练数据，以及通过与形式化环境的交互进行定理证明。

随着形式化数学推理方法的不断发展，AI在数学领域的应用前景将更加广阔。通过结合LLM的强大推理能力和形式化系统的严格验证机制，未来有望解决更复杂的数学问题，甚至在某些领域实现突破性进展。这不仅将推动数学研究的发展，还将为科学、工程和其他领域的创新提供新的工具和方法。