Propose
Split the solution recursively and search every part, from the whole argument down to single claims, for errors that could invalidate it.
One-Sided Verification Under Limited Expert Review
Stanford University
*Equal contribution
OSVerify is a verifier for settings where AI proposes candidate solutions faster than human experts can check them. It is one-sided: it rejects as many invalid candidates as possible while keeping the rate of wrongly rejected valid solutions under a fixed budget, so expert time goes to the candidates most likely to be correct. Rather than judging a whole solution at once, OSVerify decouples error proposal from error validation. A proposer searches the solution at every level of detail for errors that could invalidate it, and a validator rejects only on errors it confirms as substantial. On mathematical benchmarks it cuts the invalid candidates experts must review by 46% relative to voting, or 57% with an RL-trained validator, and on research papers it finds errors that authors and experts confirm.
(open full-size image)
Tap the figure to open it at full size.
gpt-oss-120b) cuts the invalid candidates that still need review by 52% on Putnam100 and 34% on FirstProof-Eval. Training the validator raises the cut to 83% and 41%.01The problem
Valid solutions to hard problems are rare, so discarding one is costly. At the same time, every invalid candidate that reaches an expert costs review time. We therefore treat verification as a constrained objective rather than a single accuracy number:
maximize TNR(V) subject to FNR(V) ≤ τ
TNR: fraction of invalid solutions the verifier rejects. FNR: fraction of valid solutions it wrongly rejects. Under a fixed FNR budget τ, every gain in TNR removes invalid candidates from the expert's queue.
02How it works
Checking a specific, stated error is easier than finding one. With the same model, AUROC rises from 0.68 to 0.90 when it judges a proposed error instead of the whole solution. OSVerify builds on this in three steps.
Validate
Check each proposed error on its own: does it hold, and does it invalidate the solution?
- Not-Real
- Minor
- Substantial
Decide
Reject if any error is confirmed Substantial, with a threshold set to meet the FNR budget. Otherwise, pass the solution to an expert.
Because the validator always sees the same input, a problem, a solution and one proposed error, it can be post-trained with reinforcement learning across problems.
03Use cases
OSVerify only needs a problem and a candidate solution, so it fits wherever expert checking is the bottleneck. We use it in two ways.
Refereeing research papers
In the paper, OSVerify found 45 issues in Zhu (2017), published in the Annals of Mathematics, and 88 in Liu & Wang (2026), compared with 11 and 3 from direct review with the same model. The authors confirmed the errors and revised their papers.
We now also run OSVerify as a referee on new mathematics preprints from OpenAI. Across 11 papers, it has flagged 5 major and 13 minor issues, each verified by human experts. The papers with major issues:
Global quantum geometric Langlands at irrational level
A direct-sum counterexample to the absolute pairing, a faulty global scalar identification, and incorrect cross-references.
A power saving for planar unit distances
Genericity over a coefficient field can be lost after adjoining another grid point.
An L³ bound for the trilinear Hilbert transform
A missing endpoint hypothesis, an omitted predictor term, and a mismatch in the first-failing-role convention.
Cylinder loop weights and planar nesting
An endpoint estimate is applied globally without its bounded bulk contribution.
Facilitating scientific discovery
Test-time scaling and autoresearch systems can generate many candidate solutions, but open problems rarely come with an automatic evaluator to tell which ones are right. OSVerify can fill that role. Paired with the agentic mathematical problem solver Rethlas, with no formal proof checker in the loop, OSVerify has helped resolve the open conjectures below. Human experts have confirmed all of the proofs.
-
Flatness of the loop-rotated Plancherel algebra PLX,ħ over k[ħ]
-
Commutativity of the Plancherel algebra PLX
-
The automorphic commutator relation
-
The Manin constant conjecture, and Stevens’ Conjectures I and II Latest
04Benchmarks
On competition-level Putnam100 and Hard2Verify (H2V) and research-level FirstProof-Eval, with reference solutions and formal proof checkers withheld, OSVerify rejects far more invalid solutions than LLM-as-a-judge and voting at the same FNR budget.
| Putnam100 | H2V | FirstProof-Eval | |||||||
|---|---|---|---|---|---|---|---|---|---|
| FNR ≤ | 0% | 5% | 10% | 0% | 5% | 10% | 0% | 5% | 10% |
| gpt-oss-120b | |||||||||
| LLM-as-a-Judge | 0±0 | 0±0 | 0±0 | 0±0 | 54.4±2.0 | 54.4±2.0 | 0±0 | 0±0 | 43.3±2.9 |
| Voting | 0±0 | 38.4±3.9 | 45.5±2.8 | 60.9±4.2 | 69.2±3.6 | 75.6±3.7 | 29.5±10.2 | 35.9±2.5 | 48.8±2.2 |
| OSVerify | 0±0 | 70.4±14.3 | 77.9±3.3 | 83.2±0.6 | 84.7±0.6 | 84.7±0.5 | 50.4±15.1 | 58.0±3.1 | 60.8±1.3 |
| + trained validator | 85.8±2.9 | 89.6±1.7 | 92.3±1.5 | 82.4±1.1 | 83.2±0.7 | 83.2±0.7 | 57.8±3.0 | 62.3±0.8 | 62.7±0.3 |
| gpt-5-mini | |||||||||
| LLM-as-a-Judge | 0±0 | 0±0 | 63.1±3.9 | 66.3±1.8 | 66.3±1.8 | 66.3±1.8 | 0±0 | 0±0 | 42.7±2.4 |
| Voting | 28.5±17.3 | 58.1±4.4 | 75.4±3.7 | 82.9±1.2 | 82.9±1.2 | 82.9±1.2 | 19.1±16.4 | 42.6±1.8 | 49.2±2.3 |
| OSVerify | 72.1±21.9 | 82.9±1.6 | 86.6±1.3 | 85.7±0.3 | 85.7±0.3 | 85.7±0.3 | 33.9±25.5 | 60.0±9.1 | 65.4±1.4 |
Scroll the table sideways to see all benchmarks.
Table 1. Empirical TNR (%) under empirical FNR constraints of 0%, 5% and 10%; higher is better. Mean ± standard deviation over 2,000 resampling trials; bold marks the best entry per column for each backbone. A zero includes the always-pass fallback when no nontrivial operating point meets the constraint.
Contribute
OSVerify is designed to be general. The proposer and the validator only need a problem, a candidate solution and a definition of what counts as a substantial error, so the same framework can apply wherever expert review is the bottleneck. Our current use cases, however, are all in mathematics.
We welcome contributions that extend OSVerify to more scientific domains, for example new benchmarks with expert-labeled solutions, domain-specific definitions of substantial errors, or applications to open problems in your own field.
Get in touch
- Fan Nie niefan@stanford.edu
- Haotian Ye haotianye@stanford.edu
Citation
@misc{nie2026osverify,
title = {One-Sided Verification Under Limited Expert Review},
author = {Nie, Fan and Ye, Haotian and Liu, Shurui and Wang, Zihao and Ermon, Stefano and Zou, James},
year = {2026},
note = {Preprint}
}