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

AIGC动态21小时前发布 almosthuman2014

51 0 0

文章摘要

近期，AI在数学领域的应用取得了显著进展，特别是在形式化数学推理方面。著名数学家陶哲轩认为，未来数学家可以通过AI助手来解释证明，AI将证明形式化为Lean证明，从而提高数学家的工作效率。Meta FAIR和斯坦福大学等机构的立场论文《Formal Mathematical Reasoning: A New Frontier in AI》探讨了AI在形式化数学推理方面的进展和挑战。

AI4Math领域吸引了大量研究者，他们使用自然语言处理技术开发数学LLM。常用的方法是使用数学数据对LLM进行预训练，然后在数学问题数据集上进行微调。然而，非形式化方法得到的AI数学能力基本不超过高中数学水平。非形式化方法面临的难题包括高质量高等数学数据稀缺、高等数学解难以通过比较ground truth进行评估、LLM的幻觉问题等。

为了解决这些问题，研究者开始探索形式化数学推理，即立足于形式化系统的数学推理。形式化系统可提供验证模型推理并提供自动反馈的环境，缓解数据稀缺问题，进行严格的测试时间检查，以抵抗幻觉。AlphaProof和AlphaGeometry是形式化数学推理成功的两个例子，它们使用符号表示和证明检查框架，实现前所未有的数学推理能力。

LLM的出现加速了形式化数学推理领域的研究。LLM可以合成数据或执行无微调自动形式化，缓解自动形式化进展缓慢的问题。LLM也是定理证明的强大工具，可以预测证明步骤、修复有缺陷的证明，无需基于形式化证明数据进行明确训练。

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

AI在形式化数学推理方面大有机会，研究活动蓬勃发展。AI在形式化数学推理的新兴机会导致了研究活动的蓬勃发展。通过将自动形式化与强化学习相结合，AlphaProof成为第一个在IMO中获得银牌的人工智能。该领域的进展也可直接应用于形式化验证，这是一个核心的计算机科学问题，传统上一直是形式化数学最重要的应用之一。AI可以通过自动化形式化和证明工作来大幅降低这一成本，可能导致未来大规模生产的软件和硬件系统比现在更加稳健。

本立场论文概述了该领域在数据和算法方面面临的难题，以及未来进步的可能路线。AI4Math与形式化数学推理、用于形式化数学推理的AI的最新进展、挑战与未来的方向等方面进行了深入探讨。