Source-linked AI summary
Reliable Fine-Grained Evaluation of Natural Language Math Proofs
Wenjie Ma, Andrei Cojocaru, Neel Kolhe, Bradley Louie, Robin Said Sharif, Haihan Zhang, Vincent Zhuang, Matei Zaharia, Sewon Min
TL;DR
Natural-language math proofs lack reliable, fine-grained automated evaluation, despite the need for faithful capability assessment and useful training rewards. The paper introduces ProofBench and systematically develops ProofGrader, which closely matches expert ratings and improves best-of-n proof selection. Its scope remains limited to olympiad-style mathematical correctness rather than research-level, educational, readability, clarity, or elegance evaluation.
Problem
Reliable fine-grained evaluators for natural-language math proofs are missing, limiting faithful assessment of model capabilities and accurate reward signals.
Method
The paper builds ProofBench and searches evaluator configurations across backbone models, context, instructions, and workflows, producing ProofGrader with reference solutions, marking schemes, and ensembling.
Results
ProofGrader achieves MAE 0.926 against expert scores and, at n = 16, reaches 4.14/7 versus 2.48 for a binary evaluator, closing 78% of the gap to the 4.62 human oracle.
Takeaways & Limitations
ProofGrader shows practical promise for identifying high-quality proofs in downstream best-of-n selection and as a potential reward model.
Takeaways & Limitations
The evaluation covers olympiad-style proofs and mathematical correctness, not research-level or educational settings, readability, clarity, or elegance.
Abstract
from arXiv · showhide
Recent advances in large language models (LLMs) for mathematical reasoning have largely focused on tasks with easily verifiable final answers while 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. 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/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.
1 INTRODUCTION
The paper addresses the lack of reliable, fine-grained evaluation for natural-language mathematical proofs by introducing an expert-rated benchmark and a systematic evaluator-design methodology. ProofGrader aligns closely with expert ratings and improves downstream proof selection.
- Motivation: Reliable proof evaluation remains a bottleneck because final-answer rewards cannot detect intermediate errors, while expert grading is costly and formalization is difficult.The paper therefore focuses on evaluating proofs in their natural-language representation.
- Contributions: ProofBench contains expert ratings for 145 contest problems and 435 solutions generated by Gemini-2.5-Pro, o3, and DeepSeek-R1.Its two-stage annotation uses problem-specific marking schemes and expert scoring while allowing valid alternative approaches.
- Evaluator design: ProofGrader combines a strong reasoning backbone, reference solutions, marking schemes, and simple ensembling, achieving MAE 0.926 against expert scores and outperforming naive baselines.The study searches evaluator configurations across backbone models, context, instructions, and workflows rather than training a new evaluator.
- Downstream utility: At n = 16, ProofGrader raises best-of-n selection from 2.48 with a binary evaluator to 4.14/7, closing 78% of the gap to the 4.62 human oracle.This validates its practical utility as a potential reward signal for selecting high-quality proofs.
2 PROOFBENCH: EXPERT-RATED MATH PROOF SOLUTIONS
ProofBench is constructed from olympiad-style problems, model-generated proofs, and expert annotations on a unified 0–7 scale. Its statistics show that current reasoning models remain unreliable and perform unevenly across competitions and problem novelty.
- Dataset construction: ProofBench contains 145 problems from six competitions across 2022–2025 and solutions generated by o3, Gemini-2.5-Pro, and DeepSeek-R1-0528.Official problem sources and available human solutions are used where possible to reduce transcription errors.
- Scoring scale: The unified 0–7 scale preserves fine-grained assessment across competitions, including normalization of Putnam annotations from its official 0–10 scale.Fine-grained scoring is intended to capture proof quality beyond binary correctness.
- Expert grading: Annotation uses LLM-generated, problem-specific marking schemes followed by expert grading that treats them as guidance while crediting valid alternative reasoning.Five experts with Putnam-level or national Math Olympiad experience conducted the annotations.
- Dataset statistics: Fewer than 30% of problems receive scores of 6 or higher even from the strongest models, indicating that current systems remain far from reliable.The dataset includes 435 expert-annotated evaluations and summarizes score distributions across competitions and models.
- Dataset statistics: Mean scores vary by competition, with Putnam highest at 3.09 and TST lowest at 1.26, while newer post-cutoff problems consistently receive lower scores.The latter pattern may reflect training-data contamination or a generalization gap on novel problems.
3 A SYSTEMATIC STUDY OF EVALUATOR DESIGNS
The study systematically evaluates proof-evaluator designs across model backbones, contextual inputs, instructions, ensembling, and staged workflows. It identifies a configuration combining a strong backbone, informative context, flexible instructions, and ensembling, while revealing failure modes and context sensitivity.
- 3.1 EVALUATOR DESIGNS: Stronger backbones perform better, while contextual information improves every backbone; marking schemes contribute most of the context gain, with REF+MS adding mainly for O3.The study compares NONE, REF, MS, and REF+MS settings across six models.
- 3.3 WHAT FACTORS IMPROVE SINGLE-PASS EVALUATOR?: Instruction style trades off calibration and ranking: O3 works best with flexible NORM guidance, whereas mid-tier models benefit from prescriptive STRICT instructions.The authors attribute this pattern to stronger models flexibly applying rubrics and mid-tier models needing more guidance to reduce over-crediting and variance.
- 3.3 WHAT FACTORS IMPROVE SINGLE-PASS EVALUATOR?: Evaluators tend to underperform on outputs from their own model families, while GEMINI and R1 can overscore their own responses; O3 remains strongest across generators.The per-generator results indicate evaluator-generator interactions are not uniform across models.
- 3.4 DO ENSEMBLING AND STAGED WORKFLOWS IMPROVE SINGLE-PASS EVALUATION?: Ensembling five O3 runs lowers RMSE from 1.225 to 1.169 and raises Kendall-τ from 0.540 to 0.578, with aggregation choice determining metric optima.Mean aggregation is best for RMSE and ranking correlation, while median achieves the lowest MAE and highest WTA≤1; ensembling also reduces variance.
- 3.4 DO ENSEMBLING AND STAGED WORKFLOWS IMPROVE SINGLE-PASS EVALUATION?: Staged evaluation is backbone-dependent: it improves O4-MINI but worsens O3, while reflection yields only small gains and the final verdict adds no value.For O4-MINI, RMSE falls from 1.816 to 1.650 and MAE from 1.367 to 1.245; for O3, RMSE rises from 1.273 to 1.375 and MAE from 0.964 to 1.065.
- Putting everything together: PROOFGRADER: PROOFGRADER combines O3, REF+MS context, NORM instructions, and simple ensembling as the most consistently strong configuration.The design follows findings that backbone strength dominates, marking schemes provide substantial gains, and ensembling improves stability.
- 3.5 IN-DEPTH ANALYSIS: PROOFGRADER’s errors include over-crediting 10.8% of inspected cases and under-crediting 12.2%, often involving surface heuristics or misclassified fatal logical errors.Over-scoring can reward rubric-like structure despite false central claims, while broken reductions may be treated as minor issues.
- 3.5 IN-DEPTH ANALYSIS: Reference solutions and marking schemes are important because no-context evaluators overestimate correctness in over 60% of cases, especially for low-quality proofs.The evaluation gap correlates strongly with proof quality (r = 0.699, p < 0.001).
4 DOWNSTREAM UTILITY: BEST-OF-N PROOF SELECTION
The study tests whether fine-grained proof evaluators improve best-of-n selection and finds that PROOFGRADER closely follows human-oracle performance while outperforming binary and comparison-based alternatives.
- Setup: The downstream testbed uses 16 O3-generated candidates for each of 29 problems, with evaluator-selected proofs scored against human-graded candidates.Performance is estimated by Monte Carlo subsampling, averaging selected-proof scores over subsets and problems.
- 4.1 The Value of Fine-Grained Scoring: At n=16, PROOFGRADER achieves an average score of 4.14, closely tracking the human-oracle curve as n increases.PROOFGRADER is an ensemble of five O3 runs using reference solutions and marking schemes.
- 4.1 The Value of Fine-Grained Scoring: Marking schemes are critical: REF+MS, REF, and their ensemble consistently outperform the NONE evaluator across fine-grained selection variants.The same ranking holds among the four fine-grained evaluators compared in the study.
- 4.1 The Value of Fine-Grained Scoring: Binary evaluators perform much worse because collapsing proofs into Correct or Incorrect prevents ranking multiple correct solutions by quality.They cannot distinguish an adequate proof, such as 5/7, from an excellent proof, such as 7/7.
- 4.2 Robustness Against Comparison-Based Selection Strategies: PROOFGRADER consistently dominates Tournament and Knockout selection across n, indicating that context-rich scoring is more effective than repeated pairwise comparison.Tournament and Knockout still improve over the mean baseline, but Tournament has quadratic comparison cost.
5 RELATED WORK
Existing mathematical reasoning benchmarks emphasize answer matching, while formal-proof and LLM-judge approaches leave natural-language proof evaluation insufficiently studied. The paper identifies a missing systematic study of fine-grained, rubric-driven proof evaluators.
- Benchmarks for Mathematical Reasoning: Most mathematical reasoning benchmarks target short or closed-form answers, leaving natural-language proof problems underrepresented.Competition-based benchmarks are more challenging but still emphasize answer matching.
- Automated Evaluation for Generative Outputs: LLM-as-a-judge methods enable scalable evaluation of open-ended responses, but automated evaluation of mathematical proofs remains relatively underexplored.Prior work has examined judge reliability on challenging tasks without establishing a systematic proof-evaluation methodology.
- Formal Proof Generation: Formal theorem-proving benchmarks provide automatically checkable correctness, whereas this paper focuses on proofs in their informal natural-language representation.The formal-proof line includes miniF2F, FIMO, PutnamBench, and Lean-Workbook.
- Summary: No existing work had systematically studied the evaluator design space for mathematical proofs or supplied scalable, fine-grained rubric-driven annotations for that study.The robustness-determining factors for proof evaluators therefore remained largely uninvestigated.
6 CONCLUSION
The paper introduces ProofBench and uses it to identify strong backbones, problem-specific marking schemes, and ensembling as important ingredients of ProofGrader. Its best-of-n evaluation shows that ProofGrader closely tracks oracle performance, while important scope and capability limitations remain.
- Conclusion: ProofBench is a comprehensive fine-grained proof-grading dataset spanning multiple contests and years.It supports systematic evaluation of natural-language proof evaluators.
- Conclusion: Strong backbones, problem-specific marking schemes, and ensembling produce ProofGrader, whose best-of-n selections closely track oracle performance.The conclusion presents these components as important to the evaluator’s performance.
- Limitations and Future Work: The current scope covers olympiad-style proofs but not research-level problems or educational settings, and evaluation measures mathematical correctness rather than readability, clarity, or elegance.These extensions are identified as future work.
- Limitations and Future Work: The strongest evaluators rely on closed models, and the work has not yet trained proof generators with the evaluator as a reward signal.Improving open-source evaluators and integrating evaluation into training remain future directions.
ETHICS STATEMENT
The study uses publicly accessible mathematics-competition problems and expert annotations produced by qualified, fairly compensated annotators.
- Ethics Statement: The dataset uses problems from publicly accessible mathematics competitions and expert annotations from qualified individuals who were fairly compensated.The paper identifies dataset construction and potential evaluator bias as its primary ethical considerations.
REPRODUCIBILITY STATEMENT
The paper commits to releasing its code, data, supplementary materials, benchmark contents, and reproduction scripts upon publication.
- The authors will publicly release all code, data, and supplementary materials upon publication.The release includes ProofBench problems, generated solutions, expert scores, and problem-specific marking schemes.
- The source code will include scripts reproducing the experiments, evaluator implementation, and all prompts.
- Problem counts and contest descriptions are documented in supplementary tables, while one EGMO 2023 problem was removed because its statement contained a figure.
C.1 MARKING SCHEME GENERATION: EVALUATION PROCESS
The marking-scheme evaluation compares model and prompting configurations through expert grading, calibration, and disagreement resolution, while documenting recurring rubric weaknesses.
- Rubric quality: 35 of 36 Stage 2 rubrics received ratings of 2 or 3 from both annotators, although not all available problems were evaluated.
- Configuration selection: Gemini-2.5-Pro with zero-shot prompting was selected as the final marking-scheme configuration based on quantitative scores and qualitative feedback.
- Observed limitations: Generated rubrics sometimes penalized minor calculation errors, preserved stale feedback, awarded credit for unproved statements, or failed to recognize alternative weaker solution paths.The authors identify recognition of meaningful alternative approaches as a major area for future improvement.
- Annotation protocol: Experts independently graded marking schemes and proof solutions, double-graded over 40% of solutions, and resolved disagreements through discussion and consensus.Final proof scores use a 0–7 scale with bands for incorrect, partial progress, nearly complete, and fully correct solutions.
D PROOFBENCH ABLATION BY COMPETITION AND YEAR
The contamination analysis finds positive pre-cutoff performance bias across all models, so the primary comparison uses only clean 2025 competition problems.
- Contamination findings: Gemini-2.5-Pro shows a +1.01 pre-cutoff bias and 14.4% improvement, while OpenAI-o3 and DeepSeek-R1-0528 show moderate biases of +0.44 and +0.40.Gemini-2.5-Pro has the strongest contamination signal because its January 1, 2025 cutoff leaves only 20% of the dataset clean.
- Competition variation: Contamination effects vary by competition: IMO is consistently positive across models, whereas EGMO and APMO show mixed or reverse effects.The passage suggests these differences interact with variation in problem difficulty.
- Clean-data analysis: The primary analysis uses 29 problems from 2025 competitions to ensure clean cross-model comparisons without training-data leakage confounds.This clean subset represents 20% of the full dataset, while full-dataset results are reported with contamination warnings.
E ADDITIONAL DETAILS FOR EVALUATION METRICS
The evaluation metrics compare within-problem rankings against expert judgments, aggregate metrics across problems, and classify contamination by the size of the pre-cutoff effect.
- Ranking agreement: Within-problem ranking agreement evaluates concordant and discordant solution pairs while accounting for ties in expert and evaluator scores.Problems with an undefined denominator are omitted from aggregation.
- Tables: The contamination summary table reports effects across three models, while the contest-specific table encodes potentially contaminated and clean cells by color and cutoff status.
- Contamination classification: Contamination effects are labeled strong above 1.0, moderate from 0.3–1.0, and absent or reversed below 0.3.
- Aggregation: Metrics are macro-averaged across problems with defined ranking statistics, and all problems have the same response count n.
F EVALUATION ON WEAKER, OPEN-SOURCE MODELS
Additional experiments show that evaluator reliability depends strongly on model capability: weaker generators are easier to grade, while leading open-source evaluators substantially trail frontier proprietary models.
- Weaker generators: Weaker models mostly produce incorrect 0-point proofs, making grading easier and yielding lower evaluator error rates than in the main benchmark.The benchmark therefore uses the strongest available generators to distinguish partially correct from nearly complete solutions and detect subtle errors.
- Open-source evaluators: Leading open-source models perform substantially worse as evaluators than frontier proprietary models.The comparison covers Qwen3-235B-A22B (Thinking) and Llama-3.1-70B-Instruct.
H IN-DEPTH ANALYSES
The analyses show that context, especially reference solutions and marking schemes, corrects systematic scoring errors, while ProofGrader remains vulnerable to several forms of superficial or overly rigid reasoning.
- Failure modes: ProofGrader can over-credit polished solutions whose structure resembles a rubric even when their central mathematical claim is false.This appearance-of-completeness failure rewards superficial rubric alignment over verification of the core argument.
- Failure modes: ProofGrader may treat fatal logical gaps as minor omissions and overtrust sophisticated frameworks without checking validity conditions.Examples include accepting false universal claims, unchecked path properties, and inconsistent constructed orderings.
- Failure modes: ProofGrader can undergrade valid proofs by penalizing early missteps, double-penalizing one flaw, or demanding micro-justifications for routine downstream steps.These failures can drive substantially correct solutions toward near-zero scores despite valid later arguments or substantial progress.
- Failure modes: Geometry proofs receive unstable scores because long dependency chains amplify both ignored invalid steps and over-penalized routine omissions.The cited chain runs from similarity to ratios to concurrency or cyclicity.
- Context analysis: Without reference solutions or marking schemes, evaluators over-score low-quality proofs, whereas contextual evaluators score high-quality proofs higher.No-context evaluators over-score proofs rated 0–2 by 1.7 points on average, while contextual evaluators score proofs rated 5–7 higher by 0.8 points; the gap correlates with proof quality (r = 0.699, p < 0.001).
- Context analysis: When O3 cannot solve a problem well, no-context evaluation over-scores by 1.4 points on average; when it can solve the problem, context raises scores by 0.9 points.This indicates that difficulty solving a problem impairs assessment of partial progress without reference materials.
- Marking-scheme sensitivity: Human-provided marking schemes outperform regenerated alternatives, making scheme quality a measurable source of evaluator sensitivity.The comparison evaluates O3 under REF+MS with original human, same-model regenerated, and O3-generated schemes.