The Signal-Coverage Matrix:
Stratifying Type and Semantic Errors in Statement Autoformalization

For each of the 186 ProofNet^# test problems run on DeepSeek V4-Pro under each of the four methods, we record the elaborator label (pass / fail) and the Opus label (equivalent / not-equivalent), assigning each output to one of the four cells defined in §2. Table 1 reports the four-method matrix, Figure 2 visualizes Vanilla’s cell counts, and Figure 3 shows the cross-method TC / SF comparison (computed per Equation 1). We use DeepSeek V4-Pro $\times$ ProofNet^# as the running example because it is the only (model, dataset) cell with full four-method Opus dual-judging. Appendix E extends the same $\Delta$TC / $\Delta$SF comparison to the other five cells under GTED. The cell-level view is what lets us separate elaborator-side recovery (TO$\to$TS) from semantic recovery (SO$\to$TS) rather than read both off a single aggregate rate.

Vanilla decomposes as 95 / 16 / 61 / 14. Of the 91 failures, the elaborator catches 75 (TO $+$ BF) and Opus catches 30 (SO $+$ BF), with overlap of 14. The 77 / 186 outputs off-diagonal (41.4%, SO $+$ TO) are the per-instance disagreements between the two signals. The largest single recovery target for any elab-only feedback method is the 61 TO cases: semantically correct outputs that the elaborator nonetheless rejects on surface form.

The three elab-feedback methods add 34 to 36 problems to TS, shrink TO by 20 to 24, shrink BF by 7 to 10, and shrink SO by only 5–6 from its baseline of 16, despite their algorithmic differences (feedback vs. sampling, raw Lean vs. typed IR). A bootstrap 95% CI ($B{=}10{,}000$, Table 9) shows $\Delta$TS and $\Delta$TO significant for all three methods (CI does not cross 0), while $\Delta$SO is not significant for any.

Aggregate $\Delta$s answer which cells moved on net. To resolve which problems moved, we join each problem’s Vanilla cell to its Lean-Retry cell, giving the $4{\times}4$ transition matrix in Figure 4 and the per-cell decomposition of $\Delta|\textsc{TS}|$ in Equation 2.

Writing $|c{\to}c^{\prime}|$ for the number of problems in Vanilla cell $c$ that land in Lean-Retry cell $c^{\prime}$, the net TS gain is given by

attributing $23/36\approx 64\%$ to type-stratum recovery and $14/36\approx 39\%$ to semantic flip on the rescued side. Per-cell individual rescue rates are: 96.8% of Vanilla TS stay TS, 87.5% (14 / 16) of Vanilla SO problems are individually rescued, and only 37.7% (23 / 61) of Vanilla TO are recovered, with the remainder stuck.

The aggregate SO count drops only from 16 to 10 under Lean-Retry, but this stability masks substantial per-problem turnover. 14 of 16 Vanilla SO are individually rescued (87.5%), while Lean-Retry simultaneously creates 8 new SO (4 from BF, 3 from TS regression, 1 from TO), for a net change of $-6$: aggregate stability hides a near-total replacement of the underlying error population.

Of the 2 Vanilla SO problems that remain SO under Lean-Retry, both are gold-formalization bugs, verified by Opus reasoning across all four methods. The first, Ireland-Rosen|exercise_1_30, asks “Prove that $1/2+1/3+\cdots+1/n$ is not an integer.” Gold’s summand $\frac{1}{n+2}$ does not depend on the summation index, so the gold sum evaluates to $n/(n+2)$, a different proposition from the harmonic tail. The candidate faithfully formalizes the harmonic tail, and Opus correctly judges candidate $\neq$ gold under all four methods (Example 1).

The companion case Dummit-Foote|exercise_7_2_2 has gold LHS $p\mid 0$, trivially true in any commutative ring, so the biconditional collapses to a one-sided statement (Appendix F, Case D). Both cases are documented with Opus traces and suggested corrections in the supplementary note.

Across all four methods, only 1 of 186 problems is durably SO (Ireland-Rosen|exercise_1_30). Under Lean-Retry the count rises to 2, both gold bugs. Excluding the gold bugs, zero of 186 problems are durably semantic-only across the three elab-feedback methods, so the SO plateau approximates the gold-error floor of the benchmark.

The aggregate gains of §5.1 and the transition matrix of §5.2 naturally raise the question: do the three elab-feedback methods recover the same problems at the same rate, or do they merely converge in aggregate? For each Vanilla cell $c\in\{\textsc{TS},\textsc{SO},\textsc{TO},\textsc{BF}\}$ and each elab-feedback method $m$, define the recovery rate

Table 2 reports the four rates for each of the three elab-feedback methods.

All three elab-feedback methods recover exactly 23 of the 61 Vanilla TO problems, despite differing in algorithm (sequential elaborator feedback, deterministic IR refinement, parallel $N{=}4$ sampling), in LLM call topology, and in candidate generation entropy. The point estimate has a wide Wilson 95% CI of $[26.6\%,50.3\%]$ at $n{=}61$, so we do not claim the true rate is precisely 37.7%. What we claim, and what the predictive regularity of Table 3 rests on, is that the three methods recover statistically indistinguishable populations on the type stratum: per-method CIs overlap entirely, and a Fisher exact test of pairwise homogeneity returns $p{=}1.00$ for all three pairs. Appendix A gives Wilson CIs for every cell of Table 2 and discusses the limits of the $n{=}186$ sample. The semantic recovery rate is high and tighter than the BF rate (the latter is small-$n$ noise, 14 BF problems total). The retention rate on TS is uniformly $\geq 92.6\%$, so net regression is small.

Taking any single elab-feedback method’s rates and applying them as a mass-balance rule to the Vanilla cell distribution $(|\textsc{TS}|,|\textsc{SO}|,|\textsc{TO}|,|\textsc{BF}|)=(95,16,61,14)$ yields a testable prediction for the other methods. With Lean-Retry’s rates, $\hat{\Delta\textsc{TS}}=0.377{\cdot}61+0.875{\cdot}16+0.143{\cdot}14-(1-0.968){\cdot}95=+36.0$. Table 3 compares predicted to observed: the calibration on Lean-Retry predicts the other two methods’ $\Delta\textsc{TS}$ to within 2 of 186 problems, an order of magnitude better than the bootstrap noise band of any cell.

Extending across the six (model, dataset) cells of the cross-model panel, where the test is necessarily at the TC level (Opus dual-judging is anchored on the V4-Pro $\times$ ProofNet^# cell), the recovery rate of Vanilla elab-fails under Lean-Retry fits a single linear regression in the Vanilla elab-fail rate $V_{\rm fail}$:

with per-cell residuals in $[-1.0,+1.3]$ pp (Table 4). The recovery rate of elab-fails ($\Delta TC/V_{\rm fail}$) is $41.2\%$ on ProofNet^# (range $[38.3,45.3]$) and $61.8\%$ on MiniF2F (range $[48.4,73.3]$): the same elab-signal recovers a strictly higher share of failures on type-simple benchmarks because type-simple failures concentrate in the easy surface-form band that $K{=}3$ refinement resolves.

Two consequences for method comparison follow. First, a new method’s aggregate $\Delta TC$ is partially determined by its target’s Vanilla cell distribution, not only by the method’s algorithmic innovations: a method evaluated only on a type-complex benchmark will look weaker than the same method on MiniF2F, by a benchmark-modulation factor predicted from $V_{\rm fail}$ alone. Second, the type-stratum recovery rate of $23/61$ is what current elab-feedback methods deliver, and closing the gap to the elab-only ceiling $(|\textsc{TS}|{+}|\textsc{TO}|)/n=83.9\%$ would require recovering hard TO cases that survive $K{=}3$ refinement, a population on which no current method makes progress (§6). The within-$2/186$ agreement is partly self-consistency, since the three methods already converge in aggregate (Table 1).

On the same 186 DeepSeek V4-Pro $\times$ ProofNet^# outputs, Claude Opus 4.7 and GTED $\tau{=}0.5$ give different SF% numbers (Table 5). SAF’s deterministic IR translator isolates the cause.

On Vanilla the two judges agree to within $+7$ pp. On the three elab-feedback methods they disagree by $+26$ to $+37$ pp, with Opus reading SF as rising and GTED reading it as flat or falling. The mechanism: GTED penalizes surface-form normalizations (alternative opens, IsCompact univ$\leftrightarrow$CompactSpace, $\mathrm{Fin}\,n\to\mathbb{R}$ vs. $\forall i:\mathbb{N},\,\mathrm{Icc}\,0\,1$ restatements) that elab-feedback adopts to satisfy the elaborator, while Opus recognizes these as semantically equivalent. Example 2 is a representative instance on Munkres|exercise_29_4: gold and candidate denote the same $\Pi$ type, but GTED returns similarity 0.143 because the extracted operator trees place an arrow node where the other places a $\forall$ binder.

Table 6 confirms that $\tau{=}0.5$ maintains 95.0% pooled precision on ProofNet^# and $\geq 93\%$ on every method individually (per-method breakdown in Table 10). The threshold is stable across distributions, so the gap is a structural property of elab-feedback’s surface rewriting rather than of judge calibration.

The Opus-equiv but GTED-non-equiv set ($n{=}38$ on Vanilla, $n\in[62,76]$ on the three elab-feedback methods) is what drives the gap. We classify each case by the type of rewrite that distinguishes the candidate from gold (rules and per-method audit in Appendix D):

• •

  Notational (N). Surface rewrites that preserve definitional shape: A->B vs. forall _ : A, B, Real^n vs. Fin n -> Real, coercion (ZMod 2 for the unique field of order 2), alternative open/namespace prefixes, or cosmetic renaming.

• •

  Idiomatic (I). Definitional aliases or Mathlib formulation swaps: IsConj vs. exists g, b = g*a*g^-1, Summable vs. Tendsto of partial sums, CompactSpace vs. IsCompact Set.univ, or LinearEquiv-via-Nonempty typeclass framing.

• •

  Structural (S). Binder, quantifier, or typeclass restructuring that changes the post-elaboration term: let vs. explicit hypothesis, instance binder vs. hypothesis binder, [Field] vs. (h : Field), quantifier moved inside or outside an existential, Iff direction swap, biconditional introduced or collapsed, or subtype vs. predicate-restricted set.

• •

  Residual (Z). Cases that mix multiple categories or resist single-category classification.

Table 7 reads as follows. On Vanilla, 38 of 95 elab-pass outputs ($40\%$) are surface-form rewrites Opus accepts but GTED does not, distributed across all four categories. Under each elab-feedback method the false-negative count grows by 24 to 38 problems. For Lean-Retry and Sample-Filter the growth concentrates in category S (16 of 24 and 21 of 24 added cases, respectively): the elaborator pressures the LLM to restructure binders, typeclass formulations, and quantifier orderings until the output type-checks. SAF’s growth is more diffuse: only 9 added in S (the smallest, because SAF’s deterministic ir_to_lean translator does not freely restructure binders) but $+20$ in Z, reflecting the multi-category rewrites the IR-mediated path tends to produce. The disagreement gap is therefore not random surface variance but a measurement of elaborator-driven structural rewriting, which is precisely the mechanism that recovers TO into TS (§5.2).

DeepSeek V4-Pro $\times$ MiniF2F-test $\times$ Vanilla (244 problems, Opus-judged) decomposes as TS=163, SO=24, TO=51, BF=6. The SO rate is 9.8%, essentially unchanged from 8.6% on type-complex ProofNet^#. The TO rate, by contrast, drops from 32.8% to 20.9%. Dataset type-complexity loads the type stratum and not the semantic stratum, providing supporting evidence at Vanilla-only resolution for the mechanism of §5.2. Full MiniF2F dual-judge analysis across the four methods is future work.

Figure 5 reports TC% for three subject models on both datasets. Lean-Retry $\geq$ Vanilla in 6/6 cells (mean $\Delta$TC $=$ $+10.1$ pp). SAF $\geq$ Vanilla in 5/6, the one exception (Qwen $\times$ ProofNet^#, $-12.9$ pp) being a high IR-extraction failure rate on Qwen3.5-Plus, reported without ad-hoc patching. Under GTED-only judging, $\Delta$TC $>$ $\Delta$SF holds in 6/6 cells for Lean-Retry (mean $+10.1$ vs. $+1.3$ pp, Table 11).

Figure 6 plots SAF’s K-saturation on DeepSeek V4-Pro $\times$ ProofNet^#. TC% rises 50.5 $\to$ 72.0 $\to$ 74.7 $\to$ 75.3% across $K{=}0,1,2,3$. Refinement saturates at $K{=}1$ ($+21.5$ pp), with $K{=}2,3$ contributing $+3.3$ pp combined. All three methods land within 1.0 pp at saturation (SAF 75.3, Lean-Retry 75.8, Sample-Filter 76.3), so different topologies reach the same ceiling. Per-iteration faithfulness remains high: $k^{*}{=}0$: 89/94 (94.7%), $k^{*}{=}1$: 34/40 (85.0%), $k^{*}{=}2$: 5/5 (100%), and $k^{*}{=}3$: 1/1 (100%). Of the 46 problems that never pass, 39 (84.8%) are Opus equiv-if-fixed (i.e., TO). The 16 durably TO across all four methods share a common failure mode: plausible but invalid Mathlib API names that elab errors cannot prescribe (Appendix F, Case E).