Same Math, Different Formatting, Flipped Answers — The Measurement Black Hole in Math Benchmarks

Translation and summary of a zhichai.net forum post discussing the FormInv paper.

> Ask an AI two questions: > > Q1: "For all real numbers x, √x ≥ 0 holds, right?" Q2: "For all real numbers x, 0 ≤ √x holds, right?" > > These are logically equivalent propositions — identical mathematical meaning. Claude Sonnet answered Q1 correctly and Q2 incorrectly — a 16.7% error rate. GPT-4o answered both — 0% error. If a benchmark author decides to always write inequalities as a ≥ b, Claude scores perfectly; if written the other way, GPT-4o is perfect. The benchmark author's offhand choice of notation decides which model is "better."

Paper overview

| Item | Content | |------|---------| | Paper | FormInv: A Measurement Protocol for Semantic Invariance in Mathematical Reasoning Benchmarks | | Authors | Nishal Thomas, Noel Thomas | | Affiliations | Independent Researcher & Mohamed Bin Zayed University of AI | | arXiv | 2605.29001, May 27, 2026, cs.LG; cs.AI | | Core findings | Frontier LLMs systematically flip answers on semantically equivalent rewrites; Claude Haiku: 86% accuracy but 50% semantic consistency rate (SCR); DeepSeek V3: 96.4%/82%; rankings reverse across rewrite families; 47% of auto-generated rewrites contain semantic errors; cross-model consistency can audit rewrites automatically for under $10 |

Key points

1. Auditing MathCheck

• The authors audited 129 rewrite groups from MathCheck (ICLR 2025) with 4 models, automatically flagging 4 (3.1%) semantically flawed rewrites — e.g., "unit-stripping" rewrites that silently dropped units like "20 km" → "20", changing mathematical meaning invisibly to any single-model evaluation.
• After removing those 4 rewrites, GPT-4o dropped from rank 2 to 4, Claude Haiku rose from 3 to 2, DeepSeek V3 from 4 to 3. A 3.1% rewrite-quality error moved more than half the rankings. Total audit cost: under $10.

2. Eight rewrite families, one flipped map

• FormInv is built from 103 Lean4-verified Mathlib4 theorems across 7 domains (number theory, algebra, set theory, real analysis, etc.), each rewritten into up to 8 semantically equivalent forms in three certification tiers: T1 (formally verifiable — F4 symbol variants, F6 comparison order, F7 definition expansion, F8 equivalent propositions; CAS/Lean4), T2 (template-guaranteed — F1 syntactic substitution, F2 quantifier variants, F3 active/passive), T3 (heuristic, fully human-reviewed — F5 connective variants).
• 9 models ran on 366–811 rewrite items. Claude Haiku 4.5: 86% accuracy but only 50% SCR — half of the theorems it "knows" flip under rewrites. DeepSeek V3: 96.4% accuracy, 82% SCR — a mere 10-point accuracy gap hides a 32-point SCR gap. Accuracy is flat light; SCR is an X-ray.

3. Who wins depends on the rewrite family

• F6 (comparison order, a ≥ b vs b ≤ a): GPT-4o and o4-mini tie for first (0% failure); Claude Sonnet ranks 7th with 16.7% failure.
• F7 (definition expansion, e.g., "prime" → "has exactly two positive factors"): rankings flip — Claude Sonnet rises to 3rd (6% failure), GPT-4o falls to 7th (10% failure).
• No-Free-Benchmark corollary: among 9 frontier models, none Pareto-dominates across all 8 rewrite families. Therefore, for any target ranking, some rewrite-family weight vector λ realizes it. Benchmark designers implicitly choose winners when they pick rewrite families and weights — without any intent to manipulate.

4. 47% of automatic rewrites were wrong

• Auto-generated F5 connective rewrites ("iff" → "exactly when", "just in case") were audited via cross-model consistency: a rewrite is flagged if ≥6/9 models answer the original correctly but the rewrite incorrectly. Human annotation confirmed 7 of 15 flagged rewrites (47%) contained semantic errors:
• Biconditional over-generalization (turning one-way implications into "iff")
• Passive-voice inversions introducing undefined expressions ("0 divides n" → "n divided by 0")
• Type-context stripping (losing Lean4 scope constraints, making domain-specific theorems false in wider type universes)
• GPT-4o itself answers the erroneous rewrites "correctly" under their corrupted meaning — which is exactly why single-model evaluation cannot detect rewrite errors: the question-setter and answerer share the same blind spots. Only cross-model consistency can surface them. Extrapolated to MathCheck, the method achieved 100% recall on manually confirmed rewrite errors.

5. FormInvSelector: rewrite-aware model selection

• A practical CLI tool. For definition-expansion (F7) workloads, run forminv selector --families unpack: it recommends o4-mini (2.0% failure) over GPT-4o (5.0% failure, ~2.5× worse). For comparison-direction (F6) workloads, it recommends GPT-4o (0%) over Claude (16.7% — one failure per six inferences).
• FormInv does not tell you which model is "best" — it tells you which model fits your actual input distribution.

6. Honest limitations (acknowledged in the post)

What is solid:

• Certification tiers are audited (formal verification, template guarantees, full human review), not guessed.
• Ground truth comes from formalized theorems — no manual labeling needed.
• Cross-model consistency auditing has strong empirical support (100% recall in two independent validations).
• The No-Free-Benchmark corollary has rigorous support: 8 families, 9 models, no Pareto-dominator → any ranking corresponds to some weights. This means rankings are sensitive to rewrite-family choice, not that they are random.

What is unclear:

• Coverage: 103 undergraduate-level Mathlib4 theorems may not represent "mathematical reasoning" broadly; a Track B test on 100 harder ntp-mathlib theorems showed reduced (p = 0.27) but not significant correlation, hinting at difficulty-range dependence.
• Completeness: 8 rewrite families do not exhaust the space of semantic equivalence (cross-language, cross-representation rewrites are missing); the Pareto landscape might change with more families.
• False positive rate of the ≥6/9 cross-model threshold at larger scale is not evaluated.
• SCR → downstream performance: the transfer function from semantic consistency to real-world problem-solving performance is not established.

7. The invisible variable

The deeper message is an old one: measurement quality depends on measuring the right variable. Benchmarks claiming "model X beats model Y at math" measure only accuracy, ignoring whether a model's understanding is independent of expression — which is the essence of mathematical reasoning. FormInv advances evaluation from "how many problems did it answer" to "is its understanding independent of formulation," and leaves three uncomfortable questions: which rewrite family are you asking? What does your input distribution look like? And are you sure your benchmark rewrites themselves are error-free — the answer, per FormInv, can be 47% wrong.

References

1. Thomas & Thomas, "FormInv: A Measurement Protocol for Semantic Invariance in Mathematical Reasoning Benchmarks", arXiv:2605.29001, 2026. 2. Zhou et al., "MathCheck: A Behavioral Testing Framework for Mathematical Reasoning of Large Language Models", ICLR 2025. 3. Ribeiro et al., "Beyond Accuracy: Behavioral Testing of NLP Models with CheckList", ACL 2020. 4. Northcutt et al., "Pervasive Label Errors in Test Sets Destabilize Machine Learning Benchmarks", NeurIPS 2021. 5. Cronbach et al., "The Dependability of Behavioral Measurements: Theory of Generalizability for Scores and Profiles", Wiley, 1972.