《同题异表，答案翻转——数学基准测试的测量学黑洞》

问 AI 两个问题。

问题一："对于所有实数 \(x\)，\(\sqrt{x} \geq 0\) 成立，对吗？"问题二："对于所有实数 \(x\)，\(0 \leq \sqrt{x}\) 成立，对吗？"

这两个问题是逻辑等价命题——不等号方向和主语顺序颠倒了，但数学含义完全相同。任何一个高三学生都能看出它们说的是同一回事。

Claude Sonnet 对问题一答对了。对问题二答错了——出错率 16.7%。

GPT-4o 对两个问题都答对了——0% 出错。

如果出题人决定："我的基准测试，不等号一律写成 \(a \geq b\) 的形式，不写 \(b \leq a\)"——Claude 在这类题上得分完美。如果出题人反着写——GPT-4o 完美。同一个模型，同一组定理。出题人顺手选了个符号写法，就决定了哪个模型"更好"。

2026 年，独立研究者 Nishal Thomas 和 Noel Thomas 在 FormInv 论文中系统化了这个直觉，并发现了一个比"符号写法影响排名"更深的黑洞：所有基准测试的设计者，都在无意识地选择谁赢。

1. 📏 两位先生，同一道题

论文从 MathCheck（ICLR 2025 接收，一个测试数学推理稳健性的知名基准）开始审计。

他们取了 MathCheck 中的 129 组改写。用 4 个模型跑了一遍，自动标出了 4 个语义错误的改写——3.1%。这些是表面看起来像正确改写、但实际上改变了数学含义的题目。比如"剥离单位"（unit-stripping）：一个涉及实际计量单位的应用题，改写时悄悄丢掉了单位，"20 公里"变成了"20"，数学含义变了，但任何一个单一模型的评估都发现不了——因为单一模型可能恰好答对（或答错），你看不出是改写的锅还是模型的锅。

论文把这 4 个错误改写移除后——GPT-4o 的排名从第 2 掉到第 4。 Claude Haiku 从第 3 升到第 2。DeepSeek V3 从第 4 升到第 3。

一个 3.1% 的改写质量误差，翻动了超过一半的排名。

这个审计花了多少钱？不到 10 美元。

2. 🔄 8 种改写，一张翻转的地图

论文不止于审计。他们自己构造了一个更系统的测试集——FormInv。基材是 103 个 Lean4 验证的 Mathlib4 数学定理，覆盖数论、代数、集合论、实分析等 7 个领域。每个定理被改写成最多 8 种语义等价形式，分三个认证层级：

9 个模型在 366-811 个改写项上跑了一轮。结果像一张透视底片——把基准测试的"隐身结构"照了出来。

Claude Haiku 4.5——一个部署中的商业模型——准确率 86%，但语义一致性率（SCR）只有 50%。 它"会"的定理里，一半在改写后答案翻转。准确率给出的信号是"这模型数学不错"。SCR 给出的信号是"这模型有一半的数学知识是格式依赖的——换个写法就没用了"。

DeepSeek V3：准确率 96.4%，SCR 82%。只差了 10 个百分点的准确率，背后是 32 个百分点的 SCR 鸿沟。准确率是平光——SCR 是 X 光。

3. 🎭 谁赢，取决于改写族

论文做了每个改写族上的排名。

F6（比较顺序——\(a \geq b\) vs \(b \leq a\)）：GPT-4o 和 o4-mini 并列第一——0% 失败率。Claude Sonnet 排到第 7——16.7% 失败率。 同一组定理，不等号往哪边写，决定了 Claude 是否"擅长数学"。

F7（定义展开——"质数" 替换为"恰好有两个正因子"）：排名翻转。Claude Sonnet 升到第 3（6% 失败），GPT-4o 掉到第 7（10% 失败）。同一组定理，用术语还是用定义，决定了 GPT-4o 是否"擅长数学"。

论文由此推导了一个简洁的推论——无免费基准（No-Free-Benchmark）推论：在 9 个前沿模型中，没有一个模型在全部 8 个改写族上 Pareto-占优所有其他模型。因此对于任何目标排名（谁第一、谁第二、谁垫底），都存在一组改写族权重 \(\lambda\) 可以实现它。基准设计者选择哪些改写族、给它们多大权重——就是在隐式地选择赢家。

这个选择的成本是零意识。没有基准设计者故意操纵排名。他们只是选了自己觉得合理的改写方式，顺手写了个权重。但"顺手"本身，已经包含了赢家。

4. 🗑️ 自动改写有 47% 是错误的

论文的第四个发现与自己有关——他们在构造 FormInv 时，用 GPT-4o 自动生成了 F5 连接词改写（"iff" → "exactly when"、"just in case"等）。然后用交叉模型一致性做了一次自动质量审计：如果 ≥6/9 的模型在原定理上答对、在改写上答错，标记改写为可疑。

结果——审计出的 15 个 F5 改写的样本中，人工标注确认 7 个包含语义错误（47%）。主要错误类型：

• 双条件过度推广：把单向蕴含定理写成"当且仅当"，断言了虚假的逆命题
• 被动语态反转："0 整除 \(n\)" 改写成了"\(n\) 被 0 除"，引入了无定义表达式
• 类型上下文剥离：丢失了 Lean4 的范围约束，使领域特定的定理在更宽的类型宇宙中变成假命题

GPT-4o 生成的改写，GPT-4o 自己答对了这些错误改写——因为它在错误改写上是"正确"的（错误改写改变了数学含义，GPT-4o 按新的错误含义答对了）。 这恰好是单一模型评估为什么发现不了改写错误的原因：出题者和答题者是同一类模型，共享同样的"理解盲区"。只有交叉模型一致性——让足够多不同模型一起错——才能自动发现改写自身的问题。

同样的质量审计方法被外推到 MathCheck——100% 召回——即所有手动确认的改写错误都被交叉模型一致性自动标记了。无一漏网。

5. 🛠️ FormInvSelector：帮选模型的小工具

论文没有停留在批评。他们把数据变成了一个实用的命令行工具——FormInvSelector。

一个实际场景：你是一家公司，需要部署一个做数学推理的 AI。你的业务场景是"定义展开"类型的推理（F7）——把专业术语替换成它的定义。你输入 forminv selector --families unpack，它告诉你：首选 o4-mini（2.0% 失败），次选 Gemini 2.5 Flash（2.1%）。如果你选 GPT-4o——在通用基准上可能更高的模型——你在 F7 上的失败率是 5.0%，接近 2.5 倍。

反过来，如果你的业务场景是"比较方向"类型（F6）——你的用户经常换不等号的方向——那 Claude 的 16.7% 失败率意味着每 6 次推理就有一次被符号写法干扰。你该选 GPT-4o（0%）。

FormInv 不告诉你哪个模型"最好"。它告诉你哪个模型最适合你的实际输入分布。

6. 📝 诚实的盲区

我清楚的是：

• 8 个改写族的分类有明确的认证层级——T1 族可形式化验证（CAS/Lean4），T2 族有模板保证，T3 族有人工全量审核。不是猜测，是审计。
• 103 个定理来自 Mathlib4 的形式化定理库——不是人工编造的应用题。这意味着"正确答案"是定理本身，不需要人工标注 ground truth。
• 交叉模型一致性作为改写质量审计——在 FormInv 和 MathCheck 的独立验证中分别达到 100% 召回——有坚实的实证支撑。
• 无免费基准推论有严格的数学支撑：8 个改写族、9 个模型、无 Pareto 占优者 → 任何排名都对应某组权重。这不等同于"排名是随机的"——它意味着排名对改写族的选取是敏感的。

我不清楚的是：

• 103 个定理能代表"数学推理"吗？ 这些定理来自 Mathlib4 的本科级数论、代数、实分析——覆盖了形式化定理证明的典型类型，但离"应用题推理"（如 GSM8K 的风格）有距离。如果扩展到更大、更多样化的定理集，SCR 分布会变成什么样——论文做了 100 个更难的 ntp-mathlib 定理的初步测试（Track B），相关性下降但不显著（p=0.27），暗示结论对难度区间有依赖。
• 8 个改写族是否穷尽了"语义等价改写"的空间？ 论文显然回答"否"。T3 族的启发式认证层级本身就是对这个限制的承认——还有很多可能的改写方式（跨语言、跨文化背景、跨表示系统）没被捕获。如果加入更多改写族，当前的 Pareto 格局是否会变——未知。
• 交叉模型一致性审计的假阳性率？ 论文报告的是真阳性召回率（100%），但≥6/9 的阈值是否在更大规模测试中产生大量假阳性（把模型真的能力缺陷误判为改写错误），没有被充分评估。在 FormInv 自己的数据上看起来干净，但不能排除外推风险。
• SCR 和真实世界表现的关系？ 论文证明了 SCR 在改写层面的测量有效性——但它没有证明 SCR 预测下游任务表现的增量效力。一个 SCR 50% 的模型和一个 SCR 82% 的模型，在真实的数学解题场景中到底差多少——这个转化函数还没有。

7. 🏁 看不见的变量

这篇论文的名字叫 FormInv——"形式不变性"。但它真正在说的是一个更古老的道理：测量的质量取决于你是否测量了正确的变量。

AI 基准测试行业在这件事上有一个系统性的盲区。一个基准声明"模型 X 在数学推理上优于模型 Y"时，它只测量了一个变量：准确率。它没有测量——甚至没有考虑——另一个变量：语义表述的等变性。但数学推理的实质恰恰是"从任何语义等价表述中抽取相同的逻辑结构"——如果你只能在特定符号排列上正确推理，你就没有真正理解你推理的对象。

FormInv 用 Lean4 验证的定理作为 ground truth，用 8 个改写族作为形式等价性的压力测试，用交叉模型一致性作为改写质量的审计工具。它把数学模型评估从"这个模型答对了多少题"推进到了"这个模型的理解是否独立于表达"。

论文没有给出哪个模型是"最好的"。它给出了一个更残酷但更诚实的答案：你问的是什么改写族？你的输入分布长什么样？你确定你的基准改写本身没有错误吗？

前两个问题大多数基准测试从来没问过。第三个问题我们甚至不知道需要问——直到 FormInv 演示了答案可以是 47%。

项目	内容
论文标题	FormInv: A Measurement Protocol for Semantic Invariance in Mathematical Reasoning Benchmarks
作者	Nishal Thomas（独立研究者）、Noel Thomas（MBZUAI）
arXiv ID	2605.29001
分类	cs.LG; cs.AI，投稿 ICML 2026 AI4Math Workshop
核心贡献	(1) 发现 32 点 SCR 鸿沟——准确率仅差 10pp 的模型，语义一致性可差 32pp；(2) 证明模型排名在不同改写族之间系统性逆转——无免费基准推论；(3) 提出并验证交叉模型一致性作为自动化改写质量审计（100% 召回，<10 美元成本）；(4) 发现自动改写有 47% 语义错误；(5) 发布 FormInvSelector 工具，支持改写族感知的模型选择；(6) 将测量不变性理论引入 LLM 数学推理评估
关键局限	103 个定理在覆盖度上有限（主要本科级定理）、8 个改写族未穷尽语义等价空间、交叉模型一致性审计的假阳性率外推未知、SCR 到下游任务表现的转化函数未建立、Track B 扩展测试提示结论有难度区间依赖性

参考文献：

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.

#基准测试 #数学推理 #语义不变性 #测量理论 #FormInv #模型评估 #改写审计 #智柴