Lean 形式化不能只看编译：一项研究重新定义“翻译正确”

2026年10月21日阅读约 3 分钟

导语

把自然语言数学题转换成 Lean 声明，第一道关通常是“能不能编译”。但编译器只能确认代码符合语法、类型系统和环境要求，无法判断它是否准确表达了用户的原意。一个声明即使成功通过 Lean 检查，也可能因为遗漏条件、改变量词范围或误解术语，而成为另一个定理。

论文《Beyond Compilation》关注的正是这一被编译率掩盖的问题：在没有预先给定标准 Lean 目标的情况下，如何衡量自然语言到 Lean 的陈述形式化是否忠实。

评测不再把编译当作终点。 研究要求生成结果先通过 Lean 编译，再由来自不同模型家族的两名 LLM 判断其是否与原始自然语言陈述一致。两者达成一致，结果才算被接受。
标准与人工意见具有较高一致性。 在独立随机抽样审查中，该标准与人工多数意见的一致率为 91.5%。研究指出，它很少把不忠实结果误判为正确，但会拒绝一部分实际上忠实的翻译。
编译率与忠实度存在明显落差。 研究测试了 8 个系统、共 227 条大学水平数学陈述。各系统的编译率与接受率差距介于 1.3 至 29.5 个百分点。一个带工具的 GPT-5.2 agent 编译率达到 87.2%，但最终只有 57.7% 的结果被接受。
大部分差距确实来自翻译错误。 对该 agent 被拒绝的结果进行人工复核后，29.5 个百分点的差距中有 23.8 个百分点被确认是真实翻译错误。对 7 个一次性生成系统的进一步分析也显示，其中 6 个系统的落差中，78% 至 100% 可归因于翻译问题。
评审器本身也会产生偏差。 当 GPT-5.2 评估 GPT-6 Astra 和 Claude Opus 5.5 的输出时，两者各有 83% 被接受，而一次性 GPT-5.2 只有 21%。对前两者的拒绝样本复核发现，54 个拒绝中仅 4 个属于翻译错误，说明部分系统的测量落差来自评审器能力不足，而非模型翻译失败。

这项工作提醒研究者重新审视自动形式化的“成功”定义。Lean 编译仍然是必要条件，因为它能排除大量结构和类型错误；但它不是语义正确性的充分条件。若评测只报告编译率，系统可能通过删减约束、弱化命题或改变变量关系来换取更高分数，却被错误地视为性能提升。

更可靠的评测应同时报告编译结果、语义忠实度、人工抽检以及评审器的误差边界。研究还显示，随着生成模型能力提高，评审模型未必同步更新，自动评估可能反而成为新的瓶颈。因此，未来的形式化系统不仅需要更强的代码生成能力，也需要更稳健的语义审计机制。