🤖 AI

Does the Proof Prove It That Way? Faithful Formalization of Elements Proofs

本文介绍了 Pistis，这是一个具有代理性（agentic）且由 Oracle 指导的系统，其采用了新颖的“OrderDecompose”搜索策略，通过将自然语言推理与形式化策略（tactics）进行严格对齐，为《欧几里得几何原本》生成忠实的 Lean 形式化证明，从而在速度、成功率以及人类/大语言模型偏好方面均超越了先前的基准模型，并能有效识别数学论证中的缺陷。

原作者： Tadd Mao, Tianjun Zhong, Dhruva Arekar, Yuming Feng, One An, Jiani Huang, Xujie Si, Ziyang Li

发布于 2026-08-18

📖 1 分钟阅读☕ 轻松阅读

CC BY 4.0

原作者： Tadd Mao, Tianjun Zhong, Dhruva Arekar, Yuming Feng, One An, Jiani Huang, Xujie Si, Ziyang Li

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

数学一直以来都依赖于两种截然不同的语言。一种是我们用来解释想法、讲述故事和分享见解的自然语言；它灵活、富有上下文气息，并且经常跳过人类读者看来显而易见的步骤。另一种是证明辅助工具（proof assistants）的正式语言，它们是僵化的计算机系统，通过检查每一个逻辑步骤来确保结论是无可争议的真理。几十年来，研究人员一直致力于将第一种语言转化为第二种语言，这一过程被称为自动形式化（autoformalization）。其目标很简单：将人类编写的证明转化为计算机可以验证的代码。但一个关键问题始终存在：计算机生成的证明虽然在技术上是正确的，却往往与激发它的那个人类论证毫无相似之处。计算机可能会使用完全不同的路径来解决问题，将原始的推理过程隐藏在自动化捷径构成的围墙之后。这造成了真理与理解之间的鸿番。如果计算机的证明不遵循人类的步骤，我们就无法利用它来检查人类的推理是否真的严密，也无法信任它来教导我们论证是如何运作的。

一支研究团队现在通过一种新系统解决了这一差距，该系统旨在使计算机的证明忠实于人类原始的思想过程。他们将这个系统称为 Pistis，这个名字取自古希腊语中表示“信仰”或“信任”的词汇。研究人员将该系统应用于欧几里得《几何原本》的前三卷——这是一部写于两千多年前的基础几何文本。他们的工作证明，在不丢失原始逻辑的情况下，将这些古老的论证转化为现代计算机语言是可能的，同时还能发现该文本中延续数世纪未被察觉的隐藏错误。

该团队面临的核心挑战在于，自然语言和计算机逻辑运行在不同的节奏上。人类的证明可能会说：“让我们假设这是真的，”然后继续向下进行，期望读者能填补其中的空白。然而，计算机要求每一个步骤都必须被明确陈述并得到证明。以往的翻译尝试往往会让计算机用自己的逻辑来填补这些空白，从而有效地重写了论证，使其更容易被机器求解。其结果是，证明虽然成功编译，却未能反映出人类作者的原意。Pistis 的建立正是为了防止这种情况。它不是要求计算机寻找任何可能的途径来证明该命题，而是强制计算机按照人类特定的路径，逐句进行。

为了实现这一点，研究人员开发了一种将翻译过程分为两个不同阶段的方法。首先是映射阶段，它分析自然语言文本并将其拆分为一系列微小的、原子的步骤。它精确地识别出每一句话的主张以及它所依赖的假设。这创建了一个计算机必须遵循的严格模板。第二是填充阶段，它尝试单独证明这些微小的步骤。该系统使用了一种专门的搜索策略，防止计算机采取捷径或提前跳跃。如果计算机无法使用人类文本中提到的确切工具和引用来证明某个特定步骤，它不会简单地寻找另一种方式来解决问题，而是会标记出该问题，揭示出原始的人类论证可能存在漏洞或缺失环节。

这种方法在测试欧几里得几何时表现得异常出色。研究人员为前三卷中的 92 个命题生成了形式化证明。当他们将这些新证明与以往的尝试进行比较时，差异非常显著。新的证明编译速度快了三十三倍以上，这种效率上的显著提升表明，新方法避免了旧系统那种沉重且缓慢的计算。更重要的是，评审证明的人类专家更倾向于新系统的输出。在一项盲测研究中，评审人员发现新证明具有更高的透明度，并且能更好地代表原始教科书的论证。一个经过训练以评估翻译质量的人工智能评判员也一致认为，新证明优于旧证明，比例超过五比一。

除了单纯地翻译文本外，该系统还充当了一个严谨的检查器，暴露了源材料中的真实缺陷。由于系统坚持遵循人类的逻辑，它无法掩盖错误。在一个案例中，系统识别出了现代译本中关于欧几里得的一个引用错误。文本引用了一个关于平分线段的命题，但引用的位置却指向了一个关于平分角度的命题。系统标记了这种不匹配，显示出该翻译将错误的观点关联到了错误的步骤上。在另一个案例中，系统发现了欧几里得自身推理中的一个缺口，即某个特定场景未被处理。研究人员能够通过形式化手段证明原始论证是不完整的，如果没有这样一个严格遵循原始结构的工具，这种发现将很难实现。

Pistis 的成功表明，忠实的正式化不仅是一项技术练习，更是验证人类知识的强大工具。通过迫使计算机走与人类相同的路径，该系统可以确认推理是否成立，或者在哪里失效。研究人员发现，他们的方法可以接受有效的论证，驳斥无效的论证，并精准定位证明出错的位置。这种能力可以扩展到几何学之外；该框架旨在处理任何以自然语言编写的数学论证。这项工作表明，我们不必在人类解释的灵活性与机器验证的严密性之间做出选择。只要引导机器去尊重人类原始的声音和逻辑，我们就可以兼得两者。

研究还强调了当前技术的局限性。虽然该系统在处理欧几里得前三卷时表现良好，但如果没有额外的人类指导，它无法处理后续书籍中的每一个命题。某些命题涉及到的几何概念是底层计算机系统尚未掌握如何处理的概念，例如测量曲线长度。研究人员指出，他们的系统依赖于人类或高级人工智能作为“先知”（oracle），来验证初始文本映射的正确性。这意味着该过程目前尚未实现完全自动化，但与以往的方法相比，它显著减少了手动操作的工作量。

最终，这篇论文为人工智能时代的数学证明互动设定了新标准。它超越了“计算机能否证明一个定理”的问题，转向了更深刻的“计算机是否理解该论证”的问题。通过确保形式化证明能够逐步镜像自然语言论证，研究人员创造了一个能够验证结论背后的推理过程，而不只是验证结论本身的工具。这使得数学家和学生能够相信，计算机不仅仅是在寻找一个解，而且是在真正遵循编写证明的人的逻辑。这项工作提供了一条路径，让人的洞察力与机器的精确性协同工作，在利用现代验证能力的同事，也保留了数学发现的完整性。

技术摘要：“证明过程是否忠实于原意？元素论证明的忠实形式化”

问题定义

本文探讨了形式化验证领域的一个关键空白：虽然自动化证明搜索可以生成可编译（即满足正确性）的形式化证明，但这些证明往往无法反映原始自然语言（NL）论证的推理结构。这种特性被称为忠实性（faithfulness），对于验证人类或人工智能推理的有效性、辅助数学家形式化数学草稿，以及确保教学与研究的可读性至关重要。

目前的方法通常将忠实性视为一种风格上的修饰，或依赖于语义匹配等粗略的代理指标。然而，实现真正的忠实性非常困难，主要源于三个层面的错位：

结构错位： 证明助手（如 Lean）通过策略（tactics）变换证明状态来推进，而自然语言证明则通过数学推理的句子来推进。
隐性步骤： 自然语言证明经常省略人类认为“显而易见”但形式化系统要求明确表达的步骤。忠实的形式化必须在不改变底层证明结构的前提下填补这些空白。
缺乏定义： 文献中缺乏精确且可检查的证明忠实性定义，导致评估依赖于启发式方法而非认证。

作者将该问题定义为：给定一个自然语言命题 $P_{NL}$ 、其形式化陈述以及一个自然语言证明 $F_{NL}$ ，生成一个满足五个必要忠实性条件且保持正确的 Lean 形式化证明。

方法论：Pistis

作者引入了 Pistis，一个由预言机（oracle）引导的智能体框架，用于进行忠实的证明形式化。该系统分为两个截然不同的阶段运行：

1. 映射阶段 (Map Stage)

在此阶段，一个受预言机（人类或自动化工具）引导的 LLM 智能体会将自然语言证明分割为原子断言。智能体会生成一个包含以下内容的“忠实模板”：

$\bar{s}$ ： 将自然语言证明划分为序列段 $s_1, \dots, s_n$ 的有序划分。
$\bar{\phi}'$ ： 与自然语言段对应的形式化子目标（占位符）序列。
映射关系： 函数 assumps(·) 和 assert(·)，分别将每个自然语言段映射到其形式化假设和断言。
约束条件： 智能体需确保覆盖度（各段必须覆盖整个自然语言文本）、原子性（每个段落仅包含单一断言）以及顺序（形式化步骤遵循自然语言的顺序）。

2. 填充阶段 (Fill Stage)：OrderDecompose

其核心创新是 OrderDecompose，一种新型的、递归的、分而治之的搜索算法，旨在解决映射阶段留下的 sorry 子目标。

有序分解： 不同于寻找“任何”证明项的标准证明搜索，OrderDecompose 严格按顺序证明子目标 $\phi'_1, \dots, \phi'_N$ 。
递归策略： 对于每个子目标，算法尝试直接进行基于 SMT 的证明。如果失败，它会将目标递归地分解为中间引理。
忠实性卫兵 (Faithfulness Guards)：
- 引用依赖： 系统强制要求自然语言文本中引用的任何命题必须恰好在论证调用它的位置被应用，防止使用未被引用的更强定理。
- 结构保留： 映射阶段生成的顶层结构被锁定；填充阶段只能插入中间步骤，而不能重写论证流程。
- 反驳与缺口检测： 如果一个子目标无法闭合，系统会采用反驳技术（证明其否定形式或寻找反例）来识别自然语言证明中的真实缺陷或翻译错误，而不是进行无声的修补。

核心贡献

忠实的产物： 生产了高质量的 Lean 产物，包含了对欧几里得《几何原本》第一至三卷（92 个命题）的忠实形式化证明。
忠实性分类法： 提出了一个由五个必要条件组成的严谨定义：
- 覆盖度 (Coverage)： 自然语言段拼接后等于原始证明。
- 原子性 (Atomicity)： 每个段落具有单一断言及特定的假设。
- 原子忠实性 (Atomic Faithfulness)： 形式化断言和假设忠实地代表了自然语言内容。
- 顺序 (Order)： 形式化步骤作为最终证明的一个子序列出现，并与自然语言顺序相匹配。
- 引用 (Citation)： 被引用的命题被应用于正确的逻辑点。
OrderDecompose 算法： 一种在效率与结构保真度之间取得平衡的搜索方法，防止了以往工作中常见的“黑盒式”推理步骤坍缩。
缺口识别： 能够形式化地接受或反驳自然语言证明，从而揭示真实的错误（例如翻译中的引用错误）或隐性缺口。

结果与评估

作者在 92 个命题上将 Pistis 与 LeanEuclid（此前声称具备忠实性的工作）以及普通的 LLM 智能体基准进行了对比评估。

忠实性： 在盲审的人类研究（由 14 位专家进行的 127 次评审）中，Pistis 生成的证明被选中的频率比 LeanEuclid 高出 2.89 倍。在针对第一卷的 LLM-as-a-judge 协议中，Pistis 的胜出频率是后者的 5.2 倍。Pistis 在步骤保真度、数学透明度和教科书呈现度方面均表现更优。
效率： Pistis 证明的编译速度比 LeanEuclid 快 33 倍（第一卷的编译时间为 13.3 分钟，而 LeanEuclid 为 7.3 小时以上）。这归功于分解后的结构避免了沉重的、单体式的 SMT 依赖。
成功率： 在一个 12 小时的预算消融实验中，OrderDecompose 完成了 15 个测试命题中的 100%，而基准 LLM 智能体仅完成了 40%（6/15），其余则因超时失败。
缺口发现： 系统识别出了《几何原本》证明及翻译中的 52 个缺口，其中包括翻译文本中的 2 个真实引用错误（例如在几何构造中引用了错误的命题）以及 33 个假设缺口。

意义与主张

论文声称，忠实性不仅是一种风格偏好，更是一种功能性的必要条件。通过确保形式化证明逐步镜像自然语言论证，Pistis 实现了：

推理验证： 不仅仅是验证最终定理，而是验证论证本身的有效性。
错误定位： 精确指出论证何处失效或何处存在缺口，而不是进行无声的修正。
可读性： 创建能够被人类理解的产物，架起非形式直觉与形式严谨性之间的桥梁。

作者将 Pistis 定位为一种超越“定理生产配额”、转向使人们能够“更清晰地理解和思考”数学的工具。他们承认了局限性，指出目前的范围仍限于 System E 框架内的欧几里得几何，且系统仍依赖预言机来认证初始映射，但他们断言，其方法为构建可信、可解释的数学 AI 提供了必要的基石。