CMU博士论文提出利用语言模型实现可验证的数学自动化，结合语言模型的理解能力和自动推理器的推理能力，提出了新的定理证明研究范式。
原文标题：【CMU博士论文】可验证数学自动化的语言模型交互、集成与自动形式化
原文作者：数据派THU
冷月清谈：
这篇CMU博士论文探讨了如何利用语言模型实现可信的数学推理自动化。论文指出，语言模型的强项在于语言理解和处理大量数据，而传统自动推理器的优势在于形式化推理。因此，论文的核心思想是将两者结合，利用语言模型的理解能力和自动推理器的推理能力，实现更强大的数学自动化。
具体来说，论文进行了以下几个方面的研究：
1. 评估语言模型在非正式数学推理中的表现：发现语言模型在记忆和灵活输入输出方面表现出色，但在复杂推理和代数运算方面存在不足。
2. 提出了Thor方法：结合自动定理证明器和语言模型进行证明搜索。Thor利用语言模型进行创造性推理，并使用自动定理证明器补充细节。同时，还开发了Magnushammer，一个用于过滤相关性的工具，提升了Thor的效率。
3. 探索自动形式化：使用语言模型将非正式数学定理和证明转换为形式化语言。并通过构建大规模平行数据集MMA，提高了语言模型的自动形式化能力。
4. 提出了Draft、Sketch和Prove方法：将非正式证明转换为形式化证明草图，再由自动定理证明器完成最终的证明。
总而言之，这篇论文提出了一种新的定理证明研究范式，将语言模型作为自动化引擎和人机交互的桥梁，为数学自动化提供了新的思路。
具体来说，论文进行了以下几个方面的研究：
1. 评估语言模型在非正式数学推理中的表现：发现语言模型在记忆和灵活输入输出方面表现出色，但在复杂推理和代数运算方面存在不足。
2. 提出了Thor方法：结合自动定理证明器和语言模型进行证明搜索。Thor利用语言模型进行创造性推理，并使用自动定理证明器补充细节。同时，还开发了Magnushammer，一个用于过滤相关性的工具，提升了Thor的效率。
3. 探索自动形式化：使用语言模型将非正式数学定理和证明转换为形式化语言。并通过构建大规模平行数据集MMA，提高了语言模型的自动形式化能力。
4. 提出了Draft、Sketch和Prove方法：将非正式证明转换为形式化证明草图，再由自动定理证明器完成最终的证明。
总而言之，这篇论文提出了一种新的定理证明研究范式，将语言模型作为自动化引擎和人机交互的桥梁，为数学自动化提供了新的思路。
怜星夜思：
1、论文中提到的语言模型在复杂推理和代数运算方面的弱点，未来有哪些可能的改进方向？
2、Thor方法中结合了语言模型和自动定理证明器，这种“人机合作”的模式在其他领域还有哪些潜在的应用？
3、自动形式化将非正式数学文本转化为形式化语言，这除了用于定理证明，还能在哪些方面发挥作用？
2、Thor方法中结合了语言模型和自动定理证明器，这种“人机合作”的模式在其他领域还有哪些潜在的应用？
3、自动形式化将非正式数学文本转化为形式化语言，这除了用于定理证明，还能在哪些方面发挥作用？
原文内容
来源：专知本文约1000字，建议阅读5分钟
本论文的研究提出了一种新的定理证明研究范式，在这种范式中，语言模型既是自动化众多任务的可扩展动力引擎，又是人类用户与机器推理之间的可访问桥梁。
形式化数学推理中的更强自动化提供了可扩展性、可信性和可访问性： 它使得复杂证明的高效验证成为可能，减少了在复杂计算中出错的可能性，允许非专家参与数学概念的探讨，并可能通过机器驱动的探索促进新数学见解的发现。传统上，自动推理器只能使用形式化语言库，无法利用更大规模的自然语言语料库，因为自然语言理解较为困难。尽管已有设计控制自然语言接口与形式语法（例如Naproche），它们最终由于过于僵化，难以广泛应用。另一方面，大型语言模型在语言理解方面表现出色，并且接触到人类历代积累的无数数学文献，这使它们成为理想的自动化工具。现代语言模型已在大量数据上进行了训练，能够执行令人印象深刻的任务数量。语言模型的多功能性使其与传统推理器互补，而传统推理器的僵化性严重限制了它们的广泛应用和易用性。
本论文的目标是回答：如何通过语言模型实现可信的数学推理自动化。 为此，我们提出了一种新的语言模型评估方法，以确定它们在数学推理中的适用场景。基于获得的见解，我们训练语言模型在这些场景下撰写形式化证明，并借助自动定理证明器进行辅助，使用它们将数学定理和证明从LATEX转换为形式化语言。
具体而言：
-
我们进行首次互动评估，评估语言模型在非正式数学推理中的表现。 评估结果揭示了语言模型在记忆和具有灵活输入/输出方面的内在优势，但在复杂推理和代数运算方面的弱点。
-
基于语言模型的优缺点，我们提出了结合自动定理证明器和语言模型进行证明搜索的首个方法：Thor。 Thor使用语言模型进行创意推理步骤，并调用Sledgehammer（Isabelle的工具，具有多个自动定理证明器）来填充前提选择的细节。我们还开发了Magnushammer，这是一个基于变换器的相关性过滤器的系统，并证明了Magnushammer在个体和作为Thor插件的情况下都优于Sledgehammer。
-
目前所有现有的证明搜索方法仅在自然语言或形式语言上进行操作，而未将它们各自的表达力和严谨性结合起来。 为了弥补这一二分法，我们使用语言模型进行自动形式化（autoformalization），即将非正式的数学定理和证明转化为形式化的过程。通过展示自动形式化定理可作为训练数据来改进证明搜索系统，我们验证了自动形式化的实用性。我们还将多个语言的形式化定理库转化为自然语言，最终形成了一个大规模的平行数据集MMA，证明在语言模型进行微调后，能显著提高自动形式化能力。
-
最后，我们构建了Draft、Sketch和Prove，这是一种方法论，利用语言模型将非正式证明转换为形式化证明草图，然后调用自动定理证明器填补其中的空白。 这种神经符号方法通过有效地将非正式证明转化为形式化证明并验证它们，赋予了非正式证明严谨性。
本论文的研究提出了一种新的定理证明研究范式，在这种范式中，语言模型既是自动化众多任务的可扩展动力引擎，又是人类用户与机器推理之间的可访问桥梁。
