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

更强的形式化数学推理自动化能力提供了可扩展性、可信性和可访问性：它能够高效验证复杂证明，减少复杂计算中的错误可能性，使非专家也能参与数学概念的研究，并可能通过机器驱动的探索促进新数学见解的发现。传统上，自动化推理器只能使用形式化语言资源库，而无法利用规模更大的自然语言语料库，因为自然语言理解较为困难。尽管已经设计了具有形式化语法的受控自然语言接口（例如 Naproche），但它们最终过于僵化，难以广泛使用。另一方面，大型语言模型擅长语言理解，并且接触了人类历代积累的无数数学文献，使其成为自动化工具的理想候选者。现代语言模型经过大量数据训练，能够执行多种任务。语言模型的多样性与传统推理器的僵化性形成互补，后者的局限性严重限制了其广泛应用和易用性。本论文的目标是回答如何利用语言模型实现可信的数学推理自动化。为此，我们引入了一种新颖的语言模型评估方法，以确定其在数学推理中的适用场景。基于这些见解，我们训练语言模型在自动化定理证明器的辅助下在这些场景中编写形式化证明，并利用它们将数学定理和证明从 LaTeX 翻译为形式化语言。具体而言，（1）我们首次对语言模型在非形式化数学推理中的表现进行了交互式评估。评估揭示了语言模型在记忆和灵活输入/输出方面的固有优势，以及在复杂推理和代数操作方面的弱点。（2）基于语言模型的优势和劣势，我们开发了首个结合自动化定理证明器和语言模型的证明搜索方法：Thor。Thor 使用语言模型处理创造性的证明步骤，并调用 Sledgehammer（Isabelle 的工具，可访问多种自动化定理证明器）来填充前提选择细节。我们还开发了 Magnushammer，这是一个类似 hammer 的系统，具有基于 Transformer 的相关性过滤器，并证明 Magnushammer 在单独使用和作为 Thor 插件时均优于 Sledgehammer。（3）现有的证明搜索方法要么基于自然语言，要么基于形式化语言，未能结合两者的表达能力和严谨性。为了解决这种二分法，我们使用语言模型进行自动形式化，即将非形式化的数学定理和证明转化为形式化内容。我们通过展示自动形式化的定理可以作为训练数据来改进证明搜索系统，验证了自动形式化的实用性。我们还从多语言的形式化定理库中提取内容，并将其非形式化为自然语言。这形成了一个大规模的非形式化与形式化数学定理并行数据集 MMA，当语言模型在其上进行微调时，显著提升了自动形式化能力。（4）最后，我们构建了 Draft, Sketch, and Prove 方法，该方法使用语言模型将非形式化证明翻译为形式化证明草图，然后调用自动化定理证明器填补细节。这种神经符号方法通过有效地将非形式化证明翻译为形式化证明并验证其正确性，赋予非形式化证明以严谨性。本论文的研究提出了一种新的定理证明研究范式，其中语言模型既是自动化多种任务的可扩展动力引擎，也是人类用户与机器推理之间的可访问桥梁。