Reliable Fine-Grained Evaluation of Natural Language Math Proofs

TL;DR

This paper tackles the bottleneck of evaluating natural-language mathematical proofs by introducing ProofBench, a fine-grained, expert-annotated dataset spanning 145 problems from major contests and 435 model-generated proofs. It systematically studies evaluator designs across backbone models, context, instructions, and workflows, culminating in ProofGrader, a robust 0–7 evaluator that closely aligns with expert judgments. Through best-of-n experiments, ProofGrader demonstrates strong practical value as a reward signal, substantially narrowing the gap to human oracle performance. The work also highlights the critical role of context and marking schemes in achieving reliable evaluation and points to limitations and future directions in broadening scope and improving open-source capabilities.

Abstract

Recent advances in large language models (LLMs) for mathematical reasoning have largely focused on tasks with easily verifiable final answers; however, generating and verifying natural language math proofs remains an open challenge. We identify the absence of a reliable, fine-grained evaluator for LLM-generated math proofs as a critical gap. To address this, we propose a systematic methodology for developing and validating evaluators that assign fine-grained scores on a 0-7 scale to model-generated math proofs. To enable this study, we introduce ProofBench, the first expert-annotated dataset of fine-grained proof ratings, spanning 145 problems from six major math competitions (USAMO, IMO, Putnam, etc) and 435 LLM-generated solutions from Gemini-2.5-pro, o3, and DeepSeek-R1. %with expert gradings. Using ProofBench as a testbed, we systematically explore the evaluator design space across key axes: the backbone model, input context, instructions and evaluation workflow. Our analysis delivers ProofGrader, an evaluator that combines a strong reasoning backbone LM, rich context from reference solutions and marking schemes, and a simple ensembling method; it achieves a low Mean Absolute Error (MAE) of 0.926 against expert scores, significantly outperforming naive baselines. Finally, we demonstrate its practical utility in a best-of-$n$ selection task: at $n=16$, ProofGrader achieves an average score of 4.14 (out of 7), closing 78% of the gap between a naive binary evaluator (2.48) and the human oracle (4.62), highlighting its potential to advance downstream proof generation.

Figures (7)

• Figure 1: Two example proof problems selected from well-established competitions.
• Figure 2: Example problem (USAMO 2025 P2) with its reference solution and marking scheme.
• Figure 3: Data statistics and model evaluation results. (a) Problem statistics across six competitions. (b) Score distribution showing mean (2.41) and median (1.00). (c) Model performance comparison via box plots. Each box represents the interquartile range (IQR, middle 50% of scores), with the red line showing the median and blue dashed line showing the mean. (d) Per-generator score distribution. Stacked horizontal bar chart showing the percentage of problems receiving each score (0-7) for each model. Colors indicate score values (red=low, green=high). (e) Performance heatmap by generator and competition. (f) Competition difficulty ranking with error bars: TST is the most challenging competition (mean: 1.28) and Putnam is the easiest (mean: 3.11).
• Figure 3: Per-generator evaluation accuracy (MAE; lower is better). Bold marks, for each generator (column), the best (smallest) MAE across generators.
• Figure 4: Best-of-$n$ with different selectors. Average best-of-$n$ score over 29 problems for o3 (generator) as $n$ increases from 1 to 16. ProofGrader is our ensemble evaluator: the median over five independent o3 runs using the reference solution and marking scheme.