ClaimScope: Label-Blind Witness Verification for Mathematical Claim Auditing
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 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 accepted counterexamples on invalid claims and safe completions, compared with and for checker-free generic feedback. Strict completion remains ; verdict accuracy changes from to . The claim-grouped safe-completion difference is , with a bootstrap 95% interval of . 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.
Figures & tables
| Family | Tasks | Valid / invalid | Groups | Witness check |
|---|---|---|---|---|
| Optimizer transport | 24 | 9 / 15 | 24 | numerical updates |
| Affine recurrence | 24 | 12 / 12 | 16 | exact unrolling |
| Linear algebra | 24 | 12 / 12 | 8 | exact matrix identities |
| Total | 72 | 33 / 39 | 48 |
| Field | Check and limitation |
|---|---|
| Verdict | Valid or invalid, compared with the algebraically audited reference. |
| Scope | Canonical target: optimizer direction or full transition, finite-horizon value, or matrix identity. No open-ended theorem-strength comparison. |
| Repair | Canonical correction named in the prompt, or none for a valid claim. Equivalent free-form formulas and alternative restrictions receive no automatic equivalence credit. |
| Failure mode | Canonical diagnostic label. Required for strict, but not safe, completion because different descriptions can identify the same defect. |
| Counterexample | For an invalid claim, parse the state, enforce assumptions, and recompute both expressions. Reported expected/actual values are not trusted. For a valid claim, require null. |
| Condition | JSON | Verdict | Cex | Non-null | Safe | Strict |
| /72 | /72 | /39 | /33 | /72 | /72 | |
| Direct | 72 | 46 | 15 | 26 | 18 | 15 |
| Self-reflection | 70 | 44 | 12 | 26 | 15 | 13 |
| CE-guided | 72 | 46 | 14 | 26 | 17 | 14 |
| Generic feedback | 71 | 47 | 15 | 24 | 20 | 17 |
| Verifier feedback | 71 | 46 | 23 | 25 | 25 | 17 |
Appendix figures & tables7 assets
Supplementary material from the paper’s appendix.
Appendix
| Condition | Invalid /39 | Valid /33 | Optimizer /24 | Recurrence /24 | Matrix /24 |
|---|---|---|---|---|---|
| Direct | 11 | 7 | 4 | 1 | 13 |
| Self-reflection | 8 | 7 | 3 | 1 | 11 |
| CE-guided | 10 | 7 | 4 | 1 | 12 |
| Generic feedback | 11 | 9 | 4 | 3 | 13 |
| Verifier feedback | 18 | 7 | 4 | 8 | 13 |
| Feedback | Valid claim | Invalid claim | Total |
|---|---|---|---|
| Verified refutation | 0 | 15 | 15 |
| Rejected: horizon/input-length mismatch | 12 | 9 | 21 |
| Rejected: non-refutation | 14 | 15 | 29 |
| Not applicable | 7 | 0 | 7 |
| Condition | V V | V I | V M | I V | I I | I M |
|---|---|---|---|---|---|---|
| Direct | 7 | 26 | 0 | 0 | 39 | 0 |
| Self-reflection | 7 | 26 | 0 | 0 | 37 | 2 |
| CE-guided | 7 | 26 | 0 | 0 | 39 | 0 |
| Generic feedback | 9 | 24 | 0 | 1 | 38 | 0 |
| Verifier feedback | 7 | 25 | 1 | 0 | 39 | 0 |
| Metric | ||||
|---|---|---|---|---|
| Verified invalid-claim witness | 16 | 8 | 0 | 15 |
| Safe completion | 45 | 7 | 2 | 18 |
| Strict completion | 53 | 2 | 2 | 15 |
| Verdict correct | 24 | 1 | 2 | 45 |
| Condition | Verdict | Safe | Strict |
|---|---|---|---|
| Direct | .632 | .184 | .122 |
| Self-reflection | .590 | .149 | .108 |
| CE-guided | .632 | .177 | .115 |
| Generic feedback | .642 | .205 | .142 |
| Verifier feedback | .632 | .299 | .153 |
| Always valid | .417 | .417 | .417 |
| Component | Setting |
|---|---|
| Model | Qwen/Qwen3-8B |
| Revision | b968826d9c46dd6066d109eabc6255188de91218 |
| Quantization | 4-bit NormalFloat; model thinking mode off |
| Decoding | Temperature 0; at most 512 new tokens per call |
| Hardware | One NVIDIA RTX A4500 |
| Runtime | PyTorch 2.12.1+cu126; Transformers 5.16.1; CUDA 12.6 |
| Condition | Model calls | Output tokens | Seconds |
|---|---|---|---|
| Direct | 72 | 8,719 | 853.9 |
| Self-reflection | 144 | 17,457 | 1,757.5 |
| CE-guided | 144 | 17,418 | 1,744.9 |
| Generic feedback | 144 | 17,367 | 1,772.3 |
| Verifier feedback | 144 | 17,436 | 1,672.4 |
LLM Mathematical Reasoning
Large language model mathematical reasoning studies how AI systems solve, explain, verify, and generalize across mathematical problems and proofs.
See all 270 papers