用四象限矩阵拆解自动形式化错误类型，看清模型改进真实效果。
The Signal-Coverage Matrix: Stratifying Type and Semantic Errors in Statement Autoformalization
- 构建信号覆盖矩阵，按类型和语义是否通过分四类错误
- 三种反馈方法类型错误减少64%，但语义错误几乎未改善
- 揭示错误类型分布，帮助判断模型改进究竟在哪类问题上有效
大型语言模型在陈述自动形式化中的类型正确率（TC%）两年间从约53%提升至约76%，但这一单一指标掩盖了不同方法解决的具体错误。本文提出信号-覆盖率矩阵，将瘦化推导器（通过/失败）与语义等价性判断（等价/不等价）交叉，将每个输出归入四类：真成功（TS）、仅类型对（TO）、仅语义对（SO）、均失败（BF）。在ProofNet#和MiniF2F-test上，使用DeepSeek V4-Pro对原始、重试、采样过滤及分层自动形式化（SAF）方法进行评估：(1) 三种推导反馈方法使TS提升34–36个百分点，其中约64%源于类型错误的修复，语义错误净变化为零（原87.5%语义错误被修复，新增8个）；(2) 从类型错误到成功（TO→TS）的转化率为23/61（95%置信区间[26.6%, 50.3%]），该层级恢复率可预测新方法的ΔTS，误差小于2/186，且ΔTC与原始方法推导失败率呈高度线性关系（六组模型-数据组合下$R^2=0.96$）；(3) 两位判官对推导反馈输出的分歧达26–37个百分点（原始方法仅7个百分点），其中30–56%的符号判别假阴性可归因于推导器强制重写。残余错误最终减少至两个黄金标准形式化错误。因此，应根据具体错误类别转移来评价性能提升，而非仅看总分。
原文摘要 · Abstract (English)
Headline type-correctness (TC\%) of LLM autoformalization has climbed from $\sim$53\% to $\sim$76\% in two years, yet this scalar conceals which errors each method resolves. We propose a signal-coverage matrix that crosses the Lean elaborator (pass/fail) with a semantic-equivalence judgment (equivalent/not), sorting every output into one of four cells: true success (TS), type-only (TO), semantic-only (SO), or both fail (BF). On ProofNet\# and MiniF2F-test with DeepSeek V4-Pro across Vanilla, Lean-Retry, Sample-Filter, and Stratified Autoformalization (SAF): (1) the +34 to +36 TS gain across the three elab-feedback methods is $\sim$64\% type-stratum recovery, with SO flat on net (87.5\% of original semantic errors rescued, 8 newly created). (2) The TO-to-TS rate is 23/61 for each method (Wilson 95\% CI [26.6\%, 50.3\%]), and this stratum-level recovery rate predicts $Δ$TS on held-out methods to within 2/186 and renders $Δ$TC linear in the Vanilla elab-fail rate across six (model, dataset) cells ($R^2=0.96$). (3) The two judges disagree by 26 to 37 pp on elab-feedback outputs (vs. 7 pp on Vanilla), with 30 to 56\% of symbolic-judge false negatives traceable to elaborator-forced rewrites. The persistent residual reduces to two gold-formalization errors. TC\% gains should be credited by which cell moved, not by the scalar alone.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。