Technical Summary: FormInv: A Measurement Protocol for Semantic Invariance in Mathematical Reasoning Benchmarks

1. Problem Statement

Current benchmarks for mathematical reasoning in Large Language Models (LLMs) rely heavily on aggregate accuracy metrics calculated on canonical problem formulations. This paper argues that such metrics are insufficient because they assume model performance is independent of how a question is phrased. The authors identify a critical "measurement gap": models often exhibit high accuracy on standard benchmarks yet fail to maintain semantic invariance—the ability to produce consistent answers across logically equivalent paraphrases.

The paper highlights that standard benchmarks (e.g., GSM8K, MATH, MathCheck) lack rigorous verification of paraphrase semantic equivalence. Consequently, benchmark rankings may be artifacts of specific phrasings rather than true measures of reasoning capability. The authors draw on psychometric theory, specifically Differential Item Functioning (DIF) and Generalizability Theory, to formalize this issue. They posit that if a model's answer changes based on semantically equivalent restatements, it indicates a failure in genuine mathematical understanding, relying instead on surface-pattern recognition.

2. Methodology

2.1 The FormInv Protocol

The authors propose FormInv, a measurement protocol designed to audit and quantify semantic invariance. The protocol consists of three core components:

1. The Invariance Gap (IG) and Semantic Consistency Rate (SCR):

   • IG: Formally defined as the standard deviation of a model's binary answers across an equivalence class of paraphrases. Mathematically, $IG(f, [x]_\sim) = \sqrt{p(1-p)}$, where $p$ is the probability of a correct answer within the equivalence class. An IG of 0 implies perfect invariance.
   • SCR: The proportion of theorems for which the model answers correctly across all paraphrase forms. Unlike IG, which measures variance, SCR measures the intersection of correctness and invariance.
   • Cochran's Q: Used as a statistical test for marginal homogeneity across $k > 2$ paraphrase families to determine if a model's failure rate varies significantly by family.

2. The 8-Family Paraphrase Taxonomy:
   The benchmark evaluates models across eight distinct transformation families, categorized by their verification rigor:

   • T1 (Formally Certifiable): Families F4 (notation), F6 (order), F7 (unpack), and F8 (equivalence). These rely on Lean4/FOL rules or Computer Algebra System (CAS) verification (e.g., SymPy).
   • T2 (Conditionally Valid): Families F1 (syntactic), F2 (quantifier), and F3 (passive). These depend on type context and are verified via templates or CAS where applicable.
   • T3 (Heuristic): Family F5 (connective variation). These rely on natural language heuristics and require domain-expert review.

3. Cross-Model Unanimity Audit:
   A novel quality control mechanism where a paraphrase is flagged as semantically incorrect if a supermajority of models (e.g., $\ge 6/9$) fail the paraphrase while passing the canonical version. This leverages the assumption that systematic errors in the paraphrase itself, rather than model reasoning, cause universal failure.

2.2 Benchmark Construction

• Substrate: The evaluation uses 103 curated theorems from Mathlib4 (Lean4-verified), spanning domains like number theory, algebra, and real analysis.
• Dataset: The primary dataset (FormInv v1) contains 760 items (103 theorems $\times$ ~7.4 paraphrases). An extended "Track B" evaluation uses 100 harder theorems from ntp-mathlib (811 items).
• Verification: Paraphrases are generated via GPT-4o and verified via a multi-stage protocol: CAS for algebraic families, template guarantees for surface families, and 100% human expert review for definitional families (F7/F8).

2.3 Experimental Setup

The study evaluates 9 frontier models (including GPT-4o, Claude Sonnet/Haiku, DeepSeek V3/R1, Gemini 2.5 Flash, and Llama 3.3 70B) across the 366–811 items. Models are evaluated in zero-shot mode with strict TRUE/FALSE constraints.

3. Key Results

3.1 The Invariance Gap vs. Accuracy

The most significant finding is the disconnect between aggregate accuracy and semantic consistency.

• Claude Haiku 4.5 achieves 86% accuracy but only 50% SCR, meaning half its correct answers are inconsistent across paraphrases.
• DeepSeek V3 achieves 96.4% accuracy and 82% SCR.
• A 10-point accuracy gap conceals a 32-point SCR gap. The paper notes that accuracy alone is "constitutionally blind" to this structural failure.
• There is a strong negative correlation ($r = -0.965$) between accuracy and Mean-IG, suggesting more accurate models are generally more invariant, but this correlation is algebraically driven by the definition of IG and does not guarantee invariance for specific families.

3.2 Ranking Reversals and Complementarity

Model rankings are not stable; they reverse depending on the paraphrase family:

• F6 (Comparison Order): GPT-4o fails 0.0% of items, while Claude Sonnet fails 16.7%.
• F7 (Definitional Unpack): Claude Sonnet fails ~6%, while GPT-4o fails 10.0%.
• This complementary failure pattern implies that no single model Pareto-dominates all families. Consequently, benchmark designers implicitly choose a weighting of families that determines the winner. The paper formalizes this as the "No-Free-Benchmark" corollary: for any target ranking, there exists a weighting $\lambda$ over paraphrase families that realizes it.

3.3 Quality Audit Findings

The cross-model unanimity protocol successfully identified semantically incorrect paraphrases in existing benchmarks:

• MathCheck Audit: Applied to 129 groups in MathCheck, the protocol flagged 4 semantically incorrect paraphrases (3.1%). Removing these errors shifted GPT-4o from rank 2 to rank 4, elevating Claude Haiku and DeepSeek V3.
• FormInv v1 Audit: The protocol identified 11 errors in GPT-4o-generated items, including biconditional overreach, passive-voice inversions, and type-context stripping. These errors were invisible to single-model evaluation but exposed by unanimity.

3.4 Difficulty Regime Dependence

In the "Track B" evaluation using harder theorems:

• The correlation between accuracy and invariance weakened ($r = -0.415$, not significant).
• The specific difficulty of F5 (connective variation) dissolved; all families clustered at similar failure rates (28–35%).
• Reasoning models (DeepSeek R1, o4-mini) showed the lowest IG on hard theorems, suggesting Chain-of-Thought deliberation reduces surface sensitivity only when theorems demand high-level reasoning.

4. Contributions

1. Invariance Framework: Formalizes SCR and IG as primary metrics for semantic invariance, grounded in Doob's conditional expectation theorem and DIF theory. It classifies paraphrase families into T1, T2, and T3 tiers based on verification rigor.
2. FormInv Benchmark: A dataset of 760+ items derived from Lean4-verified theorems, evaluated across 9 models with a rigorous cross-model unanimity audit.
3. FormInvSelector: An algorithm that uses per-family SCR profiles to recommend the model with the lowest expected failure rate for specific task regimes (e.g., selecting a model for definitional reasoning vs. comparison tasks).
4. Paraphrase Quality Audit: Demonstrates that cross-model unanimity ($\ge 6/9$ models failing a paraphrase) is an automated, low-cost method to detect semantically incorrect benchmark items, effectively separating benchmark errors from model errors.

5. Significance and Claims

The paper claims that FormInv is the first protocol to apply measurement invariance theory and DIF-grounded metrics to formal mathematical reasoning. Its significance lies in three areas:

• Revealing Hidden Flaws: It exposes that standard accuracy metrics can be misleading, hiding a "32-point gap" between surface performance and genuine semantic understanding.
• Benchmark Integrity: It provides a tool for benchmark builders to audit their own datasets before publication, preventing rankings from being artifacts of flawed paraphrases. The authors assert that "if you generate paraphrases programmatically, you do not know how many are wrong."
• Regime-Aware Evaluation: It challenges the notion of a single "best" model, demonstrating that rankings are regime-dependent (varying by paraphrase family and difficulty). The paper concludes that benchmark designers implicitly choose winners by selecting which families to include, and FormInv makes this choice explicit and auditable.

The authors remain modest regarding limitations, noting that full-scale certification of all paraphrases via Lean4 is future work, and that the current study relies on a curated set of 103 theorems (though extended to 100 harder ones in Track B). They emphasize that FormInv is a supplementary metric intended to augment, not replace, existing accuracy-based evaluations.