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

arXiv: https://arxiv.org/abs/2602.02377 · HTML: https://mlsanity.com/paper/2602.02377/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 10 of its 18 references that are in the map.
- First posted on arXiv 2 Feb 2026.

## Builds on (most cited first, 10 of 10)

- [DeepSeek-R1: Incentivizing Reasoning Capability in LLMs via Reinforcement Learning](https://mlsanity.com/paper/2501.12948/) (2025)
- [HybridFlow: A Flexible and Efficient RLHF Framework](https://mlsanity.com/paper/2409.19256/) (2024)
- [Understanding R1-Zero-Like Training: A Critical Perspective](https://mlsanity.com/paper/2503.20783/) (2025)
- [Large Language Monkeys: Scaling Inference Compute with Repeated Sampling](https://mlsanity.com/paper/2407.21787/) (2024)
- [Generative Verifiers: Reward Modeling as Next-Token Prediction](https://mlsanity.com/paper/2408.15240/) (2024)
- [How to Evaluate Reward Models for RLHF](https://mlsanity.com/paper/2410.14872/) (2024)
- [The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs](https://mlsanity.com/paper/2506.21621/) (2025)
- [Solving Inequality Proofs with Large Language Models](https://mlsanity.com/paper/2506.07927/) (2025)
- [Reliable Fine-Grained Evaluation of Natural Language Math Proofs](https://mlsanity.com/paper/2510.13888/) (2025)
- [MathConstruct: Challenging LLM Reasoning with Constructive Proofs](https://mlsanity.com/paper/2502.10197/) (2025)

## Built on by (most cited first, 1 of 1)

- [PAPO: Stabilizing Rubric Integration Training via Decoupled Advantage Normalization](https://mlsanity.com/paper/2603.26535/) (2026)

## Abstract (arXiv)

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.