UCR 研究：Lean 编译通过≠语义正确，agent 编译 87.2% 但仅 57.7% 忠实

ucriverside · hf · 2026-10-21

UC Riverside、亚利桑那大学与 UCSD 的研究衡量了语句自动形式化中「编译通过」高估忠实度的程度。评判标准要求 Lean 编译通过且两个不同模型家族的 LLM 评审一致；独立随机审计显示该标准与人类多数意见在 91.5% 的案例上一致。八个系统在 227 条大学级语句上，编译通过与语义接受的差距为 1.3–29.5 个百分点：工具增强 agent 编译了 87.2% 的语句，但只有 57.7% 被接受；人工复核确认 29.5 个百分点差距中的 23.8 个是真实翻译错误。