ClaimScope improves verification of mathematical claim audits
ClaimScope: Label-Blind Witness Verification for Mathematical Claim Auditing
Artificial IntelligenceMachine Learning
Summary
Checking if mathematical claims or proofs are correct is tricky. The authors introduce ClaimScope, a set of 72 tasks that require models not only to judge claims as true or false but also to provide supporting evidence or fixes when claims fail. Their tests show that having a specialized checker that verifies these supporting pieces helps models find more accurate counterexamples and safe claim completions. However, the improvement mainly comes from better handling of the evidence’s structure rather than overall reasoning skills.
What this means in practice
- •For automated theorem proving teams: Use ClaimScope to better audit mathematical claims by generating and verifying detailed evidence instead of only accepting or rejecting proofs.
- •For mathematics software developers: Incorporate witness checking to improve error detection and suggest repairs in symbolic math software handling linear algebra and recurrence relations.
Authors
Mushir Akhtar
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.