Meta、斯坦福等：AI的下一个前沿，正是陶哲轩说的形式化数学推理

AI4Math现在也有了自己的L1-L5。

原标题：Meta、斯坦福等：AI的下一个前沿，正是陶哲轩说的形式化数学推理
文章来源：机器之心
内容字数：12117字

AI 赋能形式化数学推理：从非形式化到形式化的新阶段

近年来，人工智能在数学推理领域取得了显著进展，尤其是在使用AI进行形式化数学推理方面。本文总结了Meta FAIR和斯坦福大学等机构发表的立场论文《Formal Mathematical Reasoning: A New Frontier in AI》的主要内容，探讨了AI4Math领域的发展现状、挑战以及未来方向。

1. AI4Math的非形式化方法及其局限性

早期AI4Math主要采用非形式化方法，即利用大量数学数据（例如arXiv论文和MathOverflow网页数据）预训练LLM，并在特定数据集上进行微调。这种方法在一些基准测试中取得了进展，但其能力大多局限于高中数学水平。其主要局限性在于：高质量高等数学数据稀缺；高等数学解通常不是数值，难以评估模型输出；LLM的“幻觉”问题导致评估难度加大。

2. 形式化数学推理：一条有希望的道路

论文强调，形式化数学推理，即基于形式化系统（如一阶/高阶逻辑、依赖类型理论）的推理，是推动AI4Math发展的重要方向。形式化系统提供验证模型推理和自动反馈的环境，可以缓解数据稀缺问题并抵抗幻觉。AlphaProof和AlphaGeometry是成功的案例，它们通过结合符号表示和证明检查框架，实现了前所未有的数学推理能力。

3. 形式化数学推理的进展和挑战

论文总结了AI在自动形式化和定理证明方面的进展，包括基于规则和神经网络的方法。同时，也指出了该领域面临的挑战，例如：如何将非形式化内容自动转换为形式化语言；如何改进数学推理模型架构；如何有效搜索证明；如何学习数学抽象；如何利用现有数学知识等。

4. AI辅助人类数学家和形式化验证

论文探讨了AI如何辅助人类数学家编写形式化证明，以及如何应用于形式化验证领域。AI可以降低形式化验证的成本，从而推动更稳健的软件和硬件系统的大规模生产。

5. 能力分级框架

为了更好地衡量AI在形式化数学推理方面的进展，论文提出了一个分级框架，涵盖了定理证明能力、自然语言推理验证能力、自动形式化能力和猜想能力等方面。该框架为评估AI数学推理能力提供了参考标准。

6. 未来研究方向

论文最后展望了未来研究方向，包括：改进数据和算法；开发辅助人类数学家的AI工具；将AI和形式化方法集成以生成可验证代码；建立更完善的评估标准等。论文认为，基于AI的形式化数学推理已达到一个转折点，未来几年将取得重大进展。

联系作者

文章来源：机器之心
作者微信：
作者简介：专业的人工智能媒体和产业服务平台