精选理由
这篇论文用信号覆盖矩阵把自动形式化的错误拆成类型和语义两类，告诉你每个方法的增益到底来自哪，而不是只看总分。
该论文提出信号覆盖矩阵，将自动形式化输出按Lean elaborate检验（通过/失败）和语义等价判断（等价/不等价）分为四类。在ProofNet#和MiniF2F-test上使用DeepSeek V4-Pro进行实验，发现三种精化反馈方法（Lean-Retry、Sample-Filter、SAF）相比Vanilla的TS增益+34到+36，其中约64%来自类型层恢复，语义层净变化为0。TO到TS的转换率为23/61（Wilson 95% CI [26.6%, 50.3%]），该层恢复率可预测保留方法上的ΔTS误差在2/186以内。两个判断者在精化反馈输出上的分歧达26至37个百分点（Vanilla仅7个百分点），30%至56%的符号判断假阴性源于elaborator强制重写。
AI 翻译 · 中文
该论文提出信号覆盖矩阵，将自动形式化输出按Lean elaborate检验（通过/失败）和语义等价判断（等价/不等价）分为四类。在ProofNet#和MiniF2F-test上使用DeepSeek V4-Pro进行实验，发现三种精化反馈方法（Lean-Retry、Sample-Filter、SAF）相比Vanilla的TS增益+34到+36，其中约64%来自类型层恢复，语义层净变化为0。TO到TS的转换率为23/61（Wilson 95% CI [26.6%, 50.3%]），该层恢复率可预测保留方法上的ΔTS误差在2/186以内。两个判断者在精化反馈输出上的分歧达26至37个百分点（Vanilla仅7个百分点），30%至56%的符号判断假阴性源于elaborator强制重写。
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 cross…
- orange.ai06-26 21:31原文