Formal Mathematical Reasoning: A New Frontier in AI

人工智能在数学中的应用（AI4Math）不仅在智力上引人入胜，而且对于科学、工程等领域中由AI驱动的发现至关重要。在AI4Math方面的广泛努力反映了自然语言处理（NLP）技术的应用，特别是通过精心整理的文本形式的数学数据集训练大型语言模型。作为一条补充但尚未充分探索的路径，形式化数学推理基于如证明助手等形式系统，这些系统可以验证推理的正确性并提供自动反馈。在本文中，我们倡导形式化数学推理，并认为它是将AI4Math提升到新水平不可或缺的一部分。近年来，我们在使用AI进行形式化推理方面取得了稳步进展，包括定理证明和自动形式化等核心任务，以及可验证的代码和硬件设计生成等新兴应用。然而，要使AI真正掌握数学并产生更广泛的影响，仍有许多重大挑战需要解决。我们总结了现有进展，讨论了开放性挑战，并设想了衡量未来成功的几个关键里程碑。在这个形式化数学推理的转折点上，我们呼吁研究界团结起来，推动这一领域的变革性进展。

论文试图解决如何通过形式化数学推理（如定理证明和自动形式化）来提升AI在数学中的应用，以实现更广泛的科学、工程等领域的影响。这并不是一个全新的问题，但该论文强调了形式化方法在这一领域的重要性。

关键思路是倡导将形式化数学推理作为推进AI4Math的核心途径。相比当前主要依赖于自然语言处理技术训练大型语言模型的方法，本文提出形式化系统（如证明助手）可以提供更严格的正确性验证和自动化反馈，从而推动AI真正掌握数学。

论文指出近年来在使用AI进行形式化推理方面取得了稳定进展，并列举了核心任务如定理证明和自动形式化的成就，以及新兴应用如可验证的代码和硬件设计生成。此外，它还讨论了现存挑战并设定了未来成功的里程碑。值得注意的是，作者呼吁研究社区共同努力，促进这一领域的变革性发展。

最近在这个领域内的相关研究包括：1.《Deep Learning for Theorem Proving》探讨了深度学习在定理证明中的应用；2.《Formal Methods in AI: A Survey》综述了人工智能中形式化方法的应用；3.《Autoformalization with Large Language Models》研究了大型语言模型在自动形式化中的潜力。