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

A paraphrase-quality audit of MathCheck (Zhou et al., 2024) detected 4 semantically-incorrect paraphrases in 129 groups (3.1%); removing them drops GPT-4o from rank 2 to rank 4 and elevates Claude Haiku and DeepSeek V3 above it; these ranking changes are invisible to any single-model evaluation. Cross-model unanimity found these errors automatically (≥3/4 models for MathCheck; ≥6/9 for our primary evaluation) for under \$10; in our own dataset the same protocol found that 47% of auto-generated connective-variation paraphrases were semantically incorrect. That flaw compounds a deeper measurement gap. On the theorems every model answers correctly in canonical form, where accuracy is identical by construction, a semantically equivalent rewording still flips the answer for 5-42% of them: Claude Haiku 4.5 flips a known-correct answer ~9× as often as DeepSeek V3 (41.9% vs. 4.7% on the 43 theorems all models share), a 37-point difficulty-controlled gap we call the Conditional Inconsistency Rate (CIR). Crucially CIR is anti-correlated with capability (Spearman ρ = −0.57 between canonical accuracy and CIR, vs. +0.65 for raw consistency), so it is not a relabeling of problem difficulty but an axis largely orthogonal to accuracy; the anti-correlation strengthens to ρ = −0.59 on an independent 103-theorem set, where the ranking also replicates. Raw Semantic Consistency Rates (SCR) span 50-82% across 9 models, but we show this cross-model spread is mostly a mechanical consequence of compounding accuracy over k ≈ 6 paraphrases; what is not mechanical, and what CIR isolates, is the within-theorem clustering of failures (SCR sits ~9 points above an independence null, p < 0.01 for 6 of the 8 models tested). Because no model dominates on all paraphrase families, the families a benchmark chooses to include implicitly fix its model ranking (a No-Free-Benchmark corollary). FormInv supplies the audit protocol (which reranks the published MathCheck benchmark), the difficulty-controlled CIR and SCR as invariance measures (with a proposed per-theorem Cochran's Q significance test) evaluated on 9 models across 366-811 items whose canonical statements are Lean4-verified (paraphrases are CAS- and expert-verified, with the cross-model audit as a third verification layer), and FormInvSelector for regime-aware model selection.