Source-linked AI summary
ClaimScope: Label-Blind Witness Verification for Mathematical Claim Auditing
Mushir Akhtar
TL;DR
Mathematical claim audits must assess validity, scope, failure reasons, and repairs, beyond final-answer accuracy or proof acceptance. ClaimScope benchmarks structured local-claim audits and checks model-proposed witnesses; verifier feedback increases accepted counterexamples and safe completions versus generic feedback, but the gains do not establish broader reasoning improvement.
Problem
Example agreement can conceal errors in universal claims, motivating audits that assess validity, justified scope, failure reasons, and repairs.
Source: §1 · p. 1Method
ClaimScope provides a 72-task benchmark and checks model-proposed witnesses without consulting reference verdicts or supplying replacement witnesses or repairs.
Source: §1 · p. 2Results
Verifier feedback raises accepted counterexamples from 15/39 to 23/39 and safe completions from 20/72 to 25/72, while verdict accuracy changes from 47/72 to 46/72.
Source: §3 · p. 4Takeaways & Limitations
The observed gains are located in witness-structure correction, not evidence that verification alone improves general mathematical reasoning.
Source: §5 · p. 5The benchmark is small and synthetic, and the study evaluates one quantized model with a short deterministic output budget.
Source: §4 · p. 5
Abstract
from arXiv · showhide
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.
1 Introduction
Auditing mathematical claims requires checking validity, justified scope, failure reasons, and repairs, because example agreement can conceal universal-statement errors. ClaimScope structures local-claim audits around model-proposed witnesses, which a checker validates without searching for or supplying a replacement.
1 Introduction
- Example agreement can conceal errors in quantifiers, singular cases, or whether an update direction equals a complete transition.A useful audit identifies the missing condition, gives a failing parameter state, and specifies a correction.Source: §1 · p. 1
- Existing benchmarks emphasize solution accuracy, formalization or proof, counterexamples, or diagnosis of synthetic errors rather than this structured local-claim audit.The paper situates these endpoints with MATH [Hendrycks et al., 2021], GSM8K [Cobbe et al., 2021], miniF2F [Zheng et al., 2021], LeanDojo [Yang et al., 2023], ProofNet [Azerbayev et al., 2023], AlphaGeometry, COUNTERMATH [Li et al., 2025], and MathDebugger [Liang et al., 2025].Source: §1 · p. 1
- ClaimScope checks a model-proposed witness rather than searching for or supplying a replacement, distinguishing who constructs the evidence from whether feedback informs the answer.A verified counterexample implies invalidity, while a rejected witness establishes neither truth nor falsity; diagnostic rejection can suggest a witness fix.Source: §1 · p. 2
- The work contributes a 72-task benchmark, a witness-checking protocol with an explicit information boundary, and paired analysis of classification, executable evidence, and complete audits.Constant policies, claim-grouped uncertainty, and schema-only analysis are used to distinguish structural correction from stronger mathematical reasoning.Source: §1 · p. 2
2 Benchmark and protocol
The benchmark tests local claims across three mathematical families, with references validated algebraically rather than by agreement on a finite diagnostic grid. Its protocol specifies the audit fields, safe-completion checks, and matched revision conditions, including feedback from checking the model's submitted witness.
2 Benchmark and protocol
- The 72-task benchmark has 24 tasks each for optimizer-state transport, affine recurrences, and linear algebra.Its optimizer claims vary learning-rate scaling, bias correction, stabilizer placement, decay semantics, and direction versus complete update; other tasks cover finite-horizon unrolling, indexing, singularity, and matrix identities.Source: §2 · p. 2, Table 1 · p. 2
- Reference validity follows algebraic identities under stated assumptions, with computationally verified admissible counterexamples for every invalid claim.Optimizer transports are checked by symbolic substitution; recurrence and matrix cases use standard finite-sum and matrix identities.Source: §2 · p. 2
- Each response reports an identifier, verdict, scope, failure mode, counterexample, and repair; scope names the designated evaluation target rather than the strongest possible theorem.The prompt supplies the claim, assumptions, allowed labels, and witness schema, but no answer key.Source: §2 · p. 2
- Safe completion requires valid structured output, correct identifier and verdict, reference scope and repair, and the required witness condition.Invalid claims require a verified refutation and valid claims a null witness; strict completion additionally requires the reference failure-mode label.Source: §2 · p. 3
- Each revision condition uses the same draft and one review call, while verifier feedback reports the check of the submitted state without a replacement witness or repair.The checker can return verified, rejected with a reason, or not applicable; a rejection reason may identify a horizon/input-count mismatch.Source: §2 · p. 3
3 Experiment
In this fixed Qwen3-8B evaluation, verifier feedback improves accepted counterexamples and safe completions over generic feedback, but not verdict accuracy or strict completion. The gains track witness-structure corrections, and a schema-only rule recovers the same safe-task count.
3 Experiment
- All five conditions use the same 72 prompts, and each two-pass draft is byte-identical to its direct counterpart.Each revision condition uses 144 calls versus 72 for direct generation; generic feedback is the closest checker-free control in budget and review wording.Source: §3 · p. 3
- .094 is the claim-grouped safe-completion difference for verifier versus generic feedback, with a 95% interval of [.000, .198].Six groups improve, one declines, and 41 do not change; the interval includes zero.Source: §3 · p. 4
- Accepted counterexamples on invalid claims rise from 15/39 to 23/39, while safe completions rise from 20/72 to 25/72.Strict completion remains 17/72, and verdict accuracy changes from 47/72 to 46/72.Source: §3 · p. 4, Table 3 · p. 4
- An always-valid policy with null witnesses and copied scope and identifier reaches 33/72 safe completions, exceeding every model condition.Valid claims do not require a proof in this benchmark, so safe completion alone is not a standalone measure of reliable mathematical reasoning.Source: §3 · p. 4
- All seven gains over generic feedback follow rejection of a horizon/input-length mismatch; 26 of 27 verifier revisions change only the counterexample field.Family-level safe counts for direct/generic/verifier feedback are 4/4/4 for optimizer transport, 1/3/8 for recurrences, and 13/13/13 for linear algebra, each out of 24.Source: §3 · p. 4
- A post-hoc schema rule that resets mismatched recurrence horizons to input-list length reaches the same 25 safe tasks as verifier feedback.It changes 21 direct-output records and recovers the same seven gains without a model call; it is not a prospective baseline or binary-feedback ablation.Source: §3 · p. 4
4 Discussion and limitations
The study isolates validation of model-proposed witnesses from checker-driven counterexample search, but its diagnostic feedback still conveys information about validity. Its results are limited by a small synthetic benchmark, one quantized model, and restricted task and scoring scope.
4 Discussion and limitations
- Verifier feedback is not verdict-blind: verified states entail false claims, while rejection reasons can provide diagnostic hints.A binary-only condition would be needed to isolate the value of status alone.Source: §4 · p. 5
- The benchmark is small and synthetic, uses one quantized model with a short deterministic output budget, and does not establish behavior on unseen mathematical families.The study also does not demonstrate open-ended theorem proving or optimizer performance in training.Source: §4 · p. 5
- Repeated formulas limit independence, while canonical scope and repair labels can reject an alternative mathematically sound repair.Numerical optimizer validation is tolerance-based, unlike the exact recurrence and matrix checks.Source: §4 · p. 5
- The paper identifies larger independent claim sets, semantic repair checking, and proof obligations for valid claims as important directions.Source: §4 · p. 5
5 Conclusion
The conclusion characterizes the observed gains as witness-structure correction, not broader mathematical reasoning improvement.
5 Conclusion
- Verifier feedback yields more accepted counterexamples and safe completions than matched generic feedback, without better verdict or strict-completion scores.Source: §5 · p. 5
- The claim-grouped uncertainty includes no improvement, and schema-only correction recovers the same safe-task set.Source: §5 · p. 5
- The evaluation is fixed to Qwen3-8B, and its clearest result is a witness-structure correction effect.Source: §5 · p. 5
A.1 Reference validation and admissible counterexamples
Reference validation checks optimizer claims against update discrepancies and verifies admissible counterexamples, while recurrence and matrix claims rely on exact identities under their required conditions.
A.1 Reference validation and admissible counterexamples
- For optimizer transitions, matching step directions can still leave a decay discrepancy; matching the full transition requires matched decay or an appropriate transport.For direction claims, the comparison is A = (α/η)D, equivalently ηA = αD.Source: §A.1 · p. 7
- All nine valid optimizer specifications reduce identically to zero, while each of the other 15 has a verified admissible state.The check substitutes candidate formulas and stated constraints into the appropriate discrepancy, rather than testing a finite grid.Source: §A.1 · p. 7
- Invalid optimizer examples use admissible parameter states to expose failures in decay matching, learning-rate scaling, or decay compensation.The examples distinguish direction transport from full-transition transport.Source: §A.1 · p. 7
- Recurrence and matrix specifications use exact finite-sum and matrix identities, with the ρ = 1 case handled separately and inverse checks requiring invertibility.All invalid claims across the families have exact rational witnesses in the published schema.Source: §A.1 · p. 7
A.2 Recorded worked example
The worked recurrence example shows how a checker rejection can identify an inconsistent horizon and input list, enabling a witness-structure correction.
A.2 Recorded worked example
- For PILOT-REC-023, rejection identifies that horizon 2 conflicts with one supplied input; adding a second input produces the verified refutation 7 ≠ 10.Changing the horizon to 1 also refutes the claim, so the model’s final witness is not the only admissible structural correction.Source: §A.2 · p. 7
A.3 Scoring contract
The scoring contract defines safe completion as structured compliance with the audit specification, while clarifying that agreement on labels is not unrestricted semantic assessment.
A.3 Scoring contract
- Safe completion requires valid structured output, the correct identifier and verdict, reference scope and repair, and the specified witness condition.Strict completion additionally requires the reference failure-mode label.Source: §A.3 · p. 8
- Scope and repair agreement do not establish unrestricted semantic correctness: a verified witness does not certify the repair, and the canonical repair may not be unique.Optimizer, recurrence, and matrix witnesses use scalar states, rational initial states and input lists, and rational 2 × 2 arrays, respectively.Source: §A.3 · p. 8
- The isolated witness flag treats a missing witness like null on valid claims, but safe completion still requires parseable structured output.An always-null policy meets the isolated witness requirement on 33/72 tasks but verifies no invalid claim.Source: §A.3 · p. 8
- Table 4 separates safe completion by reference verdict and task family.The caption identifies the comparison dimensions, not the table’s values.Source: Table 4 · p. 8
A.4 Feedback information and revision traces
Verifier feedback checks model-submitted states without using stored reference labels; revisions change witnesses more often than verdicts, and observed gains are concentrated in specific diagnostic cases.
A.4 Feedback information and revision traces
- The checker’s feedback is label-blind in implementation, but a verified witness logically implies an invalid claim and rejection reasons can suggest witness fixes.The implementation does not consult stored reference verdicts, repairs, failure modes, or witnesses when preparing review messages.Source: §A.4 · p. 8
- Table 5 stratifies draft feedback by audited reference verdict; non-refutation means the submitted state does not disprove the claim under its assumptions.The supplied caption identifies the stratification but does not state table outcomes.Source: Table 5 · p. 8
- Among invalid claims, accepted witnesses increase from 15 to 23, while no well-formed final revision changes a draft verdict.All 39 invalid claims already have invalid draft verdicts, and none of the verifier responses corrects the verdict on the 26 valid claims mislabeled invalid.Source: §A.4 · p. 8
- The seven safe-completion gains over generic feedback follow horizon/input-length rejection, while two valid piecewise-geometric claims are losses.No gain follows only a non-refutation message; this is descriptive attribution, not an experiment separating diagnosis from status.Source: §A.4 · pp. 8–9
A.5 Paired and grouped results
The paired analysis finds a .09375 mean safe-completion difference, with a bootstrap interval that includes zero; a post-hoc schema-only correction reaches the same 25 safe tasks. Reproducibility checks support this finite benchmark, not a general proof system for arbitrary mathematical text.
A.5 Paired and grouped results
- The 48 claim groups comprise 24 optimizer specifications, 16 recurrence specifications, and eight matrix identities; groups may still share formulas and assumptions.Prompt scores are averaged within groups, then group averages receive equal weight.Source: §A.5 · p. 9
- .09375 is the mean paired safe-completion difference across 48 groups; the 95% bootstrap interval is [.000, .198], with six groups improving, one declining, and 41 unchanged.The schema-only rule was chosen after inspecting saved feedback, and no independent-task significance claim follows from these data.Source: §A.5 · p. 9
- A post-hoc rule matching horizon to input-list length reaches the same 25 safe task identifiers as verification, without running a checker or consulting a label.The final witnesses need not be equal.Source: §A.5 · p. 9
A.6 Configuration, cost, and reproducibility
- Label-free feedback reproduction preserves the messages received by the model; reanalysis scripts score saved outputs without inference, and checks support this finite benchmark rather than arbitrary mathematical text.The original reference is preserved alongside the audited reference so label changes and aggregates can be traced to individual tasks.Source: §A.6 · p. 10