TLDR: Researchers introduce PROOFBENCH, the first expert-annotated dataset for fine-grained evaluation of natural language math proofs generated by LLMs. They also develop PROOFGRADER, an evaluator that combines a strong language model, reference solutions, and marking schemes, achieving high accuracy against human scores. This system significantly improves the selection of high-quality proofs, addressing a critical gap in AI’s mathematical reasoning capabilities.
In the rapidly evolving world of artificial intelligence, large language models (LLMs) have shown incredible progress in many areas, including mathematical reasoning. However, one significant challenge has remained: reliably generating and, more importantly, evaluating natural language math proofs. Unlike simple math problems with a single, verifiable answer, proofs require a nuanced understanding of logical steps and intermediate reasoning, making their assessment complex.
Addressing a Critical Gap in AI Math Evaluation
A recent research paper, titled RELIABLE FINE-GRAINED EVALUATION OF NATURAL LANGUAGE MATH PROOFS, highlights a critical missing piece in this puzzle: the absence of a reliable, fine-grained evaluator for LLM-generated math proofs. To tackle this, researchers Wenjie Ma, Andrei Cojocaru, Neel Kolhe, Bradley Louie, Robin Said Sharif, Haihan Zhang, Vincent Zhuang, Matei Zaharia, and Sewon Min propose a systematic approach to develop and validate evaluators that can assign detailed scores to these proofs.
Introducing PROOFBENCH: A New Standard for Proof Evaluation
To enable their study, the team introduced PROOFBENCH, the first-of-its-kind expert-annotated dataset specifically designed for fine-grained proof ratings. This extensive dataset includes 145 problems sourced from six major math competitions, such as USAMO, IMO, and Putnam, spanning from 2022 to 2025. For these problems, they gathered 435 solutions generated by state-of-the-art LLMs like Gemini-2.5-pro, o3, and DeepSeek-R1. The proofs in PROOFBENCH are meticulously rated by human experts on a 0-7 scale, mirroring the grading standards of premier mathematics competitions. This fine-grained scale allows for a much more nuanced assessment of proof quality than a simple ‘correct’ or ‘incorrect’ judgment.
Developing PROOFGRADER: The Optimal Evaluator
Using PROOFBENCH as a testing ground, the researchers systematically explored various aspects of evaluator design. They looked at different backbone LLM models, the type of input context provided (such as reference solutions and problem-specific marking schemes), the instructions given to the evaluator, and the overall evaluation workflow. Their analysis led to the development of PROOFGRADER, an evaluator that stands out for its accuracy and robustness.
PROOFGRADER combines several key elements: a powerful reasoning backbone language model, rich contextual information (including both reference solutions and detailed marking schemes), and a straightforward ensembling method where multiple evaluation runs are combined for a more stable score. This combination allows PROOFGRADER to achieve a low Mean Absolute Error (MAE) of 0.926 against expert scores, significantly outperforming simpler evaluation methods.
Also Read:
- Hard2Verify: A New Benchmark for Evaluating AI’s Math Proof Verification Skills
- Evaluating Language Models on Optimization Challenges: Introducing ExtremBench
Practical Impact: Improving AI-Generated Proofs
The practical utility of PROOFGRADER was demonstrated in a ‘best-of-n’ selection task. In this scenario, the evaluator’s job is to select the highest-quality proof from a batch of several generated solutions. At n=16 (selecting from 16 proofs), PROOFGRADER achieved an average score of 4.14 out of 7. This performance closed 78% of the gap between a basic binary evaluator (which scored 2.48) and a human oracle (which scored 4.62). This highlights PROOFGRADER’s potential to significantly advance the development of better proof-generating LLMs by providing a reliable reward signal for training.
The research underscores that the quality of an evaluator heavily depends on the strength of its underlying model, the context it receives, and the clarity of its instructions. Providing a marking scheme proved to be particularly crucial, helping evaluators distinguish between fluent but flawed arguments and genuinely correct mathematical reasoning. This work lays a strong foundation for future research in challenging, hard-to-verify mathematical reasoning tasks, pushing the boundaries of what AI can achieve in complex problem-solving.
