Paper deep dive
Quizzing the Translation: A Prover-Grounded Evaluation Metric for NL$\rightarrow$FOL
Pu Suo, Ali Emami
Intelligence
Status: not_run | Model: - | Prompt: - | Confidence: 0%
Entities (0)
Relation Signals (0)
No relation signals yet.
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:A standard pipeline for symbolic reasoning over natural-language problems translates them into first-order logic and invokes a theorem prover. The translation step is the bottleneck: swap "every" for "some" and every inference that follows is corrupted. Yet today's metrics often score more broken translations higher than less broken ones, because BLEU, BERTScore, and Smatch++ reward surface overlap that the worst errors happen to preserve. We introduce SIV, which derives two kinds of probes from the target formula and uses a theorem prover to verify the candidate translation against each. Positive probes are statements the candidate must entail, which detect translations that drop content; contrastive probes are statements the candidate must not entail, which detect translations that assert more than the original. On a controlled pool of perturbed FOLIO translations, the severity of the error accounts for 80% of SIV's score variance, compared with at most 17% for any prior metric. Across six error classes on a disjoint pool, SIV scores the reference above the perturbed candidate in over 99% of pairs. Because each probe is labeled with what it tests, the failure pattern also supplies a labeled error trace, recovering the perturbation class at macro-F1 0.638, nearly double the score-only baseline. On 434 expert-audited real LLM translations, SIV attains the top AUC, uniquely detects and grades expert-labeled major errors, and abstains, rather than mis-scoring, on out-of-vocabulary translations.
Tags
Links
- Source: https://arxiv.org/abs/2609.33612v1
- Canonical: https://arxiv.org/abs/2609.33612v1
Trouble viewing inline? Open PDF directly →
Full Text
84,158 characters extracted from source content.
Expand or collapse full text
Quizzing the Translation: A Prover-Grounded Evaluation Metric for NL→ Pu Suo Affiliation: Emory University Email: psuo2@emory.edu Ali Emami Affiliation: Emory University Email: aemami@emory.edu Abstract A standard pipeline for symbolic reasoning over natural-language problems translates them into first-order logic and invokes a theorem prover. The translation step is the bottleneck: swap “every” for “some” and every inference that follows is corrupted. Yet today’s metrics often score more broken translations higher than less broken ones, because BLEU, BERTScore, and Smatch++ reward surface overlap that the worst errors happen to preserve. We introduce SIV, which derives two kinds of probes from the target formula and uses a theorem prover to verify the candidate translation against each. Positive probes are statements the candidate must entail, which detect translations that drop content; contrastive probes are statements the candidate must not entail, which detect translations that assert more than the original. On a controlled pool of perturbed FOLIO translations, the severity of the error accounts for 80%80\% of SIV’s score variance, compared with at most 17%17\% for any prior metric. Across six error classes on a disjoint pool, SIV scores the reference above the perturbed candidate in over 99%99\% of pairs. Because each probe is labeled with what it tests, the failure pattern also supplies a labeled error trace, recovering the perturbation class at macro-F1 0.6380.638, nearly double the score-only baseline. On 434434 expert-audited real LLM translations, SIV attains the top AUC, uniquely detects and grades expert-labeled major errors, and abstains, rather than mis-scoring, on out-of-vocabulary translations. NL. “Holding companies hold several companies.” φ=∀x.HC(x)→∃y.(C(y)∧H(x,y)) \;\;\>=\;∀ x.\,HC(x)→∃ y.(C(y) H(x,y)) ↓ inner quantifier strengthened (∃→∀∃\,→\,∀) φ′=∀x.HC(x)→∀y.(C(y)→H(x,y)) =\;∀ x.\,HC(x)→ [rgb]0.75,0,0 ∀\,y.(C(y)→ H(x,y)) What existing metrics return: BLEU 0.760.76 × × BERTScore 0.870.87 × × Smatch++ 0.940.94 × × (rates near-perfect) LE 0.750.75 × × (no localization) LT 0.000.00 ✓ (binary; no localization) What SIV does. Derive probes from φ ; adjudicate each with the prover. Positives (candidate must entail): φ′⊧ ∀x.(HC(x)→∃y.C(y))∀ x.(HC(x)→∃ y.\,C(y)) ✓ φ′⊧ ∀x.(HC(x)→∃y.(C(y)∧H(x,y)))∀ x.(HC(x)→∃ y.(C(y) H(x,y))) ✓ Contrastives (candidate must not entail): φ′⊧ ∀x.(HC(x)→∀y.(C(y)→H(x,y)))∀ x.(HC(x)→∀ y.(C(y)→ H(x,y))) × × φ′⊧̸ ∀x.∃y.(C(y)∧H(x,y))∀ x.\,∃ y.(C(y) H(x,y)) ✓ φ′⊧̸ ∀x.(HC(x)→¬∃y.(C(y)∧H(x,y)))∀ x.(HC(x)→ ∃ y.(C(y) H(x,y))) ✓ φ′⊧ ∃y.(C(y)∧∀x.(HC(x)→H(x,y)))∃ y.(C(y) ∀ x.(HC(x)→ H(x,y))) × × SIV-F1 =0.667=0.667 (recall 2/22/2, precision 2/42/4) trace: two contrastives fired, flip_quantifier (inner ∃→∀∃\,→\,∀) and scope_swap (∀∃→∃∀∃\,→\,∃∀) Figure 1: An inner-quantifier-strengthened FOLIO translation: “every holding company holds every company” rather than “some.” SIV is the only metric to both flag the error and name its structural axes. 1 Introduction Translating natural language into first-order logic is the bottleneck of any system that combines natural language with symbolic inference, and the most visible recent context is the LLM-prover pipeline pursued by Logic-LM (Pan et al., 2023) and its successors (Olausson et al., 2023; Ye et al., 2023; Ryu et al., 2025). A single misplaced quantifier suffices to corrupt every inference that follows. Consider the FOLIO (Han et al., 2024) premise “Holding companies hold several companies,” whose expert formalization is φ=∀x.HC(x)→∃y.(C(y)∧H(x,y)) =∀ x.\,HC(x)→∃ y.(C(y) H(x,y)). Strengthening the inner existential to a universal converts “holds some company” into “holds every company”: downstream reasoning is now warranted by a claim the original never made. Detecting such errors is the job of a translation metric, and the metrics currently used for NL→ fall short in a characteristic way. Surface-level metrics such as BLEU (Papineni et al., 2002) and BERTScore (Zhang et al., 2020) compare formulas as token strings or embeddings, and the graph-based Smatch++ (Opitz, 2023) compares them as graphs. The Logical Equivalence (LE) score of Yang et al. (2024) compares propositional truth tables, and the logical-theory (LT) check of Brunello et al. (2026) returns a binary FOL-equivalence verdict via Z3. Figure 1 shows what each returns on the over-strengthened translation above: most rate it nearly correct (Smatch++ at 0.940.94). The deeper problem, documented in §4, is that these failures are not random. On a controlled pool of perturbed translations, BLEU, BERTScore, and Smatch++ systematically score severely-broken translations higher than partially-broken ones, because the perturbations that damage meaning the most also tend to preserve the most surface content. More wrong is not more surface-different. We propose Structural Inference Verification (SIV), a metric that evaluates a translation by quizzing it. SIV checks whether the candidate is logically equivalent to its reference: whether it asserts neither more nor less than the reference does. A candidate can fail this in exactly two ways: by understating the reference (asserting less; the reference entails the candidate but not vice versa) or by overstating it (asserting more; the candidate entails the reference but not vice versa). SIV catches both by deriving two kinds of probes from the reference and adjudicating each with the theorem prover Vampire (Kovács and Voronkov, 2013). Positive probes are statements the reference itself entails; the candidate must entail them too, or it has understated. Contrastive probes are statements stronger than the reference; the candidate must not entail them, or it has overstated. SIV’s score is the F1 over both probe sets, and each failed probe is labeled with the structural feature it tested, yielding a per-translation diagnostic trace. The Method section (§3) gives worked examples of each probe type. We establish four findings: • Existing metrics do not track error severity. On a stratified FOLIO pool, BLEU, BERTScore, and Smatch++ assign higher scores to severely-broken translations than to partially-broken ones, and LE collapses to chance (AUC =0.500=0.500) on quantifier flips. No prior NL→ metric tracks how broken a translation actually is. • SIV’s score tracks it precisely. Error severity accounts for 80%80\% of SIV’s score variance, compared with at most 17%17\% for any baseline. Across six structural error classes on a disjoint pool of 1,8651,865 verified perturbation pairs, SIV ranks the reference above the perturbed candidate in over 99%99\% of cases. This is the architectural payoff of the two-sided design: on strictly-stronger errors, positive probes are saturated by construction and the contrastive arm carries the entire detection signal. • SIV’s trace labels the structural error. Each failed probe is labeled with the structural feature it tests, so the pattern of failures classifies the error type, a signal useful for debugging translators, ranking failures, or supplying class-conditional feedback in training loops. A deterministic, parameter-free rule classifier over the trace recovers the class at six-class macro-F1 =0.638=0.638, nearly twice the 0.3330.333 of the strongest score-only baseline. • SIV transfers to real translator outputs. On 434434 expert-audited LLM translations (§7), SIV attains the top AUC point estimate (0.8410.841), is the only metric that both detects and grades expert-labeled major errors (0.200.20 vs. 0.800.80 on correct), and is the only metric with an out-of-vocabulary abstention flag (F1 0.870.87). We release the parser, the probe suites, the expert-audited real-translation pairs, and full reproduction code.11 1 Code and data: https://github.com/pu-suo/siv-metric. Prover-grnd. Quant.-aware Graded Per-trans. Diagn. trace BLEU × × × × ✓ ✓ × × BERTScore × × × × ✓ ✓ × × Smatch++ × × × × ✓ ✓ × × LE ∼ × × ✓ ✓ × × LT ✓ ✓ × × ✓ × × EPR ✓ ✓ × × × × × × SIV (ours) ✓ ✓ ✓ ✓ ✓ Table 1: Capability comparison of NL→ evaluation metrics. ✓ supported; × × not supported; ∼ partially supported. SIV is the only metric combining all five. 2 Related Work 2.1 NL→ translation and benchmarks MALLS (Yang et al., 2024) and FOLIO (Han et al., 2024) anchor the NL→ benchmark landscape. MALLS is GPT-4-generated at sentence scale and evaluated through the LE score on predicate truth tables; FOLIO is expert-written and evaluated through downstream entailment classification. Thatikonda et al. (2026) provide a taxonomy of translation errors and improve small-LM symbolic translation via error-aware fine-tuning. Brunello et al. (2026) decompose NL→ into ontology extraction and logical translation, showing that frontier dialogue-oriented LLMs perform the latter at over 0.900.90 accuracy when given a fixed signature. 2.2 Metrics for NL→ translation Table 1 summarizes existing metrics along the capability axes for per-translation evaluation. Existing metric families. Surface metrics (BLEU, Papineni et al., 2002; BERTScore, Zhang et al., 2020) and the graph-based Smatch (Cai and Knight, 2013) and Smatch++ (Opitz, 2023) compare formulas at the token, embedding, or graph level, and cannot represent quantifier scope, binding, or polarity; Funakura et al. (2025) and Thatikonda et al. (2025) both show empirically that graph-overlap does not predict logical equivalence. The LE score (Yang et al., 2024) reduces FOL to propositional truth tables, discarding quantifier structure. The LT check (Brunello et al., 2026) adjudicates first-order equivalence via Z3 correctly, but returns only a binary verdict: no gradient, and no localization of the error. EPR, the Entailment Preservation Rate of Lee et al. (2025), is likewise prover-grounded but reference-free and corpus-level: it scores a translator by whether prover inference over the translated premise set reproduces gold entailment labels, and so provides neither a per-translation score nor a diagnostic. Methodological precedent. Test-suite evaluation for SQL semantic parsing (Zhong et al., 2020; Wang et al., 2024) is the closest precedent: derive a suite of behavioral queries from the reference and grade each. We port the idea from SQL to FOL by replacing query execution with prover-adjudicated entailment. Adjacent metrics on different problems. Tree-edit metrics with logical rewrites (GTED, Liu et al., 2025b; ASSESS, Liu et al., 2025a) target Lean autoformalization; edit distance cannot tell an over-claiming candidate from an equivalent one, the case SIV’s contrastive probes handle by design. Predicate alignment (Hosseini et al., 2018) and Jaccard partial correctness (Wong and Mooney, 2007) evaluate vocabulary or clause-set overlap rather than prover-checked entailment. Where SIV fits. SIV combines capabilities that prior metrics distribute across families: prover-grounded adjudication (as in LT and EPR), a graded score (as in surface and graph metrics), and a per-translation diagnostic trace that no prior metric provides. All three come from a single mechanism: decomposing the reference into a labeled set of probes and adjudicating each independently. A principled graded notion of logical similarity is difficult in general (Paris and Vencovská, 2015); SIV makes a reference-anchored version tractable by reducing gradation to counts over independently adjudicated, prover-certified probes. 3 The SIV Metric Reference φ Parser Positive probes +P^+ weakenings of φ Contrastive probes −P^- perturbations of φ Vampire prover φ′⊧p p? Candidate φ′ SIV score F1F_1 Trace verdict + label Figure 2: SIV pipeline. Vampire adjudicates the candidate φ′ against positive and contrastive probes derived from φ ; the verdicts produce an F1 score and a labeled trace. 3.1 Overview A translation is correct when it is logically equivalent to its reference φ : it must entail what φ entails (otherwise it understates), and must not entail what φ does not (otherwise it overstates). SIV catches each failure mode with its own probe set; Figure 2 sketches the full pipeline. We use a running example throughout: the sentence “Every car has a black, round wheel” with reference φ=∀x.(CLOSE =∀ x. ( (x)→∃y.(ℎ(y)CLOSE (x)→∃ y.(Wheel(y) (1) ∧ℎ(x,y) \,HasWheel(x,y) OPENOPEN∧(y)∧(y))). \,Black(y) (y)) ). The inner existential ∃y.(ℎ(y)∧…)∃ y.(Wheel(y) …) has typing predicate ℎ(y)Wheel(y) as its restrictor, and the remaining body conjuncts ℎ(x,y),(y),(y)HasWheel(x,y),Black(y),Round(y) as its nuclei; this is the standard (restrictor, nucleus, scope) decomposition of generalized quantifiers (Barwise and Cooper, 1981).22 2 Produced by a deterministic CFG parser; round-trip parsing yields a logically equivalent formula on 99.94%99.94\% of FOLIO premises (Vampire-verified). Positive probes (+P^+) catch understatement. Each is a formula entailed by φ that isolates one piece of its structure. For (1), +P^+ contains the reference itself together with four further probes: the restrictor-only “every car has some wheel,” plus three probes that keep wheel-existence and add one further conjunct each, with the outer universal-implication scaffolding preserved at every step: ∀x.((x)→∃y.ℎ(y)), ∀ x.(Car(x)→∃ y.\,Wheel(y)), ∀x.((x)→∃y.(ℎ(y)∧(y))), ∀ x.(Car(x)→∃ y.(Wheel(y) (y))), ∀x.((x)→∃y.(ℎ(y)∧(y))), ∀ x.(Car(x)→∃ y.(Wheel(y) (y))), ∀x.((x)→∃y.(ℎ(y) ∀ x.(Car(x)→∃ y.(Wheel(y) OPENOPEN∧ℎ(x,y))). \,HasWheel(x,y))). A correct candidate must entail all five. A failure on any one is a specific weakness: missing the wheel-existence commitment, missing blackness, missing roundness, or missing the having-relation. Contrastive probes (−P^-) catch overstatement. Each is a perturbation of φ that is either a strictly-stronger statement (entailing φ but not entailed by φ ) or one incompatible with φ (jointly contradictory). A correct candidate must not entail any. Dropping the outer restrictor (x)Car(x) from (1) yields a strictly-stronger contrastive, ∀x.∃y.(CLOSE ∀ x.\,∃ y.( ℎ(y)∧ℎ(x,y) (y) (x,y) OPEN∧(y)∧(y)), (y) (y)), which asserts that every entity, not just every car, is associated with such a wheel. A candidate that entailed this would be making a structural commitment φ does not. How each probe set is built is the topic of §3.2 and §3.3; §3.4 defines the score. Every probe also carries a label naming the structural feature it tests, which feeds the per-translation diagnostic trace evaluated in §6. Scope. SIV evaluates structural fidelity within an alignable logical vocabulary, not arbitrary semantic equivalence. Candidate predicates are aligned to the reference vocabulary where possible (Appendix E); pairs whose vocabulary cannot be grounded are flagged, not silently scored (§7). 3.2 Building positive probes Positive probes are generated by recursive descent through φ . At each binder, implication, or conjunction, we emit one probe per droppable conjunct, preserving the surrounding context; disjunctions are never decomposed. A disjunction only ever enters +P^+ carried whole, as a single dropped conjunct of an enclosing conjunction, which is a sound weakening; dropping a disjunct strengthens a formula and therefore belongs to the contrastive inventory (disjunct_drop, Appendix D). Concretely, for an existential-conjunction ∃y.(R(y)∧N1(y)∧⋯∧Nk(y))∃ y.(R(y) N_1(y) ·s N_k(y)) inside scope S[⋅]S[·], with restrictor R and nuclei NiN_i, we emit the restrictor-only probe S[∃y.R(y)]S[∃ y.\,R(y)] and the restrictor-plus-one-nucleus probes S[∃y.(R(y)∧Ni(y))]S[∃ y.(R(y) N_i(y))] for each i. Universal quantifications and implications decompose analogously. Preserving the surrounding scope is what makes the construction sound: every emitted probe is a syntactic weakening of φ , so φ⊧p p holds by construction for every p∈+p ^+. In the cars example, the outer ∀x.((x)→⋅)∀ x.(Car(x)→·) is carried into every probe. Without it, the bare “∃y.ℎ(y)∃ y.\,Wheel(y)” would not be entailed by φ (a domain with no cars makes φ vacuously true but says nothing about wheels), so this probe would not appear in +P^+. Every emitted probe is also Vampire-certified against its reference at suite-build time (zero-failure audit, Appendix H), so an unsound probe cannot enter the suite. 3.3 Building contrastive probes Contrastive probes are generated in two steps: we apply structural operators to φ , then check each output against φ before admitting it into −P^-. We use ten operators, including swap_binary_args (reversing relational argument order), flip_quantifier (swapping ∀↔∃∀ ∃ on a single binder), drop_restrictor_conjunct (the operator for the cars-example contrastive in §3.1), negate_atom (flipping the polarity of an atomic predicate), and six others spanning quantifier scope, disjunct removal, connective change, and equality (full inventory in Appendix D). Each operator declares whether its output should be strictly-stronger than φ or incompatible with it, and a type-soundness check discards ill-formed outputs. The inventory was selected for systematic coverage of FOL’s structural axes rather than curated from errors observed during development; Appendix D documents per-operator provenance, the selection principle, and the inventory’s measured coverage boundary on real translator outputs (§7). Operators are only generators: an operator’s declared relation to φ is a prediction, not a guarantee. The theorem prover Vampire (Kovács and Voronkov, 2013) checks the prediction before admission. A strictly-stronger ψ is admitted only if ψ⊧φψ and φ⊧̸ψ ψ; an incompatible ψ only if φ∧ψ⊧⊥ ψ . The check runs under Vampire’s default axioms plus per-predicate and per-restrictor existence witnesses derived from φ ; for binary relations, asymmetry and symmetry axioms come from a frozen 427427-predicate label table, so that for R labeled asymmetric, ∀x,y.R(x,y)→¬R(y,x)∀ x,y.\,R(x,y)→ R(y,x) certifies swap_binary_args as incompatible on ground-atom occurrences. A perturbation that turns out to be logically independent of φ (Vampire returns neither entailment nor contradiction) is dropped. The bias is conservative: we accept lost contrastive coverage rather than risk a probe whose declared relation does not hold. §6.3 returns to the model-theoretic limits of this regime. 3.4 Scoring Let T+=p∈+:φ′⊧pT^+=\p ^+: p\ be the positive probes the candidate correctly entails, and F−=p∈−:φ′⊧̸pF^-=\p ^-: p\ the contrastive probes it correctly does not. Treating “should be entailed” as the positive class of a binary classifier, the SIV score is the corresponding F1: SIV(φ′,φ)=2|T+||T+|+|+|+|−|−|F−|.SIV( , )= 2\,|T^+||T^+|+|P^+|+|P^-|-|F^-|. (2) Concretely, a candidate that omits the blackness commitment entails three of the five positive probes from §3.1 and fails two (Black and the reference itself); being strictly weaker than φ , it entails no contrastive, so |F−|=|−||F^-|=|P^-| and SIV=6/8=0.75SIV=6/8=0.75, with the 0.250.25 drop localized to the two failed probes, both naming Blackness. Both probe arms are necessary. The positive arm alone treats a strictly-stronger candidate as equivalent to a correct one (both entail every positive probe), so the contrastive arm is what catches overstatement. The contrastive arm alone treats a vacuous candidate (one that entails nothing) as equivalent to a correct one (neither entails any contrastive), so the positive arm is what catches understatement. We report the soft variant of SIV, which treats Vampire timeouts symmetrically (a 55-second per call timeout); a strict variant that treats timeouts as “not entailed” produces identical drop magnitudes on §5’s perturbation pool. The full FOLIO probe suite contains 2,3402,340 positive and 3,9323,932 contrastive probes over 1,3931,393 premises. Cost. Probe construction and Vampire admission are paid once per reference (∼0.35 0.35 s) and reused across every candidate and system; the marginal cost of scoring one additional candidate is 6767 ms single-core, 6.86.8 ms on 1414 cores (zero timeouts in 14,29314,293 calls on the §5 pool). Evaluating N systems thus costs build-once plus N×N× seconds; the released pipeline ships prebuilt suites. Appendix K profiles cheaper variants and one pitfall. 4 Experiment 1: Severity tracking This experiment tests whether SIV’s score is calibrated to structural severity: candidates more distant from the reference should receive lower scores, and the magnitude of the drop should track the magnitude of the structural change. Tier φ′ vs. φ Skeleton Example perturbation Ref equivalent — canonical re-serialization OS strictly stronger intact add a nucleus conjunct P strictly weaker intact drop a nucleus conjunct OW strictly weaker broken flip outer ∀→∃∀→∃ Table 2: Severity tiers, ordered by structural distance from φ . Skeleton refers to the top-level quantifier-connective pattern. OW ranks below P because skeleton damage changes the formula’s structural meaning, not just its informational content. Ref candidates are logically equivalent canonical re-serializations of the gold (Vampire-verified); their surface form differs from the FOLIO gold string (§4, Setup). 4.1 Setup Tiers. We sort candidates into four severity tiers by their logical relation to the reference φ (Table 2). Ref candidates are not byte-identical copies of the gold: each is the reference’s own AST re-serialized to canonical ASCII FOL (predicate names preserved). All 105105 are Vampire-certified equivalent to their gold in both directions, and 104/105104/105 differ textually from the gold string, which is why surface metrics score Ref below 1.01.0 (Table 3). OS (overstrong) and P (partial) each represent one unit of structural change in opposite directions: OS preserves all of φ ’s content but adds a strengthening commitment, whereas P drops content from φ while preserving the top-level skeleton. OW (overweak) is worse than P because the same weakening change additionally breaks the skeleton, changing what the formula structurally means rather than merely what it asserts. Appendix A gives full tier construction rules. Pool. We apply 1414 typed perturbation operators across five formula strata to FOLIO premises. Each operator declares its target tier; every generated candidate is bidirectionally verified by Vampire and retained only if its actual logical relation to the reference matches that declaration. The final pool contains 372372 candidates (105105 Ref, 5858 OS, 2525 P, 184184 OW) drawn from 128128 FOLIO premises.33 3 Train split. SIV is evaluated against synthetic perturbations rather than learned, so no test partition is held out. Statistics. η2η^2 from one-way ANOVA with severity tier as the factor, candidate-level on the three non-Ref tiers (n=267n=267), measures the score variance attributable to severity; Cohen’s d on Ref-vs-OW measures the endpoint gap, aggregated to per-(premise, tier) means over the 5353-premise subset with ≥2≥ 2 non-Ref tiers, with 1,0001,000-resample bootstrap CIs. We use magnitude statistics rather than rank correlation because OS/P share rank by design. Baselines. BLEU (Papineni et al., 2002) (tokenized at the formula level); BERTScore (Zhang et al., 2020) (F1 on stringified formulas); Smatch++ (Opitz, 2023) (graph-overlap F1 on a deterministic FOL→ conversion with bound variables anonymized); LE (Yang et al., 2024) (truth-table comparison with greedy literal binding); LT (Brunello et al., 2026) (Z3 binary FOL equivalence). LT is excluded from η2η^2 because its binary range makes both statistics degenerate. 4.2 Results Ref OS P OW η2η^2 d Metric 105105 5858 2525 184184 SIV 1.001.00 .929.929 .442.442 .052.052 .802.802 4.714.71 LE 1.001.00 .850.850 .796.796 .713.713 .075.075 1.501.50 LT (bin.) 1.001.00 .000.000 .000.000 .000.000 — — LT (graded) 1.001.00 .500.500 .500.500 .500.500 .000‡.000 — Smatch++ 1.001.00 .806.806 .629.629 .740†.740 .072.072 1.841.84 BLEU .485.485 .396.396 .315.315 .397†.397 .027.027 1.091.09 BERTScore .872.872 .815.815 .729.729 .822†.822 .170.170 1.351.35 Table 3: Per-tier means and effect sizes. η2η^2: variance explained by tier. d: Cohen’s d on Ref-vs-OW. † : metric scores OW higher than P. LT binary; η2η^2 and d are degenerate. ‡ : graded-LT (bidirectional prover entailment scored 1/0.5/01/0.5/0; §4.2) is constant across the three error tiers, so its between-tier variance is zero. Bootstrap 95%95\% CIs on d: SIV [3.96,6.04][3.96,6.04], LE [1.29,1.83][1.29,1.83], Smatch++ [1.59,2.19][1.59,2.19], BERTScore [1.02,1.71][1.02,1.71], BLEU [0.72,1.51][0.72,1.51]; SIV’s interval does not overlap any baseline’s. Severity tier explains 80%80\% of SIV’s score variance; at most 17%17\% for any baseline. SIV reaches η2=0.80η^2=0.80; the strongest baseline (BERTScore) reaches 0.170.17. SIV’s Ref-vs-OW effect size is Cohen’s d=4.71d=4.71, more than 2.5×2.5× the strongest baseline (Smatch++, 1.841.84), with non-overlapping CIs (Table 3). Surface and graph metrics invert at P→ . BLEU, BERTScore, and Smatch++ each score the more-broken OW tier higher than P (Table 3, † ; Figure 3). P weakens content inside an intact skeleton; OW damages the skeleton yet often preserves more surface tokens (a quantifier flip changes one symbol; a nucleus drop deletes a whole conjunct), so token overlap ranks OW above P, against severity. More wrong is not more surface-different. LE collapses to chance on quantifier operators. The per-operator AUC decomposition (Appendix B) localizes LE’s η2=0.075η^2=0.075: on flip_outer_quantifier and strengthen_quantifier, LE separates the perturbed tier from Ref at AUC =0.500=0.500 (chance), while SIV reaches 1.0001.000. This reproduces Brunello et al. (2026)’s propositional-collapse prediction operator by operator: LE’s truth-table representation discards quantifier structure. BLEU charges half its range for re-serialization. BLEU scores the reference’s prover-verified logical twin at 0.4850.485; re-serializing both sides through the same printer restores it to 1.0001.000 on all 105105 premises. A metric that spends half its range on notation is not measuring logical content. The calibration is robust to design choices. Four checks (Appendix C): (i) merging the equal-rank OS/P tiers leaves SIV at η2=0.706η^2=0.706 vs. at most 0.070.07 for any baseline, with zero severity-order reversals across all 372372 candidates; (i) restricting to the pool operators structurally disjoint from SIV’s contrastive inventory leaves η2=0.759η^2=0.759, d=4.37d=4.37 [3.76,5.49][3.76,5.49], still ∼5× 5× any baseline; (i) the reference’s direct negation receives SIV 0.0220.022, below the lowest tier, while Smatch++ scores the same complement 0.8640.864, above every error tier; (iv) a graded LT (bidirectional entailment under SIV’s prover setup, scored 1/0.5/01/0.5/0) detects every §5 class yet is constant at 0.50.5 across all three error tiers (Table 3, ‡ ) and yields no trace: the prover supplies detection; gradation and diagnosis come from the two-sided probe decomposition. 5 Experiment 2: Per-class detection Experiment 1 measured aggregate calibration across error types. Experiment 2 disaggregates this by structural error class, testing whether SIV ranks the reference above the perturbed candidate and how large the score gap is. 5.1 Setup Pool. We apply six typed perturbation operators to a 642642-premise FOLIO reference set, disjoint by construction from Experiment 1’s 128128-premise design pool. After Vampire bidirectional verification, 1,8651,865 verified (reference, perturbed) pairs remain across six classes (Table 4). The classes span the three logical relations a perturbed candidate can have to its reference: incompatible (the candidate disagrees with the reference on some specific assertion), strictly stronger (the candidate makes additional commitments), and strictly weaker (the candidate drops a commitment). Figure 3: Mean metric score by severity tier (Table 3). SIV descends monotonically (Ref→ : 1.00→0.051.00→ 0.05); Smatch++, BLEU, and BERTScore invert at P→ (red ×); graded-LT is constant at 0.50.5 across all error tiers (§4.2). Binary LT omitted. Drop magnitude [95%95\% CI] Detection rate Class n Relation to ref. SIV-recall SIV-F1 recall F1 arg_swap 494494 incompatible .818.818 [.796,.841][.796,.841] .757.757 [.731,.784][.731,.784] .998.998 .998.998 negation_drop 132132 incompatible .861.861 [.820,.899][.820,.899] .820.820 [.770,.868][.770,.868] 1.0001.000 .992.992 random_substitution 638638 incompatible .960.960 [.949,.970][.949,.970] .942.942 [.928,.956][.928,.956] 1.0001.000 .998.998 flip_outer_quantifier 355355 strictly weaker .984.984 [.975,.992][.975,.992] .975.975 [.961,.986][.961,.986] 1.0001.000 .997.997 restrictor_drop⋆ 231231 strictly stronger .000.000 [.000,.000][.000,.000] .169.169 [.163,.175][.163,.175] .000⋆.000 .996.996 strengthen_quantifier⋆ 1515 strictly stronger .000.000 [.000,.000][.000,.000] .325.325 [.232,.439][.232,.439] .000⋆.000 1.0001.000 Table 4: Six perturbation classes with per-class drop magnitude (score(ref)−score(perturbed)score(ref)-score(perturbed), mean with 95%95\% bootstrap CIs) and within-pair detection rate. ⋆ : strictly-stronger classes saturate SIV-recall at 1.01.0 on both reference and perturbed candidates by construction, so SIV-F1’s signal on these classes comes entirely from the contrastive arm. Statistics. For each pair, we report drop magnitude (score(ref)−score(perturbed)score(ref)-score(perturbed), with 95%95\% bootstrap CIs over the class) and within-pair detection rate (fraction of pairs in the class with score(ref)>score(perturbed)score(ref)>score(perturbed)). 5.2 Results SIV detects every class in over 99%99\% of pairs. SIV-F1 mean drops range from 0.1690.169 on restrictor_drop to 0.9750.975 on flip_outer_quantifier; all 95%95\% CIs exclude zero, and all detection rates exceed 0.990.99 (Table 4). Drop magnitudes calibrate to perturbation severity: large structural changes (a quantifier flip, a random predicate substitution) produce large drops; small structural changes (dropping a single restrictor conjunct) produce small drops. On strictly-stronger classes, the contrastive arm carries the entire detection signal. A strictly-stronger candidate entails the reference, hence every positive probe by transitivity, so SIV-recall registers no drop at all on restrictor_drop or strengthen_quantifier (Table 4, ⋆ ); their entire SIV-F1 drops (0.1690.169 and 0.3250.325; detection 0.9960.996 and 1.0001.000) are sourced from contrastive probes the prover certifies as strictly stronger than φ . Removing the contrastive arm would drop detection on both classes to chance. Two points connect back to §4.2: random_substitution (n=638n=638) lies entirely outside SIV’s contrastive inventory yet is detected at 0.9980.998, and graded-LT detects every class here yet assigns flip_outer_quantifier and restrictor_drop the same 0.50.5, where SIV’s drops separate them by a factor of six. 6 Experiment 3: Error-class recovery from the trace The previous two experiments measured the SIV score. This experiment evaluates what its labeled trace adds: whether the pattern of per-probe verdicts identifies which structural error occurred. 6.1 Setup Classifier. A deterministic seven-rule classifier maps the (failed-positive-probes, fired-contrastive-probes) trace of each candidate to a perturbation class. Rules are applied in order; first match wins (Appendix G). Each rule implements a pre-registered prediction: each class declares its expected trace signature, and the classifier checks for that signature. There are no learned parameters, no fitted thresholds, no per-class hyperparameters. Baseline. A 55-fold stratified cross-validated decision tree on the single feature SIV-F1: the most the scalar score alone can extract about the perturbation class. The headline statistic is the recoverability delta between trace classifier and score-only baseline. Class n F1 P R R95% CI_\,95\% CI restrictor_drop 231231 .996.996 .996.996 .996.996 .976.976–1.001.00 strengthen_q 1515 .933.933 .933.933 .933.933 .681.681–.998.998 negation_drop 132132 .778.778 1.001.00 .636.636 .548.548–.718.718 random_sub 638638 .634.634 .464.464 1.001.00 .994.994–1.001.00 arg_swap 494494 .482.482 1.001.00 .318.318 .277.277–.361.361 flip_outer_q 355355 .006.006 1.001.00 .003.003 .000.000–.016.016 Table 5: Per-class trace classifier performance. R95% CI_\,95\% CI: Clopper-Pearson interval. Analyses of arg_swap and flip_outer_q in §6.3 and §6.4. Pool. Experiment 2’s 1,8651,865 verified pairs, scored by the full SIV pipeline of §3. 6.2 Results The trace nearly doubles diagnostic recovery over the score. The rule classifier reaches macro-F1 =0.638=0.638 at six-class granularity, against 0.3330.333 for the score-only baseline. This is a +0.305+0.305 recoverability delta; the unrecognized rate (Rule 7 fires) is 0.05%0.05\%. Per-class breakdown. Three classes are essentially solved (Table 5): restrictor_drop at F1 =0.996=0.996, strengthen_quantifier at 0.9330.933, and negation_drop at 0.7780.778 (perfect precision; some negation-drops fall to the catch-all rule). random_substitution, the catch-all destination when no operator-specific signature fires, reaches 0.6340.634. Two classes need analysis: arg_swap at 0.4820.482 (§6.3) and flip_outer_quantifier at 0.0060.006 (§6.4). 6.3 arg_swap: ground atoms vs. universal bodies arg_swap’s aggregate F1 hides a clean bimodal pattern (Table 10): the trace recovers swaps reliably when the swapped relation occurs as a ground atom (stratum S5S_5, recall 0.8820.882, n=127n=127) and fails when it is embedded in a universally-quantified body (S2S_2–S4S_4, recall 0.080.08–0.130.13). The failure is a logical limit, not an implementation artifact: the asymmetry axiom ∀x,y.R(x,y)→¬R(y,x)∀ x,y.\,R(x,y)→ R(y,x) certifies a swap only when the formulas jointly assert R(a,b)∧R(b,a)R(a,b) R(b,a) for concrete a,ba,b; under a universal, both formulas are vacuously satisfiable, so Vampire correctly returns “logically independent” and the contrastive is never admitted into −P^- (full account in Appendix G). 6.4 flip_outer_quantifier: detected, not named flip_outer_quantifier’s F1 of 0.0060.006 is a coverage gap in the diagnostic layer, not in SIV’s score, which detects these flips reliably (Experiment 1 AUC =1.000=1.000; Experiment 2 mean drop 0.9750.975, detection 0.9970.997). The layer cannot name the failure because the flip_quantifier contrastive is admitted on only 0.3%0.3\% of these pairs, for the same vacuous-satisfaction reason as §6.3. Closing the gap requires richer witness machinery (e.g., restrictor-existence axioms that force witnesses into both scopes); we defer it to future work to avoid post-hoc tuning to the experimental pool. 7 Experiment 4: Real translator outputs The controlled pools establish calibration; this experiment tests SIV on uncontrolled LLM translator outputs, measuring discrimination against expert correctness judgments, behavior on expert-labeled major errors, and behavior when the translator’s vocabulary diverges from the reference. 7.1 Setup We sample 150150 FOLIO premises (stratified across the §4 formula strata, seed 4242) and translate each with three configurations spanning the quality range: GPT-4.1 (OpenAI, 2025) free-vocabulary, GPT-4.1 with the reference predicate signature supplied (the high-accuracy regime of Brunello et al., 2026), and Qwen2.5-7B (Qwen Team, 2025) free-vocabulary. Of 450450 outputs, 434434 parse. Labels are expert-audited: an independent LLM screening judge (a different model family from all translators) flags candidate errors; an expert labels 121121 pairs on blind sheets, including every flagged pair, so every “incorrect” label is human-verified; disputes were jointly adjudicated. Appendix I gives the full protocol, agreement statistics, and per-configuration results. Metric AUC 95%95\% CI SIV 0.8410.841 [0.707,0.935][0.707,0.935] Smatch++ 0.8140.814 [0.715,0.899][0.715,0.899] LE 0.7990.799 [0.650,0.922][0.650,0.922] LT 0.7910.791 [0.754,0.826][0.754,0.826] BLEU 0.7080.708 [0.533,0.857][0.533,0.857] BERTScore 0.6680.668 [0.526,0.796][0.526,0.796] Table 6: AUC for separating expert-labeled correct from incorrect translations on the compatible-vocabulary stratum (n=185n=185, of which 1010 incorrect; expert-adjudicated labels). 7.2 Results Discrimination. SIV attains the top AUC point estimate (0.8410.841; Table 6), though with only 1010 incorrect pairs in this stratum the pairwise differences against Smatch++ and LE are not significant: on binary discrimination the prover- and graph-based metrics are at parity here. SIV’s advantages are the two capabilities the AUC does not measure. SIV detects and grades major errors. Mean scores on expert-correct vs. expert-major pairs: SIV 0.800.80 vs. 0.200.20; LE 0.890.89 vs. 0.620.62; BERTScore 0.890.89 vs. 0.820.82 (barely moved); binary LT 0.580.58 vs. 0.000.00 (detects, but grades nothing). SIV is the only metric that does both. SIV knows its own scope. 7171–78%78\% of free-vocabulary translations use predicate vocabulary divergent from the reference; alignment (Appendix E) resolves 5959–65%65\% of symbols, and SIV routes the genuinely out-of-vocabulary remainder to an abstention flag (F1 0.870.87, precision 0.930.93) rather than silently mis-scoring it; no baseline has an analogue. The trade-off is explicit: divergent-but-correct pairs receive a low raw score (0.290.29) plus the flag, whereas BERTScore assigns such pairs 0.810.81 and major errors 0.820.82, “handling” divergence only by failing to distinguish it from error. With the signature supplied, 100%100\% of predicates align exactly. The inventory’s boundary, located. Of 2929 adjudicated errors, 1414 are vocabulary divergence (routed to abstention) and 1515 are in-scope. One is a strict over-strengthening the inventory does not generate: a conditional rendered as a biconditional, which saturates the positive arm, fires no contrastive, and scores 1.01.0. A verified eleventh operator, implication_to_biconditional, closes the gap within the existing admission regime (1.00→0.8891.00→ 0.889 with a named trace label, no false fires on faithful conditionals; Appendix D.1). A trace spot-check on ten flagged translations is in Appendix I. FOLIO gold errors. The audit independently surfaced 16/15016/150 premises (∼11% 11\%) with erroneous gold formulas, corroborating Olausson et al. (2023); excluding them, SIV’s AUC rises to 0.8550.855 (still the top estimate). The 434434 audited pairs are released with the code. 8 Conclusion SIV evaluates an NL→ translation against two probe sets derived from the reference: positive probes the candidate must entail and contrastive probes it must not. The F1 over per-probe verdicts is the score; the labeled verdicts are the trace. On a stratified FOLIO pool, severity tier explains 80%80\% of SIV’s variance against at most 17%17\% for any baseline, and the calibration survives merged tiers, inventory-disjoint operators, and a root-negation boundary probe; on a disjoint per-class pool, SIV detects every error class in over 99%99\% of pairs; the trace recovers the perturbation class at macro-F1 0.6380.638 against 0.3330.333 score-only. On 434434 expert-audited real LLM translations, SIV attains the top AUC, uniquely detects and grades major errors, and abstains on out-of-vocabulary pairs; the score ports to MALLS with zero FOLIO metadata (Appendix J). A graded-LT ablation separates the credit: the prover supplies detection; gradation and diagnosis come from the probe decomposition. Three extensions follow: syntactic-signature admission of arg_swap contrastives (§6.3); restrictor-existence axioms certifying outer-quantifier flips (§6.4); and the verified eleventh operator closing the audit’s single in-scope gap (§7, Appendix D). Limitations Scope of the claim. SIV is a structural-fidelity metric for FOL translations within an alignable logical vocabulary; it is not a general-purpose metric for arbitrary NL→ outputs, and we make no claim about arbitrary semantic equivalence. The metric’s edit-operation taxonomy is the one used by Brunello et al. (2026) and Thatikonda et al. (2025), and the test-suite methodology follows Zhong et al. (2020); probe inventory and perturbation pools therefore share structural axes, as is standard for test-suite evaluation, though §4.2 shows the calibration does not depend on that overlap. Our experiments demonstrate calibration under controlled perturbations and discrimination, grading, and abstention on real translator outputs (§7); they do not show dominance on arbitrary candidate distributions. Errors outside the structural taxonomy, most prominently vocabulary divergence, are flagged by the abstention channel rather than scored (abstention F1 0.870.87); predicate-arity refactoring and alternative decomposition of compound concepts remain undetected, and a complete evaluation would pair SIV with vocabulary- or term-level components. Operator coverage. The ten-operator contrastive inventory is not complete, and no perturbation taxonomy can be. The boundary is instead measured and extensible: on 434434 real translations, exactly one in-scope error class fell outside the inventory (conditional-to-biconditional over-strengthening, scored 1.01.0), and a verified eleventh operator closes it within the existing admission regime (§7, Appendix D). Users applying SIV outside its validated scope should treat high scores on structurally exotic candidates with care; the positive arm still catches any candidate that loses or contradicts reference content, but overstatement detection is only as broad as the admitted contrastive set. Equal probe weighting and human severity judgments. All probes carry equal weight in the F1. This is a deliberate first choice: any severity weighting embeds a downstream-task judgment we did not want to hard-code into a reference-based metric. The F1 already carries an implicit structural weighting, since an error in central content fails the reference-itself probe plus every probe downstream of the damaged node, which is why Experiment 2’s drop magnitudes track severity (0.1690.169 to 0.9750.975); and because probes are labeled, a task-specific weighted SIV is a drop-in variant (weights over probe labels), which we leave to future work. Relatedly, our evidence for correspondence with fine-grained human severity judgments is limited: the expert audit validates the binary half (all §7 statistics are measured against human correctness labels), but real errors were overwhelmingly major (22 in-scope minor errors in 434434 pairs after adjudication), so a graded correlation against expert severity is underpowered on real data. The controlled Experiment-1 calibration remains the graded evidence, anchored at both ends by real-output behavior. Auxiliary axioms and dataset-specific metadata. Probe admission runs Vampire with default axioms together with per-predicate and per-restrictor existence witnesses; for binary relations, asymmetry and symmetry axioms come from a frozen 427427-predicate label table built from FOLIO’s vocabulary (850850 of 877877 observed predicate usages covered). The dependence is measured (Appendix J): the table enters SIV at exactly one code path (swap_binary_args admission); disabling it leaves per-class detection unchanged to three decimals in all six classes, and on MALLS, with zero FOLIO metadata, the parser accepts 96.6%96.6\% of golds and per-class detection is 1.000/0.969/1.0001.000/0.969/1.000. What the table buys is diagnostic naming: without it, arg-swap trace-F1 falls from 0.4820.482 to 0.0000.000 and macro-F1 from 0.6380.638 to 0.5500.550 (still +0.189+0.189 over the score-only baseline). Porting SIV’s score requires no metadata; only the trace’s arg-swap axis needs a domain label table or the §6.4 witness extension. FOLIO reference errors. FOLIO’s expert annotations contain approximately 11%11\% errors (Olausson et al., 2023; Brunello et al., 2026); our real-output audit independently corroborated this rate (16/15016/150 premises, Appendix I), and excluding those premises raises SIV’s AUC to 0.8550.855. On a prior pool, manual correction of the top-30 most-suspect references shifted headline statistics by ±0.02± 0.02 (Appendix F); we have not re-audited the present stratified pool and treat the prior stability as indicative. Pool composition. Pool composition in Experiment 1 concentrates some tiers on a small set of operators (OS: 69%69\% from OS_add_nucleus_conjunct; P: n=25n=25, 72%72\% from P_drop_conjunct). Per-operator AUC (Appendix B) shows the metric ordering is consistent across operators, so the headline statistics are not driven by any single operator. In Experiment 2, the strengthen_quantifier class yields 1515 verified pairs after Vampire filtering; the architectural-payoff finding rests primarily on restrictor_drop (n=231n=231). Diagnostic admissibility ceiling. The diagnostic classifier names a structural failure only when the corresponding contrastive is admitted into −P^-. Under our admissibility regime, flip_quantifier contrastives are admitted on 0.3%0.3\% of outer-quantifier-flip pairs and swap_binary_args on ∼13% 13\% of universal-body swaps. Per-class diagnostic performance is correspondingly uneven (Table 5): restrictor_drop at F1 0.9960.996 and strengthen_quantifier at 0.9330.933, against flip_outer_quantifier at 0.0060.006. The score detects both perturbation types reliably (Experiments 1 and 2); only the diagnostic layer’s per-class naming is affected. Closing these gaps requires extending the witness machinery (§6.4). References Barwise and Cooper (1981) Jon Barwise and Robin Cooper. 1981. Generalized quantifiers and natural language. Linguistics and Philosophy, 4(2):159–219. Brunello et al. (2026) Andrea Brunello, Luca Geatti, Michele Mignani, Angelo Montanari, and Nicola Saccomanno. 2026. Do LLMs really struggle at NL-FOL translation? Revealing their strengths via a novel benchmarking strategy. In Proceedings of the 40th Annual AAAI Conference on Artificial Intelligence (AAAI-26). ArXiv:2511.11816. Cai and Knight (2013) Shu Cai and Kevin Knight. 2013. Smatch: an evaluation metric for semantic feature structures. In Proceedings of the 51st Annual Meeting of the Association for Computational Linguistics (Volume 2: Short Papers), pages 748–752, Sofia, Bulgaria. Association for Computational Linguistics. Funakura et al. (2025) Hayate Funakura, Hyunsoo Kim, and Koji Mineshima. 2025. A theorem-proving-based evaluation of neural semantic parsing. In Proceedings of the 8th BlackboxNLP Workshop: Analyzing and Interpreting Neural Networks for NLP, pages 295–306, Suzhou, China. Association for Computational Linguistics. ArXiv:2510.11225. Han et al. (2024) Simeng Han, Hailey Schoelkopf, Yilun Zhao, Zhenting Qi, Martin Riddell, Wenfei Zhou, James Coady, David Peng, Yujie Qiao, Luke Benson, Lucy Sun, Alexander Wardle-Solano, Hannah Szabó, Ekaterina Zubova, Matthew Burtell, Jonathan Fan, Yixin Liu, Brian Wong, Malcolm Sailor, et al. 2024. FOLIO: Natural language reasoning with first-order logic. In Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 22017–22031. Association for Computational Linguistics. Hosseini et al. (2018) Mohammad Javad Hosseini, Nathanael Chambers, Siva Reddy, Xavier R. Holt, Shay B. Cohen, Mark Johnson, and Mark Steedman. 2018. Learning typed entailment graphs with global soft constraints. Transactions of the Association for Computational Linguistics, 6:703–717. Kovács and Voronkov (2013) Laura Kovács and Andrei Voronkov. 2013. First-order theorem proving and Vampire. In Computer Aided Verification (CAV 2013), volume 8044 of Lecture Notes in Computer Science, pages 1–35, Berlin, Heidelberg. Springer Berlin Heidelberg. Lee et al. (2025) Jinu Lee, Qi Liu, Runzhi Ma, Vincent Han, Ziqi Wang, Heng Ji, and Julia Hockenmaier. 2025. Entailment-preserving first-order logic representations in natural language entailment. In Proceedings of the 63rd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 5729–5742, Vienna, Austria. Association for Computational Linguistics. Liu et al. (2025a) Xiaoyang Liu, Tao Zhu, Zineng Dong, Yuntian Liu, Qingfeng Guo, Zhaoxuan Liu, Yu Chen, and Tao Luo. 2025a. ASSESS: A semantic and structural evaluation framework for statement similarity. Preprint, arXiv:2509.22246. Liu et al. (2025b) Yuntian Liu, Tao Zhu, Xiaoyang Liu, Yu Chen, Zhaoxuan Liu, Qingfeng Guo, Jiashuo Zhang, Kangjie Bao, and Tao Luo. 2025b. Generalized tree edit distance (GTED): A faithful evaluation metric for statement autoformalization. In AI for Math Workshop at ICML 2025. ArXiv:2507.07399. Olausson et al. (2023) Theo Olausson, Alex Gu, Ben Lipkin, Cedegao Zhang, Armando Solar-Lezama, Joshua Tenenbaum, and Roger Levy. 2023. LINC: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. In Proceedings of the 2023 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 5153–5176, Singapore. Association for Computational Linguistics. OpenAI (2025) OpenAI. 2025. Introducing GPT-4.1. https://openai.com/index/gpt-4-1/. Opitz (2023) Juri Opitz. 2023. SMATCH++: Standardized and extended evaluation of semantic graphs. In Findings of the Association for Computational Linguistics: EACL 2023, pages 1595–1607, Dubrovnik, Croatia. Association for Computational Linguistics. Pan et al. (2023) Liangming Pan, Alon Albalak, Xinyi Wang, and William Yang Wang. 2023. Logic-LM: Empowering large language models with symbolic solvers for faithful logical reasoning. In Findings of the Association for Computational Linguistics: EMNLP 2023, pages 3806–3824, Singapore. Association for Computational Linguistics. Papineni et al. (2002) Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu. 2002. BLEU: A method for automatic evaluation of machine translation. In Proceedings of the 40th Annual Meeting of the Association for Computational Linguistics, pages 311–318, Philadelphia, Pennsylvania, USA. Association for Computational Linguistics. Paris and Vencovská (2015) Jeffrey Paris and Alena Vencovská. 2015. Pure Inductive Logic. Perspectives in Logic. Cambridge University Press. Qwen Team (2025) Qwen Team. 2025. Qwen2.5 technical report. ArXiv:2412.15115. Ryu et al. (2025) Hyun Ryu, Gyeongman Kim, Hyemin S. Lee, and Eunho Yang. 2025. Divide and translate: Compositional first-order logic translation and verification for complex logical reasoning. In The Thirteenth International Conference on Learning Representations (ICLR 2025). ArXiv:2410.08047. Thatikonda et al. (2025) Ramya Keerthy Thatikonda, Wray Buntine, and Ehsan Shareghi. 2025. Assessing the sensitivity and alignment of FOL closeness metrics. In Findings of the Association for Computational Linguistics: EMNLP 2025, pages 16775–16785. Association for Computational Linguistics. ArXiv:2501.08613. Thatikonda et al. (2026) Ramya Keerthy Thatikonda, Jiuzhou Han, Wray Buntine, and Ehsan Shareghi. 2026. Improving symbolic translation of language models for logical reasoning. Preprint, arXiv:2601.09446. Wang et al. (2024) Zhongyuan Wang, Richong Zhang, Zhijie Nie, and Jaein Kim. 2024. Tool-assisted agent on SQL inspection and refinement in real-world scenarios. Preprint, arXiv:2408.16991. Wong and Mooney (2007) Yuk Wah Wong and Raymond Mooney. 2007. Learning synchronous grammars for semantic parsing with lambda calculus. In Proceedings of the 45th Annual Meeting of the Association of Computational Linguistics, pages 960–967, Prague, Czech Republic. Association for Computational Linguistics. Yang et al. (2024) Yuan Yang, Siheng Xiong, Ali Payani, Ehsan Shareghi, and Faramarz Fekri. 2024. Harnessing the power of large language models for natural language to first-order logic translation. In Proceedings of the 62nd Annual Meeting of the Association for Computational Linguistics (Volume 1: Long Papers), pages 6942–6959, Bangkok, Thailand. Association for Computational Linguistics. Ye et al. (2023) Xi Ye, Qiaochu Chen, Isil Dillig, and Greg Durrett. 2023. SatLM: Satisfiability-aided language models using declarative prompting. In Advances in Neural Information Processing Systems 36 (NeurIPS 2023). Zhang et al. (2020) Tianyi Zhang, Varsha Kishore, Felix Wu, Kilian Q. Weinberger, and Yoav Artzi. 2020. BERTScore: Evaluating text generation with BERT. In 8th International Conference on Learning Representations (ICLR 2020), Addis Ababa, Ethiopia. OpenReview.net. Zhong et al. (2020) Ruiqi Zhong, Tao Yu, and Dan Klein. 2020. Semantic evaluation for text-to-SQL with distilled test suites. In Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing (EMNLP), pages 396–411. Association for Computational Linguistics. Appendix A Severity Tier Construction The Experiment 1 candidate pool is constructed via a stratified, pre-registered design. The design predates generation and was not revised against observed metric outcomes; the configuration is included in the reproduction package (Appendix L). Tier definitions. The four severity tiers are defined in Table 2 of the main text. Tier labels are determined by Vampire-verified logical relation plus a structural skeleton check, not by LLM self-assessment. The P/OW boundary is operationalized as a structural AST property: walking the candidate and reference ASTs, we compare the top-level quantifier and connective sequence (ignoring predicate names, argument lists, and inner-clause content). A candidate that preserves this sequence is classified P; otherwise OW. Generation. Candidates are generated by applying 1414 typed perturbation operators across the five formula strata S1,…,S5\S_1,…,S_5\. Each operator declares its target tier (OS/P/OW) and an applicability predicate; the design specifies a per-(operator × stratum) cell target. Operators include OS-tier strengthening operators (OS_add_nucleus_conjunct, OS_narrow_consequent, OS_strengthen_predicate, OS_strengthen_quantifier, OS_drop_conjunctive_restrictor), P-tier weakening operators (P_drop_conjunct, P_weaken_predicate, P_drop_disjunctive_restrictor), and OW-tier scaffolding-damage operators (OW_flip_outer_quantifier, OW_de_quantify_to_c0, OW_weaken_to_existential, OW_overrestrict_antecedent, OW_drop_consequent_severely, OW_weaken_predicate_severely). Verification. Each generated candidate is verified by Vampire in both directions (cand⊧ref cand ref and ref⊧cand ref cand) and, where applicable, by the structural skeleton-match check. A candidate is retained iff its verdict matches its declared tier. Verification retention: 547547 generated, 529529 retained (96.7%96.7\%). Cell-target outcomes. Several (operator × stratum) cells have target 88 but 00 retained, because Vampire dropped all generated candidates when the operator’s applicability predicate did not fire on the stratum (e.g., OS_strengthen_predicate on S4S_4 nested-quantifier; P_weaken_predicate on S2S_2 universal-simple). These outcomes are disclosed pool composition. Pre-registration discipline. Three S2S_2-cell operators (OW_weaken_to_existential, OW_overrestrict_antecedent, P_drop_disjunctive_restrictor) were initially excluded by a bookkeeping error; their applicability predicates do fire on ∀-implications with non-atomic consequents. The 5656 affected candidates were correctly generated and Vampire-verified before this was caught, and no scoring had occurred when they were added back. We disclose this because pre-registration discipline depends on noting late changes to the design. The absent stronger-and-skeleton-breaking cell. The design space contains a cell the tier system does not instantiate: perturbations that are strictly stronger and also break the top-level skeleton. The tiers order structural distance for single typed edits, the errors translators actually make, and a strengthening edit that also breaks the top-level skeleton requires compound edits; the cell is correspondingly rare as a single-edit translation error, which is why the pool lacks it. The root-negation boundary probe of §4.2 tests the adjacent extreme (whole-formula complements) directly. Appendix B Per-Operator AUC Decomposition We report per-operator AUC for separating Ref from each operator’s candidate set, per metric. Two operators localize the LE propositional collapse documented in §4: Operator LE AUC SIV AUC OW_flip_outer_quantifier 0.5000.500 1.0001.000 OS_strengthen_quantifier 0.5000.500 1.0001.000 Table 7: LE is at chance on both quantifier-manipulation operators; SIV saturates at 1.0001.000. This reproduces Brunello et al. (2026)’s propositional-collapse prediction operator by operator on the stratified pool. LE’s AUC values on the remaining operators range from 0.660.66 to 1.001.00. The chance behavior is specific to operators that manipulate quantifier scope or type without altering predicate vocabulary: LE’s truth-table representation cannot detect changes that do not register at the propositional level. Appendix C Robustness Checks for Experiment 1 This appendix details the four checks summarized in §4.2. Merging the equal-rank tiers. OS and P share severity rank by design (§4), so one may ask whether the headline η2η^2 depends on splitting tiers the design calls equal. Recomputing η2η^2 with OS and P merged into a single level, giving the statistic zero credit for separating them, yields SIV η2=0.706η^2=0.706, against at most 0.070.07 for every baseline, a roughly 10×10× margin that survives the merge entirely. The score asymmetry between OS and P is itself informative rather than inconsistent: an OS candidate still asserts everything the reference asserts (it errs by adding), while a P candidate fails to assert the reference’s content (it errs by losing), and a recall-bearing F1 prices lost content more heavily. At the per-premise level, SIV produces zero severity-order reversals across all 372372 candidates: it never ranks a more-broken tier above a less-broken one, and where it does not strictly separate, it ties. Operators disjoint from SIV’s inventory. Only 33 of SIV’s 1010 contrastive operators are exercised by Experiment 1’s 1414 pool operators at all; 99–1010 of the 1414 are structurally disjoint from the inventory (conjunct addition, predicate-hierarchy substitution, quantifier elimination, and others on no contrastive axis). Restricting Experiment 1 to the disjoint operators leaves SIV at η2=0.759η^2=0.759 (vs. 0.8020.802 on the full pool) and Cohen’s d=4.37d=4.37 [3.76,5.49][3.76,5.49], against at most 0.160.16 for every baseline, with non-overlapping CIs and AUC =1.00=1.00 on every disjoint severe-tier operator. Experiment 2’s random_substitution class (n=638n=638) is likewise out-of-inventory and detected at 0.9980.998. SIV’s validation was already mostly outside its own taxonomy. Candidate SIV LE LT Sm++ BLEU BS root negation .022.022 .000.000 .000.000 .864.864 .419.419 .858.858 (OW mean) .052.052 .713.713 .000.000 .740.740 .397.397 .822.822 Table 8: Root-negation boundary probe: the direct negation of the reference, scored for all 105105 Experiment-1 premises (Vampire-verified incompatible, 105/105105/105), with the OW-tier means for comparison. Sm++: Smatch++; BS: BERTScore. A root-negation boundary probe. The tiers order structural distance for single typed edits, the errors translators actually make, so whole-formula complements were not a tier; the direct negation of the reference is the natural boundary probe. We score it for every Experiment-1 premise (Table 8). SIV places the negation below its lowest defined tier (0.0220.022; the bootstrap CI’s upper bound, 0.0480.048, is itself below the OW mean of 0.0520.052), so the hierarchy’s endpoints extrapolate in the right direction without having been designed for this case. LE and LT also correctly score the negation at 00: a root negation is exactly what a truth-table representation catches; this row is not evidence against them. The surface and graph metrics do not: Smatch++ scores the reference’s logical complement above every error tier, including over-strengthened but content-preserving translations. Graded-LT construction. The graded LT of §4.2 is the strongest we could build: bidirectional entailment under SIV’s exact prover setup (Vampire, same axioms and timeout), scored 1.0/0.5/0.01.0/0.5/0.0 for equivalent / one-directional / neither, run on both experimental pools. It detects every Experiment-2 perturbation class in 100%100\% of pairs: the prover’s strength is real. But it is a three-valued function of the logical relation, so it scores the mildest error tier (OS) and the most severe, skeleton-broken tier (OW) identically at 0.50.5; on Experiment 2 its only two drop values track relation type rather than severity, assigning flip_outer_quantifier (SIV’s largest drop, 0.9750.975) the same 0.50.5 as restrictor_drop (SIV’s smallest, 0.1690.169); and it produces no trace. Appendix D Contrastive Operator Inventory The contrastive probe set −(φ)P^-( ) is generated by applying ten operators at all valid sites of the reference. Each operator produces either a strictly-stronger contrastive (ψ⊧φψ but φ⊧̸ψ ψ, used to detect under-constraining translations) or an incompatible contrastive (φ∧ψ⊧⊥ ψ , used to detect drift along a specific structural axis). • negate_atom: flips negation on a single atomic predicate. Incompatible. • swap_binary_args: reverses argument order in binary predicates (R(a,b)→R(b,a)R(a,b)→ R(b,a)). Incompatible; admissibility requires asymmetry-axiom certification (§3.3). • flip_quantifier: swaps ∀↔∃∀ ∃ on a single binder. Strictly-stronger when changing ∃ to ∀ inside an implication; incompatible otherwise. Admissibility on outer-quantifier flips is the disclosed coverage limit of §6.4. • drop_restrictor_conjunct: removes a single conjunct from a restrictor. Strictly-stronger. • flip_connective: swaps ∧↔∨ at a single junction. Incompatible. • replace_subformula_with_negation: wraps a subformula in negation. Incompatible. • disjunct_drop: removes a disjunct from a disjunction. Strictly-stronger. • converse: reverses an implication’s direction (α→β↦β→α→β β→α). Incompatible. • scope_swap: permutes adjacent quantifiers of opposite type. Strictly-stronger. • equality_drop: removes an equality literal from a conjunction. Strictly-stronger. Each operator validates its output with a type-soundness check; ill-formed candidates are discarded. The full FOLIO suite contains 1,6781,678 strictly-stronger and 2,2542,254 incompatible generated contrastives across 1,3931,393 premises (mean 2.822.82 per premise). The fraction admitted into −P^- depends on the active axiom set; admissibility rates per class and per operator are reported with the diagnostic experiment (§6). Asymmetry-axiom label table. The frozen 427427-predicate asymmetry/symmetry/unknown label table used to admit swap_binary_args contrastives is released alongside the code. The table covers 850850 of 877877 predicate usages observed in the experimental pools; the remaining 2727 usages map to the 2121 unknown-labeled predicates and contribute no axiom. D.1 Provenance, selection principles, and extensibility Operator Axis Provenance negate_atom polarity (atom) priora,b flip_quantifier quantifier type priora,b flip_connective connective priora,b replace_subf._w_neg. polarity (subf.) adaptedc swap_binary_args argument order new drop_restrictor_conj. restrictor newd disjunct_drop disjunction new converse implication dir. new scope_swap quantifier scope new equality_drop equality new implic._to_bicond. implication str. newe Table 9: Contrastive-operator provenance. aBrunello et al. (2026); bThatikonda et al. (2025); cliteral-level negation generalized to subformulas; dderived from the Barwise–Cooper decomposition (Barwise and Cooper, 1981), not from an error taxonomy; epost-audit extension operator, verified but not used in the §4–§7 experiments (see below). Table 9 records, for each operator, the structural axis it targets and whether it comes directly from a prior error inventory, is adapted from one, or is newly introduced here. Selection principle. The inventory was selected for systematic coverage of FOL’s structural axes (quantifier type, scope, polarity, argument order, connective, restrictor, equality, implication direction), one operator per axis and two where granularities differ. The operators were not curated from observed errors: none was added or shaped in response to errors seen during development. Each operator is only a generator; its declared relation to the reference must be certified by Vampire before admission (§3.3), so the inventory is a closed, axis-motivated, prover-filtered set. Measured boundary and a verified extension. The real-output audit (§7) located the inventory’s boundary concretely: of 1515 in-scope structural errors, 11 was a strict over-strengthening no current operator generates, a conditional rendered as a biconditional (∀x.(R(x)→N(x))∀ x.(R(x)→ N(x)) translated with ↔ ), which saturates the positive arm, fires no contrastive, and receives SIV 1.01.0. The fix stays inside the architecture, and we verified it: an eleventh operator, implication_to_biconditional, is admitted as strictly-stronger by Vampire under the existing witness regime, fires on the audited candidate (SIV falls from 1.001.00 to 0.8890.889 with the trace naming the axis), and does not fire on the reference or on faithful conditional translations. We report it as a verified extension rather than folding it into the experimental inventory, so that every number in §4–§7 reflects the pre-registered ten-operator set. The taxonomy is not complete; its boundary is measurable and extensible. Appendix E Predicate Alignment Procedure Candidate translations may use predicate vocabulary that differs from the reference (e.g., HasWheels vs. HasWheel). We perform deterministic alignment via a similarity threshold of 0.60.6, applied to embedding-based symbol matching with a layered fallback over exact match, lemma match, and substring match. Aligned candidate predicates are rewritten to the reference vocabulary before scoring; unaligned predicates are adjudicated against the candidate’s original symbol. Sensitivity. On the operator-driven Experiment 1 pool used for the headline statistics, alignment is effectively the identity map because candidates inherit canonical predicate names from the SIV inventory by construction. The threshold of 0.60.6 was set during initial development and was not tuned against evaluation outcomes. Behavior on real translator outputs. On the §7 pool, alignment behavior splits cleanly by translator configuration. With the reference signature supplied, 100%100\% of candidate predicates align exactly. Free-vocabulary translators diverge heavily (7171–78%78\% of pairs contain divergent vocabulary), and the layered alignment resolves 5959–65%65\% of divergent symbols, leaving a remainder that is genuinely out of vocabulary. Out-of-vocabulary abstention. When alignment leaves reference-critical predicates unresolved, SIV emits an out-of-scope abstention flag for the pair instead of a confident score. On the §7 pool the flag identifies vocabulary-divergent pairs at F1 0.870.87 (precision 0.930.93). This is deliberate: on divergent-but-correct pairs SIV’s raw score is low (0.290.29), and the flag marks the score as ungrounded rather than pretending to adjudicate vocabulary the prover cannot align. Appendix F Reference Correction Sensitivity We surface candidate reference errors via a weighted score combining four signals: SIV-soft recall <1.0<1.0 on the reference (weight 100×100×), SIV-strict recall <1.0<1.0 on the reference (weight 10×10×), predicate-Jaccard between SIV canonical and FOLIO gold <0.8<0.8 (weight 5×5×), and SIV-soft F1 <1.0<1.0 on the reference (weight 1×1×). On the prior submission’s pool of 368368 premises, 6969 triggered at least one signal; the top 3030 by weighted score were inspected manually. Five confirmed transcription errors (entity mismatches between NL and gold formula, missing negations, reversed implications) were corrected and one premise with a typo in the source NL was excluded. Recomputing the prior submission’s headline statistic on the corrected subset and on the full corpus with corrections applied yielded a stability of ±0.02± 0.02. We have not re-run this correction pass on the new stratified Experiment 1 pool; the prior result is indicative of the FOLIO reference-error magnitude but not a direct sensitivity check for the new design. The §7 audit independently corroborates the magnitude: 1616 of 150150 stratified premises (∼11% 11\%) carried erroneous gold formulas, matching the rate reported by Olausson et al. (2023), and excluding them raises SIV’s real-output AUC from 0.8410.841 to 0.8550.855. Appendix G Diagnostic Classifier Rules Reference stratum n Recall S_5 ground-atom relations 127127 0.8820.882 S8S_8 other 99 0.6670.667 S6S_6 negation 1616 0.2500.250 S3S_3 universal-multi-restrictor 176176 0.1250.125 S2S_2 universal-simple 4949 0.0820.082 S4S_4 nested-quantifier 8686 0.0810.081 S7S_7 existential 3131 0.0650.065 Table 10: arg_swap recovery by reference stratum (discussed in §6.3). Why universal bodies defeat the asymmetry route (§6.3). Ground-atom occurrences trigger the axiom directly: the reference asserts R(a,b)R(a,b), the swap asserts R(b,a)R(b,a), asymmetry forbids the conjunction, and Vampire admits the swap as incompatible. In a universally-quantified body, neither formula asserts a specific R-fact: both are conditional and vacuously satisfied in any model where the antecedent is empty, so asymmetry never fires and the classifier loses its signal. This is a limit of asymmetry axioms under standard FOL semantics, not a Vampire timeout or a missing predicate-label entry. The diagnostic classifier (§6) maps the labeled trace (failed_positives,fired_contrastives)(failed\_positives,fired\_contrastives) to a perturbation class via the following rules, applied in order; first match wins. 1. drop_restrictor_conjunct fired AND failed_positives empty → restrictor_drop. 2. flip_quantifier fired AND failed_positives empty → strengthen_quantifier. 3. flip_quantifier fired AND failed_positives non-empty → flip_outer_quantifier. 4. swap_binary_args fired → arg_swap. 5. negate_atom OR replace_subformula_with_negation fired → negation_drop. 6. failed_positives non-empty AND no contrastives fired → random_substitution. 7. Otherwise → unrecognized. The rule table implements a pre-registered prediction pattern per class (declared in advance of any scoring): each class names its expected (failed_positives, fired_contrastives) signature, and the classifier checks for that signature. There are no learned parameters, fitted thresholds, or per-class hyperparameters. Appendix H Detailed Probe Statistics The full FOLIO evaluation suite contains 1,3931,393 of 1,4711,471 premises with at least one well-formed probe (94.7%94.7\%); 2,3402,340 positive probes (mean 1.681.68 per premise); and 3,9323,932 generated contrastive probes (mean 2.822.82 per premise; 2,2542,254 incompatible, 1,6781,678 strictly-stronger). Total: 6,2726,272 structural probes generated. The admitted-into-−P^- count depends on the active axiom set (§3.3, §6). Full suite construction includes additional audit calls reaching 7,9347,934 Vampire invocations, with 00 hard failures across the audit. Of the 156156 references containing a disjunction, none contributes a positive probe by disjunct removal; disjunctions enter +P^+ only carried whole (§3.2). Appendix I Real-Translator Audit: Protocol and Detailed Results Translator configurations. The three configurations of §7 span the quality range documented by Brunello et al. (2026): GPT-4.1 with free predicate vocabulary, GPT-4.1 with the reference predicate signature supplied in the prompt (the high-accuracy regime of that study), and Qwen2.5-7B with free vocabulary. Each translates the same 150150 stratified FOLIO premises (seed 4242). Of 450450 outputs, 434434 parse; the malformed counts are 33, 00, and 1313 respectively. Labeling protocol. An independent LLM screening judge, drawn from a different model family than all three translators, first flags candidate errors. An expert annotator then labels 121121 pairs directly on blind sheets (translator identity and metric scores hidden), including every pair the judge flagged as incorrect, so the entire “incorrect” class in the analysis is human-verified. A second human annotator double-annotated a 5050-pair overlap: human–human agreement on the binary correct/error boundary is κ=0.68κ=0.68 (84%84\% raw agreement), identical to expert–judge agreement (κ=0.68κ=0.68, 87%87\% raw). Agreement on the major/minor severity boundary is lower (κ=0.57κ=0.57), so every pair with a disputed label was jointly adjudicated before analysis. Error composition. After adjudication, the audit contains 2929 confirmed errors: 1414 vocabulary-divergence errors, which SIV routes to the abstention flag (Appendix E), and 1515 in-scope structural errors, of which 22 are minor and 11 is the conditional-to-biconditional over-strengthening outside the ten-operator inventory (Appendix D.1). The scarcity of in-scope minor errors (22 in 434434 pairs) is why a graded correlation against expert severity is underpowered on real data (Limitations). Compatible-vocabulary stratum. The AUC comparison of Table 6 is computed on the stratum where all metrics are defined without vocabulary confounds: n=185n=185 pairs with compatible vocabulary, of which 1010 are expert-labeled incorrect. With 1010 positives, pairwise AUC differences against Smatch++ and LE are not significant; SIV’s mean-score separation on expert-major vs. expert-correct pairs (0.200.20 vs. 0.800.80) and its abstention flag are the capabilities the AUC comparison does not capture. Trace spot-check. We spot-checked the diagnostic trace on 1010 flagged translations. Two proved correct on adjudication; one of these was a confirmed FOLIO gold error, on which SIV had scored 1.001.00 and stayed silent, consistent with that label. Of the 88 confirmed errors, the trace named the exact structural axis in 11, localized the broken content through failed positive probes in 66, and was silent in 11, the biconditional coverage gap now closed by the verified eleventh operator. The axis-naming case is instructive: for the FOLIO premise “In Love City, everyone is scared of animals, or loves animals, or both,” GPT-4.1 dropped the antecedent restricting the rule to Love City, turning it into a claim about everyone, and the trace fired a single contrastive, drop_restrictor_conjunct, naming exactly that error. Released artifacts. The 434434 audited (premise, translation, label) triples, the blind annotation sheets, and the per-pair metric scores are released with the code. Appendix J Metadata Ablation and MALLS Portability We tested the dependence on FOLIO-specific metadata from two directions: in-domain, by disabling the 427427-predicate table on our own pools and measuring what breaks, and cross-domain, by running SIV on MALLS (Yang et al., 2024), where the table barely applies. The two agree. In-domain ablation (FOLIO, table disabled). The 427427-predicate table enters SIV at exactly one code path: swap_binary_args admission. Removing it deletes 336336 of 2,5532,553 admitted contrastives, all on that one operator, and per-class detection is unchanged to three decimals in all six §5 classes (arg_swap 0.9980.998 with or without the table; SIV-recall exactly invariant across all 2,5052,505 scored candidates). What the table buys is diagnostic naming: arg-swap trace-F1 falls from 0.4820.482 to 0.0000.000 (misrouting to the catch-all class), and macro-F1 from 0.6380.638 to 0.5500.550, though the trace still beats the score-only baseline by +0.189+0.189 with zero metadata. Cross-domain probe (MALLS, zero FOLIO metadata). With no domain adaptation of any kind, the parser accepts 96.6%96.6\% of MALLS gold formulas. Probe density is higher than on FOLIO (5.655.65 vs. 2.822.82 admitted contrastives per premise), so the mechanism does not thin out without metadata. Per-class detection on the three ported classes is 1.0001.000 / 0.9690.969 / 1.0001.000 (negation-drop / restrictor-drop / outer-quantifier-flip), with restrictor-drop reproducing the architectural-payoff finding of §5 on a new domain: recall saturates and the contrastive arm alone carries detection. Enabling the full FOLIO table on MALLS changes admission by 22 probes out of 565565; it covers 8%8\% of MALLS’s binary predicates and is genuinely FOLIO-specific, but nothing that carries detection depends on it. Summary. Porting SIV’s score requires no metadata at all; only the trace’s arg-swap axis needs a domain label table or the witness extension of §6.4. Appendix K Runtime Profile Decomposition. Profiling on the §5 pool (14-core workstation): probe construction plus Vampire admission is paid once per reference (∼0.35 0.35 s, ∼24 24 prover calls) and reused across every candidate and every system evaluated. The marginal cost of scoring one additional candidate is 6767 ms single-core and 6.86.8 ms parallel (∼5.7 5.7 prover calls, median 1212 ms, zero timeouts in 14,29314,293 calls). Evaluating N systems on a benchmark costs build-once plus N×N× seconds, which is how the released pipeline already works: suites are prebuilt and loaded. Cheaper variants, and a pitfall. For iterative loops we profiled two cost reducers. Reducing the per-call timeout is inert: no call approaches it. A naive one-probe-per-axis cap buys 1.8×1.8× but silently breaks the restrictor_drop detection class (0.996→0.0170.996→ 0.017), because it discards all but one probe of each restrictor group; a corrected cap that keeps restrictor groups intact restores detection above 0.990.99 at about 1.6×1.6×. Appendix L Reproducibility Theorem prover. All probe adjudication uses Vampire v5.0.15.0.1 with a per-call timeout of 55 seconds. The release script auto-downloads the pinned binary; CI verifies binary checksum. Timeouts are treated as “not entailed” for both positive and contrastive probes in the strict variant, and symmetrically in the soft variant; we report the soft variant in the main text (§3). Reproduction snapshot. All experiments are reproduced from the single code release linked in §1. Each is a one-command invocation against its design artifact: configs/severity_correlation_v1.yaml for Experiment 1, run_perturbation_detection.py for Experiment 2, run_diagnostic_trace.py for Experiment 3, and run_real_translator_audit.py for Experiment 4, alongside orchestrators for the robustness checks of §4.2 and the ablations of Appendices J and K. The 427-predicate asymmetry/symmetry label table used by the diagnostic experiment is shipped with the code as siv/asymmetry_axioms.py; the 434434 expert-audited real-translation pairs ship under data/audit/. Per-experiment artifacts (per-tier means, drop magnitudes, classifier predictions, contrastive-firing matrix) are regenerated by re-running the orchestrators; reference outputs are included under reports/experiments/ for direct comparison. Random seeds. All deterministic experiments are seed-independent given fixed Vampire output. Pool construction uses seed 4242 for within-cell ordering and for any tie-breaking; bootstrap CIs use 1,0001,000 resamples with seed 4242. The diagnostic classifier (§6) is rule-based and has no random component; the score-only baseline uses 5-fold stratified cross-validation with seed 4242. Alignment threshold. The predicate-alignment threshold (Appendix E) is fixed at 0.60.6 across all experiments and was not tuned against evaluation outcomes.