ProofVerifier: A Scalable, Diversity-Driven Framework for Natural-Language Proof Verification

arXiv:2602.02377 · cs.CL · Submitted 2026-02-02 · Read on arXiv

cs.CL

Submitted: 2026-02-02

Updated: 2026-09-16

Comments: Under review

Code: https://github.com/project-numina/aimo-progress-prize

Project page: https://web.evanchen.cc/problems.html

License: http://creativecommons.org/licenses/by/4.0/

The gist: While large language models (LLMs) have achieved strong performance on mathematical problems with verifiable answers, many advanced problems are proof-based and require evaluating full proofs.

Terminology

Abstract

While large language models (LLMs) have achieved strong performance on mathematical problems with verifiable answers, many advanced problems are proof-based and require evaluating full proofs. However, training such verifiers requires diverse and trustworthy question-proof-check (QPC) examples at scale, which are scarce. To address this challenge, we develop a human-audited, LLM-assisted data pipeline that produces large-scale QPC triplets with limited human effort. By systematically varying problem sources, generation strategies, and generator models, the pipeline creates diverse problem-proof pairs spanning multiple difficulty levels, linguistic styles, and error types. We combine multi-LLM agreement with hierarchical human auditing to obtain accurate proof-correctness labels. Using these data, we train generative proof verifiers and introduce an auxiliary fluency filter together with balanced token weighting to stabilize binary-reward long-form verification RL. Experiments show that our verifier improves proof-judgment accuracy across different proof styles and provides useful guidance for test-time selection. Overall, our results provide a practical data and training framework for natural-language proof verification.

Sources

Related papers