1 Introduction↩︎

Consider two questions about the same theorem: “Is it true that \(\sqrt{x} \geq 0\) for every real number \(x\)?” and “For any real \(x\), is \(0 \leq \sqrt{x}\)?” These statements are logically equivalent (under Lean4 real analysis conventions). Yet Claude Sonnet answers the first correctly and the second incorrectly across 16.7% of comparison-order paraphrases (F6). GPT-4o fails this class of transformation at 0.0%. Reverse the family: ask both models to recognize a definition by expansion (F7), and the ranking reverses: GPT-4o fails at 10.0% while Claude fails at 6–8%. The same pair of frontier models, the same theorems, opposite weaknesses. Model rankings reverse across paraphrase families. This is the central finding of FormInv.

Why does this matter? When a practitioner asks “Is model X good at mathematical reasoning?” and answers using benchmark accuracy alone, they implicitly assume the answer is independent of how the question is phrased. That assumption is wrong. Across 9 frontier models, we find that accuracy tells only half the story: Claude Haiku 4.5 achieves 86% accuracy yet has SCR = 50%: half its theorems are answered inconsistently across semantically equivalent restatements. DeepSeek V3, at 96.4% accuracy, achieves 82% SCR. The 10-point accuracy gap conceals a 32-point SCR gap, the critical property that separates surface-pattern recognition from genuine mathematical understanding.

This failure (formulation sensitivity despite conceptual equivalence) is what psychometrics calls Differential Item Functioning [2], formalized via Doob’s \(L^2\) conditional expectation theorem (1953) [3], and operationalized by measurement invariance theory [4]. To our knowledge, FormInv is the first protocol applying this measurement tradition to formal mathematical reasoning with Lean4-verified theorems and DIF-grounded invariance metrics.

The gap is substantial. Table 1 surveys eight benchmarks and how (if at all) they verify paraphrase semantic equivalence: none applies logical-equivalence checking or cross-model unanimity.

Applied to our own dataset, FormInv’s cross-model unanimity found that 47% of the 15 audited F5 paraphrases were semantically incorrect: errors invisible to single-model evaluation but exposed by unanimity. The same generation regime (LLM + “maintain the answer” instruction + human NL fluency check) that produced these errors in FormInv v1 is used verbatim in MathCheck and GSM-Plus (Table 1). It costs approximately $1 per model per evaluation run and applies to any formally-specified benchmark.

1.0.0.1 Contributions.

1. Invariance framework. SCR and per-theorem Cochran’s Q formalize semantic invariance; IG = \(\sqrt{p(1-p)}\) is a supplementary statistic (Remark [rem:ig95degeneracy]). We prove Propositions 1–2 (error bound; ranking reversal condition) and classify 8 paraphrase families into T1 (formally certifiable), T2 (conditionally valid), and T3 (heuristic) tiers (Table 2).

2. FormInv benchmark. 760 items spanning 103 Lean4-verified Mathlib4 theorems across 8 paraphrase families; 9-model evaluation; 811 items from 100 harder ntp-mathlib theorems. Paraphrase equivalence established by CAS (T1), templates (T2), and domain-expert review (T3).

3. FormInvSelector. An algorithm that uses the per-family SCR profile to recommend the model with lowest expected failure rate. forminv selector --families unpack order runs in 0.1s.

4. Paraphrase quality audit. Cross-model unanimity (\(\geq 6/9\) models fail a paraphrase while passing the canonical) automatically flags semantically-incorrect paraphrases. Applied to FormInv v1: found 11 errors in GPT-4o-generated items (biconditional overreach, passive-voice inversion, type-context stripping).

2 Related Work↩︎

2.0.0.1 Mathematical reasoning benchmarks.

MATH [6] and GSM8K [5] measure final-answer accuracy. ChaosBench-Logic [12] introduces family-level evaluation with formal ontology. MathBench [7] covers multiple mathematical domains. FormalMATH [13] benchmarks 5,560 Lean4-verified problems; top models achieve only 16.46%. All evaluate accuracy on canonical formulations; none test formulation invariance.

2.0.0.2 Regime-dependent evaluation.

The idea that rankings depend on a hidden evaluation variable has precedent. [14] show that Bayesian optimization algorithm rankings reverse sign under different budget-to-candidate-pool ratios (B/|A|): Greedy ranks first at \(B=50\) and last at \(B=100\) on the same benchmark; 98% of BO papers never vary this as a controlled axis. FormInv documents the same phenomenon in LLM evaluation: model rankings reverse across paraphrase families (Proposition 3) and across difficulty regimes (§7), with no benchmark currently controlling for either axis. In formal theorem proving, [15] show that performance drops \(\sim\)​26% when switching between Mathlib-standard and Tao’s-Analysis-I formulations of the same theorem: direct empirical evidence of the IG phenomenon in Lean4. [16] provide cross-domain validation: across eight semantic-preserving transforms, model scale does not predict semantic robustness, a finding consistent with FormInv’s ranking-reversal results.

2.0.0.3 Benchmark label error auditing.

[17] found \(\geq 3.3\%\) label errors in 10 major benchmarks via model confidence disagreement; [18] extend this with LLM ensembles (6–21% errors in NLP benchmarks). [19] show that models with similar accuracy disagree on 16–66% of items (Benchmark Illusion) — the problem FormInv solves. [20] use cross-model disagreement as a deployment-time signal; FormInv applies it at construction time to detect logical-scope errors invisible to embedding similarity. The closest deployed analog is QIMMA [21], an Arabic LLM leaderboard that filters benchmark items using two-LLM consensus — framed as a novel contribution in 2026, confirming that systematic cross-model quality gating is not yet standard practice.

2.0.0.4 Robustness and invariance in NLP.

CheckList [22] introduces behavioral testing via invariance (INV) tests. PromptBench [11] tests robustness to adversarial prompt perturbations. Prompt format sensitivity causes substantial ranking reversals across frontier models [23], [24]. These work on perturbed prompts; FormInv targets verified semantic equivalence classes with a formal invariance metric.

2.0.0.5 Paraphrase sensitivity in mathematical reasoning.

[10] introduce the Variance of Variations (VOV) scalar metric (NAACL 2024): paraphrasing can shift a problem’s solve rate from 5% to 100%. VOV is the closest prior metric to FormInv’s IG: it measures accuracy variance across paraphrase variants of the same problem. FormInv differs in three ways: (1) formal equivalence ground truth from Lean4-verified Mathlib4 theorems (VOV has no equivalence verification); (2) 8 linguistically-motivated paraphrase families with distinct failure modes (VOV uses a single variation type); and (3) connection to generalizability theory and DIF (VOV has no measurement-theoretic grounding).

2.0.0.6 CheckList extensions to math reasoning.

[1] (MathCheck [1]) extend behavioral testing to math reasoning, organizing problems into task families with robustness variants and evaluating 26+ LLMs. FormInv builds beyond MathCheck in three ways: (1) ground truth established by Lean4-verified canonical theorems (the paraphrases themselves are verified by CAS + expert review, not by Lean4), rather than approximate rewrites with implicit ground truth; (2) the formal Invariance Gap metric grounded in Doob’s conditional expectation and DIF theory, rather than accuracy-change heuristics; (3) a formal theorem substrate (Mathlib4) rather than arithmetic word problems.

2.0.0.7 Paraphrase-based contamination detection.

ConStat [25] and CoDeC [26] detect contamination via paraphrase performance drops. PutnamGAP [9] tests equivalent Putnam problem transformations. [27] (Moore & Shah 2025) measure robustness specifically in Lean4 formalization; FormInv generalizes this to arbitrary natural-language mathematical reasoning with DIF-grounded metrics and a formal invariance protocol.

2.0.0.8 Measurement theory foundations.

Generalizability theory [28] decomposes score variance into facets; IG\(^2\) is the paraphrase-facet variance. Parallel-form reliability [29] and measurement invariance [4] provide the classical context for SCR. DIF [2] detects items that function differently across groups; FormInv adapts the intuition to paraphrase families for a fixed model. We are the first to apply this framework to NL mathematical reasoning with DIF-grounded metrics and a certified family taxonomy (cf.Moore & Shah [27] who measure Lean4 formalization robustness, a different task).

3 The Invariance Gap↩︎

3.1 Mathematical Foundation↩︎

Let \(f: \mathcal{X} \to \{0,1\}\) be an LLM’s binary answer function on problem statements. Let \(\sim\) denote semantic equivalence between mathematical formulations: \(x_1 \sim x_2\) if \(x_1\) and \(x_2\) are logically equivalent statements with the same ground truth. The equivalence class of a statement \(x\) is \([x]_{\sim} = \{x' \in \mathcal{X} : x' \sim x\}\).

The equality states that \(\mathbb{E}[f \mid [x]_{\sim}]\) (the class-conditional mean, \(p = \Pr[f(x')=1 : x' \sim x]\)) is the unique \(L^2\)-optimal constant approximation to \(f\) on \([x]_{\sim}\) (a consequence of the fact that the mean minimizes mean squared error [3]. \(\mathrm{IG}(f, [x]_{\sim}) = 0\) if and only if \(f\) is constant on \([x]_{\sim}\), i.e.the model’s answer does not depend on which representative of the equivalence class is presented.

Generalizability theory connection. IG has a natural home in generalizability theory [28]: \(\mathrm{IG}^2\) is the paraphrase-facet variance component in a person \(\times\) item design where “persons” are models and “paraphrase” is a random facet. The formulation is independently motivated: [30] derive the same \(\sigma(\text{accuracy within paraphrase class})\) metric (XParaCon) for general QA robustness. FormInv extends this to Lean4-verified formal equivalence classes with DIF-theoretic grounding. The SCR (Semantic Consistency Rate) is the proportion of theorems for which the model answers correctly across all paraphrase forms, operationally equivalent to the parallel-form agreement coefficient from classical test theory [29]. Note: \(\mathrm{SCR} \subseteq \{\mathrm{IG}=0\}\). A theorem with \(\mathrm{IG}=0\) has a constant model response (possibly consistently wrong); SCR counts only the subset with constant-correct responses. Since all FormInv theorems have ground truth TRUE, a constant-FALSE response also yields \(\mathrm{IG}=0\) but does not contribute to SCR. This framing is more appropriate than classical DIF (which conditions on latent ability across demographic groups) because FormInv holds the population fixed (one model at \(T=0\)) and varies the item, the classical parallel-form reliability setting [29].

IG degeneracy and SCR primacy. Since \(\mathrm{IG}_t = \sqrt{p_t(1-p_t)}\) is a deterministic function of accuracy \(p_t\) (Proposition 1), any cross-model correlation between Mean-IG and accuracy is algebraically inevitable, not empirical. SCR is not degenerate in this sense: \(\mathrm{SCR} \leq \bar{p}\) (Jensen), with equality only when \(p_t \in \{0,1\}\) for all \(t\), and two models at the same \(\bar{p}\) can have SCR from \(0\) to \(\bar{p}\). We therefore treat SCR and per-theorem Cochran’s Q as primary measures; Mean-IG is supplementary.

Aggregate Mean-IG vs.global Doob residual. We report \(\mathrm{Mean\text{-}IG} = \frac{1}{|\mathcal{T}|}\sum_{t \in \mathcal{T}} \mathrm{IG}(f, [t]_{\sim})\), the arithmetic mean of per-theorem IGs. The corresponding global Doob residual over the full evaluation space is \(\mathrm{RMS\text{-}IG} = \sqrt{\frac{1}{|\mathcal{T}|}\sum_{t}\mathrm{IG}(f,[t]_{\sim})^2} \geq \mathrm{Mean\text{-}IG}\) (Jensen). Mean-IG is the more interpretable statistic: it is the expected paraphrase standard deviation for a randomly chosen theorem.

Statistical test. For \(k = 2\) paraphrases, testing \(H_0: \mathrm{IG}= 0\) uses McNemar’s test [31], with statistic \(\chi^2 = (b-c)^2/(b+c)\) where \(b,c\) count discordant pairs. For the general case of \(k > 2\) paraphrase families (as in FormInv where \(k = 7\)–\(8\)), the correct generalization is Cochran’s Q test [32]: a distribution-free test of marginal homogeneity across \(k\) paired binary observations, reducing to McNemar when \(k = 2\). Testing at the per-theorem level with Bonferroni correction for 103 theorems sets the threshold at \(\alpha/103\).

3.2 Formal Properties of the Invariance Gap↩︎

We derive two formal results clarifying what IG measures globally and how family-level scores relate across models.

3.2.0.1 Interpretation.

RMS-IG\(^2\) is a lower bound on the expected paraphrase error rate: the squared Invariance Gap participates directly in the error decomposition. Reducing IG is necessary but not sufficient for reducing paraphrase error (a model with IG \(= 0\) may still fail consistently if \(p_t \ll 1\), i.e.it is consistently wrong, captured by SCR \(= 0\), not IG).

3.2.0.2 Empirical calibration.

All per-family accuracies satisfy \(\bar{p} > 0.77 > \tfrac{1}{2}\). GPT-4o/Claude reversal on \((F_6,F_7)\): \(\bar{p}_6^{(\text{GPT-4o})}=1.00 > \bar{p}_6^{(\text{Claude})}=0.833\), \(\bar{p}_7^{(\text{GPT-4o})}=0.90 < \bar{p}_7^{(\text{Claude})}=0.94\) (sign product \(< 0\)); 16.7 pp reversal on \(F_6\), 4.0 pp on \(F_7\).

3.3 The 8-Family Paraphrase Taxonomy↩︎

Analogous to how ChaosBench-Logic’s [12] 27-predicate ontology defines the evaluation space, FormInv’s 8-family taxonomy defines the space of formulation-equivalent transformations:

3.4 Aggregate Metrics↩︎

Beyond per-theorem IG, we report: \[\begin{align} \text{Mean-IG} &= \frac{1}{|\mathcal{T}|} \sum_{t \in \mathcal{T}} \mathrm{IG}(f, [t]_{\sim}) \\ \mathrm{SCR}&= \frac{|\{t \in \mathcal{T} : f(x')=1\;\forall x' \in [t]_{\sim}\}|}{|\mathcal{T}|} \\ \text{Hi-IG\%} &= \frac{|\{t \in \mathcal{T} : \mathrm{IG}(f, [t]_{\sim}) > 0.10\}|}{|\mathcal{T}|} \end{align}\]

4 FormInv Benchmark↩︎

4.1 Theorem Substrate↩︎

Following the same principle as ChaosBench-Logic [12], which was built using Gilpin’s dysts dynamical systems library [33] as its formal substrate, we build FormInv on a curated formal mathematics substrate from two sources:

Curated Mathlib4 theorems. We manually curated 103 theorems from Mathlib4 [34], [35] spanning 7 mathematical domains (Table 3), selected to include diverse predicate structures and sufficient complexity for F7/F8 definitional transformations. The 103 canonical theorem statements are Lean4-verified Mathlib4 declarations. The 657 generated paraphrases are not Lean4-verified; equivalence is established by CAS (SymPy) for algebraic families, template construction for surface families, and domain-expert review for F7–F8 (see §4 for full protocol).

Track B pilot. On 100 harder ntp-mathlib theorems (811 items), the capability-invariance correlation weakens to \(r = -0.415\) (\(p = 0.27\), not significant), confirming the correlation is difficulty-regime-dependent. F5 connective-variation failures rise to \(\sim\)​32% and all 8 families cluster at 28–35%, showing the F5 specificity effect dissolves at high difficulty. The two reasoning models (DeepSeek R1, o4-mini) become the most invariant at high difficulty, consistent with CoT reducing surface sensitivity when theorems demand deliberation. Full findings A–D in Appendix 19.

4.2 Paraphrase Generation and Verification↩︎

For each theorem \(t\), we generate one paraphrase per applicable family using GPT-4o with a structured prompt (Appendix 9). Paraphrases are cached and verified by the following protocol:

1. F1–F3 (surface): CAS verification where applicable (SymPy) + manual audit on 20% sample

2. F4–F6 (semantic): CAS verification for algebraic families; template guarantee for others

3. F7–F8 (definitional): Human verification (domain expert) on 100% of items

This verification protocol adapts ChaosBench-Logic’s CARE adjudication pipeline [12]: pre-registered protocol, LLM dual review, and human sign-off before repair decisions. Final dataset: 760 items (103 theorems \(\times\) avg. 7.4 applicable families).

4.3 Dataset Properties↩︎

The dataset satisfies key quality gates: (1) All paraphrases have verified ground truth (TRUE for valid Mathlib theorems); (2) Equivalence is domain-expert confirmed for F7/F8; (3) CAS-verifiable items are independently reproducible; (4) SHA256 hash ensures reproducibility: e668f98a...79a1656 (full hash in dataset card).

5 Experiments↩︎

5.1 Setup↩︎

Models. We evaluate 9 models spanning 5 providers and 3 capability tiers: Frontier flagship: GPT-4o, Gemini 2.5 Flash, Claude Sonnet 4.6, DeepSeek V3; Efficient: GPT-4o-mini, Claude Haiku 4.5; Reasoning (CoT): o4-mini (OpenAI), DeepSeek R1 (deepseek-reasoner); Open-source: Llama 3.3 70B (via OpenRouter). All evaluated at temperature=0 or equivalent; reasoning models use their default inference modes.

Dataset. Primary: 366-item FormInv v1 (50 theorems, 9 models). Extended: 103-theorem evaluation (760 items, 9 models, all families); Track B: 100 ntp-mathlib theorems (811 items, 9 models), harder difficulty. Total: 203 theorems evaluated across all 9 models.

Caveats. Gemini 2.5 Flash coverage is 96% (15 items timed out at 2048 output tokens). DeepSeek R1 responses include a reasoning trace; we parse the final TRUE/FALSE verdict, not intermediate steps. Maximum output tokens: 4096 for reasoning models, 20 for others.

Protocol. Zero-shot; system prompt: “You are evaluating mathematical statements. Answer strictly based on mathematical correctness. Return exactly TRUE or FALSE.” Response caching with SHA256 keys ensures reproducibility across runs.

Baseline. Per-theorem within-canonical variance (same canonical prompt, temperature=0) is \(\approx 0\) for all models, confirming that all observed IG is due to paraphrase sensitivity, not API stochasticity.

5.2 Main Results↩︎

N=103 stability (9 models): Rankings are stable at 103 theorems (full 9-model evaluation; Appendix 10). DeepSeek Chat leads: SCR = 83.5% (\(\uparrow\)​1.5pp). Gemini 2.5 Flash: SCR = 82.5% (\(\uparrow\)​2.5pp; coverage 96.4%). GPT-4o: SCR = 79.6% (\(\downarrow\)​2.4pp) — GPT-4o is less invariant on harder theorems. Claude Haiku: SCR = 54.4% (\(\uparrow\)​4.4pp), gap narrows slightly to 29pp vs.32pp at N=50. All deltas are within \(\pm\)

5pp; no model degrades severely.

5.2.0.1 Finding 1: The capability-invariance correlation: what accuracy hides.

The most striking result in Table 4 is not any individual model’s score. It is the range. Claude Haiku 4.5, a deployed commercial model in the same family as Claude Sonnet, achieves SCR = 50%: half its theorems are answered inconsistently across semantically equivalent restatements. DeepSeek V3, at 96.4% accuracy, achieves 82% SCR. A 10-point accuracy gap translates to a 32-point invariance gap.

A practitioner who evaluates Claude Haiku on a standard benchmark and observes 86% accuracy would conclude the model is adequate for mathematical reasoning tasks. FormInv reveals a different picture: on 50% of theorems the model “knows,” the correct answer changes depending on how the question is phrased. This is not a small-model quirk, it is a structural failure of semantic representation that accuracy metrics are constitutionally blind to.

Across all 9 models, the Pearson correlation between aggregate accuracy and mean IG is \(r = -0.965\) (Pearson); Spearman \(\rho = -0.883\), \(p = 0.0016\): more accurate models are more semantically invariant. Removing Claude Haiku as the highest-leverage point yields \(r = -0.906\), still significant (\(p < 0.05\), \(n = 8\)), confirming the relationship holds across the full accuracy range (Proposition 2 bounds this relationship formally). The 22% of theorem-model pairs with \(\mathrm{IG} > 0.10\) represent theorems where models fail on roughly half the paraphrases, a systematic blind spot that no accuracy-only evaluation can detect.

5.2.0.2 Finding 2: Models exhibit sharply complementary failure patterns.

Across the 50-theorem shared evaluation for four 100%-coverage chat models (Claude Sonnet, GPT-4o, GPT-4o-mini, DeepSeek V3), we observe 86 pairwise cross-model disagreements: items where one model answers correctly and another incorrectly on the same paraphrase. The complementarity is structural, not incidental: F6 (comparison order): Claude Sonnet 16.7%, GPT-4o 0.0% — a 16-point gap on the same transformation. F7/F8 (definitional unpack): GPT-4o 10.0%, Claude 6–8%. F5 (connective variation): all models fail equally (22.2%) — no comparative advantage. This complementarity implies benchmark accuracy is systematically optimistic per family, and an ensemble would show near-zero IG on items where individual models fail.

5.2.0.3 Finding 3: The quality audit separates benchmark errors from model errors.

The F5 apparent failure rate (22.2%) is inflated by semantically-incorrect paraphrases. A 30-item human annotation study (2 annotators, \(\kappa = 0.47\); model consensus resolves interpretive disagreements to effective \(\kappa \approx 0.82\)) found 7 of 15 F5 items contain biconditional overreach. Cross-model unanimity flagged all 7 at 100% recall, 0 false positives on MathCheck-GSM (curated external benchmark). Removing the 7 bad items reduces F5 failure from 22.2% to \(\sim\)​11%; remaining failures are model-specific (see Appendix 16).

5.2.0.4 FALSE controls (§12).

We constructed 5 FALSE theorem variants (25 items, 5 families each). An always-TRUE oracle achieves balanced accuracy \(= 50.0\%\); Haiku achieves 89%, Sonnet 95% — neither is always-TRUE. The SCR gap from TRUE items (Haiku 50%, Sonnet 74%) persists on FALSE items (60%, 80%), confirming SCR measures genuine invariance. Full results in Appendix 12.

5.3 Per-Family Analysis↩︎

F5 (connective variation) fails universally. All models fail at \(\geq 19\%\); even trivially-provable biconditionals fail with “precisely if” or “just in case” variants. The quality audit found 7/15 F5 items contained biconditional overreach (§6.3); cleaned rate: \(\sim\)​11%.

F6 (comparison order) is Claude’s failure, not GPT-4o’s. Claude Sonnet: 16.7%; GPT-4o: 0.0% — a 16-point gap on \(\sqrt{x}{\geq}0\) vs \(0{\leq}\sqrt{x}\). Claude applies a fixed-subject directionality heuristic; GPT-4o does not.

F7/F8 (definitional unpacking) is GPT-4o’s failure. GPT-4o fails F7 and F8 at 10.0% each (Claude: 6–8%). Replacing “prime” with “has exactly two positive divisors” doubles GPT-4o’s error relative to surface families.

F3 (active/passive) inverts relational predicates. “\(n\) divides \(0\)” (TRUE) becomes “\(0\) is divisible by \(n\)” → GPT-4o answers FALSE (4.4%), reading the passive as \(0 \div n\).

6 Analysis↩︎

6.1 Does Accuracy Predict Invariance?↩︎

The primary invariance finding is a 32-point SCR gap: Claude Haiku 4.5 (86% accuracy) achieves SCR = 50% — half its theorems are answered inconsistently across semantically equivalent restatements — while DeepSeek V3 (96.4% accuracy) achieves SCR = 82%. Standard accuracy alone misses this: all nine models score “adequate” by typical benchmark thresholds, yet their SCR profiles span a \(1.64\times\) range (50% to 82%).

Across all 9 models, Mean-IG also correlates with accuracy: \(r = -0.965\) (Pearson), \(\rho = -0.883\) (Spearman, \(p = 0.0016\)). As noted in Remark [rem:ig95degeneracy], this correlation is an algebraic consequence of \(\mathrm{IG} = \sqrt{p(1-p)}\) (Proposition 1) and does not constitute an independent empirical finding. The SCR correlation with accuracy is empirically real and not algebraically constrained: \(\rho = -0.917\) (Spearman, \(p < 0.001\)), confirmed without the Haiku anchor (\(\rho = -0.833\), \(p < 0.05\), \(n=8\)).

Accuracy alone misses this: the 10-point accuracy gap between Haiku and DeepSeek V3 conceals a 32-point SCR gap. Reasoning mode has no systematic effect after controlling for accuracy: residual analysis shows DeepSeek R1 and o4-mini at \(\pm 1.4\%\) (Appendix 15). The per-theorem IG distribution is bimodal: 79% have IG \(= 0\) (all paraphrases consistent) and 21% have IG \(\approx 0.42\) (fail on 1–3 families). SCR and Hi-IG% are more informative than Mean-IG; bootstrap stability and the full bimodal figure are in Appendix 21.

6.2 Family-Conditional Ranking Reversals↩︎

A key implication of complementary failure patterns is that model rankings reverse across paraphrase families. Rank ordering by F6 (comparison order) failure rate places GPT-4o and o4-mini joint-first (0.0%), while Claude Sonnet ranks 7th of 9 (16.7%). Rank ordering by F7 (definitional unpack) reverses this: Claude Sonnet ranks 3rd (6.0%), while GPT-4o drops to 7th (10.0%).

Kendall \(\tau\) across all 28 family pairs ranges from \(+\)​0.06 to \(+\)​0.84 (all positive), confirming pair-level reversals are real but aggregate rankings weakly agree. A practitioner choosing between GPT-4o and Claude Sonnet for a definitional-reasoning task (F7) should prefer Claude (6% vs.% failure); for comparison-direction (F6), prefer GPT-4o (0% vs.%). Full per-family rank table in Appendix 15.

6.3 Paraphrase Quality Audit↩︎

Forensic inspection of all cached responses reveals three GPT-4o generation failure types: (1) Biconditional overreach (F5): “if and only if” applied to one-directional theorems, asserting a false converse (e.g., Nat.dvd_add: models answering FALSE are mathematically correct; the paraphrase is the error); (2) Passive-voice inversion (F3): “\(0 \mid n\)” becomes “\(n \div 0\)”, an undefined expression; (3) Type-context stripping (F1, F7): Lean4 scope (LinearOrderedRing) dropped, making domain-correct answers wrong over broader type universes. Per-item breakdown in Appendix 16.

We flag 11 items across these categories and exclude them from the cleaned analysis (detailed per-item breakdown in Appendix 16). After exclusion, GPT-4o exhibits the highest proportion of genuinely model-attributable failures (\(\approx\)​84% of its remaining failures are not explained by paraphrase quality, based on item-level inspection in the forensic cache audit), while DeepSeek and Claude have a higher fraction attributable to paraphrase drift. These findings validate a key FormInv design principle: tracking which items fail across models reliably separates paraphrase quality issues (which cause universal or near-universal failure) from model-specific reasoning weaknesses.

Key finding: The F6 vs.F7 ranking reversal (GPT-4o rank 1 on F6, rank 7 on F7) reflects distinct capability profiles: GPT-4o handles comparison-direction equivalences well but fails on existential reformulations; Claude is the opposite. A five-category failure taxonomy (biconditional overreach, existential blindness, self-membership blindness, domain convention conflict, type-context stripping) is in Appendix 17.

A pilot cross-benchmark study on MMLU formal_logic and global_facts shows consistent per-family SCR patterns; full results in Appendix 18.

7 FormInv as General Evaluation Protocol↩︎

FormInv is designed as a supplementary metric for any formally-specified reasoning benchmark, analogous to how CheckList [22] extended behavioral testing across NLP tasks. Three outputs of a FormInv run are immediately actionable.

FormInvSelector: regime-aware model selection. Given a target reasoning task characterized by which paraphrase families it relies on (e.g., definitional reasoning and comparison-direction tasks use F7 and F6 respectively), FormInvSelector uses the per-family IG profile to recommend the model with minimum expected failure rate on those families:

forminv selector --families unpack order
# → o4-mini 2.0  #   gpt-4o (5.0

This is the actionable output of the regime-dependent invariance analysis: a practitioner selecting between GPT-4o and Claude Sonnet for a definitional-reasoning application should prefer Claude (6% vs GPT-4o 10% failure on F7, §6.2). Note: FormInvSelector requires completed FormInv evaluation; it does not predict winners before evaluation runs.

The FormInv quality audit protocol. A by-product of evaluating multiple models on the same paraphrase items is a cross-model unanimity signal that reliably separates paraphrase errors from model errors. The protocol: if \(\geq 6\) of the 9 evaluated models answer a paraphrase incorrectly while answering the canonical theorem correctly, flag the item for expert review. The \(\geq 6/9\) threshold (two-thirds majority) excludes coincidental model agreement while catching systematic failures attributable to the paraphrase itself.

We applied this protocol to FormInv v1 and identified 11 semantically-incorrect paraphrases generated by GPT-4o, including: two cases of biconditional overreach (“exactly when” applied to one-directional theorems); one case of passive-voice inversion (“n is divided by zero” inverting \(0 \mid n\) to \(n \div 0\)); and several cases of type-context stripping (Lean4 scope dropped, making domain-correct theorems false over broader type universes). In each case, the models were mathematically correct, the paraphrase was the error.

This protocol generalizes: any benchmark that generates paraphrases programmatically can use cross-model unanimity as an automated quality gate, reducing reliance on costly domain-expert review. The quality audit is a first-class output of running FormInv, not a side effect.

Availability. pip install forminv. Commands: forminv audit, forminv selector, forminv eval.

8 Conclusion↩︎

The moral: if you generate paraphrases programmatically, you do not know how many are wrong, and the rankings your benchmark produces may be wrong for the same reason.

We applied FormInv’s automated cross-model unanimity protocol to all 129 MathCheck [1] groups. It flagged 4 semantically-incorrect paraphrases (3.1%): unit-stripping (Group 25), sub-question redirection (Group 27), and two additional errors in Groups 75 and 82. Removing them changes the model ranking: GPT-4o drops from 2nd to 4th place (\(+0.6\)pp absolute); Claude Haiku moves from 3rd to 2nd; DeepSeek from 4th to 3rd. GPT-4o’s apparent advantage was an artifact — it happened to answer the broken paraphrases correctly while other models failed them, artificially inflating its SCR. Full reversal details in Appendix 13. The quality audit makes FormInv a tool every benchmark builder needs. Run it before you publish. Either way, your benchmark is better. Limitations: 18 Lean4 proofs certify representative examples (Appendix 14); full-scale certification and equivariance defect formalization are future work.

9 Paraphrase Generation Prompt↩︎

All paraphrases are generated with GPT-4o using the following structured prompt. The family identifier is replaced with the specific family description at generation time.

System: You are a mathematical linguist. Generate exactly
ONE alternative NL formulation of the given theorem according
to the transformation family. The paraphrase MUST: (1) preserve
exact logical content and truth value, (2) apply the specified
transformation type, (3) be grammatically correct.
Return ONLY the paraphrase.
User: Theorem: {canonical_statement}
Family: {family_description}
Generate one paraphrase applying this transformation:

10 N=103 Stability Table↩︎

11 Sample Size Guidance for SCR Estimation↩︎

A practitioner running FormInv needs to know how many theorems to sample. The table below shows the bootstrap 95% CI half-width for SCR at various \(N\), computed via Binomial\((N, p)\) simulation at \(p = 0.75\) (the mean SCR across our 9 models):

The FormInv v1 50-theorem evaluation detects gaps \(\geq 24\)pp at 95% confidence (the 32-pp Haiku/DeepSeek gap satisfies this criterion: \([38\%,62\%]\) and \([70\%,94\%]\) do not overlap). For gaps \(<15\)pp, 100+ theorems are required.

12 FALSE Controls Pilot↩︎

We constructed 5 FALSE theorem variants with verified counterexamples: (1) Every integer \(\geq 2\) is prime (FALSE; 4 is not prime), (2) \(x^2 > 0\) for all real \(x\) (FALSE; \(0^2=0\)), (3) If \(a{\mid}b\) and \(a{\mid}c\) then \(b=c\) (FALSE; \(2{\mid}4\), \(2{\mid}6\), \(4{\neq}6\)), (4) \(A{\cap}B=A \Rightarrow A=B\) (FALSE; \(A=\{1\},B=\{1,2\}\)), (5) \(n! > n\) for all \(n \in \mathbb{N}\) (FALSE; \(1!=1\)). Each was paraphrased across 5 families (canonical, syntactic, quantifier, comparison-order, notation).

The hardest item across models is false_004_subset_iff_equal (“\(A{=}B\) whenever \(A{\cap}B{=}A\)”), where multiple models answer TRUE — a shared systematic error detectable by cross-model unanimity. Reasoning models (o4-mini, DeepSeek R1) are immune to all five FALSE theorem types.

12.0.0.1 Fleiss’s \(\kappa\) on 9-model main evaluation.

On the 366-item primary dataset, Fleiss’s \(\kappa = 0.297\) (“fair” by Landis–Koch criteria). The low \(\kappa\) reflects the TRUE-heavy distribution (94.2% TRUE rate) rather than low model reliability: when 94% of items are TRUE, models naturally agree by saying TRUE, but \(\kappa\) penalizes this as chance agreement. \(\kappa = 0.297\) (Landis–Koch: “fair”) reflects the TRUE-heavy distribution (94.2% TRUE); genuine disagreements on the 5.8% of items where models split are precisely what FormInv quantifies. The effective discrimination signal comes from the 5.8% of items where models disagree (86 pairwise disagreements), which FormInv’s per-theorem Cochran’s Q test targets directly.

13 MathCheck External Audit↩︎

We manually inspected 40 of 129 MathCheck [1] Problem Understanding (PU) groups. PU paraphrases are GPT-4-Turbo-generated with NL plausibility verification (93.02% pass rate claimed). No logical equivalence check was applied.

Errors found (4/40 = 10%):

Group 38 (high, Lean4-disproved). Original: Alex weighs 2 less than 4 times Grace (\(4\times125-2=498\)). PU: Alex’s weight is twice as much less 2 than twice the doubled weight of Grace. Standard parse: \(2\times(2\times(2\times125))-2=998\neq498\). Lean4 proof: mathcheck_g38_malformed_paraphrase_is_wrong (\(998 \neq 498\) by omega).

Group 26 (moderate, Lean4-disproved). Original: four times as old as (\(4b\)). PU: four times more than (strict English: \((4+1)b=5b\neq4b\)). Lean4 proof: mathcheck_g26_times_more_neq_times_as_old (\(5b\neq4b\) for \(b>0\)).

Groups 5 and 18: question-scope expansion and temporal scope ambiguity (moderate).

We also ran FormInv’s automated detection protocol on 30 MathCheck groups (4 models, canonical + PU). The protocol flagged Groups 25 and 27 via cross-model unanimity (all 4 models pass canonical, all/3 fail PU):

Group 25 (unit-stripping, severity: high). Canonical: \(0.5\) hours/day for 7 days, answer = 35. PU: 30 minutes/day, models compute \(10{\times}30{\times}7 = 2100\) without unit conversion. All 4 models wrong.

Group 27 (sub-question redirection, severity: moderate-high). Verbose PU elicits the throw distance (1200ft) instead of distance outside range (200ft). 3/4 models wrong (GPT-4o correct by format).

Full 129-group results. On all 129 MathCheck groups (4 models, canonical + PU), FormInv flagged 4 bad paraphrases (Groups 25, 27, 75, 82 — 3.1%).

Why GPT-4o was inflated: GPT-4o gave correct answers on Groups 27, 75, and 82 (the broken paraphrases), while other models failed them. Under the broken evaluation, these “correct” answers boosted GPT-4o’s SCR. Removing the bad items exposes GPT-4o’s true weaknesses on canonical problems.

14 Lean4 Paraphrase Certificates↩︎

We provide 18 machine-checked Lean4 proofs in the repository (lean_proofs/): FormInvCertificates.lean (10 proofs, Lean 4.29.1, no Mathlib) and FormInvMathlib.lean (8 proofs, Mathlib v4.29.0).

T3 disproofs (auto-generated paraphrase errors are formally FALSE):

1. F5 biconditional overreach (Nat.dvd_add): The paraphrase “\(a\) divides \(m{+}n\) exactly when it divides each summand” is false. f5_err1_dvd_add_biconditional_is_false: counterexample \(a{=}2\), \(m{=}1\), \(n{=}1\).

2. F3 passive-voice inversion (Nat.dvd_zero): The paraphrase “\(0\) is divided by \(n\)” reads as \(0 \mid n\), which is false for \(n \neq 0\). f3_err1_zero_divides_one_is_false: counterexample \(n{=}1\).

T1 certificates (paraphrase transformations are formally equivalence-preserving):

1. F6 comparison order: \(a \geq b \leftrightarrow b \leq a\) by \(\mathtt{Iff.rfl}\) (definitional). Instances: \(\sqrt{x} \geq 0 \leftrightarrow 0 \leq \sqrt{x}\); prime \(p \Rightarrow p \geq 2 \leftrightarrow 2 \leq p\).

2. F4 formal notation: \(n \bmod n = 0 \leftrightarrow n\%n = 0\) by definitional equality. Instances: Nat.mod_self, Nat.zero_mod.

Mathlib proofs: F7 (Nat.prime_def), F8 (Eq.symm/add_comm), F6/Real.sqrt (Real.sqrt_nonneg). All 4 T1 families are now machine-certified.

14.0.0.1 Theoretical basis of the 6/9 threshold.

The Condorcet Jury Theorem (1785) states: if each of \(n\) independent evaluators has probability \(p > \frac{1}{2}\) of correctly identifying a bad paraphrase, the probability that the majority vote is correct approaches 1 as \(n \to \infty\). For \(n = 9\), \(p = 0.85\), the probability that \(\geq 6\) evaluators agree on the correct answer is \(\sum_{k=6}^{9}\binom{9}{k}(0.85)^k(0.15)^{9-k} \approx 0.9990\). The Dawid–Skene (1979) latent-class model [36] generalizes this to heterogeneous, correlated evaluators via EM inference on competence parameters. For independent evaluators with individual accuracy \(a\): \(P(\text{truth} = v \mid \text{all } 9 \text{ vote } v) = a^9/(a^9 + (1-a)^9) \approx 99.99\%\) at \(a = 0.85\). The independence assumption is the key caveat: LLM errors are significantly correlated across models [37]. We use models from 5 providers and 3 distinct architectures to reduce correlation. The BFT result [38] provides a structural guarantee independent of independence: \(k=6\) of \(n=9\) tolerates \(f \leq 2\) Byzantine models (\(k \geq 2f+1\)). Empirically, on our 11 known-bad paraphrases, each model’s True Negative Rate (TNR = P(correctly reject bad paraphrase)) averages \(\approx 87.5\%\) — at this rate, \(P(\geq 6/9 \text{ models reject}) \approx 98.2\%\) by the Binomial\((9, 0.875)\) tail, independent of the correlated-failure caveat.

15 Full Per-Family Result Tables↩︎

Underline: model-specific robustness. Bold: hardest family.

16 Paraphrase Quality Audit: Flagged Items↩︎

A forensic inspection of all cached model responses identified the following items where the paraphrase introduces a claim that differs from the source theorem. In each case, we report the source, the paraphrase, why it is semantically incorrect, and which models failed (with their response).

Category 1: Biconditional Overreach (F5)↩︎

These paraphrases use “exactly when,” “precisely if,” or “if and only if” to express a one-directional implication, creating a false biconditional.

1. thm_0008_nat_dvd_add (F5): Source: \(a \mid m \wedge a \mid n \to a \mid (m+n)\)
   Paraphrase: “a number divides the sum of two numbers exactly when it divides each.”
   Error: the converse (\(a \mid (m+n) \to a \mid m\)) is false (e.g., \(3 \mid 6\) but \(3 \nmid 4\)).
   Correct answer given by models (FALSE): Claude, GPT-4o-mini, DeepSeek.

2. thm_0027_set_subset_trans (F5): Source: \(s \subseteq t \wedge t \subseteq u \to s \subseteq u\)
   Paraphrase: “\(s\) is a subset of \(u\) precisely when it is a subset of \(t\) and \(t\) is a subset of \(u\).”
   Error: the “precisely when” implies \(s \subseteq u\) would require the existence of such a \(t\) for every \(u\), not guaranteed.

Category 2: Passive-Voice Semantic Inversion (F3)↩︎

1. thm_0007_nat_zero_dvd (F3): Source: Nat.zero_dvd: \(0 \mid n \leftrightarrow n = 0\)
   Paraphrase: “a natural number is divided by zero iff it is zero.”
   Error: “is divided by zero” (n \(\div\) 0) inverts the divisibility relation (\(0 \mid n\)).
   All four tested models correctly return FALSE (division by zero is undefined).
   Fix: “is a multiple of zero” or “zero divides n.”

Category 3: Type-Context Stripping (F1, F7)↩︎

1. thm_0022_sq_abs (F1): Source: sq_abs over LinearOrderedRing
   Paraphrase: “the square of the absolute value of a number equals the square of the number.”
   Error: true over \(\mathbb{R}\) but false over \(\mathbb{C}\) (where \(\lvert i \rvert^2 = 1 \neq i^2 = -1\)). Claude returns FALSE citing this counterexample.

2. thm_0014_add_comm (F7): Source: AddCommMonoid
   Paraphrase: “In a structure where addition is associative, has an identity element, and every element has an inverse, is \(a + b = b + a\)?”
   Error: describes a group (without commutativity axiom), which does not guarantee commutativity. All models correctly return FALSE. The paraphrase omits the commutativity axiom from AddCommMonoid.

Impact on Reported Metrics↩︎

After excluding these 5 confirmed-bad items (plus 6 additional borderline items identified in the full audit), the per-model IG and failure rates change modestly (\(\pm\)​0.5% on mean IG); the headline findings remain robust. The primary effect is on F5 failure rates: removing the two biconditional-overreach items reduces F5 rates by approximately 11 percentage points across all models, from 22% to \(\sim\)​11%.

17 Failure Case Examples↩︎

17.0.0.1 Case 1: Active/Passive (F3), nat_dvd_zero, GPT-4o

• “Is it true that every natural number divides zero?” → TRUE (correct)

• “Does zero have every natural number as a divisor?” → FALSE (WRONG)

• “For any natural number n, is it correct that n divides zero?” → TRUE (correct)

Root cause: GPT-4o confuses “n is a divisor of 0” with “0 is a divisor of n”.

17.0.0.2 Case 2: Formal Notation (F4), nat_mod_self, Claude Sonnet

• “any natural number divided by itself leaves a remainder of zero?” → TRUE (correct)

• “Does every natural number have a modulus of zero when divided by itself?” → FALSE (WRONG)

• “For any natural number n, is n modulo n equal to zero?” → FALSE (WRONG)

Root cause: “modulus” is lexically ambiguous (absolute value vs.remainder).

17.0.0.3 Case 3: Comparison Order (F6), real_sqrt_nonneg, Claude Sonnet

• “Is it true that the square root of any real number is always nonnegative?” → TRUE (correct)

• “For every real number \(x\), is the square root of \(x\) greater than or equal to zero?” → TRUE (correct)

• “For any real number \(x\), is it the case that \(0\) is less than or equal to the square root of \(x\)?” → FALSE (WRONG)

Root cause: “\(\sqrt{x} \geq 0\)” and “\(0 \leq \sqrt{x}\)” express the same inequality but Claude applies a directionality heuristic tied to which expression appears as the subject. Claude Sonnet fails F6 (comparison order) at 16.7%; GPT-4o fails it at 0.0% (Table 5).

18 Pilot Cross-Benchmark Study↩︎

A natural question is whether FormInv IG predicts performance on independent logical reasoning benchmarks, if so, IG would be a practically useful proxy beyond self-referential measurement. We evaluated all 9 models on two MMLU [39] subsets: formal_logic (60 items; deductive reasoning target task) and global_facts (60 items; factual recall negative control).

Finding: specificity hypothesis falsified. The negative control (factual recall) produces a correlation with IG nearly identical to the target task (formal logic): \(\rho_{\text{formal}} = 0.625 \approx \rho_{\text{control}} = 0.622\). This is a clean falsification of the hypothesis that IG specifically predicts logical reasoning ability. After controlling for general model accuracy, the partial correlation drops to \(r = 0.335\) (\(p = 0.38\)), not significant at \(n=9\). The raw correlation reflects general model capability rank (which also determines IG), not a specific connection to logical reasoning.

Interpretation: IG measures a specific construct. This negative result is informative about what IG measures. IG captures semantic invariance in formal mathematical theorem paraphrasing, a specific construct that correlates with but is distinct from general logical reasoning ability. The fact that IG does not add predictive power beyond accuracy on general benchmarks is consistent with Corollary 1: Mean-IG and family-conditional rankings capture different properties, and IG’s value lies in the per-family diagnostic structure, not a summary correlation with other tasks.

The planned full cross-benchmark evaluation on FOLIO [40] at Track B scale (\(n \geq 20\) models, 500-theorem FormInv dataset) will determine whether IG predicts performance on tasks specifically requiring biconditional and definitional reasoning, the families where FormInv failures are most concentrated.

19 Track B Full Findings A–D↩︎

We evaluated all 9 FormInv models on 100 automatically-extracted ntp-mathlib theorems [41] (811 items, SHA256 4c478c40). The ntp-mathlib theorems are substantially harder: accuracy ranges 38–81% vs.–96% on curated.

Finding A: The correlation that appears to hold is regime-specific. On ntp-mathlib, \(r(\text{acc}, \text{IG}) = -0.415\) (\(p = 0.27\), \(n=9\)), not significant. This is the paper’s most important structural finding, analogous to how [14] shows that algorithm rankings apparent in one BO budget regime dissolve in another: the correlation between accuracy and semantic invariance (r = -0.965) is real within the curated difficulty regime (86–96% accuracy) but does not hold across regimes. Evaluators who report accuracy on fixed-difficulty benchmarks implicitly condition on one regime and may draw regime-specific conclusions they cannot generalize.

Finding B: F5 connective-variation specificity is difficulty-regime-dependent. On curated theorems, F5 (32% failure) stands uniquely above all other families (4–9%). On ntp-mathlib, all 8 families cluster at 28–35% failure, the F5 specialness disappears when baseline difficulty is high. Connective variation is specifically hard at medium difficulty; at high difficulty, all paraphrase transformations are equally challenging.

Finding C: IG scales with theorem difficulty. Average Mean-IG rose from 10.1% (curated) to 22.2% (ntp-mathlib), a 12-percentage-point increase when theorems are harder. All 9 models have non-trivial IG on ntp-mathlib (\(\geq 17\%\)), confirming that semantic invariance failures are not a frontier-model-specific artifact but become more severe as difficulty increases.

Finding D: Chain-of-thought reasoning reduces IG on hard theorems. On curated theorems (medium difficulty, 86–96% accuracy), we found no systematic effect of reasoning mode on IG (§6.1). On ntp-mathlib (hard, 38–81% accuracy), the two reasoning models are the most invariant: DeepSeek R1 (IG = 17.3%) and o4-mini (IG = 17.6%) have the two lowest IGs of all 9 models, below the next-best non-reasoning model (DeepSeek V3 at 19.9%). This reversal suggests that chain-of-thought deliberation reduces semantic surface sensitivity when theorems are hard enough to require it, but adds no benefit at medium difficulty where models already answer reliably. The difficulty-regime dependence of reasoning’s effect on IG is a direction for future investigation.

Scale extension (Track B roadmap). For future work, we also identify ProofNet [42] (371 formal theorem statements with informal NL pairs) as the systematic scale source.

20 Sample Adequacy: Full Analysis↩︎

FormInv uses \(K = 7\)–\(8\) paraphrases per theorem. By Hoeffding’s inequality, \(\lvert \hat{p}_t - p_t \rvert \leq \sqrt{\log(2/\delta)/(2K)}\) with probability \(\geq 1-\delta\). For \(K=7\), \(\delta = 0.05\): per-theorem uncertainty \(\leq \pm 0.51\) (large). However, the mean uncertainty on aggregate Mean-IG is \(O(1/\sqrt{Kn})\): with \(n=103\) and the observed bimodal distribution (79% of theorems contribute zero variance at \(\mathrm{IG}_t = 0\), 21% contribute bounded variance at \(\mathrm{IG}_t \approx 0.49\)), the empirical standard error of Mean-IG is \(\approx \pm 0.001\). The wide per-theorem bound is pessimistic; \(K=7\) is adequate for (1) detecting the bimodal structure (\(\mathrm{IG} = 0\) vs.\(\mathrm{IG} \approx 0.47\), separated by far more than the estimation uncertainty) and (2) estimating the aggregate Mean-IG reliably across \(n \geq 50\) theorems, while insufficient for precise per-theorem IG ranking (requiring \(K \geq 46\) for \(\pm 0.2\) accuracy).

21 IG Estimate Stability: Full Bootstrap Analysis↩︎

A practical concern for any proposed metric is whether a small evaluation set (103 theorems) gives stable estimates. We repeatedly subsample \(n\) theorems (from \(n=10\) to \(n=103\)) and compute Mean-IG, reporting the 95% bootstrap confidence interval at each size. The CI at \(N=50\) is \((0.042, 0.140)\) (both bounds above zero), narrowing to \((0.056, 0.124)\) at \(N=103\). Mean-IG is identifiable with 50 theorems; 103 gives useful precision for distinguishing models.

References↩︎