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

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

来源：https://arxiv.org/html/2606.28013

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

###### 摘要

大语言模型自动形式化的标题级类型正确性（TC%）在两年内从约53%攀升至约76%，但这一标量掩盖了每种方法分别解决了哪些错误。我们提出一种信号-覆盖矩阵，将 Lean 解释器（通过/失败）与语义等价判断（等价/不等价）交叉，将每个输出归入四个单元之一：真成功（TS）、仅类型错误（TO）、仅语义错误（SO）或两者均失败（BF）。在 ProofNet# 和 MiniF2F-test 上，使用 DeepSeek V4-Pro 在 Vanilla、Lean-Retry、Sample-Filter 和分层自动形式化（SAF）四种方法下：（1）三种基于解释器反馈的方法在 TS 上获得 +34 到 +36 个百分点的增益，其中约64%来自类型层的恢复，而 SO 层净保持平稳（87.5%的原始语义错误被修复，新产生8个）。（2）每种方法的 TO→TS 转化率为23/61（Wilson 95% CI [26.6%, 50.3%]），这个层级的恢复率在留出方法上预测 ΔTS 误差在2/186以内，并且使得 ΔTC 在六个（模型、数据集）单元中与 Vanilla 的解释器失败率呈线性关系（R²=0.96）。（3）两个判断器在解释器反馈输出上分歧为26到37个百分点（在 Vanilla 上为7个百分点），其中30%到56%的符号判断器假阴性可归因于解释器强制重写。持续存在的残差最终归结为两个黄金形式化错误。TC% 的增益应归功于哪个单元发生了变化，而非仅仅归功于标量本身。

自动形式化，语句形式化，语义忠实度，解释器反馈，信号-覆盖矩阵，LLM 作为判断器

## 1 引言

语句级自动形式化将自然语言定理映射为一个带有 `sorry` 占位符体的 Lean 4 签名。在 ProofNet 类基准（Azerbayev 等，2023（https://arxiv.org/html/2606.28013#bib.bib2）；Poiroux 等，2024（https://arxiv.org/html/2606.28013#bib.bib12））上，标题级类型正确性（TC%）在两年内从约53%（GPT-4o（OpenAI，2024（https://arxiv.org/html/2606.28013#bib.bib11）））攀升至约76%（DeepSeek V4-Pro（DeepSeek-AI，2026（https://arxiv.org/html/2606.28013#bib.bib4））），这得益于那些针对 Lean 解释器进行精炼的方法。由于 TC% 不能保证指称正确性，语义忠实度（SF%）估计器会与之一起报告：反向翻译（Zhou 等，2024（https://arxiv.org/html/2606.28013#bib.bib19））和广义树编辑距离（GTED，Liu 等，2025b（https://arxiv.org/html/2606.28013#bib.bib9））。

标题级指标掩盖了机制。TC% 提升15个百分点掩盖了哪个错误层被修复、哪个未被修复，而 SF% 判断器的选择可能使报告值在基于解释器反馈的方法上产生≥25个百分点的偏移（§5.5（https://arxiv.org/html/2606.28013#S5.SS5））。目前没有任何已发表的报告按层和方法分解 TC% 的增益。我们提供了这样一个报告。

现有方法沿三个轴聚类。**单 oracle 针对解释器精炼**（Wu 等，2022（https://arxiv.org/html/2606.28013#bib.bib15）；Poiroux 等，2024（https://arxiv.org/html/2606.28013#bib.bib12）；Guo 等，2025（https://arxiv.org/html/2606.28013#bib.bib5）；Lu 等，2024（https://arxiv.org/html/2606.28013#bib.bib10））在精炼过程中仅查阅解释器（或一个近似代理），该类方法在 ProofNet# 上的 TC% 已趋近于约75%，无论拓扑结构如何。**语义忠实度判断**包括 LLM 反向翻译（Zhou 等，2024（https://arxiv.org/html/2606.28013#bib.bib19））和通过 Lean LSP 进行的符号 GTED（Liu 等，2025b（https://arxiv.org/html/2606.28013#bib.bib9）），它们被用作独立的 SF% 估计器，但从未在大规模下相互校准。**类型化的结构化中间表示**由 Draft、Sketch 和 Prove（Jiang 等，2023（https://arxiv.org/html/2606.28013#bib.bib6））为 Isabelle 引入，其 sketch 是一个文本化证明骨架，而非类型化的结构化对象。更广泛的关于前提选择、证明生成和数学预训练的形式化数学 LM 文献（Polu & Sutskever，2020（https://arxiv.org/html/2606.28013#bib.bib13）；Yang 等，2023（https://arxiv.org/html/2606.28013#bib.bib17）；Azerbayev 等，2024（https://arxiv.org/html/2606.28013#bib.bib3）；Lin 等，2025（https://arxiv.org/html/2606.28013#bib.bib7））处理流水线的不同阶段，是互补的。

我们在 DeepSeek V4-Pro × ProofNet#（186个问题）上实例化一个 2×2 的信号-覆盖矩阵（解释器通过/失败 × 判断器等价/不等价），采用双判断器协议，配对 Claude Opus 4.7（Anthropic，2026（https://arxiv.org/html/2606.28013#bib.bib1））与 GTED（τ=0.5），追踪每个问题从 Vanilla 到 Lean-Retry、Sample-Filter 和分层自动形式化（SAF）的转换。本文做出三个贡献：

（1）**诊断框架及其产生的预测规律性。** 一个 2×2 的信号-覆盖矩阵和一个 4×4 的转换矩阵将任何 TC% 增益分解为类型层恢复、语义层更新以及一个持久残差。在这种视角下，三种算法不同的方法各自恢复了 23/61 的 Vanilla TO（Wilson 95% CI [26.6%, 50.3%]），并且 ΔTC 在六个（模型、数据集）单元中与 Vanilla 的解释器失败率呈线性关系（R²=0.96）（§2（https://arxiv.org/html/2606.28013#S2），§5.2（https://arxiv.org/html/2606.28013#S5.SS2），§5.4（https://arxiv.org/html/2606.28013#S5.SS4））。

（2）**经过校准的双判断器协议。** Opus 与 GTED（τ=0.5）配对在基准上达到 94.4% 至 95.0% 的精确率，一个四类分类法将 30% 至 56% 的 GTED 假阴性归因于解释器强制结构重写（§5.5（https://arxiv.org/html/2606.28013#S5.SS5））。

（3）**SAF 作为因果归因探针。** 分层自动形式化（SAF）针对解释器精炼一个类型化 JSON 中间表示，并通过一个确定性翻译器生成 Lean。其确定性使得候选的表面形式仅依赖于 IR，从而将 Opus 与 GTED 之间 +37 个百分点的差距归因于解释器驱动的表面几何，而非 LLM 采样噪声（§5.5（https://arxiv.org/html/2606.28013#S5.SS5））。SAF 在聚合指标上与 Lean-Retry 和 Sample-Filter 持平。它在此处的作用是诊断性的，而非追求最先进优化。

## 2 信号-覆盖矩阵

在语句级范围内（NL 语句 S → Lean 4 签名 σ，其中包含 `:= by sorry`），一个未能满足其规范的输出恰好属于两个层之一。**类型层**失败意味着 σ 不能通过类型检查（未知标识符、无法合成、应用类型不匹配等），因此数学可能被理解但 Lean 表面形式无效。**语义层**失败意味着 σ 能通过类型检查，但表示一个与 S 不同的命题，例如将 S 中的“任意大小为 2 的域”硬编码为 `ZMod 2`，当 S 断言序列有极限时使用 `Summable f`，反转不等式，或遗漏一个假设。（第三个实现层用于证明级自动形式化，不在讨论范围内。）

实践中使用的两种精炼信号是针对特定层的。Lean 解释器在类型层上是完备的，因为每个失败都会引发一个错误，但在语义层上是沉默的，因为一个语义错误但类型正确的 σ 可以在没有警告的情况下被解释。语义判断器，即反向翻译（Zhou 等，2024（https://arxiv.org/html/2606.28013#bib.bib19））和 GTED（Liu 等，2025b（https://arxiv.org/html/2606.28013#bib.bib9）），覆盖语义层但忽略类型层，因为一个无法编译的片段会反向翻译成噪声 NL。

将解释结果（通过/失败）与语义判断（等价/不等价）交叉，将 n 个输出划分为四个单元（图1（https://arxiv.org/html/2606.28013#S2.F1））：真成功（TS）、仅类型失败（TO）、仅语义失败（SO）和两者均失败（BF）。这些标签表示失败模式，而非正确性模式。两个非对角线单元正是解释器与判断器之间在实例上的分歧，它们的大小、来源以及跨方法的动态是本文的核心实证对象。

以 |c| 表示单元 c 中的计数，则
TC% = (|TS| + |SO|) / n，SF% = |TS| / n，n = Σ_c |c|。    (1)

（请参见图注）

图1：信号-覆盖矩阵：解释器（通过/失败）× 判断器（等价/不等价）给出 2×2 单元分解及 TC%/SF%。

## 3 分层自动形式化

由于精炼信号是针对特定层的（§2（https://arxiv.org/html/2606.28013#S2）），SAF 通过一个类型化中间表示（IR）来分解自动形式化。LLM 生成一个 IR，一个确定性的大约30行的翻译器从中产生 Lean，并且在解释失败时，精炼的是 IR 而非 Lean 源码。这种确定性至关重要：每个精炼后的 SAF 输出都仅是 IR 的函数。在聚合指标上，SAF 在 TC 和 Opus 评判的 SF 上与 Lean-Retry 和 Sample-Filter 持平（§5（https://arxiv.org/html/2606.28013#S5））。它在本文中的作用是 §5.5（https://arxiv.org/html/2606.28013#S5.SS5）中的因果归因探针，其中 Opus 与 GTED 之间 +37 个百分点的差距被归因于解释器驱动的表面几何，而非 LLM 采样噪声。

精炼循环（算法1（https://arxiv.org/html/2606.28013#alg1））交替进行 LLM 的 IR 生成和解释器检查，直到候选通过类型检查。LLM 总预算为 K+1（一次提取加 K 次精炼），我们在所有实验中使用 K=3。

一个 SAF IR 是一个包含五个字段的 JSON 对象：
{
  "imports": ["Mathlib"],
  "opens": ["Polynomial", "Real"],
  "objects": [
    {"name": "G", "type": "Type*", "binding": "implicit"},
    {"name": "", "type": "Group G", "binding": "instance"},
    {"name": "a", "type": "G", "binding": "explicit"}
  ],
  "hypotheses": [{"id": "h", "expression": "a*b=b*a"}],
  "conclusion": ""
}

**算法1** SAF 精炼循环

输入：NL 语句 S，重试预算 K
输出：通过类型检查的 Lean 签名，或 ⊥

1: ir ← LLM.extract_IR(S)
2: for k = 0 to K do
3:   σ ← ir_to_lean(ir)
4:   (ok, errors) ← LeanElaborator.check(σ)
5:   if ok then
6:     return σ
7:   end if
8:   ir ← LLM.refine_IR(S, ir, errors)
9: end for
10: return ⊥

`imports` 和 `opens` 字段携带 Mathlib 环境，`objects` 声明带有绑定模式的类型化绑定器，`hypotheses` 列出命名前提，`conclusion` 以 Lean 4 表达式形式保存目标。`ir_to_lean` 翻译器是一个大约30行的模板替换，将每个字段映射到其 Lean 对应项：`imports` 映射为 `import` 行，`opens` 映射为 `open` 行，每个 `objects` 条目映射为一个类型化绑定器（根据 `binding` 分别为 `(x : T)`、`{x : T}`、`[T]`），`hypotheses` 映射为前提绑定器，`conclusion` 映射为以 `:= by sorry` 结尾的定理体。翻译器纯粹基于模板（无 LLM、无模糊匹配、无错误恢复），格式错误的 IR 会快速失败。

## 4 实验设置

#### 数据集。
**ProofNet#**（Poiroux 等，2024（https://arxiv.org/html/2606.28013#bib.bib12））是类型复杂基准：186个本科教科书问题（Rudin、Munkres、Dummit-Foote、Artin、Axler、Herstein、Pugh、Putnam、Ireland-Rosen、Shakarchi），涉及 Mathlib 类型类机制（Group、MeasurableSpace、ContinuousMap、Sylow 等）。**MiniF2F-test**（Zheng 等，2022（https://arxiv.org/html/2606.28013#bib.bib18））是类型简单基准：244个奥林匹克问题，主要采用原始类型形式化。这两个基准横跨类型系统复杂性轴。

#### 主体模型。
**DeepSeek V4-Pro**（49B 活跃 / 1.6T 总 MoE 参数）是主要主体，在 ProofNet# 上运行完整电池，在 MiniF2F 上运行三种方法。**Qwen3.5-Plus**（Qwen 团队，2026（https://arxiv.org/html/2606.28013#bib.bib14））（480B 级）和 **MiMo-v2.5-Pro**（小米 MiMo 团队，2026（https://arxiv.org/html/2606.28013#bib.bib16））（小米，禁用思考轨迹）作为跨族方向检查。所有解码在温度=0.0 下进行，除非 N=4 采样本身就是方法。黄金判断器分析以 DeepSeek V4-Pro × ProofNet# 为锚点，跨模型和跨数据集运行作为机制方向检查，采用较粗的（仅 GTED）判断器分辨率。

#### 方法。
四种方法，预算大致相同（约4次 LLM 调用）。
- **Vanilla**：一次性生成。
- **Lean-Retry**（Guo 等，2025（https://arxiv.org/html/2606.28013#bib.bib5）风格）：生成 Lean 签名，通过将解释器错误反馈给 LLM 进行精炼，K=3 次重试。
- **Sample-Filter**（Poiroux 等，2024（https://arxiv.org/html/2606.28013#bib.bib12）风格）：采样 N=4 个候选，保留通过解释器的候选，选取第一个。
- **SAF**（本文，§3（https://arxiv.org/html/2606.28013#S3））：类型化 JSON IR 针对解释器精炼，通过确定性的大约30行过程翻译为 Lean，K=3。

#### 判断器。
双判断器协议将 **Claude Opus 4.7**（Anthropic，与所有四个主体家族无重叠）作为黄金交叉判断器，与 **GTED**（Liu 等，2025b（https://arxiv.org/html/2606.28013#bib.bib9））作为可扩展的符号代理配对。Opus 比较候选 Lean 与黄金 Lean 的语义等价性：当候选通过解释时使用 STRICT 提示，否则使用 EQUIV-IF-FIXED 提示，在 DeepSeek V4-Pro × ProofNet# × {Vanilla, Lean-Retry, SAF, Sample-Filter} 上产生 744 个判定，在 DeepSeek V4-Pro × MiniF2F × Vanilla 上产生 244 个判定，总共 988 个判定。GTED 在 LSP 提取的类型化操作符树上计算广义树编辑距离，返回 [0,1] 之间的相似度，在 τ=0.5 处阈值化，并在所有 19 个（模型、数据集、方法）组合上运行。

#### 基础设施。
Lean 4.19.0，通过 lean_interact，预构建 Mathlib，基于 ATLAS 的（Liu 等，2025a（https://arxiv.org/html/2606.28013#bib.bib8））GTED LSP 后端，解释超时 60 秒，所有流水线支持 JSONL 断点续传。

## 5 实验结果与分析

### 5.1 各方法单元分解

（请参见图注）

图2：Vanilla 信号-覆盖矩阵（DeepSeek V4-Pro × ProofNet#）。玫瑰色标出的非对角线单元标记解释器/Opus 分歧。

对于在 DeepSeek V4-Pro 上运行的 186 个 ProofNet# 测试问题（每种方法），我们记录解释器标签（通过/失败）和 Opus 标签（等价/不等价），将每个输出分配到 §2（https://arxiv.org/html/2606.28013#S2）中定义的四个单元之一。表1（https://arxiv.org/html/2606.28013#S5.T1）报告了四种方法的矩阵，图2（https://arxiv.org/html/2606.28013#S5.F2）可视化了 Vanilla 的单元计数，图3（https://arxiv.org/html/2606.28013#S5.F3）显示了跨方法的 TC / SF 比较（根据公式1（https://arxiv.org/html/2606.28013#S2.E1）计算）。我们以 DeepSeek V4-Pro × ProofNet# 作为运行示例，因为它是唯一具有完整四种方法 Opus 双判断的（模型、数据集）单元。附录E（https://arxiv.org/html/2606.28013#A5）将相同的 ΔTC / ΔSF 比较扩展到 GTED 下的其他五个单元。单元级视图使我们能够区分解释器端的恢复（TO→TS）与语义恢复（SO→TS），而不是从单一聚合率中同时解读两者。