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

在定理证明领域，传统基准测试主要评估针对固定形式语句的证明搜索能力，但自然语言到Lean的形式化任务需要生成形式语句本身。最新研究发现，编译通过仅能验证语法正确性，却无法保证语义忠实性——生成的Lean声明可能通过类型检查，但遗漏假设、改变定义域或表达空洞主张。

研究团队构建了包含400个研究生级别数学问题的基准集，涵盖实分析、复分析、拓扑和代数等领域。他们开发了一套结合Lean编译检查、跨模型语义评判和专家校准的评估协议。结果显示：完整工具增强代理达到89.5%的编译通过率，但共识忠实度仅60.5%，暴露出29.0个百分点的“编译通过但语义不忠实”差距。

人工审计验证了该指标的保守决策边界：在共识肯定的输出中，96.0%经人工确认为忠实；而在编译通过但共识否定的输出中，82.4%被确认为语义错误。研究表明，现有单次形式化模型和面向证明的Lean模型在此指标下表现仍较低，提示形式有效性、证明导向能力和忠实语句生成应分别报告。

通过全因子实验设计，研究分解了形式化流程中三个关键干预措施：参数化专家起草、Mathlib上下文搜索和Lean细化反馈。其中细化反馈对有效性提升最大，但也暴露更多“编译通过但语义失败”案例；搜索主要改善基础性和选择性；而微调起草在获得反馈和基础支持后基本可被替代。这项工作为形式化系统评估提供了更精细的度量框架。