超越编译：评估自然语言到Lean语句的忠实形式化

arXiv cs.AI 2026/07/01 04:00 论文

formal-verification lean natural-language-processing theorem-proving benchmark evaluation

摘要

本文提出了一个用于自然语言到Lean语句忠实形式化的基准测试和评估协议，揭示了编译通过与共识忠实性之间29个百分点的差距，并分解了专家起草、上下文搜索和细化反馈的效果。

arXiv:2606.31002v1 公告类型：新摘要：定理证明基准测试针对固定形式化语句评估证明搜索，但自然语言到Lean的形式化必须生成形式化语句本身。在此背景下，编译仅是一种有效性检查：一个Lean声明可能通过类型检查，但省略了假设、改变了定义域或表达了空洞的主张。本文将忠实语句形式化作为一个评估问题和瓶颈归因问题进行研究。在一个涵盖实分析、复分析、拓扑和代数的400条目研究生级基准测试上，我们的协议结合了Lean编译、跨模型语义判断和人类专家校准。得到的结果与编译率评估不同：一个完整的工具增强型智能体达到了89.5%的编译通过率，但只有60.5%的共识忠实性，暴露了29.0个百分点的编译通过但共识不忠实的差距。有针对性的人类审计支持该指标作为保守的决策边界：在可用的案例级审计中，96.0%的共识正例输出被人类确认为忠实，而82.4%的编译通过但共识负例输出被人类确认为语义失败。在此指标下，现有的一次性形式化模型和面向证明的Lean模型仍然表现较低，这表明形式有效性、面向证明的Lean能力和忠实语句生成应分别报告。然后，我们使用一个完整的$2^3$因子设计来分解形式化流程中三个反复出现的干预措施：参数化专家起草、Mathlib/上下文搜索和Lean细化反馈。细化反馈是最大的有效性干预措施，但它也暴露了更大的编译通过语义失败桶；搜索主要改进基础性和选择性；一旦反馈和基础性可用，微调后的起草在此工具栈中基本上是可替代的。

查看原文

查看缓存全文

缓存时间: 2026/07/01 05:36

# 超越编译：评估从自然语言到 Lean 命题的忠实形式化
来源：https://arxiv.org/abs/2606.31002
查看 PDF (https://arxiv.org/pdf/2606.31002)

> 摘要：定理证明基准测试针对固定的形式化命题评估证明搜索，但自然语言到 Lean 的形式化则必须自行生成形式化命题本身。在此设定下，编译仅是一种有效性检查：一条 Lean 声明虽然可以通过类型检查，却可能省略假设、改变定义域或表达一个空洞断言。我们将忠实的命题形式化同时作为一个评估问题和瓶颈归因问题来研究。在一个包含 400 条研究生级别条目、涵盖实分析、复分析、拓扑学和代数的基准测试中，我们的协议结合了 Lean 编译、跨模型语义评判以及人类专家校准。得到的结论与编译率评估截然不同：一个完整的工具增强型智能体达到了 89.5% 的编译率，但仅有 60.5% 的共识忠实度，暴露出一个 29.0 个百分点的“编译通过但共识不忠实”的差距。针对性的审计支持该指标作为保守的决策边界：在现有个案级别的审计中，96.0% 的共识正例输出被人类确认为忠实，而 82.4% 的编译通过但共识负例输出被人类确认为语义失败。在该指标下，现有的一次性形式化模型和面向证明的 Lean 模型表现仍然偏低，这表明形式有效性、面向证明的 Lean 能力以及忠实的命题生成应分别报告。随后，我们采用完整的 $2^3$ 析因设计来分解形式化流程中三种常见的干预措施：参数化专家草稿、Mathlib/上下文搜索、以及 Lean 细化反馈。细化反馈是最大的有效性干预措施，但它也暴露了更大的“编译通过但语义失败”的类别；搜索主要改进了基础与选择性；而在此工具栈中，一旦反馈和基础化可用，微调草稿在很大程度上是可以被替代的。

## 提交历史

来自：Ke Zhang [查看邮件 (https://arxiv.org/show-email/b58c5a3e/2606.31002)] **\[v1\]** 2026年6月30日星期二 00:27:53 UTC (257 KB)

超越编译：评估自然语言到Lean语句的忠实形式化

相似文章

我们形式化基准测试中的缺陷：Lean定理证明的数据集缺陷和评估失败

测量AI的忠实度——无论好坏

计算机科学逻辑的理论级自动形式化

评估Lean 4中证明自动形式化的鲁棒性

未完成项并非难点：半自动形式化的专家评审案例研究

提交意见反馈