ClaimScope：不看标签的见证验证，让数学命题审计更可靠

大模型做数学题，通常看答案对不对，或者证明能不能被接受。但现实中还有一类更棘手的工作——审计别人提出的数学命题：这个结论成立吗？在什么范围内成立？如果错了，反例是什么？能不能修正？

一篇新论文提出了 ClaimScope，一个 72 个任务的基准，专门用来评测模型对数学命题的审计能力。它要求模型输出四样东西：判定、适用范围、反例、修复方案。看似简单的四元组，实际上把"分类"和"可执行证据"彻底分开了。

任务设计：三类数学场景，72 个审计目标

ClaimScope 覆盖三类问题：优化器状态传输、有限时域仿射递推、以及精确的 2×2 线性代数。这三类都有共同特点：命题的正确性不靠直觉，而靠可验证的结构。

比如"优化器状态传输"涉及动量、二阶矩估计在不同设备或不同步数间的迁移是否等价；仿射递推则考察递推若干步后的闭式表达是否正确。命题往往带参数，边界条件一换，对错就可能翻转。

这种设计让"真假"不再是一个标签，而是一个需要构造证据的判定过程。模型一旦只给 verdict 而不给 witness，就很难判断它是否真的理解了范围。

标签盲的见证验证：只查提交的状态

论文的核心机制是一个标签盲（label-blind）的见证检查器。它只看模型提交的状态，不参考参考答案里的 verdict，也不提供替代的 witness。也就是说，检查器不会"告诉"模型正确答案，只会对提交的证据做结构性检验。

这种设置很克制，但反馈仍有信息量：一个被验证的反驳，证明了命题为假；而拒绝的理由，往往暗示了结构上可以怎么修。换句话说，模型得到的不是"你对/你错"，而是"你的证据在哪一步断了"。

这跟常见的自我反思提示有本质区别。后者通常给的是泛泛的"请再检查一遍"，而前者给的是针对具体 witness 的判定结果。

见证（witness） 是计算复杂性理论中的核心概念：当要证明某个命题为真或为假时，除了给出结论，还需要附带一个可被独立、快速检验的凭证。例如证明"存在满足条件的解"，witness 就是那个具体解本身，验证者只需代入检查；证明"命题为假"，witness 就是一个具体的反例。见证检查器的关键特征是健全性（soundness）：只接受能被机械验证的 witness，而不管提出者的身份或自信程度。这与神经网络式的"打分"或"概率判断"截然不同，它是二值的、可复现的。因此当模型提交一个被接受的反例时，这个结果在逻辑上是强制成立的，而不依赖于检查器是否"相信"模型。ClaimScope 采用标签盲设计，正是为了避免把参考答案的 verdict 泄漏给模型，从而测出模型独立构造有效见证的能力。

实验对比：验证器反馈 vs 无检查器的通用反馈

论文用 Qwen3-8B 做了直接生成，以及四种配对的两轮条件，每一轮都从同一个草稿出发。

关键数据：在无效命题上，验证器反馈得到 23/39 个被接受的反例，而无检查器的通用反馈只有 15/39。安全完成方面，前者 25/72，后者 20/72。严格完成仍然是 17/72；verdict 准确率从 47/72 变成 46/72，几乎没动。

这组数字很有意思：verdict 准确率没提升，但反例和安全完成都涨了。说明验证器反馈真正改善的是见证结构，而不是命题分类能力。

按 claim 分组的 safe-completion 差异为 .094，bootstrap 95% 区间是 [.000, .198]，下界刚好压线。任务层面的七项收益，全部跟 horizon 或输入长度诊断方向一致。

另一个耐人寻味的发现：对直接输出做一次后验的纯 schema 修正，不用再调一次模型，也能达到同样的 25 个安全任务。这意味着部分收益可能来自输出格式的规整，而非深层推理的提升。

Bootstrap 置信区间 是一种不依赖分布假设的统计推断方法：通过从原始样本中有放回地重复抽样（例如 10000 次），重新估计统计量（这里是 safe-completion 的组间差异），并取分位数得到区间。当区间下界恰好为 .000 时，意味着按 95% 置信水平，观测到的差异"刚好"与零假设不可区分，也就是差异显著性的边界非常脆弱。这在样本量仅 72 的情况下很常见：点估计看似可观（.094），但不确定性很大。论文如实报告这一区间，说明作者对结论保持审慎，没有把小样本上的方向性收益夸大为稳健结论。读者在解读此类小基准结果时，也应关注置信区间而非仅看点估计。

多源观察与边界：收益来自见证结构，而非推理跃迁

从实验设计看，ClaimScope 的贡献更多是把"命题审计"拆成了可测量的组件：判定、范围、反例、修复。它没有宣称模型变聪明了，反而明确把观测到的增益定位在witness-structure correction上。

这也解释了为什么 verdict 准确率几乎不变。模型原本能大致分类对错，但一旦要求给出可执行的反例或修复，能力就暴露了。验证器的价值在于迫使模型把隐含的判断显式成结构，而不是替模型做推理。

对做数学 agent 评测的人来说，这提示了一个方向：答案准确率和证明接受率之外，也许该把"审计质量"单独拿出来量。而 schema-only 修正能达到同等效果这一点，也提醒我们警惕把格式收益误读为推理收益。

Schema-only 后验修正 指在不调用模型生成新内容的前提下，仅对已有输出做结构化解析与格式规范（如把自由文本中的判定、范围、反例重新对齐到规定的 JSON 字段），再交给验证器。之所以能达到与验证器反馈相当的安全完成数，一种解释是：模型原始输出中其实已经包含了正确的反例或修复内容，只是格式散乱导致被拒绝；规整化把这些隐含信息显式化。另一种解释是验证器反馈本身就主要在施加格式约束，而非提供新的推理信号。两种解释都指向同一个方法论警示：在评测"推理能力"时，必须把格式合规带来的增益单独剥离，否则容易把解析收益误认为认知跃迁。可以设计 ablation，例如固定格式但不给反馈，来区分这两类贡献。