Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
AI 深度解读
背景
当前，定理证明领域的基准测试普遍采用一种"固定形式语句 + 自动证明搜索"的评测范式：给定一个已经形式化好的目标命题（通常以 Lean 等证明助手的代码形式呈现），评测系统只衡量模型能否找到正确的证明路径。然而，在实际数学研究或形式化工程中，一个更上游、也更关键的环节是：将自然语言描述的数学命题自动转化为 Lean 形式语句。这一步的质量直接决定了后续证明搜索是否有意义——如果生成的形式语句本身偏离了原命题的语义，那么即使证明搜索成功，整个流程也是无效的。
现有评测几乎只关注"编译通过率"（compile rate），即生成的 Lean 代码能否通过类型检查。但编译通过远不等于语义忠实：一个 Lean 声明完全可以类型检查通过，同时却遗漏了关键假设、改变了量词辖域、或者表达了一个空洞的真命题。这种"编译通过但语义失真"的现象，在现有评测体系下被完全掩盖了。
核心内容
本文以"忠实性"（faithfulness）为核心，系统研究了自然语言到 Lean 形式语句的转化问题，将其同时定位为评测问题和瓶颈归因问题。
评测协议与基准
研究构建了一个包含 400 条研究生水平数学命题的基准，覆盖实分析、复分析、拓扑学和代数四个领域。评测协议由三个层次组成：
- Lean 编译检查：最基础的语法与类型有效性验证。
- 跨模型语义判断：利用多个模型对生成语句与自然语言原命题之间的一致性进行语义层面的比对，形成"共识忠实度"评分。
- 人类专家校准：由数学专家对样本进行人工审核，作为最终校准依据。
核心发现：编译通过与语义忠实之间存在巨大鸿沟
实验结果揭示了一个被现有评测严重忽视的现象：一个配备完整工具链的 agent 可以达到 89.5% 的编译通过率，但其共识忠实度仅为 60.5%，两者之间存在高达 29.0 个百分点的差距。这意味着近三成"编译通过"的输出在语义上是有缺陷的。
人类专家审核进一步验证了这一指标的可靠性：
- 在共识判定为忠实的输出中，96.0% 经人工确认确实忠实；
- 在编译通过但共识判定为不忠实的输出中，82.4% 经人工确认存在语义错误。
这表明"共识忠实度"是一个保守但有效的决策边界——它不会轻易将错误输出判为正确，同时能可靠地识别出大多数语义失败案例。
现有模型的表现
在忠实度指标下，现有的"一次性形式化模型"（one-shot formalizer models）以及面向证明的 Lean 模型表现均不理想。这提示我们：形式有效性（编译通过）、证明导向的 Lean 能力、以及忠实语句生成能力是三个应当分别报告、独立评估的维度，不能互相替代。
干预措施的因子分解
研究进一步采用完整的 2³ 因子设计，对形式化流水线中三种常见干预措施进行分解分析：
- 参数化专家起草（parametric expert drafting）：由微调模型直接生成候选形式语句。
- Mathlib/上下文搜索（Mathlib/context search）：从形式化库中检索相关定义和定理作为参考。
- Lean 精化反馈（Lean elaboration feedback）：利用 Lean elaboration 阶段的错误信息进行迭代修正。
关键结论：
- 精化反馈是提升有效性（编译通过）的最大贡献者，但它同时也暴露了更多"编译通过但语义失败"的案例——即它帮助模型生成类型正确的代码，但不保证语义忠实。
- 搜索主要改善的是基础性和选择性（grounding and selectivity），帮助模型更准确地定位相关数学概念。
- 微调起草模型在很大程度上是可替代的——一旦流水线和反馈机制与检索基础能力就位，专门微调的起草模型带来的边际增益有限。
关键要点
- 编译通过 ≠ 语义忠实：Lean 类型检查可以轻易通过，同时遗漏假设、改变辖域或生成空洞命题，现有评测体系对此完全失明。
- 29 个百分点的忠实度鸿沟：工具增强 agent 编译通过率 89.5%，共识忠实度仅 60.5%，暴露了"编译通过但语义不忠实"的巨大盲区。
- 三层评测协议：编译检查 + 跨模型语义共识判断 + 人类专家校准，形成可验证的忠实度评估框架。
- 人类审核验证指标可靠性：共识忠实输出中 96.0% 人工确认正确；编译通过但共识不忠实输出中 82.4% 人工确认语义失败。
- 三种能力应独立报告：形式有效性、证明导向的 Lean 能力、忠实语句生成能力不可互相替代，需分别评测。
- 精化反馈是双刃剑：最大幅度提升编译通过率，但也制造更多"编译通过但语义失真"的案例。
- 搜索改善概念定位：Mathlib/上下文检索主要提升模型对相关定义和定理的准确调用能力。
- 微调起草模型边际价值有限：在具备反馈和检索能力后，专门微调的起草模型可被通用方案替代。
意义与影响
本文对形式化数学和自动定理证明领域的评测方法论提出了根本性挑战。长期以来，编译通过率被默认为形式化质量的代理指标，本文以严谨的实验证明这一代理指标存在系统性偏差——它高估了模型的实际语义理解能力，掩盖了形式化流水线中最关键的瓶颈。
从实践角度看，研究指出的"三种能力独立报告"原则，意味着未来形式化系统的评估需要更细粒度的指标体系，而非单一编译通过率。这对于 Mathlib 等大型形式化库的建设、以及面向数学研究的 AI 工具开发具有直接指导意义。
从方法论角度看，2³ 因子设计对三种干预措施的分解，为形式化流水线的优化提供了清晰的优先级指引：与其投入大量资源微调起草模型，不如优先建设可靠的检索基础和精化反馈机制。这一结论对工程资源的分配具有实际参考价值。
此外，论文揭示的"精化反馈暴露更多语义失败"现象也提醒我们：工具增强在提升表面指标的同时，可能引入新的、更隐蔽的失败模式，需要更精细的监控手段。