对于人工智能领域的研究人员来说，数学不仅是一个挑战也是衡量技术发展水平的重要标准。最近，随着AI推理能力的提高，AI在证明数学问题上的研究成为了热门方向。著名的数学家陶哲轩便是这一方向的积极推动者，他预言数学家未来可以向类似GPT的AI解释证明，AI则将这些证明转化为Lean格式。这种AI助手不仅能生成LaTeX文件，还能辅助论文提交，大幅提高数学家的工作效率和便利性。
目前，已经出现了如Gemini 2.0 Flash Thinking和o1/o3等强大的推理模型，那么AI在形式化数学推理方面的研究进展如何？最近，多个科研机构如Meta FAIR和斯坦福大学共同发表的立场论文《Formal Mathematical Reasoning: A New Frontier in AI》可能为您提供相关答案。论文的核心观点是下一阶段的AI4Math将采用形式化系统来实现形式化数学推理。
AI4Math的意义不仅在于，许多推理和规划任务本质上都是数学问题，数学作为定量科学的基础，AI4Math有望推动科学、工程等领域的人工智能创新。因此，大型语言模型（LLM）开发者通常将数学问题解决能力作为核心评价标准，致力于创造出超越人类的AI系统。
AI4Math领域贡献了众多研究者，他们使用自然语言处理（NLP）技术开发数学领域的大型语言模型（LLM）。常见的策略是利用数学数据持续预训练LLM，并在精选数学问题数据集上进行微调。这些数据集会提供详细的分步解决方案，这种方法被称为非形式化方法。类似于通用的大型语言模型，数学LLM的秘密在于数据的整理和编制。那些在GSM8K、MATH、AIMO Progress Prize等基准上取得进展的数学LLM，通常包含了精致的训练数据集、思维链等技术、自我一致性和工具使用能力。
然而，直到本文落笔之时，非形式化方法培养的AI在数学上的能力大多只达到数学能力评估（AIME）的高中数学水平。紧接着的一个问题则是：非形式化方法的规模扩展路向还可以走多远？它能够使数学大型语言模型解决更有挑战性的竞赛问题（如IMO、国际数学奥林匹克）甚至还未解决的数学问题吗？
从高中水平到更高级数学知识，非形式化方法面临的挑战无法仅依靠规模扩展来解决。首先，训练数学LLM需要高质量的数据，而高等数学的高质量数据非常稀缺。对于新兴的研究性数学问题，不可能在网络上找到同类问题的解答或大规模手动标记的数据，这限制了LLM利用Scaling Law的潜力。此外，许多高等数学解决问题的答案不是数值，因此不易通过比较参考答案来评估。
幻象问题也是一大难题，可能会生成看似可行的推理步骤，使得评估模型输出或获取有用反馈变得极为困难。OTAI o1展现了一个可能的方向：在推理时间扩展非形式化方法，比如将搜索与神经验证器结合起来应对推理的幻象问题。尽管方法吸引大众的目光，其在解决高等数学问题上的有效性尚需进一步验证。
立场论文关注的是未被广泛探索的补充方法：形式化数学推理。研究者认为，立足于形式化系统的推理称为形式化数学推理，包括但不限于一阶/高阶逻辑、依赖类型理论以及带有形式规则注解的计算机程序。形式化系统提供验证模型推理环境和自动反馈。它们与现代LLM使用的“工具”不同，建模广泛命题的真实性和证明性。系统反馈可缓解数据稀缺问题，并可进行严格的测试时间检查，以对抗幻象。不同于现代LLM，非形式化数学是一种常见的数学文本，把自然语言和符号（比如LATEX）交织在一起，依靠非形式文本传递含义的重要部分。
AlphaProof和AlphaGeometry是这一思路成功的案例，有很多试图用LLM解决奥数级的数学问题的研究者失败。这些系统的关键区别在于使用了符号表示和证明检查框架，符号组件的作用是执行神经网络的推理步骤并生成高质量的合成数据，实现前所未有的数学推理能力。
在LLM和形式化推理研究基础设施迅速成熟的背景下，Lean这种用于编写形式化证明的语言越来越受欢迎。现在已有多个框架支持LLM和Lean间的交流，这些框架支持基于人编写的形式化证明来提取训练数据，并助力定理证明。Coq和Isabelle等也在构建中。
LLM已被用来协助人类数学家编写形式化证明，并可能启动数据飞轮，不断增长的人类编写的形式化数学数据会产生更强大的LLM，使人能轻松创建更多数据。AI在形式化数学推理领域拥有巨大机会，研究蓬勃发展。形式化验证是计算机科学的核心问题之一，以往因成本过高而未广泛应用。AI可以自动形式化和证明工作，大幅降低成本，推动未来大规模生产的软件和硬件系统更稳健。团队认为基于AI的形式化数学推理已到一个转折点，预计在未来几年内取得重大进展，但依旧有很多工作要做。
本立场论文概述了该领域在数据和算法方面的挑战及未来可能的方向。数学推理是AI领域的前沿研究方向。首先介绍了非形式化方法及其局限，然后阐述推进AI4Math的形式化数学推理等有希望的路径。本节的内容还覆盖自动形式化和定理证明这两个关键任务的进展，以及自然语言与代码生成领域，它们可从形式化实现的可验证推理中受益。在自动形式化方面，介绍基于规则的自动形式化、基于神经和LLM的自动形式化及应用。在神经定理证明方面，介绍了专家迭代、学习及库学习等多个主题。
该团队分享了待解决的挑战和有希望的方向，包括形式化数学推理的数据和算法问题，以及帮助人类数学家和证明工程师的AI工具，并集成AI和形式化方法以生成可验证代码。数据稀缺是首要问题，可能的解决方案包括从各种文本中自动形式化非形式化数学内容、基于数学公理生成合成猜想和证明、跨领域知识迁移。在算法方面，如何让AI自动转换非形式化内容到形式化数学语言，提升模型架构及有效搜索证明都是待解决问题，并提出了一系列解决方案，如建立自动形式化语句的评估指标、改进与形式系统的交互等。
进一步，研究者提出了为辅助人类数学家的工具。这些问题包括资源和激励措施、工程开发、支持分布式协作的工具等。形式验证和验证生成方面的主要问题在于如何辅助人类开发正确、安全的软件系统。
最后，评估标准的建立变得尤为关键。团队根据自动驾驶汽车的自动化等级制定评估AI数学推理能力的分级框架，并强调在新兴领域需建立新的基准与评估方法。自动定理证明分级、自然语言推理验证能力、自动形式化的能力和猜想能力都提出了相应评估体系。研究团队在形式化验证与验证生成方面也设计了4级能力评估体系。AI在程序和系统验证中的应用与数学研究很不同，因此了解领域挑战、建立衡量标准极为关键。
相关文章
