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

Lean 验证生成的声明是否类型正确，但不验证它是否表达了用户想要的语句。我们研究了没有规范Lean目标的自动形式化的两个问题：大语言模型法官是否可以为人类语义审查提供可用的代理，以及编译在多大程度上夸大了跨系统的忠实度。我们的标准将Lean编译与 GPT-5.2 和 Gemini-2.5-Pro 之间严格的语义共识结合起来。在独立审计的随机样本中，它在 89.7% 的情况下与人类大多数一致（威尔逊 95% CI：82.1--94.3%）。在对 400 份研究生水平陈述进行评估的 8 个系统中，每个系统都存在非零的编译忠实度差距，观察到的差距幅度在 3.0 到 29.0 个百分点之间。完整的 GPT-5.2 工具增强代理显示出最大的差距，编译 89.5%，同时满足 60.5% 的语义标准。人工审查、独立的第三家庭法官和 BEq 正式交叉检查提供了补充证据，证明公认的核心是可靠的，并且差距中的大多数审计输出都是真正的语义不匹配。二次 $2^3$ 因子分析表明，详细反馈是最大的有效性干预，但并不能消除语义漂移。因此，LLM 的评审作为一种人工校准的、保守的综合衡量标准是有用的，而不是作为一种对等预言。