【CMU博士论文】可验证数学自动化的语言模型交互、集成与自动形式化

形式化数学推理中的更强自动化提供了可扩展性、可信性和可访问性： 它使得复杂证明的高效验证成为可能，减少了在复杂计算中出错的可能性，允许非专家参与数学概念的探讨，并可能通过机器驱动的探索促进新数学见解的发现。传统上，自动推理器只能使用形式化语言库，无法利用更大规模的自然语言语料库，因为自然语言理解较为困难。尽管已有设计控制自然语言接口与形式语法（例如Naproche），它们最终由于过于僵化，难以广泛应用。另一方面，大型语言模型在语言理解方面表现出色，并且接触到人类历代积累的无数数学文献，这使它们成为理想的自动化工具。现代语言模型已在大量数据上进行了训练，能够执行令人印象深刻的任务数量。语言模型的多功能性使其与传统推理器互补，而传统推理器的僵化性严重限制了它们的广泛应用和易用性。 本论文的目标是回答：如何通过语言模型实现可信的数学推理自动化。 为此，我们提出了一种新的语言模型评估方法，以确定它们在数学推理中的适用场景。基于获得的见解，我们训练语言模型在这些场景下撰写形式化证明，并借助自动定理证明器进行辅助，使用它们将数学定理和证明从LATEX转换为形式化语言。 具体而言：

1. 我们进行首次互动评估，评估语言模型在非正式数学推理中的表现。 评估结果揭示了语言模型在记忆和具有灵活输入/输出方面的内在优势，但在复杂推理和代数运算方面的弱点。
2. 基于语言模型的优缺点，我们提出了结合自动定理证明器和语言模型进行证明搜索的首个方法：Thor。 Thor使用语言模型进行创意推理步骤，并调用Sledgehammer（Isabelle的工具，具有多个自动定理证明器）来填充前提选择的细节。我们还开发了Magnushammer，这是一个基于变换器的相关性过滤器的系统，并证明了Magnushammer在个体和作为Thor插件的情况下都优于Sledgehammer。
3. 目前所有现有的证明搜索方法仅在自然语言或形式语言上进行操作，而未将它们各自的表达力和严谨性结合起来。 为了弥补这一二分法，我们使用语言模型进行自动形式化（autoformalization），即将非正式的数学定理和证明转化为形式化的过程。通过展示自动形式化定理可作为训练数据来改进证明搜索系统，我们验证了自动形式化的实用性。我们还将多个语言的形式化定理库转化为自然语言，最终形成了一个大规模的平行数据集MMA，证明在语言模型进行微调后，能显著提高自动形式化能力。
4. 最后，我们构建了Draft、Sketch和Prove，这是一种方法论，利用语言模型将非正式证明转换为形式化证明草图，然后调用自动定理证明器填补其中的空白。 这种神经符号方法通过有效地将非正式证明转化为形式化证明并验证它们，赋予了非正式证明严谨性。

本论文的研究提出了一种新的定理证明研究范式，在这种范式中，语言模型既是自动化众多任务的可扩展动力引擎，又是人类用户与机器推理之间的可访问桥梁。