💻 computer science

Pseudo-Formalization for Automatic Proof Verification

本文介绍了伪形式化，一种结合自然语言灵活性与形式化模块性的混合证明格式，以及相应的块验证算法，该算法在准确验证奥林匹克竞赛及研究级基准上的数学证明方面，显著优于现有的“大语言模型即裁判”基线方法。

原作者： Slim Barkallah, Luke Bailey, Kaiyue Wen, Mohammed Abouzaid, Tengyu Ma

发布于 2026-05-21

📖 1 分钟阅读☕ 轻松阅读

原作者： Slim Barkallah, Luke Bailey, Kaiyue Wen, Mohammed Abouzaid, Tengyu Ma

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

想象你是一家享有盛誉的数学期刊的高级编辑。你收到了一篇由一位才华横溢但略显混乱的数学家（或人工智能）撰写的 50 页证明。这篇证明是用自然语言写成的，充满了“由此可得”、“显然”和“众所周知”等表述。你的任务是找出那个会毁掉整个证明的微小逻辑错误。

这样做就像以每小时 100 英里的速度阅读一本小说，同时试图找出其中的一个拼写错误。如果你错过了错误，你就会发表荒谬的内容；如果你读得太慢，你就永远无法完成。

这篇论文《用于自动证明验证的伪形式化》提出了一种解决该问题的新方法。它在人类书写数学时那种混乱而灵活的方式，与计算机检查数学时那种僵化而机械的方式之间，寻找了一个中间地带。

以下是他们解决方案的分解，使用了简单的类比：

1. 问题：“文字墙”

目前，当我们要求人工智能检查数学证明时，我们通常只是将整个证明喂给人工智能，然后问：“这是对的吗？”

问题所在： 这就像要求一个人在一口气读完一份 100 页的法律合同后，找出其中的一个矛盾之处。人工智能会感到困惑，读到结尾时已经忘记了开头，从而错过错误。这被称为“上下文腐烂”——你喂给它的文本越多，它发现错误的能力就越差。

2. 解决方案：“伪形式化”（乐高类比）

作者们引入了一种名为**伪形式（PF）**的新格式。

类比： 想象那团混乱的证明是一团巨大的、纠缠不清的毛线球。伪形式化就是剪断那团毛线，并将其重新编织成整齐、独立的乐高积木的过程。
工作原理： 证明不再是一个长长的段落，而是被分解成许多小的、自包含的“块”（如引理、命题和定理）。
规则： 每个块必须清楚地说明：
1. 前提： 我们基于什么假设开始？
2. 结论： 在这个特定的块中，我们要证明什么？
3. 证明： 从 1 到 2 的步骤。
好处： 现在，人工智能不再需要检查整团毛线，而只需一次检查一块乐高积木。这是一个微小且易于管理的任务。

3. 过程：“工厂装配线”

该论文描述了一个用于验证证明的四步装配线：

翻译（建筑师）： 人工智能将混乱的自然语言证明重写为这些整齐的乐高块（伪形式格式）。这就像一位翻译，将一段漫无边际的演讲转化为结构化的大纲。
块验证（质检员）： 现在，人工智能充当质检团队。每位质检员只查看一块乐高积木。他们检查：“给定前提，该积木内的证明是否确实得出了结论？”他们不担心建筑物的其余部分；他们只检查自己特定的积木。
校准（经理）： 有时，质检员可能会过于挑剔（标记出拼写错误）或遗漏某些内容。一位“经理”人工智能会查看所有质检员的报告，并决定：“好吧，这里确实有一个错误，或者那只是误报吗？”它将调查结果汇总为最终裁决。
并行扩展（大众）： 为了格外确保万无一失，他们将整个流程运行 8 次（就像 8 支不同的质检团队）。如果任何一支团队发现错误，该证明就会被拒绝。这确保了他们能捕捉到几乎所有的问题。

4. 结果：优于基线

作者在两种类型的数学上测试了这种方法：

奥林匹克数学： 高难度的竞赛问题（如国际数学奥林匹克）。
研究数学： 来自 arXiv 的真实已发表学术论文，作者们自己承认其中存在错误。

发现：

与仅仅要求人工智能阅读整个证明的标准方法相比，“伪形式”方法在发现错误方面表现更好。
它发现了更多的错误（更高的召回率），而没有编造虚假的错误（更高的精确率）。
在数学验证领域，这是一种“帕累托改进”——意味着他们在不牺牲任何质量的情况下获得了更好的结果。

5. 新基准："ArxivMathGradingBench"

为了证明他们的方法在现实世界研究中有效，作者构建了一个新的测试数据集。

他们选取了 35 篇真实的数学论文，这些论文已由作者更新以修复错误。
他们利用这些“已知错误”来测试他们的人工智能能否找到作者已修复的具体错误。
这就像一场“驾驶考试”，考官确切知道坑洼在哪里，并观察新车（人工智能）是否能撞上它们。

总结

该论文认为，我们不需要强迫人工智能使用“机器人语言”（如 Lean 或 Isabelle）来检查数学。相反，我们可以教会人工智能将人类数学组织成整齐的小块。通过将巨大而令人困惑的证明分解成小而清晰的乐高积木，人工智能可以以激光般的专注力检查每一部分，找出如果试图一次性阅读整个证明就会错过的错误。

他们并未声称：

他们并未声称这将取代人类数学家。
他们并未声称这适用于非数学领域（尽管他们推测可能适用）。
他们并未声称人工智能是完美的；他们只是表明，在发现错误方面，它比以前的方法更好。

技术摘要：用于自动证明验证的伪形式化

问题陈述

可靠的数学证明自动验证仍然是训练和评估复杂数学推理人工智能系统的关键瓶颈。虽然完全形式化的证明（例如在 Lean 或 Isabelle 中）因其语义精确性和模块化而易于验证，但大多数证明——特别是由人工智能生成或以自然语言撰写的人类证明——缺乏这些特性。由于形式化库的不完整以及所需巨大的专家工作量，将自然语言证明翻译为完全形式化语言对于前沿数学而言往往不可行。因此，当前的验证方法（如"LLM 作为裁判”——直接评估自然语言证明）在精确度和召回率方面表现挣扎，往往无法识别长而复杂论证中的具体错误。

方法论：伪形式化与块验证

作者提出了**伪形式化（Pseudo-Formalization, PF）结合块验证（Block Verification, BV）**的框架，旨在弥合自然语言的灵活性与形式化证明的可验证性之间的差距。

1. 伪形式化证明格式

伪形式化证明将自然语言论证分解为一系列自包含的模块（引理、命题、断言）。每个模块是一个元组 $(P, c, \pi)$ ，表示：

前提（ $P$ ）： 明确陈述的假设和继承的上下文。
结论（ $c$ ）： 正在证明的具体断言。
证明（ $\pi$ ）： 从 $P$ 建立 $c$ 的自然语言论证。

该结构由两个图控制：

依赖图（ $G$ ）： 一个有向无环图（DAG），如果某个模块调用了另一个模块的结论，则存在一条边。这防止了循环论证。
作用域继承森林（ $T$ ）： 一种森林结构，以层次化方式组织模块（例如，命题内的引理），允许上下文（定义、假设）被继承而无需重述。

作者将“良好的伪形式化证明”定义为符合两个期望属性的证明：简洁性（简短的证明，调用较少的其他节点）和有界作用域深度（浅层继承树）。理论上，验证此类证明允许每个验证步骤所需的上下文长度独立于证明的总大小，从而缓解“上下文腐烂”（即随着输入长度增加，LLM 性能下降的现象）。

2. 验证流程（PF+BV）

验证过程包含四个步骤，均利用现成的 LLM 而无需微调：

翻译： 一个 LLM 将原始自然语言证明 $\Pi$ 翻译为伪形式化证明 $\hat{\Pi}$ 。一个可选的自我修复循环将 $\hat{\Pi}$ 与 $\Pi$ 进行比对，以确保忠实性。
块验证： 一个验证器 LLM 独立检查 $\hat{\Pi}$ 的每个模块。它接收模块的完整前提（包括继承的上下文）、结论、证明以及任何被调用的子模块的已验证结论。它输出接受裁决或具体的错误描述。
校准： 一个校准器 LLM 将每个模块的错误报告汇总为最终裁决。它可以应用可配置的严格性阈值，并将块级错误映射回原始证明的结构（例如，识别具体的步骤或引理）。
并行扩展： 整个流程独立运行 $k$ 次。仅当所有 $k$ 次运行都接受该证明时，证明才被接受（悲观聚合）。这允许通过改变 $k$ 来权衡精确度和召回率。

主要贡献

伪形式化（PF）： 一种新的证明格式，既保留了自然语言的灵活性，又强制实施了可靠验证所需的模块化和明确的前提 - 结论结构。
块验证（BV）： 一种通过将证明分解为独立块来验证证明的算法，理论上降低了上下文需求，并在经验上提高了错误检测能力。
ArxivMathGradingBench： 一个新的基准，包含 35 篇来自 arXiv 的研究级数学论文，其中包含已知的、经作者修正的错误。该数据集填补了现有基准的空白，通过在现实世界的研究证明而非竞赛级问题上测试验证能力。
理论依据： 作者提供了一个定理（定理 1），证明对于“良好”的伪形式化证明，块级验证可以由固定大小的 Transformer 模拟，其上下文长度独立于证明大小，这与全证明验证所需的线性上下文增长形成对比。

实验结果

该方法在两个基准上进行了评估：Hard2Verify（奥林匹克/普特南级别问题）和ArxivMathGradingBench（研究级论文）。

性能与基线对比： 在两个基准上，PF+BV 均帕累托优于"LLM 作为裁判”的基线。这意味着对于任何给定的召回率水平（发现错误的能力），PF+BV 都能实现更高的精确度（更少的误报），反之亦然。
Hard2Verify： PF+BV 在召回率（约 90%）上与基线持平，但显著减少了每篇证明标记的错误数量（在 $k=8$ 时，误报减少了 40% 以上）。
ArxivMathGradingBench： 该基准极具挑战性，在 $k=8$ 时，两种方法都留下了约 50% 的标注错误未被发现。然而，PF+BV 在召回率、误报率以及所有标注错误均被发现的论文比例方面，始终优于基线。
定性分析： 案例研究（例如 IMO 2024 P6）表明，PF+BV 通过将逻辑跳跃隔离到局部块中而取得成功。这使得验证器能够在无需重新评估整个全局论证的情况下，检测到证明何时错误地加强了前提（例如，从“没有 $d$ 和 $-d$ "推断出“符号相同”）。

意义与主张

该论文主张，伪形式化为验证现代数学研究提供了一种替代自动形式化（翻译为 Lean/Isabelle）的实用方案。虽然自动形式化提供了更强的正确性保证，但由于库的不完整，它对于当前的研究往往难以处理。PF+BV 牺牲了形式化验证的绝对确定性，以换取对更广泛数学领域的适用性，它利用自然语言丰富的词汇和标准技术，同时施加一种使错误更容易定位的结构。

作者将这项工作定位为迈向可扩展的 AI 推理监督的一步，提供了一种机制，用于在训练 LLM 解决高难度数学问题时生成可信的奖励信号，并协助人类数学家审查证明。他们承认了局限性，指出生成忠实的伪形式化重写并非易事，未来的工作可能涉及训练模型直接以这种格式生成证明。