数学常被称为通用语言。但人类在教科书中书写的数学 (非形式化、直观且充满自然语言) 与计算机可验证的数学之间存在显著差异。后者需要形式化 (formalization) , 即将数学概念严谨地转换为定理证明器 (如 Isabelle 或 Lean) 可以执行并检查逻辑有效性的代码。

这种转换过程被称为自动形式化 (autoformalization) , 是该领域的巨大瓶颈。构建大型形式化数学库通常需要人类专家社区数年的努力。但如果大型语言模型 (LLMs) 能承担这一重任呢？

在本文中，我们将深入探讨 Zhang、Quan 和 Freitas 撰写的论文 “Consistent Autoformalization for Constructing Mathematical Libraries”。我们将探索一种旨在使 LLMs 不仅能翻译数学，而且能一致地进行翻译，从而构建可靠数学库的新框架。

问题: 为什么 LLMs 不能直接写数学代码？

你可能认为，因为像 GPT-4 这样的 LLMs 擅长编写 Python 或 C++，它们应该同样擅长编写像 Isabelle/ZF 这样的形式化数学语言。然而，形式化数学推理提出了独特的挑战:

  1. 专业化与漂移 (Specialization and Drift) : 当你深入特定领域 (如拓扑学或复代数) 时，概念对于模型来说变得越来越“分布外” (OOD) 。模型可能懂基础微积分，但在处理研究论文中的专业引理时会很吃力。
  2. 库的一致性 (Library Consistency) : 这一点至关重要。在软件库中，如果你定义了一个函数 add_numbers，后续必须完全照此调用。在数学库中，新定理建立在先前的定义之上。如果 LLM 翻译了一个陈述，但使用了与当前知识库 (KB) 中存在的术语或语法略有不同的表达，代码就是无用的。这破坏了语义一致性 。

研究人员提出了一种解决方案，协调三种不同的机制来解决这些问题: 最相似检索增强生成 (MS-RAG) 、去噪 (Denoising) 和带语法错误反馈的自动修正 (Auto-SEF) 。

整体框架包含三个阶段: 检索增强生成、去噪和带语法错误反馈的自动修正。

如上方的 图 1 所示，该框架分阶段运行，从自然语言输入转变为经过改进的形式化验证输出。让我们详细分解其工作原理。

阶段 1: 语境至关重要 (MS-RAG)

使用 LLMs 完成此任务的标准方法是“少样本提示 (few-shot prompting) ”，即给模型几个固定的“自然语言 \(\rightarrow\) 形式化代码”对，教它模式。

问题在于？固定的例子是静态的。如果你试图形式化一个关于拓扑学的陈述，但你的固定例子是关于算术的，模型就不会知道拓扑学所需的特定语法或定义。

研究人员提出了最相似检索增强生成 (MS-RAG) 。 系统不再使用固定例子，而是查看输入陈述 \(s\) 并搜索知识库 (KB) 以查找最相似的现有例子。

转换函数从标准提示词变更为依赖检索语境的函数:

根据相似度使用检索到的例子进行转换的方程。

这里:

  • \(s\) 是你的输入 (数学句子) 。
  • \(\{(s_i, \phi_i)\}_s\) 表示从库中检索到的相似例子集 (文本和代码对) 。
  • \(p_{auto}\) 是指令提示词。

通过根据输入的主题动态交换提示词中的例子，LLM 可以看到类似的概念过去是如何被形式化的。这有助于确保模型使用现有库中的正确“方言”和定义，从而显著提高生成有效代码的几率。

阶段 2: 输出去噪

LLMs 被训练成乐于助人的助手。这种“乐于助人”实际上是自动形式化的障碍。当被要求翻译一个定理时，LLM 经常会添加:

  • 对话填充词 (“这是您要求的代码……”)
  • 逻辑解释 (“我使用了归纳法原则，因为……”)
  • 主动提供的证明 (试图立即证明定理，通常是不正确的) 。

定理证明器就像编译器；它期望严格的语法。如果 LLM 将对话文本倾倒进文件中，编译器就会崩溃。此外，代码的风格需要与库匹配 (例如，使用特定的运算符如 \<in> 对比 \in) 。

研究人员引入了去噪 (Denoising) 来剥离这些“噪声”。他们探索了两种方法:

  1. 基于代码的去噪 (CBD) : 使用硬编码规则 (如正则表达式) 去除已知的对话模式。
  2. 基于提示的去噪 (PBD) : 要求 LLM 自己清理其输出。

事实证明，当你明确指示模型保持风格一致时, 基于提示的去噪特别强大。

请看下表，了解去噪对真实示例的影响。注意“原始 (Raw) ”输出如何包含注释和错误的语法 (如 neighborhood system of) ，而去噪版本 (特别是 PBD 1D) 剥离了文本并修正了语法以匹配库的风格。

展示使用 Mistral 的表格示例，对比原始输出与各种去噪策略。

用于此去噪步骤的提示词不仅仅是“删除文本”。它明确要求模型充当专家，严格只输出代码，同时匹配所提供示例的运算符风格。

阶段 3: 反馈循环 (Auto-SEF)

即使有了 RAG 和去噪，生成的代码仍可能有错误。也许少了一个括号，或者变量未定义。在标准软件工程中，当代码编译失败时，你会查看错误消息并修复它。

研究人员使用带语法错误反馈的自动修正 (Auto-SEF) 自动化了这一过程。

概念如下:

  1. LLM 生成形式化代码 \(d(s)\)。
  2. 系统将此代码发送给 Isabelle 定理证明器。
  3. 如果 Isabelle 接受它，太好了！我们完成了。
  4. 如果 Isabelle 返回错误 \(e_k\)，此错误消息将作为新的提示词反馈回 LLM。

指导这一迭代过程的方程为:

展示使用错误反馈进行迭代生成过程的方程。

这里，\(g_{k+1}(s)\) 是基于前一次代码 \(g_k(s)\) 和具体错误消息 \(e_{k,1}\) 在迭代 \(k+1\) 中生成的新代码。

这将 LLM 从“一次性”翻译器转变为可以调试自己工作的开发者。它允许模型利用符号定理证明器的严密逻辑来指导其神经生成。

实验结果

为了测试这个框架，作者基于 IsarMathLib (一个集合论和抽象代数库) 创建了一个名为 MathLibForm 的数据集。他们测试了几个模型，包括 Mistral、Llemma 和 GPT-3.5-Turbo。

他们使用了几种指标来评估成功，包括 BLEU 和 CodeBERTScore (与真实值的相似度) ，但最关键的指标是 Pass : 代码真的没有错误地编译通过了吗？

RAG 有帮助吗？

毫无疑问。查看下方的 表 1 , 我们可以看到，与零样本或固定的 3-样本提示相比，引入检索 (RAG) 显著提高了几乎所有指标的性能。

展示自动形式化结果的表 1。带有检索的设置始终优于基线。

这里一个有趣的发现是, Mistral (7B)——一个相对较小的模型——当配备 MS-RAG 时，在某些指标上的表现与基本状态下的 GPT-3.5 相当甚至更好。这表明，通过检索提供正确的语境与模型的原始规模一样重要，甚至更重要。

反馈循环的影响

Auto-SEF 机制 (反馈循环) 显示出明显的好处，尽管收益递减。

展示 Pass 率随迭代次数提高的图表。

如 图 2 所示，前几次错误修正迭代带来了成功率的最大飞跃。对于 GPT-3.5 (蓝线) ，通过率从大约 65% 跃升至近 71%。Mistral (红线) 也有所提升，尽管它更早进入平台期。这证实了只要错误在概念上不是太深奥，LLMs 确实可以“阅读”编译器错误消息并修复语法错误。

关于评估指标的说明

衡量自动形式化的“正确性”是很棘手的。仅仅因为代码编译通过 (Pass) 并不意味着它捕捉到了正确的数学含义。反之，代码可能在语义上很接近，但由于缺少括号而无法编译。

研究人员分析了不同指标之间的相关性:

热图显示了 BLEU、RUBY 和 Pass 等指标之间的相关系数。

图 4 中的热图显示 RUBY (一种编辑距离指标) 与其他指标之间存在很强的正相关关系。这表明，虽然没有单一指标是完美的，但它们通常在什么构成“好”的形式化方面是一致的。作者建议同时使用 Pass (语法正确性) 和 BLEU (语义相似度) 以获得全面的了解。

结论与未来启示

论文 “Consistent Autoformalization for Constructing Mathematical Libraries” 为 AI 辅助数学的未来提供了蓝图。通过超越简单的提示词，并整合 检索 (RAG) 、去噪 (Denoising) 和 符号反馈 (Auto-SEF) , 作者展示了一种构建不仅庞大而且一致、实用的形式化库的方法。

核心要点:

  • 语境为王: 检索相似示例有助于模型适应特定领域并保持库的一致性。
  • 输入净，输出清: 去噪对于弥合“健谈”的 LLMs 与严格的编译器之间的鸿沟至关重要。
  • 神经-符号协作: 最强大的系统不仅仅是神经网络；它们是集成了符号逻辑求解器 (定理证明器) 的神经网络，后者可以检查并指导输出。

随着这些技术的完善，我们正走向这样一个世界: 数学验证不仅限于少数专家，而是任何拥有研究问题和 AI 助手的人都能触手可及。