Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection

Large language models have achieved remarkable success on final-answer mathematical problems, largely due to the ease of applying reinforcement learning with verifiable rewards. However, the reasoning underlying these solutions is often flawed. Advancing to rigorous proof-based mathematics requires reliable proof verification capabilities. We begin by analyzing multiple evaluation setups and show that focusing on a single benchmark can lead to brittle or misleading conclusions. To address this, we evaluate both proof-based and final-answer reasoning to obtain a more reliable measure of model performance. We then scale two major generative verification methods (GenSelect and LLM-as-a-Judge) to millions of tokens and identify their combination as the most effective framework for solution verification and selection. We further show that the choice of prompt for LLM-as-a-Judge significantly affects the model's performance, but reinforcement learning can reduce this sensitivity. However, despite improving proof-level metrics, reinforcement learning does not enhance final-answer precision, indicating that current models often reward stylistic or procedural correctness rather than mathematical validity. Our results establish practical guidelines for designing and evaluating scalable proof-verification and selection systems.

AI systems are becoming very good at finding final answers to math problems, but a right answer can still be backed by a faulty explanation. This matters because advanced mathematics, such as olympiad-style problems, requires a proof that every step is logically sound. In this work, we study how to automatically check and select AI-generated mathematical proofs. We find that judging proofs using only one benchmark can be misleading, because AI checkers may learn shortcuts from the dataset instead of truly checking the math. To address this, we evaluate proof checkers using both full proof correctness and final-answer correctness. We also study two ways of using extra computing effort: comparing candidate proofs against each other and asking an AI judge to score individual proofs several times. The best practical strategy combines these ideas, first narrowing down candidates through comparisons and then using repeated judging to choose the final proof. Training the judge with reinforcement learning makes it less sensitive to prompt wording, but does not reliably improve its ability to check the underlying mathematics. Our results provide guidance for building better mathematical proof checkers, while showing that human review is still important for difficult or high-stakes proofs.