ClaimScope: Label-Blind Witness Verification for More Reliable Mathematical Claim Auditing

When large models do math problems, we usually check whether the answer is correct, or whether the proof is acceptable. But in reality there is a trickier kind of work—auditing mathematical claims proposed by others: Does this conclusion hold? Within what scope does it hold? If it's wrong, what is the counterexample? Can it be fixed?

A new paper introduces ClaimScope, a benchmark of 72 tasks specifically designed to evaluate a model's ability to audit mathematical claims. It requires the model to output four things: a verdict, a scope of applicability, a counterexample, and a repair. This seemingly simple quadruple actually completely separates "classification" from "executable evidence."

Task Design: Three Types of Mathematical Scenarios, 72 Auditing Targets

ClaimScope covers three types of problems: optimizer state transfer, finite-horizon affine recurrence, and exact 2×2 linear algebra. All three share a common characteristic: the correctness of a claim does not rely on intuition, but on verifiable structure.

For example, "optimizer state transfer" involves whether momentum and second-moment estimates are equivalent when migrated across different devices or different step counts; affine recurrence examines whether the closed-form expression after several recurrence steps is correct. Claims often carry parameters, and when boundary conditions change, correctness can flip.

This design makes "true or false" no longer a label, but a judgment process that requires constructing evidence. Once a model gives only a verdict without a witness, it is hard to tell whether it truly understands the scope.

Label-Blind Witness Verification: Only Checking the Submitted State

The core mechanism of the paper is a label-blind witness checker. It only looks at the state submitted by the model, does not reference the verdict in the reference answer, and does not provide an alternative witness. In other words, the checker does not "tell" the model the correct answer; it only performs structural validation on the submitted evidence.

This setup is restrained, but the feedback still carries information: a verified refutation proves that the claim is false; and the reason for rejection often hints at how the structure could be fixed. In other words, what the model receives is not "you're right/you're wrong," but "at which step your evidence broke down."

This is fundamentally different from common self-reflection prompting. The latter usually gives a vague "please check again," while the former gives a judgment result targeting the specific witness.

Witness is a core concept in computational complexity theory: when proving that a claim is true or false, in addition to giving the conclusion, one must attach a certificate that can be independently and quickly verified. For example, to prove "there exists a solution satisfying the conditions," the witness is the specific solution itself, and the verifier only needs to plug it in and check; to prove "the claim is false," the witness is a specific counterexample. The key feature of a witness checker is soundness: it only accepts witnesses that can be mechanically verified, regardless of the identity or confidence of the proposer. This is completely different from neural-network-style "scoring" or "probability judgment"; it is binary and reproducible. Therefore, when a model submits an accepted counterexample, this result is logically forced to hold, and does not depend on whether the checker "believes" the model. ClaimScope adopts a label-blind design precisely to avoid leaking the reference answer's verdict to the model, thereby measuring the model's ability to independently construct valid witnesses.

Experimental Comparison: Verifier Feedback vs. Generic Feedback Without a Checker

The paper uses Qwen3-8B for direct generation, as well as four paired two-turn conditions, each starting from the same draft.

Key data: on invalid claims, verifier feedback yields 23/39 accepted counterexamples, while generic feedback without a checker yields only 15/39. For safe completion, the former is 25/72, the latter 20/72. Strict completion remains 17/72; verdict accuracy goes from 47/72 to 46/72, essentially unchanged.

This set of numbers is interesting: verdict accuracy did not improve, but counterexamples and safe completion both increased. This shows that verifier feedback truly improves the witness structure, not the claim classification ability.

The safe-completion difference grouped by claim is .094, with a bootstrap 95% interval of [.000, .198], the lower bound just touching the line. The seven gains at the task level are all consistent with the direction of horizon or input-length diagnostics.

Another intriguing finding: applying a single post-hoc schema-only correction to the direct output, without calling the model again, also achieves the same 25 safe tasks. This means that part of the gain may come from regularizing the output format, rather than from improvements in deep reasoning.

Bootstrap confidence interval is a statistical inference method that does not rely on distributional assumptions: by repeatedly resampling from the original sample with replacement (for example, 10000 times), re-estimating the statistic (here, the between-group difference in safe-completion), and taking quantiles to obtain the interval. When the lower bound of the interval is exactly .000, it means that at the 95% confidence level, the observed difference is "just" indistinguishable from the null hypothesis, i.e., the boundary of significance is very fragile. This is common when the sample size is only 72: the point estimate may look considerable (.094), but the uncertainty is large. The paper honestly reports this interval, showing that the authors remain cautious about the conclusion and did not exaggerate a directional gain on a small sample into a robust conclusion. Readers interpreting such small-benchmark results should also focus on confidence intervals rather than only point estimates.

Multi-Source Observations and Boundaries: Gains Come from Witness Structure, Not a Reasoning Leap

From the experimental design, ClaimScope's contribution is more about breaking "claim auditing" into measurable components: verdict, scope, counterexample, repair. It does not claim that the model has become smarter; instead, it clearly locates the observed gains in witness-structure correction.

This also explains why verdict accuracy remains almost unchanged. The model could already roughly classify right and wrong, but once it is required to give an executable counterexample or repair, its ability is exposed. The value of the verifier is that it forces the model to make implicit judgments explicit as structure, rather than doing reasoning for the model.

For those evaluating mathematical agents, this suggests a direction: beyond answer accuracy and proof acceptance rate, perhaps "audit quality" should be measured separately. And the fact that schema-only correction can achieve the same effect also reminds us to be wary of misreading format gains as reasoning gains.

Schema-only post-hoc correction refers to, without calling the model to generate new content, only performing structured parsing and format normalization on existing output (such as realigning the verdict, scope, and counterexample from free text into prescribed JSON fields), and then handing it to the verifier. One explanation for why it can achieve safe-completion counts comparable to verifier feedback is: the model's original output actually already contains the correct counterexample or repair content, but the format is messy and causes rejection; normalization makes this implicit information explicit. Another explanation is that verifier feedback itself mainly imposes format constraints, rather than providing new reasoning signals. Both explanations point to the same methodological warning: when evaluating "reasoning ability," the gain brought by format compliance must be separated out, otherwise it is easy to mistake parsing gains for cognitive leaps. Ablations can be designed, such as fixing the format but giving no feedback, to distinguish these two types of contributions.

One-line Summary

ClaimScope evaluates mathematical claim auditing with 72 tasks and a label-blind witness checker, finding that gains come from witness structure rather than reasoning ability.

Paragraph Summary

ClaimScope is a benchmark of 72 tasks specifically designed to evaluate large models' ability to audit mathematical claims, requiring the model to simultaneously output a quadruple of verdict, scope of applicability, counterexample, and repair. Its core mechanism is a label-blind witness checker: it only looks at the executable evidence submitted by the model, does not reveal the reference answer, and does not provide an alternative witness. Experiments on Qwen3-8B show that verifier feedback obtains 23/39 accepted counterexamples on invalid claims, significantly higher than the 15/39 from generic feedback without a checker; safe completion rises from 20/72 to 25/72, but verdict accuracy remains almost unchanged (47/72 to 46/72). Based on this, the authors point out that the gains come from witness-structure correction rather than improvements in classification or reasoning ability, and remain cautious about the significance boundary on small samples.