摘要：14是圆周率（π）的常用近似值，从2020年起，每年的3月14日被定为国际数学日，也被昵称为 “π Day”。数学作为一门古老而深奥的学科，不仅是人类理解世界本质的语言，也是其他科学的基石。进入人工智能时代，数学推理能力也成为衡量大模型智能水平的关键指标之一。

编者按：3.14是圆周率（π）的常用近似值，从2020年起，每年的3月14日被定为国际数学日，也被昵称为 “π Day”。数学作为一门古老而深奥的学科，不仅是人类理解世界本质的语言，也是其他科学的基石。进入人工智能时代，数学推理能力也成为衡量大模型智能水平的关键指标之一。今天，让我们相约在 π Day，一起来看看微软亚洲研究院的研究员透过数学现象，看到了怎样的推理本质。

数学贯穿人类历史，被视为宇宙的语言。万事万物中都蕴含着数学理论，借助数学思维，人们得以洞察事物的本质。如今，数学建模在气候科学、医学成像、疾病控制以及人工智能等诸多领域，都发挥着重要作用。

在3月14日“国际数学日”，我们邀请到近年来专注于人工智能数学推理研究的微软亚洲研究院高级研究员张宪，深入探讨了他和同事们在大语言模型数学推理领域的探索与突破。张宪表示，他们的研究并非从数据角度出发，而是更多地从规则角度入手，通过形式化和符号化的方法，让大语言模型基于数学领域的知识学习内在规则，并实现自动化扩展和应用，推动数学推理能力的发展。

微软亚洲研究院高级研究员张宪

Q：大语言模型的数学推理研究对人工智能的发展有什么意义？

张宪：首先，数学推理是人工智能的必要组成部分。随着数学推理能力的提升，大语言模型通过学习数学的方法、规则，能够增强模型整体的推理性能。数学推理与逻辑规则紧密相连，这种能力的提升不仅能够帮助大模型更好地理解和处理复杂任务，还能将数学推理方法泛化到其他领域，如代码优化、常识推理，甚至是语义理解等，展现出更高的效率和准确性。

另外，数学还是科学研究的基础，尤其在当前备受关注的 AI for Science（科学智能）领域，大模型数学能力的提升将直接促进人工智能在科学计算、工程建模等科学研究中的应用，进一步推动科研进程，加速科学发现的探索步伐。

Q：当前，人工智能在数学推理方面处于哪一发展阶段？其能力提升的主要阻碍是什么？

张宪：现阶段，人工智能在数学推理方面的能力很大程度上依赖于训练数据的质量和数量。当训练数据丰富且多样时，模型能够在某些数学领域表现出色，甚至能够解决复杂的奥数题，并能举一反三地解答变形题目。然而，当训练数据不足或分布不均时，即使是简单的小学题目，模型也可能出错。这是因为大语言模型本质上是对所学数据的拟合，一旦某领域的训练数据不足，模型就容易出现“幻觉”，找不到合理的解题方法。

数据不足是当前人工智能数学推理能力提升的主要阻碍之一。理论上，如果数据足够丰富，那么大模型在数学领域的推理能力将有可能达到顶级水平。这就像“题海战术”与“天才战术”的差异：通过大量练习，人们可以积累经验并掌握解题技巧；而天才则能够凭借快速学习和理解能力迅速掌握复杂概念。尽管两者之间的界限难以明确划分，但一个成绩优异的人通常见过许多场景，学过大量知识。因此，丰富的数据对于提升大语言模型的数学推理能力至关重要。需要特别指出的是，在单一任务上，目前的大语言模型需要远大于人类个体接受的训练数据量。

Q：你和团队在大语言模型数学推理方面进行了哪些研究？取得了哪些重要成果？

张宪：在数学推理这个方向上，我们主要从规则而非数据的角度进行研究，希望大语言模型能够学习和理解数学领域的规则，并自主扩展和应用这些规则来进行泛化推理。

我们开展了形式化、符号化的研究，让大语言模型可以将自然语言的数学问题转化为形式化语言，类似于“翻译”，从而使大语言模型能够读懂题目，理解数学问题的内在规律。例如，通过形式化方法，模型可以像计算器一样处理各种数学运算，展现出强大的泛化能力。

Autoformalizing Mathematical Statements by Symbolic Equivalence and Semantic Consistency

论文链接：

https://openreview.net/pdf?id=8ihVBYpMV4

针对不等式证明方面，我们让模型在奥林匹克竞赛级别的复杂问题上进行了严格推理，验证了形式化模型具备学习并应用数学规则的能力，为推理能力的进一步拓展奠定了基础。同时，我们还尝试将这些方法推广到更广泛的代数、几何和数论领域，希望实现大语言模型在数学推理上的全面突破。

Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoning

论文链接：

https://openreview.net/pdf?id=FiyS0ecSm0

为了解决大语言模型因训练数据有限而导致的能力不足问题，我们还进行了数学数据合成方面的研究。通过形式化方法生成多样化的数学问题与答案对，就像老师为了锻炼学生新编写的变形题，从而为模型提供更丰富的训练素材。这种方法不仅增加了模型训练的数据量，还提升了数据的多样性和质量，让模型能够在更多场景中学习和验证推理能力。

Neuro-Symbolic Data Generation for Math Reasoning

论文链接：

https://openreview.net/pdf?id=CIcMZGLyZW

Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutation

论文链接：

然而，对于提升人工智能性能来说，单纯依赖海量数据和计算资源的“规模法则（scaling law）”并非长久之计。因此，我们从生成数学题、理解题目、解答证明这三个方面入手，让大语言模型能够更全面地理解数学推理的规律，然后通过一种自动化且可扩展的方法来处理复杂的推理问题，而不是仅停留在表面的数据拟合上。

Q：数学推理与常识推理有什么不同？目前大语言模型为什么无法解答“执竿入城”这类兼具数学逻辑和常识要素的问题？

张宪：数学推理是通过运用数学知识以及明确的规则和方法来解决问题，具有较强的逻辑性与确定性。而常识推理则更多依赖于人类在日常生活中积累的经验和对世界的认知，涉及对各种概念、场景的理解与判断。

对于“执竿入城”这类问题，不仅需要数学计算能力，还需要对物理空间和物体运动的直观理解。大语言模型是基于自然语言数据训练的，缺乏对空间概念和常识的理解。模型本质上并不理解“竿”和“城”的具体概念，只是从文字表面去理解问题，对物体的形状、运动等概念没有认知，因此，在解决这类问题时大语言模型容易出错。这种空间智能的缺失是大语言模型亟待突破的难题。

Q：数学问题种类繁多，人工智能在数学推理中是否也可以实现一个“大脑”处理所有问题？你认为大模型进行数学推理的本质是什么？

张宪：目前来看，用一个大语言模型来处理初高中或本科阶段的数学问题是可行的。这一阶段的数学知识体系相对固定，问题类型和解题方法较为明确，通过对大量相关数据的学习和训练，大模型能够掌握其中的规律，从而进行有效的推理和解答。

但对于前沿的数学领域，业界还没有明确的解决方案。数学是一个非常有趣且复杂的领域，例如哥德尔不完备定理指出，在特定的公理体系中，可能存在一些虽然正确但无法用当前公理体系证明的命题。当前的人工智能模型在进行数学推理时，通常采用形式化方法，基于一套固定的公理体系，这使得模型在这套体系下必然会遇到某些难以证明的命题。

人类最伟大之处就在于不断突破自我，突破底层固有的公理、系统，探索新的规律来解决问题。就像爱因斯坦发现相对论，打破了经典力学的局限。虽然目前我们的方法在理论上没有上限，但在涉足前沿数学研究时，确实可能遭遇现有体系无法证明某些命题的困境。这意味着，人工智能也要跳出现有框架，构建更高级别的公理体系来兼容那些无法证明的命题。

Q：你如何看待人工智能数学推理未来的发展趋势？数学推理能力的提升将给现实世界创造哪些价值？

张宪：在进行数学推理时，人类会根据需要借助各种工具，如计算器、查阅资料等，而不是一味地心算。对大语言模型而言，未来在推理时精准调用合适工具的能力至关重要。这种能力不仅对数学推理本身非常重要，对于代码编写、常识判断等领域也同样具有重要意义。

人工智能数学推理能力的提升将率先在教育领域发挥作用。具备强大推理能力的模型可以为学生提供更精准、高效的数学学习辅助，帮助他们更好地理解数学概念、掌握解题技巧，并为个性化学习提供支持。

从工业角度来看，当人工智能在数学形式化推理方面表现出色时，结合其常识和知识储备，将极大地推动代码形式化的发展。这对于工业界开发稳定、可靠的软件十分关键，这也是当前众多科研团队积极探索的重要方向之一。

此外，在数学研究领域，尽管让人工智能解决所有数学问题不太现实，但它可以在未解决的数学难题上为人类提供新的思路和视角。已经有数学家通过借助人工智能的发散性“思维”，再结合自身的专业知识，来寻找解决难题的突破口了。这种人机协作的方式将为数学研究带来新的发展机遇，也将为未来的科学研究开辟新的路径。

来源：微软亚洲研究院