OSVerify cuts expert review of AI math proofs by 46%

Fan Nie@FanNie1208

AI-generated scientific output is scaling beyond available human review capacity. Scaling scientific discovery requires scaling verification.

We introduce OSVerify, a framework for one-sided verification: rejecting as many invalid solutions as possible while preserving rare valid ones for expert review.

We used OSVerify to referee 11 recent OpenAI math preprints, identifying 5 major and 13 minor issues, all verified by human experts.

Our key insight: checking a proposed error can be easier than judging an entire solution. Instead of directly judging solution correctness, OSVerify decouples verification into error proposal (searching for potential errors) and error validation (checking whether they are real and substantial).

On competition and research mathematical benchmarks, OSVerify reduces invalid solutions requiring expert review by 46% on average compared to voting under the same low-FNR constraint, or 57% with an RL-trained validator.

Verification can also guide discovery. OSVerify can be integrated into existing scientific discovery workflows. Paired with an agentic math solver, it helped resolve 3 open conjectures in the Langlands program and contributed to resolving the Manin constant conjecture. All proofs were confirmed by mathematicians.

Our broader goal is to provide verification-based evaluation signals for scientific discovery, enabling test-time scaling and self-improvement even when reliable automatic evaluators are unavailable.

Project: t.co/pSW9iJhvHg
Paper: t.co/WUXDDhIz0o
GitHub: t.co/2BF5EfdbUe

[1/n]