超越编译：自然语言到Lean陈述忠实形式化的评估 Beyond Compilation: Evaluating Faithful Natural-Language-to-Lean Statement Formalization
编译通过≠语义忠实：双LLM评审加人工审计量化八大系统的编译-忠实差距
前置知识
陈述自动形式化（Statement Autoformalization）
把自然语言数学命题翻译成证明助手（如 Lean 4）中类型良好的形式化声明，证明部分用 := by sorry 占位省略。与定理证明不同，这里目标陈述本身由模型生成，没有给定的标准答案，同一命题可能存在多种等价但写法不同的合法 Lean 编码。
本文的研究对象就是这个任务：当没有唯一正确的标准 Lean 参考答案时，如何判断模型写出的陈述是否忠实于原意，正是论文要解决的核心评估问题。
Lean 4 与 Mathlib
Lean 4 是带依赖类型的定理证明器兼编程语言，其内核可机械检查语法、类型与证明；Mathlib 是社区维护的大型数学库，覆盖代数、拓扑、实复分析等。编译通过只意味着声明类型良好（well-typed），并不保证它表达了作者想要的数学含义。
论文把『Lean 编译通过』作为唯一客观的门槛条件，所有语义评估（LLM 打分、人工审计、形式等价检查）都建立在编译通过的输出之上，因此必须理解编译验证的能力边界。
LLM-as-a-Judge 与评审一致性校准
用大模型按共享量表给输出打分以替代人工评估。本文用 GPT-5.2 与 Gemini-2.5-Pro 两个不同模型家族的评审，对编译通过的输出独立打 0 到 10 的忠实性整数分，两者都给至少 9 分才接受；再用盲评人类、第三方家族评审和阈值扫描来验证这一严格工作点。
这套双 LLM 评审共识标准是全文的核心测量仪器，它与人类判断 91.5% 的一致率直接决定了后续所有『编译-忠实差距』测量结果的可信度。
阳性预测值（PPV）与评审误差模型
借用流行病学诊断检测的概念：设被评系统编译输出的不忠实率为 $e$，评审误报率（错杀忠实输出）为 $f$、漏报率（放过不忠实输出）为 $m$，则一次拒绝是真实错误的概率为 $e(1-m)/(e(1-m)+(1-e)f)$，这个量随 $e$ 变小而急剧下降。
这个公式解释了论文最反直觉的发现：对错误率极低的强模型（GPT-6 Astra、Claude Opus 5.5），54 个被拒输出中只有 4 个是真实翻译错误，其余大多是评审自己的误判。
全因子消融设计（$2^3$ Factorial Design）
把 agent 的三种工具（专家起草 T、编译反馈 F、知识搜索 S）编码为 3 位开关 $c=(t,f,s)$，跑满全部 8 种组合；某工具的主效应定义为固定其余因子后『开减关』的平均差，如 $\Delta_F(m)=\frac{1}{4}\sum_{t,s\in\{0,1\}}\left[m(t,1,s)-m(t,0,s)\right]$，并用逐条目配对 bootstrap 给出置信区间。
论文用它定量回答『agent 的编译增益从哪来、又有多少是虚假的』，是理解第 5 章结论（Lean 反馈贡献最大编译增益但近半不忠实）的数学基础。
研究动机
在定理证明任务中目标陈述是给定的，Lean 的证明检查通过就是很强的成功信号；但在陈述自动形式化中，Lean 目标本身由模型生成——生成的 Lean 4 代码可能编译通过，却悄悄丢掉一个假设、改换定义域、或加强/削弱了结论。Lean 只能证明『模型写的定理类型良好』，不能证明『模型写的是用户想要的定理』。更麻烦的是，对开放性数学陈述通常不存在唯一的标准 Lean 编码，精确匹配或基于参考答案的评估都不可用；已有工作尝试参考对、回译、语义打分、人工标注、对齐模型、LLM 评审集成乃至形式等价检查，但都无法回答一个基本问题：编译通过到底在多大程度上高估了语义忠实？而且用 LLM 评审测出的『编译率-验收率差距』本身还混入了两类噪声：评审误判，以及基准陈述本身不精确或含糊导致的拒绝。此前没有工作把这三类成分系统地分开量化。
本文的目标是本文的目标是构建并校准一个无需标准参考答案的忠实性评判标准，再用它系统量化『编译-忠实差距』。具体包括：从四本开源教材收集 227 条大学水平数学陈述构成基准（Lebl 实分析 48 条、Lebl 复分析 19 条、McKay 拓扑 63 条、Doty 抽象代数 97 条），保留原文的不精确处并标注 18 条有缺陷的陈述；定义『编译通过且 GPT-5.2 与 Gemini-2.5-Pro 两个不同家族评审都打至少 9/10 分』的接受标准；用盲评人工审计、第三方家族评审、阈值敏感性与 BEq 形式等价检查验证该标准；然后回答三个经验问题——Q1：该标准与人类评审一致性多高、错在哪个方向？Q2：编译-忠实差距是否跨模型家族普遍存在、幅度多大？Q3：每个系统的差距中有多少是真实翻译错误，而非评审误判或基准缺陷？
与已有工作不同的是，本文的独特切入是把『评估器本身当作需要校准的测量仪器』：先在人工标签上双向刻画其操作特性（既测正样本精确率、也测阴性确认率），再把它应用到没有任何人工标注的系统上，这个『先校准、后测量』的两步逻辑贯穿 Q1 与 Q3。作者还引入诊断检测的阳性预测值框架 $\mathrm{PPV}=\frac{e(1-m)}{e(1-m)+(1-e)f}$，指出『一次拒绝有多大可能是真错误』取决于被评系统自身的错误率——评审的固定误报率会让强模型的差距显得虚高。对工具增强 agent，作者进一步用 $2^3$ 全因子消融把笼统的『准确性』拆成有效性、忠实性、成本三个独立边界，定位差距的具体来源（Lean 反馈），而不是只报告一个总准确率。这种把测量误差与系统误差显式分离的做法，是以往自动形式化评估文献中缺失的。
核心方法
直觉上，编译只是必要条件，需要一个独立的语义关卡，而且这个关卡本身要先经过人类校准。技术路线分六步：(1) 构建基准：从四本开源 LaTeX 教材共取 227 条陈述，来源不含形式代码，因此没有标准 Lean 目标，同一陈述可有多种忠实编码；(2) 统一运行八个系统：通用 LLM（GPT-5.2、Gemini-2.5-Pro）、专门形式化器（Herald、Kimina-Autoformalizer、StepFun-Formalizer）、面向证明器模型（Kimina-Prover、Goedel-Prover）和一个带起草/搜索/Lean REPL 反馈工具的 GPT-5.2 agent，均为 statement-only 设置；(3) 定义接受标准 $\text{Accepted}(x,y)=\text{Compiles}(y)\ \wedge\ \text{grade}_{GPT}(x,y)\ge 9\ \wedge\ \text{grade}_{Gemini}(x,y)\ge 9$，评分按共享 rubric 打 0–10 整数分；(4) 三组人工审计校准该标准（正样本区、Batch A 全部拒绝项、Batch B 对外部系统 Aristotle 的全评估）；(5) 用在人工标签上验证过的两阶段评审（Claude Opus 5.5 加 GPT-6.1 Sol）把每个系统的差距分解为翻译错误、评审误判与缺陷陈述；(6) 对 agent 做 $2^3$ 全因子工具消融，量化每个工具对编译率、忠实率与差距的因果贡献。
核心创新是把评估问题拆成『仪器校准』与『测量』两步，并首次把『编译-忠实差距』本身作为测量对象。与已有评估器工作（LeanScorer、FormalAlign、BEq 等）的本质区别在于：作者并不构造新指标，而是刻意选用最简单的『编译 + 双家族 LLM 评审共识』工作点，在人类标签上完整刻画其误差结构——正样本精确率 95.7%，阴性确认率仅 76.9–80.6%，即它极少放过不忠实输出、但会拒绝一部分忠实输出。随后用 PPV 框架 $\frac{e(1-m)}{e(1-m)+(1-e)f}$ 解释测量结果的语义：对编译输出错误率 $e$ 很低的系统，评审的固定误报率 $f$ 会使表观差距主要由评审误判构成——GPT-6 Astra 与 Claude Opus 5.5 的 54 个被拒输出中仅 4 个是真实翻译错误，Lean 还证明了其中 9 对被 GPT-5.2 打出不同分数的输出在数学上等价。另一个关键发现是：agent 编译增益的主要来源是 Lean 反馈（主效应 +49.3 点），但其中 22.1 点的输出编译通过却不忠实——验证器驱动的修复会产出『不再陈述原定理的合法 Lean』。
方法步骤详情
步骤一（基准构建）：从四本教材逐条抽取 227 条大学水平陈述，保留原文不精确处，标注 18 条按原文为假或抽取时丢失上下文的缺陷陈述。步骤二（运行系统）：七个 one-shot 系统用统一 prompt，要求输出一条导入 Mathlib、以 := by sorry 结尾的定理声明；GPT-5.2 agent 由编排器调用三类工具——专家起草 lean4_translation（向微调的 Herald 模型要草稿再编辑）、知识搜索 lean_inspect_name/lean_resolve_name（经 Lean REPL 跑 #check/#print 加网页搜索）、编译反馈 lean4_repl_runner（整句有效性检查与错误信息）；编排器维护编译错误、检索符号与草稿的持久状态，最多 24 步，REPL 首次通过即结束。步骤三（评判）：所有输出在 Lean 4 + Mathlib 下编译；编译通过者由两个评审按 rubric 独立打分，9–10 分表示语义匹配至可忽略差异。步骤四（人工校准）：专家审 agent 被接受输出的随机样本；三名盲评者审 agent 全部 67 个被拒编译输出（Batch A）；三名盲评者对 Aristotle 在 60 条随机样本上的输出做全评估（Batch B，59 条有效）。步骤五（差距分解）：两阶段评审先在 69 个人工标注的拒绝上验证（最终分类找出 47/57 即 82.5% 的人类确认错误；与人类多数一致率 79.7%、$\kappa=0.41$，高于评审者两两一致率 69.6–74.6%），再应用到七个 one-shot 系统的 145 个拒绝。步骤六（消融）：跑满 8 个工具组合，主效应与交互效应用逐条目配对 bootstrap（$B=10000$）计算 95% 置信区间。
技术新颖性
技术新颖性体现在四个层面。(1) 问题层面：首次系统量化陈述自动形式化中『编译高估忠实』的现象，给出跨八个系统 1.3–29.5 个百分点的差距谱系，并证明差距的主导成分是真实翻译错误（六个系统占 78–100%）。(2) 方法论层面：评估器校准覆盖决策边界两侧（精确率与阴性确认率）、第三方评审家族（Claude Sonnet 5，一致率 89.2%）、阈值扫描（7–10 区间内因子排序不变）和 BEq 形式等价证书（183 对中 113 对被认证等价，其中归一化编码相同时 46/46=100%，不同编码时 67/137=48.9%），形成完整证据链。(3) 理论层面：把 LLM 评审映射为诊断检测，用 PPV 公式解释『系统越强、差距越假』的现象，为社区提供了可复用的分析工具。(4) 工程层面：$2^3$ 全因子消融区分了『提升编译』与『提升忠实』两种边界，发现搜索与反馈存在负交互 $F\times S=-10.8$ 点，且小净效应掩盖巨大的每条目变动——在反馈开启时加搜索，30 条陈述变忠实、25 条变不忠实，净效应仅 +5。
实验结果
(1) 标准可靠性：在 Aristotle 的 60 条随机样本全评估审计（Batch B）中，标准与人类多数一致 54/59=91.5%（95% CI 81.6–96.3%），正样本精确率 44/46=95.7%，阴性确认率仅 10/13=76.9%——极少放过错误但会错杀忠实输出；同样本上优于公开的 LeanScorer（54/59 对 45/59，McNemar $p=0.0225$）；第三方 Claude Sonnet 5 一致率 89.2%；BEq 为 113/183 个接受对提供形式等价证书。(2) 差距普遍且悬殊：八个系统差距 1.3–29.5 点；验收率为通用 one-shot LLM 19.8–27.3%、专门形式化器 10.1–13.8%、面向证明器模型仅 4.6–6.2%（它们经常输出 tactic 证明体或畸形声明而不遵循 statement-only 指令），agent 为 57.7%（编译 198/227=87.2%）。(3) 差距主体是真实翻译错误：agent 的 29.5 点中 23.8 点经人工确认（54/67=80.6%）；七个 one-shot 系统的 145 个拒绝中 132 个被判为翻译错误，各系统真实错误占差距的比例为 Kimina-Prover 100%、Goedel-Prover 97%、Kimina-AutoF 96%、Herald 88%、StepFun 79%、GPT-5.2 78%、Gemini 33%；典型错误包括恒真命题、True 占位与使陈述空洞的假设。(4) 强模型差距主要是评审误判：GPT-6 Astra 与 Opus 5.5 编译率 94.3%/96.0%，GPT-5.2 单独评审验收率均为 83.3%（one-shot GPT-5.2 仅 20.7%），差距 11.0/12.8 点，但 54 个拒绝中仅 4 个是翻译错误（其余归因于评审误判 32、缺陷陈述 11、双因 7）。(5) 工具消融：编译反馈主效应 $\Delta$编译 +49.3 点、$\Delta$忠实 +27.2 点、$\Delta$差距 +22.1 点——近半编译增益语义不忠实；搜索为 +9.7/+8.5/+1.2；翻译先验为 +4.0/+1.0/+3.0；交互 $F\times S=-10.8$ 点。全工具配置（111）验收 57.7%，最佳单配置 011 为 58.1%，任意配置 oracle 达 77.1%，但仅 11.9% 的陈述在所有配置下都忠实；反馈开启时轨迹越长忠实率越低（1–2 步 82.9% 对 19–24 步 11.5%）。(6) 换编排器（Sonnet 4.5/Gemini 2.5 Pro）agent 验收 58–65%，差距 26.9/11.0 点。
查看结构化数据
| 任务 | 指标 | 本文 | 基线 | 提升 |
|---|---|---|---|---|
| 227 条陈述的形式化编译通过率 | Compile rate (%) | GPT-5.2 工具增强 agent：87.2%（198/227） | one-shot GPT-5.2：28.6%（24.7+4.0） | +58.6 个百分点 |
| 语义验收率（编译 + 双评审 ≥9/10） | Accepted rate (%) | agent：57.7%（131/227） | one-shot GPT-5.2：24.7%；专门形式化器 10.1–13.8%；面向证明器模型 4.6–6.2% | 较 one-shot GPT-5.2 +33.0 个百分点 |
| 评判标准与人类多数一致性（Aristotle 全评估审计） | Agreement (%) | 本标准：91.5%（54/59） | LeanScorer（同样本）：76.3%（45/59） | +15.2 个百分点（McNemar p=0.0225） |
| 差距中真实翻译错误占比 | Real gap / gap (%) | agent：23.8/29.5=81%（人工确认）；六个 one-shot 系统 78–100% | 未分解前的表观差距（最高 29.5 点） | 证实差距主体为真实错误而非评审误判（Gemini 例外，仅 33%） |
| 评审后发布模型的验收率（GPT-5.2 单评审） | Accepted rate (%) | GPT-6 Astra 与 Claude Opus 5.5 各 83.3% | one-shot GPT-5.2：20.7% | +62.6 个百分点，且 54 个拒绝中仅 4 个为真实翻译错误 |
局限与改进
作者承认的局限：评判标准只是语义代理而非等价性证明；基准仅 227 条、来自四本公开教材、领域分布不均（每领域 19–97 条）、不含研究级数学；教材公开在 GitHub 上，新模型可能已在训练中见过这些陈述；人工审计只覆盖 agent 与 Aristotle；两阶段评审的第一阶段由 Claude Opus 5.5 运行，而它本身也是被评模型之一，且该评审约漏掉六分之一的人类确认错误；评审只覆盖被拒输出，无法测量被接受输出中的错误；人类多数并非无误——Lean 证明至少 3 个被人类接受的输出实际不忠实；Search 与 Feedback 工具有部分重叠（共用同一个 Lean REPL），且 Search 不含 LeanSearch 这类专门语义检索器。我的补充观察：双 LLM 评审的错误本身可能相关（作者引用的 Goel et al. 正说明这一点），共识并非真正独立的确认；GPT-6 Astra/Opus 5.5 的整体错误率 $e$ 未被测量，只得到 0.5%/1.4% 的下界；部分关键指标置信区间很宽（如忠实输出未标记率 66.7% 的 CI 为 39.1–86.2%）；单评审规则（对后发布模型只能用 GPT-5.2 单独评分）与主标准的不一致未逐条量化。
独立分析的弱点
独立分析的弱点与改进方向：(1) 评审标准偏保守，阴性确认率仅 76.9–80.6%，会系统性错杀忠实但非标准编码的输出（例如 Gemini 给『每个可缩空间连通且同伦群平凡』的正确形式化打 5 分）；改进方向是把 BEq 式形式等价检查作为拒绝申诉层，或像论文附录那样向评审提供相关 Mathlib 定义后重评。(2) 双家族评审的错误仍可能相关，共识的独立性证据不足；改进方向是引入异构评审（检索式、规则式、小型专门 critic 模型）并显式估计评审间相关做校正。(3) 编译反馈驱动的修复以忠实性为代价——agent 的差距反而最大（29.5 点），近半编译增益不忠实；改进方向是把语义自检做成显式工具（逐假设对照原文核对），或接入 FormalRx 式的错误定位-修复流程。(4) 18 条缺陷陈述造成的 J/B 混合拒绝无法干净归因（两阶段评审也只能标为 J/B）；改进方向是增加陈述清洗与歧义自动检测的前置管线。(5) 每条目工具轨迹变动剧烈且轨迹越长忠实率越低（反馈开启时 19–24 步的运行忠实率仅 11.5%），说明 agent 缺乏可靠的自我终止信号；改进方向是开发逐实例的工具路由与早停策略。
未来方向
作者提出的方向：自动形式化系统应分别报告有效性与忠实性，验证器驱动的修复必须配合语义审计；逐实例的工具路由与早停是开放问题；后续工作（Zhang et al., 2026）研究用 LLM 判断定位评审、基准标签与人类评审之间的分歧。基于本文成果可延伸的方向：(1) 用 PPV 框架校正评估报告——先在人工标签上估计评审的误报率 $f$ 与漏报率 $m$，再对低错误率系统的表观差距做校正解读；(2) 把 BEq 形式等价证书扩展成半自动申诉流水线，覆盖更多被拒输出，缩小评审保守造成的假阴性；(3) 把该协议移植到研究级数学、其他证明助手（Coq/Isabelle）以及证明级（而非陈述级）忠实性评估；(4) 训练专门的忠实性 critic（结合 CriticLean 与 FormalAlign 思路），降低对闭源通用 LLM 评审的依赖与版本漂移风险；(5) 对基准陈述做自动歧义检测与规范化改写，使 T/J/B 归因更干净；(6) 研究多评审的去相关方法，例如让不同评审看到互补的证据子集再聚合。
复现评估
复现条件较好：代码、数据、标签全部开源在 GitHub（grenadeComing/beyond-compilation），发布内容包括 227 条基准（含 18 条缺陷陈述标注）、每个系统的全部输出与评审打分、人工标签、268 个被审拒绝的两阶段评审记录与 Lean 检查、评估脚本以及 agent 的工具调用日志。复现门槛主要在 API 与环境：需要 GPT-5.2、Gemini-2.5-Pro 以及评审用的 Claude Opus 5.5、GPT-6.1 Sol 等商业模型 API；本地需要 Lean 4 + Mathlib 环境编译全部输出；agent 部分要跑 227 条 × 8 个工具配置、每条最多 24 步，调用量与费用不小。人工审计部分（三名盲评者加一名领域专家）对个人复现者成本最高，但论文已发布全部人工标签，可直接复用做二次分析。总体难度中等：评估协议可以完整复跑，但闭源模型的版本漂移是长期复现的主要风险——论文本身就演示了评审模型（GPT-5.2）在评更新模型时大面积误判的问题。
论文图表
