💻 computer science

ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

本文介绍了 ITPEval，这是首个用于评估跨四种主要交互式定理证明器的自动化形式化证明翻译的基准测试和统一基础设施，揭示了当前的语言大模型由于库不匹配而导致在证明翻译方面面临显著困难，并且仅靠原生类型检查往往会高估语义保真度。

原作者： Jiayi Wu, Robert Joseph George, Anima Anandkumar

发布于 2026-07-23

📖 1 分钟阅读☕ 轻松阅读

原作者： Jiayi Wu, Robert Joseph George, Anima Anandkumar

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

想象一个数学家们说着四种不同语言，但都在试图解决完全相同的谜题的世界。在“形式化定理证明”这一高风险领域，计算机充当着终极裁判，检查数学证明的每一个步骤，以确保其 100% 正确。然而，就像说法语、日语、斯瓦希里语和阿拉伯语的人类一样，这些计算机系统（被称为交互式定理证明器，简称 ITP）也有其独特的语法、词汇和预先批准的事实库。用一种系统完美编写的证明，在其他系统看来往往是乱码。这创造了一个孤独的问题：如果一个精妙的证明是用一种语言编写的，它就无法被其他系统轻松使用或检查。科学家们一直试图构建“通用翻译器”来弥合这一差距，希望人工智能（AI）能够学习自动翻译这些数学证明，从而让整个社区能够共享他们的成果。

于是有了 ITPEVAL，一项类似于针对 AI 的大规模、严苛语言考试的新研究。研究人员想要观察当今最智能的 AI 模型是否真的能够在这四个主要系统——Lean 4、Rocq、Isabelle 和 HOL Light 之间翻译形式化数学证明。他们不仅仅是让 AI 去猜测；他们构建了一个专门的测试场，其中包含超过 1,500 个源文件和近 7,000 个定理。他们将测试分为两个级别：一个是“受控”级别，包含简单的、自包含的数学问题（就像没有外部引用的词汇测验）；另一个是“生态系统”级别，使用真实的、复杂的库代码，这些代码依赖于特定系统的复杂规则（就像一场包含俚语和文化背景的完整对话）。

结果既有“还不错”的一面，也有“依然非常困难”的一面。当 AI 尝试仅翻译定理的“陈述”（即“是什么”）时，表现最好的模型达到了约 29.1% 的正确率。但当被要求翻译实际的“证明”（即“如何做”）时，成功率骤降至仅为 10.5%。研究发现，最大的障碍并非数学本身或不同的逻辑基础，而是“生态系统”。当 AI 必须处理目标系统中特定的库、命名规范和自动化风格时，它表现得最为吃力。这就像 AI 能理解“猫坐在垫子上”这个句子，但在被要求将其翻译成一种需要使用特定品牌垫子和特定类型猫的特定方言时失败了。

此外，研究人员发现，仅仅让计算机说出“这看起来是正确的”（类型检查）是不够的。他们进行了更深层的“意义检查”，发现即使在 AI 的翻译通过了计算机的基础测试时，在 46% 的案例中，其数学强度仍较弱或与原意略有不同。该研究表明，虽然 AI 在基础方面正在进步，但它仍需学习如何适应每个数学系统的独特“文化”，才能真正成为一名通用翻译官。作者还探索了一种“往返”测试，即将数学翻译成自然语言再翻译回来，发现结果因使用的系统而异，这暗示着结合使用多个系统可能会有所帮助，但目前还不是万灵药。

技术摘要：ITPEVAL —— 跨交互式定理证明器的形式化翻译基准测试

1. 问题陈述

形式化定理证明生态系统目前处于碎片化状态。尽管大语言模型（LLMs）在自动化定理证明和自动形式化方面取得了显著成功，但经过验证的结果仍被隔离在互不兼容的交互式定理证明器（ITPs）中。每个系统（例如 Lean 4、Rocq、Isabelle、HOL Light）都实现了自己的逻辑基础、策略语言（tactic language）和数学库。因此，在一个系统中证明的定理无法直接在另一个系统中调用，这导致了重复的形式化工作，并限制了用于学习型证明器的训练数据量。

跨 ITP 翻译——即在保持正确性的前提下，在不同系统之间转换形式化证明的任务——尚未得到系统的研究。现有的工作，如“形式化 100 个定理”目录或像 Dedukti 这样的互操作性框架，侧重于追踪覆盖范围或通过中间表示实现证明交换，但缺乏用于评估翻译质量的标准基准。此外，现有的评估方法不足；简单的类型检查往往会导致语义正确性的高假阳性率，且代码翻译基准测试未能考虑到 ITPs 固有的深层逻辑基础差异。

2. 方法论与基准设计

作者提出了 ITPEVAL，这是首个旨在评估四大主流 ITPs（Lean 4、Rocq（原 Coq）、Isabelle 和 HOL Light）之间自动化形式化证明翻译的基准测试。该基准涵盖了两种截然不同的逻辑基础：归纳构造演算（CIC）和高阶逻辑（HOL）。

2.1. 数据结构

该基准包含 1,560 个源文件 和 6,848 个定理，分为两个不同的层级以隔离难点来源：

Tier A（受控层）： 包含 64 个自包含、已公理化的文件（660 个引理），这些文件源自 Babel-formal 基准。这些文件包含其自身的定义和假设，避免了对特定证明器库的依赖。该层级隔离了基础翻译问题（例如：类型理论、宇宙层级、隐式参数）。
Tier B（生态系统层）： 包含取自真实社区库的形式化内容，暴露了 API 不匹配、命名约定和证明风格的差异。该层级包括：
- 来自 Formalizing 100 Theorems 的 232 个文件（4,924 个引理），在所有四个系统中均已对齐。
- 来自 miniF2F 的 1,264 个单定理文件（仅含陈述），提供了多样化的竞赛数学内容。

设计上强制执行了四向交集要求：每个文件必须在所有四个 ITPs 中都已完成形式化，以确保在没有缺失数据混淆的情况下进行清晰的方向性比较。

2.2. 翻译任务

ITPEVAL 评估两个主要任务：

陈述翻译（Statement Translation）： 生成目标 ITP 代码，其中证明体被占位符（如 sorry）替换。验证要求生成的代码在目标系统中通过类型检查。
证明翻译（Proof Translation）： 生成完整的、可编译的证明文件，不含占位符。验证要求整个文件在目标证明器中成功编译。

2.3. 验证基础设施

该方法论的一个关键组成部分是 itpeval，一个统一的多 ITP 验证基础设施。为了应对 ITP 执行模型异构性（例如 Isabelle 和 HOL Light 沉重的启动成本），该系统采用了：

状态隔离的热后端（State-isolated warm backends）： 确保每次检查在观察上都等同于在全新的环境中验证一个制品，从而防止声明泄漏。
原生目标证明器检查： 所有标签均由实际的目标 ITP 生成，而非基于表面启发式方法。
自适应调度： 使用持久化工作进程、会话批处理和 fork 服务器来管理吞吐量，同时保留单文件检查语义。

2.4. 语义等价性检查

意识到类型检查是必要但不充分的，作者为 Lean 4 目标实现了**双向扩展定义等价性（BEq）**检查。这种确定性检查通过受限的证明搜索，验证生成的陈述 $G$ 与参考陈述 $R$ 是否相互蕴含（ $G \vdash R$ 且 $R \vdash G$ ），从而避免了额外的模型依赖变异。

3. 核心贡献

四向对齐基准： 一个涵盖 Lean 4、Rocq、Isabelle 和 HOL Light 的数据集，包含 1,560 个文件和 6,848 个定理，通过受控层和生态系统层进行结构化，以量化库依赖带来的成本。
统一验证基础设施： 一个状态隔离的客户端（itpeval），能够在具有原生检查语义的异构证明器之间实现可扩展、可复现的评估。
系统性 LLM 评估： 对五种前沿及开源权重模型（GPT-5.5, Claude Sonnet 4.6, Gemini 3.1 Pro, DeepSeek-V4-Pro, Qwen3-235B-A22B）在 12 个定向翻译对上的评估。
语义保真度分析： 应用 BEq 来证明仅靠类型检查会大幅高估语义正确性。
探索性往返研究： 调查自动形式化与自动非形式化循环，以评估目标依赖的验证模式以及多 ITP 上下文的潜在益处。

4. 结果

4.1. 翻译性能

陈述翻译： 表现最好的模型 GPT-5.5 在整体上达到了 29.1% 的 pass@1 率。DeepSeek-V4-Pro 以 27.1% 紧随其后。其他模型的性能显著下降（Gemini 为 14.0%，Qwen 和 Claude 低于 10%）。
证明翻译： 性能大幅下降，GPT-5.5 在整体上仅达到 10.5% 的 pass@1。
层级差距： 受控层（Tier A）始终比生态系统层（Tier B）更容易。对于证明翻译，GPT-5.5 在受控文件上达到 29.7%，但在生态系统文件上仅为 5.2%。这表明 库不匹配（API、命名、自动化）是观察到的最大失败来源，而非逻辑基础本身的差异。
方向性不对称： 翻译难度随目标而异。Isabelle 和 HOL Light 是陈述翻译的强力目标，但 Isabelle 成为证明翻译中最难的目标。逻辑基础的相似性（例如从 CIC 到 CIC）并不保证更高的成功率；目标生态系统的惯例起到了更大的作用。

4.2. 语义等价性 (BEq)

在对来自 miniF2F 的已验证 Lean 4 陈述翻译应用 BEq 时：

只有 54.0% 的已验证翻译通过了等价性检查。
在已验证的翻译中，Claude Sonnet 4.6 的 BEq 通过率最高（83.8%），而其他模型在 34.5% 到 48.4% 之间。
这一结果表明，一个陈述在语法上是有效的（通过类型检查），但在语义上可能比原始定理更弱或发生了偏移。

4.3. 往返与自动形式化

在多 ITP 往返研究（自然语言 $\to$ 形式化 $\to$ 自然语言 $\to$ 形式化）中，Rocq 和 HOL Light 在两个形式化步骤中分别验证了约三分之一的输出，而 Lean 4 在最后一步徘徊在 11% 左右，Isabelle 则降至 4.3%。多 ITP 上下文显示出对特定模型-目标组合的潜在益处（例如，将 Lean 4 第一步的通过率从 4.8% 提高到 10.6%），但结果在不同系统中并不统一。

5. 重要性与主张

本文声称 ITPEVAL 提供了第一个系统的四向翻译基准，揭示了跨 ITP 翻译的主要障碍不是逻辑基础本身，而是生态系统层级的依赖（库、API 和证明惯例）。

作者强调：

原生验证至关重要： 仅靠表面启发式方法或类型检查不足以评估语义保真度。
基础设施很重要： 可靠的跨 ITP 评估需要状态隔离的验证，以防止诸如声明泄漏之类的混淆因素。
未来方向： 该领域必须优先考虑检索、库映射和 API 对齐，而非仅仅关注基础层面的翻译。论文还指出了局限性，包括零样本评估设置、BEq 对 Lean 4 目标的限制，以及 miniF2F 等公开数据集中训练数据污染的可能性。

这项工作为衡量形式化翻译的进展奠定了基础，表明未来的系统必须解决“库不匹配”问题，以实现形式化证明生态系统之间稳健的互操作性。