cs.CLFeb 2, 2026

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

Authors: Haotong YangZitong WangShijia KangSiqi YangWenkai YuXu NiuYike SunYi Hu+2 more

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.

Explore similar work

CardsList
  1. Pseudo-Formalization for Automatic Proof Verification

    May 19, 2026Slim Barkallah, Luke Bailey, Kaiyue Wen +2ProofFormalization