🤖 AI

Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

本文认为，仅依靠 Lean 编译率来评估自然语言到 Lean 的形式化过程具有误导性，因为语法有效性与语义忠实度之间存在显著差距，据此本文提出了一种严谨的人类校准共识指标，并指出阐述反馈（elaboration feedback）是提高形式化陈述准确性的最关键干预手段。

原作者： Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy, Yi Xie, Zhi Wang, Maziar Raissi

发布于 2026-07-01

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy, Yi Xie, Zhi Wang, Maziar Raissi

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

核心理念：翻译数学，而不只是检查它

想象你有一个由纯英文（如教科书）编写的复杂数学问题库。你想把这些问题翻译成一种严格的、计算机可读的语言，叫做 Lean。

过去，研究人员主要关注第二步：给计算机一个“完美”的翻译，并询问：“你能证明这是正确的吗？”
而这篇论文关注的是第一步：“你首先能否将英文句子正确地翻译成 Lean？”

作者认为，仅仅因为一个翻译“可行”（计算机接受了它且没有报错）并不意味着它实际上表达了与原始英文句子相同的意思。这就像是一个翻译员写出的句子语法完全正确，但却不小心改变了原意。

核心问题：“编译” vs. “忠实度”

论文引入了一个至关重要的区别：

编译（语法检查）： 计算机检查 Lean 代码是否符合语法规则。如果符合，代码即可“编译”。
- 类比： 想象一名学生在写论文。老师检查他们是否使用了正确的拼写和标点符号。如果做到了，这篇论文就“通过”了。
忠实度（含义检查）： 代码是否真的表达了原始数学问题的意思？
- 类比： 学生可能拼写完美，但当题目要求写“狗”时，他却写了“猫”。这篇论文通过了语法检查，但在含义检查上失败了。

重大发现：
作者发现这两者之间存在巨大的鸿沟。

他们最优秀的 AI 系统可以让 89.5% 的翻译能够“编译”（通过语法检查）。
然而，只有 60.5% 的翻译实际上是“忠实”的（即它们表达的意思是正确的）。
差距： 在大约 29% 的情况下，AI 生成的代码对计算机来说看起来很完美，但实际含义却是错误的。它可能遗漏了一个条件、改变了一个数字，或者把陈述变得太简单（或太难）了。

他们是如何衡量这一点的

由于计算机无法总是判断一个翻译是否具有“意义”，作者创建了一套新的测试协议：

基准测试（Benchmark）： 他们从研究生水平的教科书（实分析、复分析、拓扑学和代数）中收集了 400 个困难的数学问题。
“评委”小组： 作者没有只使用一台计算机，而是使用了两个不同的先进 AI 模型来充当评委。他们询问这些评委：“这段 Lean 代码的意思与英文句子一致吗？”
共识规则： 对于一个翻译要被视为“忠实”，两个 AI 评委都必须一致认为它是好的。
人工审计： 为了确保 AI 评委没有胡言乱乱语，人类数学专家随机检查了结果。他们证实，当 AI 评委说“不，这是错的”时，他们通常是正确的。

工具箱：如何修复翻译

作者测试了一个“工具增强型智能体”（一个聪明的 AI 助手），它可以利用三种特定的工具来修复其错误。他们像进行科学实验一样，通过开启或关闭这些工具来观察哪一个最有帮助。

把这个 AI 想象成一名试图进行数学翻译的学生。这些工具分别是：

专家起草 (T)： AI 向一个专门的“翻译机器人”请求一份初稿。
- 类比： 在进行编辑之前，向专业翻译寻求一份粗略的草案。
搜索 (S)： AI 在数学库 (Mathlib) 或网络上查找定义和符号。
- 类比： 在字典中查词，以确保自己使用的是正确的术语。
反馈 (F)： AI 尝试编译代码。如果失败，计算机会给出错误信息，然后 AI 尝试修复它。
- 类比： 老师批改论文并说：“你这里漏掉了一个逗号，”或者“这句话逻辑不通。”

工具箱的结果：

反馈 (F) 是 MVP（最有价值球员）： 这是最强大的工具。它修复了最多的“语法错误”（编译问题）。然而，它也揭示了一个问题：通过过度积极地修复语法，它有时会创造出语法完美但含义仍然错误的代码。
搜索 (S) 有助于落地： 它帮助 AI 选择正确的词汇，但不如反馈功能强大。
专家起草 (T) 变得不再重要： 一旦 AI 拥有了反馈和搜索功能，来自“专家机器人”的“初稿”就没能提供太多价值。如果有了其他工具，AI 完全可以靠自己做得一样好。

主要结论

论文的结论是，我们不能仅仅因为 AI 能“编译”代码就对其表示赞赏。

旧方式： “看！AI 写出了计算机接受的代码！”
新方式： “看！AI 写出了计算机接受且确实表达了我们所要求之意的代码！”

作者表明，虽然 AI 在处理数学代码的“语法”方面做得非常好，但在保持“含义”完整性方面仍然面临困难。他们提供了一种衡量这种差距的新方法，并表明使用工具组合（尤其是反馈和搜索）是弥补这一差距的最佳方式，但即便如此，仍有相当一部分翻译会丢失原始含义。

简而言之： 仅仅因为计算机说“做得好”，并不意味着 AI 真的理解了数学。我们需要检查含义是否得到了保留，而不仅仅是检查代码能否运行。

技术摘要：超越编译：评估忠实的自然语言到 Lean 陈述形式化

1. 问题陈述

本文探讨了自然语言到 Lean 陈述形式化的任务：即自动将非正式的数学陈述翻译为有效的 Lean 4 定理声明。这一任务与定理证明不同。在定理证明基准测试（如 MiniF2F、LeanDojo）中，形式化陈述是固定且可信的；系统的目标是生成被检查器接受的证明。而在陈述形式化中，系统必须生成陈述本身。

核心挑战在于，编译是成功完成任务的必要而非充分条件。一个 Lean 声明即使能够通过类型检查（编译），仍可能出现以下情况：

遗漏关键假设。
改变了论域。
强化或削弱了原有的断言。
编码了一个空洞的版本。

以往的工作通常依赖于编译率或基于引用的等价性指标（例如 BEq、回译）。本文认为，仅靠编译会产生一个“编译通过差距”（compile-pass gap），即系统看似成功，却未能保留预期的数学含义。作者将核心问题定义为评估忠实的陈述形式化：生成的声明既要能编译，又要能保留自然语言输入的语义意图。

2. 方法论

2.1 基准测试构建

作者策划了一个由 400 个自然语言陈述组成的研究生水平基准测试，这些陈述源自开源 LaTeX 讲义和教科书。该数据集在四个领域之间保持平衡：

实分析 (100 条)
复分析 (100 条)
拓扑学 (100 条)
代数学 (100 条)

至关重要的是，这些陈述没有附带金标准 Lean 声明，从而确保了该任务代表的是真正的翻译而非检索。

2.2 评估协议

本文提出了一种经人类专家校准的**共识 LLM-as-Judge（大模型作为评判者）**指标，用于评估忠实度。该协议包含两个阶段：

编译器验证： 任何无法编译的代码立即被视为不忠实。
语义共识： 对于编译通过的代码，两个独立的 LLM 评判者（GPT-5.2 和 Gemini-2.5-Pro）会将生成的 Lean 声明与原始自然语言陈述进行对比。它们会分配一个忠实度分数（0–10）。
- 成功指标： 当且仅当生成的声明既能编译且两位评判者的评分均 $\ge 9$ 时，才被视为忠实（Faithful）。
- 这种严格的共识方法旨在作为系统比较的一个保守操作点，而非形式化的等价性证明。

2.3 人类校准

为了验证自动化指标，作者进行了人工审计：

共识正向（Consensus-Positive）： 被严格共识判定为忠实的输出中，有 96.0% 经人工审核确认是忠实的。
共向负向（Consensus-Negative / 编译通过）： 在编译通过但被共识拒绝的输出中，有 82.4% 被人工确认是真实的语义失败。
这证实了该指标是一个高精度、保守的过滤器，能有效识别语义漂移。

2.4 实验设置：析因设计

作者使用 $2^3$ 析因设计评估了各种系统（通用 LLM、专门的形式化工具、面向证明的模型以及工具增强型智能体），以分解三种常见干预措施的影响：

参数化专家起草 (T)： 使用微调模型（Herald）生成初始草案。
知识搜索 (S)： 使用工具查询 Mathlib（符号查找、命名空间解析）并进行网络搜索以实现落地。
Lean 精化反馈 (F)： 使用 REPL 迭代编译代码并接收错误信息以进行修复。

智能体架构使用一个中央编排器（GPT-5.2），该编排器维护状态并根据配置决定调用哪些工具。

3. 关键结果

3.1 编译通过差距

最重要的经验发现是编译率与语义忠实度之间的分歧：

一个全工具增强的智能体实现了 89.5% 的编译率。
然而，在严格的共识指标下，仅有 60.5% 的输出被判定为忠实。
这留下了 29.0 个百分点的差距，即输出虽然编译通过，但未能通过语义检查。人工审计证实，大多数“编译通过但共识负向”的情况确实是真实的语义失败（例如：缺失假设、断言空洞）。

3.2 模型性能

专门形式化工具与证明模型： 专门的陈述形式化工具（如 Herald、Kimina-Autoformalizer）和面向证明的模型（如 Goedel-Prover、Kimina-Prover）在未提供形式化目标时，在生成陈述方面的表现很差。它们的忠实度范围仅在 4.0% 到 12.3% 之间。
通用 LLM： 单次提示（one-shot）的通用模型达到了 19.8–28.0% 的忠实度。
工具增强型智能体： 全功能智能体框架显著优于单次提示基准，达到了 60.5% 的忠实度。然而，尽管基准不同，不同的编排器（Sonnet 4.5、Gemini-2.5-Pro）最终都收敛到了相似的性能水平（60–65%），这表明收益主要源于工具增强方法的结构性优势，而非特定编排器模型的特性。

3.3 干预措施的析因分解

研究隔离了三种工具的影响：

精化反馈 (F)： 这是有效性（编译）的最大驱动力，显著提高了编译率。然而，它也扩大了“编译通过但不忠实”的范畴，因为它允许更多语法正确但语义漂移的陈述通过。
搜索 (S)： 搜索主要提高了落地性（grounding）和选择性。它缩小了编译通过差距（即它有助于过滤掉那些虽然能编译但语义错误的陈述），并通过减少所需的 REPL 迭代次数提高了效率。其边际收益在缺乏反馈的情况下最高。
专家起草 (T)： 一旦具备反馈和搜索功能，微调后的起草先验知识在很大程度上是可替代的。事实上，在拥有完整反馈的情况下，起草先验反而略微损害了性能，这表明在特定的工具栈中，一个带有编译器反馈的强力编排器可以超越专门的起草模型。

3.4 特定领域的变化

复分析从编译器反馈中获得的收益最高（忠实度提升了 54.2 个百分点），这可能是由于 Mathlib 的覆盖较为成熟。
实分析和代数的收益较小，表明要么是库支持有限，要么是内在的形式化难度较高。
拓扑学在处理高级概念（如覆叠空间）时表现出特定的挑战，在这些情况下，反馈往往会导致有效但语义发生偏移的陈述。

4. 重要性与主张

本文主张，陈述形式化必须被评估为意义保留，而不仅仅是 Lean 的接受程度。其主要贡献包括：

一种新指标： 一种经过人类校准、基于共识的指标，揭示了“编译通过差距”，表明许多系统生成的陈述虽然语法有效，但在语义上是错误的。
诊断性分解： 通过析因分析表明，工具并非单调的增益项。虽然反馈可以修复语法，但它可能掩盖语义错误；搜索提高了落地性但存在收益递减；而专门的起草在反馈丰富的循环中并非总是必要的。
系统比较： 证据表明，目前的证明导向模型和专门的形式化工具，在没有显式的以陈述为中心的训练或工具增强协议时，并不能自动将其证明能力迁移到语义忠实的陈述生成任务中。

作者总结道，未来的系统应当将强大的 Lean 反馈与语义评估相结合，并制定决策策略来决定何时进行搜索、修复或停止，而不是仅仅依赖于平均准确率的提升。本文明确避免声称其指标是形式化的等价性证明，而是将其定位为一个保守且可扩展的系统比较决策边界。