💻 computer science

Benchmarking Testing in Automated Theorem Proving

本文介绍了"T"，这是一种新颖的框架，通过验证依赖后继定理是否成功编译来评估人工智能生成的形式化定理的语义正确性，揭示了当前大型语言模型在定理生成能力方面与传统词汇或人工评估方法相比存在的显著差距。

原作者： Jongyoon Kim, Hojae Han, Seung-won Hwang

发布于 2026-04-28

📖 1 分钟阅读☕ 轻松阅读

原作者： Jongyoon Kim, Hojae Han, Seung-won Hwang

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

想象一下，你正在聘请一支建筑师团队来设计一座新桥。

旧有的测试方式（编译）
过去，在评估这些建筑师（在本文中即 AI 模型）时，我们仅检查他们的蓝图是否“语法正确”。我们会问：蓝图是否符合语法规则？线条是否连接？计算机是否显示“语法通过”？

如果蓝图在纸面上看起来完美无缺，我们便假设这座桥能够稳固。但问题在于：一位建筑师可以画出一张写着“这座桥由纯金制成”的蓝图，而计算机仍会显示“语法通过！”，因为这句话在语法上是正确的。然而，如果这张蓝图本应是用于“钢制悬索桥”的，那么即便语法完美，这位建筑师也未能胜任实际工作。

在数学和计算机代码的世界中，这被称为编译。AI 写下一个定理（一个数学陈述），计算机检查它是否能编译（即无错误地运行）。该论文认为，这是判断 AI 是否真正理解数学的糟糕方法。

新的测试方式（T2 框架）
该论文的作者提出了一种名为**T2（定理测试）**的新方法。他们不再仅仅检查蓝图的语法，而是问：当我们尝试围绕它建造整座城市时，这张蓝图是否真的行得通？

他们使用了一个名为集成测试的概念。想象这座桥只是庞大城市的一部分。

目标：AI 被要求证明一个特定的定理（例如，“加法具有交换性”，即 $a + b = b + a$ ）。
后继者：在真实的数学中，一旦证明了一个小事实，其他数学家就会利用该事实证明更大、更复杂的内容。该论文考察了所有依赖于 AI 答案的其他定理。
测试：将 AI 的答案嵌入这些“下游”证明中。
- 如果 AI 给出了一个“虚假”的答案（例如一个总是成立但毫无实际意义的重言式），下游证明就会崩溃。由于它们依赖于 AI 未能提供的特定含义，它们将无法编译。
- 如果 AI 给出了正确的答案，下游证明就能顺利运行。

重大发现
作者利用来自"Lean"编程语言的 2,206 个现实世界数学问题，构建了一个庞大的测试套件。他们测试了 18 个当时最智能的 AI 模型（包括来自 Google、OpenAI 和 Anthropic 的模型）。

以下是他们利用我们的桥梁类比所发现的：

“语法”陷阱：大多数 AI 非常擅长通过旧测试。它们写出了看起来完美且能无错误编译的蓝图。在旧测试中，它们的成功率约为 80%。
现实检验：当作者应用新的“城市集成”测试时，得分急剧下降。表现最好的 AI 仅获得了约**39%**的正确率。
差距：这意味着，对于 AI 声称建造的每 100 座桥，当有人试图在上面修路时，大约有 60 座会立即坍塌。AI 擅长伪造数学的外观，却不擅长把握数学的含义。

为何这很重要
该论文表明，当前衡量 AI 数学技能的方法正在欺骗我们。

词汇相似度（BLEU）：检查 AI 的词汇是否与人类词汇相似毫无用处。AI 可以写出看似数学的胡言乱语，却依然能通过测试。
专用模型：即使是专门训练为“数学专家”的模型，表现也未比通用聊天机器人好多少。它们只是更擅长伪造语法。
解决方案：唯一能确认 AI 是否真正理解数学的方法，是看当其他证明试图建立在它的工作之上时，其成果是否依然稳固。

简而言之
该论文为 AI 数学引入了一种新的“压力测试”。它不再问“这句话看起来像数学吗？”，而是开始问“当我们尝试利用这些数学解决更大问题时，它们是否真的有效？”结果是一次残酷的现实检验：尽管当今最先进的 AI 模型看起来完美无缺，但它们仍在努力进行真实、有意义的数学工作。

以下是 Jongyoon Kim、Hojae Han 和 Seung-won Hwang 的论文《Benchmarking Testing in Automated Theorem Proving》的详细技术总结。

1. 问题陈述

大型语言模型（LLMs）的快速发展提升了它们在 Lean 等系统中生成形式化证明的能力。然而，当前的评估方法存在一个致命缺陷：它们将语法有效性与语义正确性混为一谈。

编译的局限性： 现有的基准测试（如 MiniF2F、ProofNet）主要通过检查生成的定理是否能编译来评估模型。虽然编译验证了代码在孤立情况下的语法有效性和逻辑一致性，但它并不能保证该定理捕捉到了预期的数学含义。
“重言式”问题： 模型可以生成一个平凡的重言式（例如， $a + b = a + b$ ），该式能成功编译，但未能证明预期的非平凡陈述（例如，交换律 $a + b = b + a$ ）。
代理指标的不足： 现有衡量语义正确性的尝试依赖于不可靠的代理指标，例如与人工标注参考文本的词汇重叠（BLEU 分数）或人工检查。这些方法要么噪声过大，要么需要昂贵的人力，要么无法区分正确与错误的语义含义。

2. 方法论

作者提出了一种受软件工程中的集成测试启发的范式转变。他们不再孤立地评估一个定理，而是根据它与代码库其余部分的交互方式来评估它。

核心概念：定理测试（T2）

借鉴柯里 - 霍华德对应（其中证明对应于程序），作者将生成的定理视为一个函数，而依赖该定理的其他定理则视为“测试用例”。

依赖图： 他们构建了一个依赖图，其中目标定理（ $t_{GT}$ ）具有前驱（它使用的定义/引理）和后继（调用或基于它构建的定理）。
集成测试逻辑： 如果生成的定理（ $t_{fl}$ ）在语义上是错误的（例如，它定义了一个重言式而不是预期的属性），那么任何依赖它的后继定理都将无法编译。
切消类比： 该过程在逻辑上基于切消（Cut Elimination）原理。如果证明链（ $X \to Y \to Z \to W$ ）在中间引理（ $Y$ ）被替换为生成的候选项时失败，则该候选项在语义上是错误的。

T2 基准

作者构建了一个大规模基准 T2 以促进此类评估：

来源： 提取自 5 个真实的 Lean 4 仓库（涵盖代数、拓扑、数论等）。
规模： 2,206 个问题，每个问题平均配对 41 个后继定理。
困难子集： 一个包含 389 个“困难”问题的子集，模型必须生成命题（陈述）和证明，而不仅仅是为给定的陈述填充证明。
自动化： 提取流程完全自动化，无需人工标注依赖结构。自然语言（NL）描述由强大的 LLM（Claude Sonnet 4.5）生成，并对样本进行了人工验证。

指标：测试准确率（TA）

论文引入了**测试准确率（Testing Accuracy, TA）**作为主要评估指标：
$TA = E_{P \sim D} \left[ \prod_{i=1}^{k} \text{compiles}(t^{(i)}_{succ} \mid t_{fl}) \right]$
只有当原始定理被替换为生成的定理后，其所有依赖的后继定理都能成功编译时，生成的定理才算通过。

3. 主要贡献

T2 基准： 首个大规模、富含依赖关系的形式化定理证明基准，超越了孤立问题，转向真实世界的仓库上下文。
测试准确率（TA）： 一种新颖的、自动的、无需参考的指标，通过依赖模块的编译直接验证语义正确性。
实证差距分析： 对 18 个最先进模型（包括开源和闭源）的全面评估，揭示了编译成功与语义正确性之间存在巨大脱节。
上下文洞察： 证明了提供后继定理作为上下文能显著提高语义正确性，而仅提供自然语言证明则不能。

4. 实验结果

作者在 T2 基准上评估了 18 个模型（包括 GPT-5、Claude-Sonnet-4.5、Llama-3.1 以及 DeepSeek-Prover 等专用数学模型）。

语义差距：
- 编译准确率： 模型实现了较高的编译率（例如，Claude-Sonnet-4.5 在完整集上达到 80.3%）。
- 测试准确率（TA）： 相同模型在 TA 分数上表现 drastically 更低（例如，Claude-Sonnet-4.5 在完整集上为 38.9%；在困难集上仅为 4.5%）。
- 假阳性： 高达 93.1% 的可编译定理在针对后继定理进行测试时被发现是语义错误的。
现有指标的失效：
- BLEU： 高词汇相似度（BLEU 分数）与语义正确性几乎无相关性（相关性：0.123）。模型可以生成文本相似但逻辑错误的证明。
- 专用模型： 专门为定理证明微调的模型通常实现了更高的编译率，但在 TA 指标上表现不如或与通用模型相当，表明它们过度拟合了语法而非语义。
上下文的影响：
- 将后继定理作为输入上下文 consistently 提高了 TA（例如，Claude-Sonnet-4.5 提升了 +4.9%）。
- 仅提供自然语言证明而不提供后继定理并未提升性能，有时甚至降低了性能。
- 少样本提示和迭代优化（利用编译器反馈）在困难集上带来的提升微乎其微，表明难点在于深层语义推理，而不仅仅是任务格式。

5. 意义与结论

这篇论文从根本上挑战了当前自动定理证明（ATP）评估的现状。

重新定义成功： 它证明了“编译”是定理生成的必要条件，但非充分条件。一个模型可以是语法完美的，但在语义上毫无用处。
可信度： T2 基准和 TA 指标提供了一种严格的、自动化的方法，用于评估 LLM 是真正理解了数学概念，还是仅仅在幻觉式地生成语法有效的代码。
未来方向： 这项工作表明，未来的 ATP 系统必须评估其集成到现有代码库的能力（感知依赖的生成），而不是解决孤立的谜题。它还强调，在生成过程中向模型提供“测试套件”（后继定理）是提高语义对齐的关键策略。

总之，该论文认为集成测试是评估 LLM 进行形式化数学的缺失环节，揭示了当前最先进模型在定理证明中远未达到可靠的语义正确性。