ClaimScope: Label-Blind Witness Verification for Mathematical Claim Auditing

AI summary

Overview

Research area: Evaluation of large language models on mathematical reasoning, specifically the design of benchmarks and verification protocols for auditing already-stated mathematical claims.

Technical level: Intermediate. Readers should be comfortable with LLM benchmarking, pass/fail scoring conventions, and basic optimization and linear-algebra notation, but the paper is written in an unusually plain style for a reasoning benchmark paper.

Scope: The paper introduces ClaimScope, a 72-task benchmark with a checker that validates model-proposed counterexamples without access to reference labels, and reports a paired evaluation of Qwen3-8B under five generation conditions.

What This Paper Is About

Mathematical agents are usually graded on final-answer accuracy or on whether a proof is accepted, but a useful audit of a claim also needs to say how far the claim holds, why it fails, and how to repair it. ClaimScope turns this into a structured task: given a claim and its assumptions, the model must produce a verdict, a scope, a failure mode, a counterexample, and a repair, and a checker then recomputes the model's submitted witness rather than searching for one itself.

The paper's central question is whether feedback from such a checker helps a model revise its audit better than generic "your witness may be wrong" feedback, when both conditions get the same draft and the same number of model calls. The answer is a narrow yes on witness structure and accepted counterexamples, but not on verdict accuracy or strict completion, and the authors are careful to argue that the gain is a correction effect rather than evidence of better mathematical reasoning.

Key Contributions

1. A 72-task auditing benchmark with executable counterexample validation. Three families of 24 tasks each (optimizer-state transport, finite-horizon affine recurrences, exact 2×2 linear algebra), containing 33 valid and 39 invalid claims organized into 48 formal claim groups. Invalid claims are backed by computationally verified witnesses, and reference validity rests on algebraic identities rather than agreement on a finite diagnostic grid.

2. A label-blind witness-checking protocol with a stated information boundary. The checker returns verified, rejected, or not applicable on the model's own submitted state. It never supplies a replacement witness, repair, or proof, and it does not consult the stored reference verdict, repair, or diagnostic label. The authors explicitly note that this is label-blind but not verdict-independent, since a verified refutation logically implies the claim is false.

3. A paired analysis that separates classification, executable evidence, and complete structured audits. All five conditions use the same 72 prompts, and every two-pass draft is byte-identical to its direct counterpart, so revision conditions use 144 calls against 72 for direct generation. The analysis includes claim-grouped uncertainty, deterministic constant policies, and class-conditional metrics.

4. A schema-only post-hoc analysis testing whether the gains require verification at all. A single deterministic rule applied to direct outputs (set the reported horizon to the input-list length when they disagree) reaches the same 25 safe tasks as verifier feedback, without another model call.

Main Findings

• More accepted counterexamples. Verifier feedback produces 23/39 verified counterexamples on invalid claims, versus 15/39 for checker-free generic feedback.

• More safe completions, but no change in strict completion. Safe completion rises from 20/72 (generic) to 25/72 (verifier), with seven gains and two losses. Strict completion stays at 17/72 for both conditions.

• Verdict accuracy does not improve. It moves from 47/72 under generic feedback to 46/72 under verifier feedback. The direct drafts label all 39 invalid claims invalid but also reject 26 of the 33 valid claims, so the bottleneck is recognizing true claims, not finding more refutations.

• The claim-grouped difference is not statistically conclusive. Grouped safe completion is .205 for generic feedback and .299 for verifier feedback, a difference of .094, with a 10,000-sample paired bootstrap 95% percentile interval of [.000, .198]. Six groups improve, one declines, and 41 do not change.

• Gains are concentrated in one failure signature and one family. All seven gains over generic feedback follow a rejection message identifying a horizon/input-length mismatch; none follows only a non-refutation message. Family-level safe counts for direct/generic/verifier are 4/4/4 for optimizer transport, 1/3/8 for recurrences, and 13/13/13 for linear algebra, each out of 24.

• Revisions touch only the witness. Of 27 verifier-condition revisions, 26 change only the counterexample field and one produces no parseable audit. No parseable revision changes the verdict.

• Class-conditional effects move in opposite directions. Among invalid claims, safe completion rises from 11/39 (generic) to 18/39 (verifier); among valid claims it falls from 9/33 to 7/33. The two safe losses, PILOT-REC-004 and PILOT-REC-017, are valid piecewise-geometric claims that generic feedback accepts and verifier feedback continues to reject.

• Trivial policies beat every model condition on the headline metric. An always-valid policy that copies the prompt's scope and identifier, emits a null witness, and selects no repair or failure mode obtains 33/72 safe completions, exceeding all model conditions. An always-invalid policy scores 39/72 verdicts. The authors use this to argue that safe completion must be read alongside counterexample and classification scores.

• Rejection is informative but not a disguised label. In the saved drafts, all 15 verified states belong to invalid claims; the 21 horizon/input-length rejections split into 12 valid and nine invalid claims, and the 29 non-refuting states split into 14 valid and 15 invalid claims.

• A deterministic rule reproduces the result. The schema-only correction applied to direct outputs changes 21 records and reaches the same 25 safe tasks as verifier feedback, including the same seven gains over direct generation, though the final witnesses need not be equal.

• Cost is doubled for a small effect. Direct generation used 72 model calls, 8,719 output tokens, and 853.9 seconds of host-measured generation time; verifier feedback used 144 calls, 17,436 output tokens, and 1,672.4 seconds.

Methodology in Plain English

The authors built three families of small, precisely specified mathematical claims. Optimizer tasks ask whether one can transport state between two optimizer formulations, varying learning-rate scaling, bias correction, stabilizer placement, decay semantics, and the difference between matching a gradient direction and matching a complete parameter update. Recurrence tasks ask about finite-horizon unrolling of an affine recurrence, including indexing and the singular case ρ = 1. Matrix tasks ask about determinant, inverse, trace, and transpose identities for 2×2 matrices.

Each claim's true label was established algebraically, not by testing examples. For optimizer claims, symbolically substituting the candidate transport into the update yields either an identically zero discrepancy or a refutable expression; all nine valid optimizer specifications reduce identically to zero, and each of the other 15 has a verified admissible state. Recurrence and matrix checks use exact rational arithmetic, while numerical optimizer checks use a relative tolerance of 10⁻¹⁰ and an absolute tolerance of 10⁻¹².

Each prompt gives the claim, assumptions, allowed labels, and the witness schema, but no answer key. The model must return a task identifier, verdict, scope, failure mode, counterexample, and repair. A checker then parses the submitted state, enforces the assumptions, and recomputes both sides of the claim, ignoring the model's reported expected and actual values. It replies verified, rejected, or not applicable, with a rejection reason such as "horizon must equal the number of supplied inputs."

Five conditions were compared on the same 72 prompts with Qwen3-8B (4-bit NormalFloat quantization, one NVIDIA RTX A4500, temperature zero, thinking disabled, at most 512 new tokens per call): direct generation; self-reflection; counterexample-guided revision; generic feedback that warns the witness may be wrong while stating that no checker supplies a task-specific signal; and verifier feedback. Scoring for "safe completion" is a conjunction of valid structured output, correct identifier and verdict, reference scope and repair, plus a verified refutation for invalid claims or a null witness for valid claims. Strict completion additionally requires the reference failure-mode label.

Why This Matters

The paper makes a methodological point that applies well beyond its own benchmark: finding more counterexamples is not the same as classifying claims correctly, and a headline "safe completion" number can be inflated by trivial behavior if valid claims require no proof. By reporting class-conditional counts, constant policies, and a deterministic schema-only baseline alongside the main comparison, the authors show how easily a verification result can be over-read. The explicit distinction between label-blind and verdict-independent checking is also a useful piece of vocabulary for anyone designing tool-use evaluations.

Real-world applications:

• Reviewing derivations and implementations in machine learning papers, where a claimed equivalence between two optimizer formulations may hold for the update direction but fail for the full transition because learning rates or weight-decay factors differ.
• Porting training code between frameworks, where an audit that exhibits a specific parameter state at which a proposed identity fails is more actionable than a pass/fail on a handful of runs.
• Internal technical review of reports and documentation, where claims are stated as universal but actually hold only under unstated conditions such as matched decay or restricted horizons.
• Educational feedback on mathematical statements, where identifying the missing condition and naming a repair is more useful to a learner than simply marking a claim false.

Industry relevance is mainly for teams building or evaluating reasoning agents: the result suggests that tool feedback of this kind yields structural corrections on a narrow class of errors, and that claims about "verification improving reasoning" should be tested against matched checker-free controls and doubled inference budgets.

Future Directions

• Isolate status from diagnosis. The authors state that a binary-only feedback condition would be needed to separate the value of a verified/rejected status from the informational content of specific rejection reasons; the current design confounds them.

• Scale up and diversify the claim set. The benchmark is described as small, synthetic, and limited to one quantized model with a short deterministic output budget. Repeated formulas across distinct assumptions limit independence, and the grouped interval includes zero, so larger independent claim sets and unseen mathematical families are needed.

• Replace canonical labels with semantic checking. Scope and repair are scored by normalized label comparison, so an alternative mathematically sound repair can fail. Semantic repair checking is named as an open direction.

• Add proof obligations for valid claims. Because valid claims currently require only a null witness, an always-valid policy reaches 33/72 safe completions; requiring proofs for valid claims would close this gap and make safe completion a stronger measure.

Target Audience

Researchers and practitioners working on LLM evaluation and mathematical reasoning will get the most from this paper, particularly those designing benchmarks that involve tool feedback, self-correction, or verifier-in-the-loop protocols. It is also relevant to ML engineers who need to audit equivalence claims when transferring optimizer state or porting training code, and to reviewers and reproducibility-focused readers interested in how to report class-conditional results and trivial baselines honestly. The writing is accessible to graduate students with basic familiarity with LLM benchmarking.

Authors’ abstract

Mathematical agents are commonly evaluated by answer accuracy or proof acceptance. We introduce ClaimScope, a 72-task benchmark for auditing proposed claims through a verdict, scope, counterexample, and repair. Tasks cover optimizer-state transport, finite-horizon affine recurrences, and exact $2\times2$ linear algebra. We evaluate Qwen3-8B with direct generation and four matched two-pass conditions, each starting from the same draft. A witness checker evaluates only the model's submitted state, without consulting reference verdicts or supplying a replacement witness. Its feedback still conveys information about validity: a verified refutation establishes that the claim is false, and rejection reasons can suggest structural fixes. In this evaluation, verifier feedback yields $23/39$ accepted counterexamples on invalid claims and $25/72$ safe completions, compared with $15/39$ and $20/72$ for checker-free generic feedback. Strict completion remains $17/72$; verdict accuracy changes from $47/72$ to $46/72$. The claim-grouped safe-completion difference is $.094$, with a bootstrap 95\% interval of $[.000,.198]$. All seven task-level gains follow horizon/input-length diagnostics. A post-hoc schema-only correction of the direct outputs reaches the same 25 safe tasks without another model call. These results separate claim classification from executable evidence, while locating the observed gains in witness-structure correction rather than demonstrating broader reasoning improvement.