信号-覆盖矩阵：在语句自动形式化中对类型错误与语义错误进行分层

背景

近年来，大型语言模型（LLM）在数学语句自动形式化（Statement Autoformalization）领域的表现取得了显著进步。以 Lean 定理证明器为例，模型生成的语句在“类型正确性”（Type Correctness, TC%）这一单一标量指标上，从两年前的约 53% 攀升至约 76%。

然而，这种整体准确率的提升掩盖了模型内部错误的具体构成。仅仅关注最终的 TC% 分数，无法揭示不同方法究竟解决了哪一类错误，也无法区分是修复了语法/类型层面的问题，还是真正提升了语义层面的等价性。为了更精细地评估和优化自动形式化模型，我们需要一种能够解耦类型错误与语义错误的分析框架。

核心内容

本文提出了一种名为“信号-覆盖矩阵”（Signal-Coverage Matrix）的分析工具，旨在对自动形式化输出进行细粒度的分层评估。该矩阵通过交叉验证两个关键维度来对每个输出进行分类：

1. Lean elaborator（ elaborator 通过/失败）：即生成的代码是否能被 Lean 编译器成功解析和类型检查。
2. 语义等价性判断（Semantic-equivalence judgment）：即生成的形式化语句是否与原始自然语言语句在数学语义上等价。

基于这两个维度，所有输出被划分为四个象限（Cell）：

• 真正成功（True Success, TS）：类型检查通过且语义等价。
• 仅类型正确（Type-Only, TO）：类型检查通过，但语义不等价。
• 仅语义正确（Semantic-Only, SO）：类型检查失败，但语义等价（通常是因为形式化存在语法瑕疵但意图正确）。
• 双重失败（Both Fail, BF）：类型检查失败且语义不等价。

研究团队在 ProofNet# 和 MiniF2F-test 数据集上，使用 DeepSeek V4-Pro 模型，对比了四种策略的效果：Vanilla（基础方法）、Lean-Retry（Lean 重试）、Sample-Filter（样本过滤）以及 Stratified Autoformalization (SAF，分层自动形式化)。主要发现如下：

1. 类型层恢复是准确率提升的主要驱动力 在三种基于 elaborator 反馈的方法中，TS（真正成功）的提升幅度为 +34 到 +36。深入分析显示，这一增长中约 64% 来源于对“类型层”错误的恢复。相比之下，SO（仅语义正确）的数量在净效果上保持平稳：虽然挽救了原始语义错误的 87.5%，但也新产生了 8 个语义错误。这表明当前的优化策略主要集中在解决“写得对”（类型正确）的问题，而非“写得准”（语义等价）的问题。

2. TO-to-TS 转化率具有预测性 对于每种方法，从 TO（仅类型正确）转化为 TS（真正成功）的比率均为 23/61。根据 Wilson 95% 置信区间计算，该比率处于 [26.6%, 50.3%] 之间。这一分层恢复率（stratum-level recovery rate）具有高度的预测能力：

• 它能将未见过的模型在 TS 上的变化量（$\Delta$TS）预测误差控制在 2/186 以内。
• 它揭示了 $\Delta$TC（类型正确性的变化）与 Vanilla 方法的 elaborator 失败率之间存在线性关系（在六个模型-数据集组合中，$R^2=0.96$）。

3. 评估器之间的分歧揭示了系统性偏差 在基于 elaborator 反馈的输出中，两个评估器（elaborator 和语义评判器）之间的分歧高达 26 到 37 个百分点，而在 Vanilla 方法中这一分歧仅为 7 个百分点。研究发现，符号评判器（symbolic judge）中 30% 到 56% 的假阴性（False Negatives）可追溯至由 elaborator 强制进行的重写操作。这意味着，当 elaborator 强制修改代码以通过类型检查时，可能会无意中破坏原有的语义意图，导致语义评判器判定为错误。经过分析，这种持续的残留误差最终被归结为两个黄金标准（gold-formalization）本身的错误。

关键要点

• 指标陷阱：单一的 TC% 指标具有误导性，它掩盖了模型是在修复类型错误还是语义错误。
• 分层评估框架：Signal-Coverage Matrix 通过交叉验证“类型检查”和“语义等价”，将输出分为 TS、TO、SO、BF 四类，提供了更细致的诊断视角。
• 类型修复主导增长：当前自动形式化模型的性能提升（+34% 至 +36% 的 TS 增益）中，约 64% 归功于类型层错误的恢复，而语义层的净改善有限。
• TO 到 TS 的转化规律：TO 到 TS 的转化比率（23/61）在不同方法间保持一致，且该比率能有效预测新模型的性能提升，同时解释了 TC 提升与初始失败率之间的线性关系。
• 评估器的系统性冲突：Elaborator 强制重写代码以通过类型检查，是导致语义评判器出现大量假阴性的主要原因（占 30%-56% 的假阴性）。
• 归因原则：TC% 的提升不应仅被视为整体分数的增加，而应根据具体哪个象限（Cell）发生了移动来进行归因。

意义与影响

这项研究对自动形式化领域的模型评估和优化具有重要指导意义：

1. 从“黑盒”到“白盒”评估：传统的评估往往只关注最终结果是否“类型正确”，而本文提出的矩阵揭示了模型在类型和语义两个正交维度上的具体表现。这有助于研究人员识别模型当前的瓶颈是语法层面的还是逻辑层面的。
2. 优化方向的明确化：数据显示，当前的改进主要来自于类型层的修复，而语义层的改进相对停滞。这提示未来的研究重点可能需要从单纯的“让代码跑通”转向“确保语义保真”，特别是在处理 Elaborator 强制重写导致的语义漂移问题时。
3. 评估器的校准：研究指出了 Elaborator 和语义评判器之间的系统性分歧，特别是 Elaborator 强制重写对语义评估的负面影响。这呼吁开发更鲁棒的评估机制，或者在训练过程中引入对“重写代价”的惩罚，以平衡类型正确性与语义保真度。
4. 可预测的性能建模：TO-to-TS 转化率的稳定性及其对 $\Delta$TS 的预测能力，为建立更精确的性能预测模型提供了基础。开发者可以利用这一指标，在资源有限的情况下更准确地预估不同策略或模型在未见数据上的表现。

总之，Signal-Coverage Matrix 不仅是一个分析工具，更是一种新的评估范式，它强调在自动形式化中，类型正确性只是通往语义正确性的必要非充分条件，必须对两者进行分层解耦和独立考量。