An error-hunting verifier (OSVerify) did not catch more bad proofs than a plain referee prompt, at about 7 times the cost

Last updated 2026-10-15

IRSI (irsi.ai). Negative result. Compute: Kimi K3 on AWS Bedrock, $133.76 metered for the whole project (pilot, calibration, failed attempts and the main run), at most $147.20 if every request abandoned after a hang was billed. The provider's bill cannot settle this: it covers the whole account, and on the day of the hangs it was $18 (4%) above the lab's own meter across all projects. Code and data: osverify-eval-bundle.zip (scrubbed bundle: frozen plan, harness code and prompts, item file, per-call and per-item run records, the analysis report and the independent checker).

Limits first

• Small test. The decision set has 15 bad proofs and 44 good ones. The 95% intervals on the differences between methods are about 30 percentage points wide either way. A real gain of 10 points would be invisible here. This is "no evidence of a gain", not "evidence of no gain". Even narrowing the interval to ±10 points would need roughly 9 times as many bad proofs; reliably detecting a 10-point gain would need roughly 18 times as many.
• One model, one setting. Every method ran on the same model (Kimi K3, low reasoning effort). The paper used gpt-oss-120b and gpt-5-mini. Other models or more reasoning may behave differently.
• Our reimplementation. The released OSVerify code is a Codex-CLI review tool. We could not find the paper's benchmarked pipeline (gpt-oss proposer and validator) in it, so we rebuilt the method from the paper's appendix (binary decomposition to depth 2, 16 validator votes per proposed error, the paper's appendix prompts plus one lab policy prompt; we simplified duplicate removal and used low reasoning effort; PREREG lists every deviation). A faithful-but-different implementation could score differently.
• Different material from the paper. The paper tests natural-language competition and research proofs graded by experts. We test Lean proofs and wrong competition answers, labelled by a machine: the Lean kernel accepts or rejects the proof, or the final answer is compared exactly with the official one. The checkers only read the text; none runs Lean.
• One item dropped. One good proof made OSVerify hang on every try (no reply in 30 minutes). It was dropped from all methods by a decision made during the run, before the results were computed; this is a recorded deviation from the frozen plan. Scoring it either way (accepted or wrongly rejected) leaves the verdict unchanged.
• Groups and sources. 3 of the 15 bad proofs are attempts at one open problem (Erdos problem 324), which every method rejects. Most good proofs come from one source that has no bad proofs.

The question

OSVerify (Nie, Ye et al., "One-Sided Verification Under Limited Expert Review", arXiv:2610.18089) checks a proof by asking a model to propose specific errors, then asking 16 more times whether each error is real and substantial. The paper reports large gains over plain voting when few good proofs may be wrongly rejected (for example on Putnam, at most 5% of good proofs rejected: 70% of bad proofs caught against 38% for voting, on gpt-oss-120b; paper Table 1). The paper's voting used 16 samples per proof (ours used 8). The paper also reports that OSVerify reaches voting's catch rate with less compute, so our cost result disagrees with theirs, on different material and a different model.

We asked whether this would help the lab's own checking. We compared three methods on the same 76 items, all on Kimi K3: OSVerify, the lab's referee prompt sampled 5 times, and plain voting (8 samples of "accept or reject"). Each method's rejection threshold was fitted on 4 of 5 folds (items from the same source or theorem always share a fold) and tested on the fifth, so no item set its own threshold. Intervals are 95% bootstrap intervals that resample those item groups (2,000 draws).

We found no other independent test of OSVerify. The closest work using Lean labels for proof verifiers, LeanPRM (arXiv:2610.17697), trains a step-level verifier and does not compare against voting.

The result, in plain words

OSVerify did not catch more bad proofs than the referee prompt, and caught slightly fewer than plain voting (CHECKED, adversary SURVIVED).

• OSVerify minus referee: +0 percentage points at both budgets (95% interval -35 to +25 at 5%; -29 to +27 at 10%).
• OSVerify minus voting: -7 points at 5% (-44 to +20) and -13 points at 10% (-40 to +20).
• Three of OSVerify's five catches at 5% are the open-problem attempts that every method rejects. Without them, at 5%, OSVerify and the referee prompt each catch 2 of 12 and voting 3; at 10%, 3, 3 and 5 of 12.
• On the 30 Lean items whose full text a reader can check (15 good, 15 bad; this leaves out proofs that import unseen modules), with thresholds fitted on the same items: at 5%, OSVerify caught 0 of 15 bad proofs, the referee prompt 6 and voting 5. At 10%, each caught 6. OSVerify gave the maximum score, 16 of 16 votes, to a good Mathlib proof, and it scored a good proof and a bad attempt at the same theorem identically.
• Cost: OSVerify made about 22 model calls per item against 5 and 8, so it cost about 7 times the referee prompt. It spends most on bad items, where it proposes about 9 errors each (1.5 on good items).
• Adding 17 wrong competition answers (all bad) to the pool: OSVerify catches as many as voting and more than the referee prompt (63% against 47% at 5%), but that difference is not significant (interval -38 to +31 points).

Decision under our plan, set before the run: do not replace the referee prompt with OSVerify.

How it was checked

• Plan, item file and code were frozen before the main run, after two independent build reviews by AI models.
• CHECKED: every decision number was recomputed from the raw scores by a separate checker script, written from the plan by a different AI session that did not read the harness's metric code; 9 of 9 comparisons matched exactly. (Codex wrote the harness core; Claude sessions wrote the checker and later extended the harness's metric code, so the two are separate code, not separate models.)
• Adversary SURVIVED: a separate AI reviewing agent refitted every threshold itself, recomputed the costs from the call records, and tried to rescue OSVerify (hand-checkable subset, removing the open-problem group, matched proof pairs). Every attack strengthened the negative verdict. Its remaining doubt is sample size only.

What would settle it

A test with 40 or more independent bad proofs that a reader can check in full, with no shared groups, would show whether OSVerify has a large advantage (about 25 points or more) over one referee prompt. Ruling out a 10-point gain would need several hundred. At the cost measured here we see no strong reason to fund one.