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

文章背景与核心概要

在交互式定理证明领域，Lean 等工具虽然能够通过类型检查来自动验证生成的声明是否符合语法和类型规范，但却无法判断该声明是否真正准确捕捉了用户的原始语义意图。本文针对缺乏规范 Lean 目标的自动形式化场景，深入探讨了两个核心问题：大语言模型裁判能否作为人类语义审查的可靠代理？在不同系统中，代码编译检查在多大程度上夸大了实际的语义忠实度？

为了解决这些问题，作者提出了一种结合了 Lean 编译检查与 GPT-5.2、Gemini-2.5-Pro 严格语义共识的综合评估标准。在独立审计的随机样本测试中，该标准与人类多数共识的一致性高达 89.7%（Wilson 95% 置信区间：82.1%–94.3%）。研究发现，所有测试系统均存在编译-忠实度鸿沟（Compile-Faithfulness Gap），其差距在 3.0 到 29.0 个百分点之间。该研究为未来更可靠、语义更忠实的人工智能数学形式化工具开发提供了重要的评估方法与理论支撑。

Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization

Metadata

Metadata

arXiv ID: 2606.31002 [cs.AI]
Subjects: Artificial Intelligence (cs.AI); Computation and Language (cs.CL); Logic in Computer Science (cs.LO)
Authors: Ke Zhang, Patricio Gallardo Candela, Sudhir Murthy, Yi Xie, Zhi Wang, Maziar Raissi
Dates: Submitted on 30 June 2026; Last revised 3 September 2026 (v2)
License: CC BY 4.0

Abstract Summary

Abstract Summary

While the Lean theorem assistant can successfully verify whether a generated declaration is well-typed, it cannot determine whether the statement actually captures the user's intended meaning. This paper addresses two primary questions regarding autoformalization without canonical Lean targets:

Can LLM judges serve as a reliable proxy for human semantic review?

To what extent does code compilation overstate actual faithfulness across different systems?

虽然 Lean 定理助手可以成功验证生成的声明是否具有良好的类型，但它无法确定该声明是否真正捕捉了用户的意图含义。本文探讨了在没有标准 Lean 目标的情况下的自动形式化的两个主要问题： 1. 大语言模型裁判能否作为人类语义审查的可靠代理？ 2. 在不同系统中，代码编译在多大程度上夸大了实际的忠实度？

The authors propose a semantic evaluation criterion combining Lean compilation with a strict semantic consensus between GPT-5.2 and Gemini-2.5-Pro. Tested on an independently audited random sample, this criterion agrees with human majority consensus on 89.7% of cases (Wilson 95% CI: 82.1–94.3%).

作者提出了一种语义评估标准，将 Lean 编译与 GPT-5.2 和 Gemini-2.5-Pro 之间的严格语义共识结合起来。在独立审计的随机样本上进行测试时，该标准在 89.7% 的情况下与人类多数共识达成一致（Wilson 95% 置信区间：82.1–94.3%）。

Key Findings

The Compile-Faithfulness Gap: Evaluating eight systems across 400 graduate-level statements revealed a non-zero compile-faithfulness gap for every system, ranging from 3.0 to 29.0 percentage points.

System Performance: The full GPT-5.2 tool-augmented agent exhibited the largest gap, successfully compiling \(89.5\%\) of statements while satisfying the strict semantic criterion on only \(60.5\%\).

Validation: Human review, an independent third-family judge, and a BEq formal cross-check confirm that the accepted core is reliable, and that outputs falling into the compilation gap are genuine semantic mismatches.

Intervention Analysis: A secondary \(2^3\) factorial analysis demonstrated that while elaboration feedback is the most impactful validity intervention, it still fails to completely eliminate semantic drift.

核心发现

编译-忠实度鸿沟（The Compile-Faithfulness Gap）： 对 400 个研究生级别的声明跨八个系统进行评估发现，每个系统都存在非零的编译-忠实度鸿沟，范围从 3.0 到 29.0 个百分点不等。
系统性能： 完整的 GPT-5.2 工具增强型代理表现出最大的差距，成功编译了 \(89.5\%\) 的声明，但仅在 \(60.5\%\) 的声明上满足严格的语义标准。
验证： 人工审查、独立的第三家族裁判以及 BEq 形式交叉检查证实，被接受的核心是可靠的，落入编译鸿沟中的输出则是真正的语义不匹配。
干预分析： 二次 \(2^3\) 析因分析表明，虽然细化反馈（elaboration feedback）是最具影响力的有效性干预措施，但它仍然无法完全消除语义漂移。

Ultimately, the study concludes that LLM judging functions best as a human-calibrated, conservative aggregate measure rather than a foolproof equivalence oracle.

最终，研究得出结论：大语言模型评判作为一种经人工校准的、保守的综合度量指标效果最好，而不是一个万无一失的等价性神谕。

Access & Full-Text Links

Access & Full-Text Links