Reliable Fine-Grained Evaluation of Natural Language Math Proofs
Authors: Wenjie Ma
Andrei Cojocaru
Neel Kolhe
Haihan Zhang
Vincent Zhuang
Matei Zaharia
Sewon Min
Venue: ICLR 2026 Poster (2026)
Keywords: automated proof evaluation; LLM-as-a-judge; LLM-generated math proofs; rubric-guided grading; prompt optimization; expert-annotated proof dataset; evaluator reliability; reward modeling
Primary area: foundation or frontier models, including LLMs
TL;DR: LLMs lack reliable proof evaluators. We introduce ProofBench and a 0–7 methodology; our ProofGrader (marking schemes + ensembling) hits RMSE 1.093 vs experts and lifts best-of-8 to 4.05/7, closing >90% of the gap to a human oracle.

Abstract: 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.

Published as a conference paper at ICLR 2026
RELIABLE FINE-GRAINED EVALUATION OF NATURAL LANGUAGE MATH PROOFS
Wenjie Ma Andrei Cojocaru'
Neel Kolhe' Haihan Zhang
Vincent Zhuang?: Matei Zaharia' UC Berkeley
Sewon Min 1.4
2 Google DeepMind
Peking University
4 Allen Institute for Al
ABSTRACT
Recent advances in large language models (LLMs) for mathematical reasoning have largely focused on tasks with easily verifiable final answers while generat- ing and verifying natural language math proof' remain open challenge. We identify the absence of a reliable, fine-grained evaluator for LLM-generated math proofs critical gap. To address this, propose systematic methodology for developing and validating evaluators that assign fine-grained scores on a 0-7 scale to modee-ggnerrted math proofs. To enable this study, we introduce PROOF- BENCH, the first expert-annotater 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-RL. Using PROoFBENCE as a testbed, we systematically explore the evaluator de- sign 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 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 selee- tion task: at 16, PROOFGRADER achieves average score of 4.14 closing 78% the gap between a naive binary evaluator (2.48) and the human oracle (4.62), highlighting its potential to advance downstream proof generation.
INTRODUCTION
USAMO 2025 Pl. Fix positive integers & and d. Prove that for all sufficienlly large odd positive integers n, the digits of the mase-2n representation of are greater than
IMO 2024 P2. Determine all positive integers a and such that there exists positive integer g with god(a" b" a) = for all sufficiently large Tt.
Figure 1: Two example proof problems selected from well-established competitions.
Large language models (LLMs) have recently achieved remarkable progress in mathematical rea- soning, attaining strong performance on a variety of benchmarks. Such models are especially strong solving final-answer problems because they can trained using reinforcement learning against
simple answer verifiable rewards (Shao et al. 2024 DeepSeek-Al et al. 2025 Yang et al. 2025 Yu
cct al. 2025) Wang et al. 2025). However, these methods do not transfer to proof generation for two reasons: (i) many proof problems do not admit single, easily checkable final answer (Figure left);
and (ii) even when a final answer exists (Figure I] right), verifying it is insufficient to assess proof validity, the reasoning may contain substantial intermediate errors (Petrov al., 2025 Dekon- iick et al. (025). Because proof-generation tasks constitute large share of mathematical problem solving in research and education, this necessitates reliable proof evaluation methods.
We identify the absence of a reliable proof evaluator as a key bottleneck for improving proof generation, which is essential for providing faithful assessments of model capabilities and accurate reward signals for training models. Expert grading, while accurate, is slow and costly. While formal math (e.g., Lean) offers absolute certainty, it remains detached from the natural language used in
"Correspondence: hwirdssy@eezeeeeey...
Dataset contributors.
Served advisory capacity only.

---

Published as a conference paper at ICLR 2026
most human mathematics education and research; furthermore, automatically translating natural- language proofs into formal languages is brittle and remains extremely challenging (Gao et al. 2025] Liu et al. 2025a). Our work therefore focuses the critical and complementary task of evaluating proofs in their natural representation. While LLM--a-aajudde (Zheng et al.] 2023a Sheng et al,, 2025 Dekoninck et al.] 2025] Huang & Yang 2025) is promising, its application to math proofs is unsettled, and outcomes are sensitive to evaluator design-moot choice, available context, rubric construction, and prompting all of which are poorly understood.
This paper tackles this bottleneck by developing a methodology to create high-fidelity, fine-grained evaluators, and demonstrates for the first time that they can nearly match human oracle performance in downstream tasks. Our objective is to design an automated evaluator, E, that takes a problem p. a model-generated solution 8, and an optional set of contextual materials Crontext to produce a We identify the optimal evaluator not through model
fine-grained integer score, ý E {0, (........77 77. training. but by searching over a discrete space of configurations C. We adopt the 0-7 scoring scale used in premier competitions to enable nuanced assessment beyond binary correctness.
First, to support our study, we introduce PROOFBENCHS the first expert-annotated dataset for fine- grained proof evaluation that spans problems from multiple contests and years. It spans 145 prob- lems from EGMO, USAMO, IMO, USA TST, APMO, and PUTNAM 2022-2025), with 435 LLM-generated solutions from state-of-the- art models (GEMINI-2.5-PA)
03, DEEPSEEK-R. Data annotation follows a two-stage process: (i) generate a problem-specific marking scheme to standardize criteria while allowing valid alternative approaches; (ii) have experts score each solu- tion with that scheme while allowing for valid alternative solutions.
Using PROOFBENCH testbed, we systematically explore the evaluator design space, including four primary axes: backbone models, input context (such as reference solutions and problem-specific marking schemes). instruction sets and evaluation workflows. We consider single-pass evaluators as well as more advanced techniques, including (I) ensembling multiple evaluation runs and (2) staged workflows that decompose the complex evaluation task into focused, sequential steps. Our analysis delivers PROOFGRADER, an LLM--ased evaluator that combines a strong backbone LM with informative context (both reference solutions and a marking scheme) and simple ensembling that is surprisingly effective; it achieves low Mean Absolute Error (MAE) of 0.926 against expert scores, significantly outperforming naive baselines.
Finally, we validate the evaluators' practical utility in downstream best-of-n selection task, stan- dard proxy for assessing its potential as a reward signal (Gao et al., 2022 Frick et al. 2024 Malik eet al., 2025). At the performance gap between a naive binary evaluator (2.48) and the human oracle (4.62). It also outperforms computationally intensive, pairwise selection methods such Knockout tournament selection (Liu et al., 2025b). These results highlight PROOFGRADER's effectiveness in identifying high-quality proofs. To summarize, our contributions are three-fold:
16. PROOFGRADER achieves average score of 4.14/7, closing 78% of
We introduce PROOFBENCI an expert-graded math proof dataset consisting of problems from well-established contests and solutions from state-of-the-art reasoning models ($..
We conduct systematic study of key evaluator design factors and introduce PROOFGRADER, our best-performing evaluator that combines a strong reasoning LMM, a problem-specific marking scheme, and simple ensembling, achieving a strong alignment with expert ratings ($3).
We show that PROOFGRADER is on par with experts in a best-of-n selection task, improving a score from 2.48 (binary evaluator) to 4.14, highlighting its promise as reward model ($4).
2 PROOFBENCH. EXPERT-RATER MATH PROOF SOLUTIONS
We assess proof evaluators for human aligument on 0-7 scale, which requires fine- expert annotations on model-ggneeatee proofs across diverse sources and years. Existing resources are limited in scale or scoring granularity (Petrov al.) 2025] [ekoninck et al. (025). We therefore construct our own dataset, PROOFBENCH, consisting of 145 proof problems from six major math competitions across four years, with model-generated solutions by the state-of-the-art reasoning models: o3, Gemini-2.5-Pro, and DeepSeek-RR -0528. This section describes the data collection, annotation process, and statistics; 3
then describes how we use it to evaluate proof evaluators.
'The full dataset available at huggi
2

---

Published as a conference paper at ICLR 2026
PUTNAM
100
PUTNAX
Modan
USAMO
C4
125
APMO
3.00
100
RGMO
USAMO
Maxt:
150
3.08
10
20
3
Number of Unique Problems
Score 7)
Average Score (D 7)
(a) Problem Distribution
(b) Overall Score Distribution
(c) Competition Difficulty
Crnaf
Mone Median
Cust
1:30
7.12
7.00
1.00
3.80
3.19
Arg Scorr
Score Detribbtton
1.96
R1
0.72
0.30
1.33
2.05
2.10
2.89
151
D4G
USAKO
20%
43%
00%
133%
Problere
Gemina
R3
(d) Model vs. Competition
(e) Per-model Score Breakdown
(f) Contamination Analysis
Figure 2: Dataset information. (a) Distribution of unique problems across the six competitions. (b) Aggregate histogram of scores (0-7) across all models. (c) Competition difficulty ranking based on average scores; Putnam yielded the highest performance (3.09), while TST was the most challeng- ing (1.26). (d) Heatmap of average scores by model and competition (Green indicates higher per- formance). (e) Stacked bar chart detailing the percentage of problems achieving each score (Red=0, Green=7). (f) Per-model box plots comparing performance on problems released before vs. after the model's knowledge cutoff. There is consistent drop in mean and median scores post-cutoff.
Why 0-7 Scale? The 0-7 scale aligns the dataset with the established grading standards of pre- mier mathematics competition the source of our benchmark problems. Moreover, its fine-grained nature is critical for a nuanced assessment of proof quality, which is not captured by the binary "correc"/"inconttt grading, as we show throughout $3 and $4
2.1 DATASET CONSTRUCTION
Problem Sources. We collected 145 problems from the official websites of prestigious mathemat- ies competitions, including the APMO, EGMO, IMO, Putnam, USA TST, and USAMO, spanning the years 2022-2025. Whenever possible, problems were parsed from official PDFs, normalized, and accompanied by all available human-writte written solutions. This ensures the reliability of both prob- lem statements and ground-truth solutions, avoiding transcription errors commonly found in sec- ondary sources. When official solutions were unavailable, we supplemented the data with materials from reliable third-party websites. More details about each competition are provided in B
Proof Generation. For each problem, we generate proof from models (generators) using a stan- dardized prompt ($K) that asks for complete, self-contained proof. We generate proofss from three state-of-the-art reasoning models: OpenAl o3 (OpenAl 2025). Gemini-2.55Prr (Google DeepMind] 2025), and DeepSeek- -1-ee-----522 (DeepSeek-Al et al. 2025 which span both proprietary and open- source families.
Expert Grading Pipeline. Finally, annotation proceeds in two stages: marking scheme generation and model-generatee proof grading. All annotations were conducted by a team of five experts with Putnam-level national Math Olympiad experience, using carefully designed web interface.
Stage 1: Marking Scheme Finalization. A central challenge in creating this benchmark was en- suring consistent and scalable expert grading. While human-written rubrics are the gold standard, automated generation offers superior scalability and systematic way recognize key steps from provided reference solutions. In our method, the marking scheme is produced by an LLM MMS-
"The official Putnam Competition uses 0-10 scale. For consistency across competitions, we normalize all expert annotations unified 0-7 scale.
3

---

Published as a conference paper at ICLR 2026
Given the problem and reference solutions S, .Ms is prompted to output (i) a list of conditions under which scores are awarded or deducted, and (ii) a list trivial cases that should not be awarded any points. This generator graded the quality of the generated marking schemes, providing feedback that led to the selection of gemini-2.5-pro as the final MMs (see for details). An example of a generated marking scheme logether with problem text and reference solution is also provided in [C] (Fiure 4). From our expert evaluations, approximately 85% of the generated marking schemes in our final dataset were judged to be reasonable and of high quality.
developed through rigorous refinement process where experts also
Stage 2: Proof Grading, With problem-specife marking scheme, an expert annotator scores proof. Experts were instructed to treat the marking scheme as a detailed reference for the expected solution path, rather than rigid checklist. This is particularly important for fairly evaluating proofs that employed a novel method different from the provided ground-truth solutions, ensuring that valid alternative reasoning paths were credited appropriately. The experts will assign a score on a 0-7 scale. Before large-scale annotation, our experts underwent a cali- bration phase to align their judgments and finalize rules for handling edge cases, a critical step for minimizing inconsistencies. We assign 41% of the solutions to more than one annotator and their within-I-point agreement is 87.5%. Disagreements are further resolved through discussions.
given
2.2 DATASET STATISTICS
In total, PROOFBENCH consists 145 proof problems and 435 expert-annotated evaluations of proofs generated by OpenAI o3, Gemini-2.5-Prr and DeepSeck-RI R1-cc-------8.. Figuree 2] summarizes the dataset statistics, including the problem distribution across competitions (Figure 2ab and the aggregate score frequencies (Figure 2b).
Our analysis reveals several key findings about state-of-the-an reasoning models:
As shown in Figure 2el current models remain far from reliable; even the strongest models achieve scores of 6 or higher on fewer than 30% of problems. OpenAl o3 demonstrates the strongest overall performance with the highest
scores in 5/6 competitions (Figure 2d).
Performance varies considerably across problem sources (Figure 2c Figure 2d). Models per- form best PUTNAM (mean 3.09) but struggle markedly TST (mean 1.26).
Comparison of performance on problems released before versus after the knowledge cutoff (Fi- ure 2f) reveals consistent drop in scores newer problems, suggesting potential contamina- tion in the training data or a generalization gap on novel problems.
3 A SYSTEMATIC STUDY OF EVALUATOR DESIGNS
Using PROOFBENCII, systematically study the key design factors for math proof evaluator that produces fine- fine-grained scores (0-7) for model-generated solutions. We demonstrate that (i) a strong reasoning backbone with informative context (like marking schemes) yields substantial gains, and (ii) simple ensembling further improves accuracy and robustness.
3.1
EVALUATOR DESIGNS
Given the task of scoring model-generated solutions, naive evaluator would simply take problem and a generic instruction and assign a score. Instead, we systematically investigate design choices that enhance evaluation quality beyond this baseline. We first analyze single-pas, evaluators along three key dimensions: (i) backbone model, (ii) contextual input, and (iii) instruction set. We then extend this design to ensemble- beeeble-basedd and multi-stage evaluation workflows.
Single-Past Methods. A single-pass evaluator prompts backbone model M (which may or may not be the same as MMS) ) to grade a solution in one step. We analyze single-pass evaluators along three dimensions: the backbone LM, the context provided and the instructions given.
Backbone Model Choice. This refers to the LLM that is prompted to execute the evaluation. We compare six models that span different model families, sizes and reasoning capabilities: 03, GPT-5 (GPT-S-Thinking (OpenAl 2025)), GEMINI (Gemini-2.5-Pro)) 04-MINI (OpenAl 2025). RI (DeepSeck-BP R1-0528). and GPT-40 (OpenAl 2024).
Context. We consider four different context configurations, including: providing both the pre- generated marking scheme and the reference solution(s) (REF+MS); providing only the marking
4

---

Published as a conference paper at ICLR 2026
Model
Context
RMSE
MAE
WTAgi (%)
Kendall-7 1
Bias
Quality
REF+MS
1.273 = 0.16
0.964 = 0.12
76,5 = 4.3
0,502
-0.008
MS
1,418 0.17
1.069 + 0.14
72.8 4.3
0.477
-0.311
03
REF
1.575 0.14
1.330 +: 0.12
65.3 4.66
0.481
0.478
NONE
1.901
1.680 0.15
49.5
0.435
0.924
REF+MS
1.696 = 0.17
1.342 0.15
62.7 =
0.529
0.626
MS
1,502 = 0.17
1.142 = 0.14
70.0 4.2
0,488
0.151
GEMINI
REF
2.177 1. 0.14
1.910
0.15
39,9
1. 5.2
0.410
1.285
NONE
2.397 a 0.15
2.107
1: 0.16
36.6 1.
0.319
1.496
REF+MS
1,816 = 0.22
1.367 + 0.19
67.6 = 4.6
0.476
0.762
MS
1,636 = 0.22
1.234 +: 0.18
69.5
: 4.8
0.505
0.309
04-MINT
REF
1.858 = 0.19
1.504
+ 0.16
61.3 4.8
0.465
0.950
NONE
2.276 0.23
1.914 1: 0.21
49.5 5.3
0.430
1.569
REF+MS
1,353 = 0.16
1.055 + 0.13
73.2 = 4.6
0.532
0.295
MS
1.350 = 0.17
1.018 + 0.14
74.9
= 4.2
0.536
-0.175
GPT-5
REF
1.617 0.13
1.400
0.12
57.0
+ 5.4
0,501
0.799
NONE
1,919 = 0.14
1.708 + 0.14
46.5
= 5.4
0,404
1.034
REF+MS
1,735 0.22
1.357 +: 0.18
66.4 ::
0.429
0.732
MS
1,682 = 0.22
1,298 + 0.18
68.5 :
0.450
0.422
RI
REF
3.187 = 0.23
2.736 + 0.22
30.3 = 5.0
0.289
2.450
NONE
3,273 1 0.25
2.842 1: 0.25
33.5 1. 4.9
0,102
2.581
REF+MS
2.599 = 0.20
2.197 + 0.20
39.7 +
0.479
1.824
MS
2.245
0.21
1.827 + 0.19
50.4 :
0.377
1.001
GPT-40
REF
2.726 - 0.19
2.371
+ 0.18
36.0 + 4.9
0.343
1.887
NONE
3,402 = 0.26
3.001 + 0.26
31.9 = 4.9
0.208
2.614
Table 1: Performance comparison of 6 LLMs on 0-7 scale evaluation tasks under different context designs. Contexts: REF+MS (reference marking scheme), MS (marking scheme only), REF (reference only), NONE (no context). Values shown model bold; best and worst context highlighted. Arrows: & lower better, 1 higher better, closer zero better. Quality: Excellent, Good, Fair, Poor, Bad.
with + 95% CI. Best values per
scheme (MS); providing only the reference solution(s) (REF); and naive baseline where only basic grading instructions without any problem-specific context provided (NONE).
Instruction. The instruction set refers to the prompt that guides the evaluator on how to interpret and apply the provided context and perform the task. our study, the most informative context setting, REF+MS, we compared 3 types of instructions to understand how guidance using the context affects performance. These include NORM (Normal), flexible instruction that directs the model to follow the marking scheme but allows checkpoints; STRICT requires the model to adhere strictly to the provided marking scheme and penalize any deviation; and BASIC has minimal guidance on how use the provided materials.
map valid alternative approaches equal
Ensemble. We consider simple ensembling technique, which runs the same evaluator indepen- dently multiple times and combines the individual ratings with an aggregation operator, such as the mean or median. This technique is expected to produce more stable final score, reducing the variance of single-pass evaluators.
Staged Evaluation. We consider staged workflows that decompose the complex task of evalua- tion into sequence of more focused reasoning steps. We implement Binary & Errors Fine- Grained, which first predicts the binary correctness of the proof and identifies key errors, and then makes a second pass that uses this output generate a more calibrated, (-- score.
3.2 EVALUATION METRICS
We evaluate on the 0-7 scale using per per-problem metrics. All problems have the same number of responses (ri). Let P be the number of problems. For each problem p = 1,..., with expert scores yp and evaluator outputs Spi. we compute
1
MAE P
Voo
RMSE,
Σ n
Upi Upa)
1=1
i=1
5

---

Published as a conference paper at ICLR 2026
Biasp
71 2 (pp Ups), (
1 7V 2 1pps
Mpil S 1).
MAE and RMSE both measure errors relative to expert scores (lower is better) but RMSE penal- izes large mistakes more. WTAç1 measures the fraction of predictions that land within one point of the expert score. Bias measures the average signed error (systematic shift), with positive val- ues indicating over-scoring and negative values indicating under-scoring. For ranking agreement within a problem, we use Kendall's 76 (ties-adjusted). Detailed definitions of Kendall's 's 7y as well as aggregation formulas are provided in
3.3 WHAT FACTORS IMPROVE SINGLE-PASS EVALUATOR?
Effects of backbone model and contextual information. Table shows the results of single-pass evaluators across different backbone models and context settings. First, the strength of the backbone model strongly correlates with performance: moving from weaker to stronger models brings better calibrations (03 leads in nearly all metries). Second, contextual information consistently improves all metrics for every backbone, with the marking scheme (MS) contributing the majority of the gain relative to the reference solution alone (REF); combining both (REF+MS) provides small additional improvement primarily for the strongest backbone (03).
Model
Instruction
RMSE +
MAE
WTAg1 (%) f
Kendall-r f
Bias R
NORM
1.273
0.964
76.5
0.502
-0.008
03
STRICT
1.420
1.095
72.8
0.457
0.304
BASIC
1.348
1.039
73.0
0.501
0.165
NORM
1.816
1.367
67.6
0.476
0.762
04-MINI
STRICT
1.718
1.266
69.2
0.443
0.396
BASIC
1.817
1.360
67.6
0.437
0.724
NORM
1.696
1.342
62.7
0.529
0.626
GEMINI
STRICT
1.581
1.231
67.4
0.475
0.316
BASIC
1.773
1.424
61.7
0.469
0.832
Instruction ablation under REF+MS. Three instruction styles guide how the evaluator uses context: NORM (flexible use of the marking scheme, allowing valid alternatives). STRICT (literal adherence with penalties for deviations), and BASIC (minimal guidance). For Bias, the closer to 0, the better; for other metrics, means the lower the better while means the opposite.
Table 2:
Instruction style under REF+MS should match the backbone. With context fixed at REF+MS, instruction choice modulates the cilibration-ranking trade-off Table 2}. The strongest backbone (03) attains the best overall accuracy and near-zero bias with the more flexible NORM prompt, whereas mid-tier models (e.g., GEMINI, 04-MINI) benefit from the more prescriptive STRICT prompt. This pattern suggests that stronger models can reliably and flexibly apply the marking scheme (e.g., mapping alternative derivations to equivalent checkpoints), while mid-tier models re- quire more prescriptive guidance to reduce over-crediting and variance.
Per-generator results. A natural question that can arise is the potential bias when evaluators models.
MAE +
Bias
Evaluator
assess outputs generated by their To investigate this, we evaluate three single-pass evaluators, each using the same reference so- lutions and marking scheme, on per- per-generator splits, i.e., response sets grouped by their gener- ators 1R1, GEMINI, 03). The results in TTble 3 are mixed. On one hand, the strongest evaluator remains consistent across all generators: the 03- based evaluator. On the other hand, each evalua- tor exhibits its highest MAE outputs produced by its model family, indicating tendency toward within aethinggenerator underperformance. GEMINI and R exhibit a tendency to overscore their own responses, bias not observed in the 03 evaluator.
GEM.
03
GEM.
R1
03
1.12
0.78
0.99
-0.37
0.31
-0.07
GEMINI
1.23
1.62
1.18
-0.09
1.42
0.45
R1
1.18
1.43
1.50
0.23
0.96
0.99
Table 3: Per-generator evaluation accuracy.
Red cells indicate highest MAE and highest positive bias for each evaluator.

---

Published as a conference paper at ICLR 2026
3.4
Do ENSEMBLING AND STAGED WORKFLOWS IMPROVE SINGLE- PASS EVALUATION?
We next extend single-pass evaluators through either ensembling or multi-stage pipelines.
Model
Run
RMSE 4
MAE
WTAg1
kendall-7 t
Bias
1.265
0.981
75.5
0.509
0.018
Single (mean=std; n=5)
(#0.039)
(#0.028)
(#1.126)
(20.022)
(40.020)
03
Best single
1.225
0.944
77.1
0.540
0.009
MEAN
1.169
0.940
69.7
0.578
0.018
MEDIAN
1.185
0.926
77.7
0.540
0.008
MAJORITY
1.186
0.926
75.6
0.523
0.004
Table 4: Ensembling over multiple runs boosts performance and reduces variance for the 03 evaluator. We compare five individual runs against three aggregation strategies. Both mean and median aggregation achieve lower RMSE than the best single run. Mean aggregation is optimal for RMSE and ranking correlation (Kendall-T), while median aggregation excels on MAE and WTAg1-
Ensembling helps. For ensembling, we aggregate five independent 03 evaluation runs under REF+MS, with results reported Table 4] Compared to the best single run, averaging all runs reduces RMSE by ~0.06 (.225-+1.169) and improves rank agreement (Kendall-7 from 0.540 to 0.578). Median aggregation delivers the lowest MAE and highest WTAg1, and Majority matches that MAE while giving the smallest bias. Bolded cells in Table 4 mark these optima. Although abso- lute performance gain seems modest, one advantage of ensembling is reducing variance: single-pass evaluators, even with richer context, have high variance, whereas ensembling mitigates it.
Model
Design
RMSE
MAEJ
WTAgi (%))
Kendall-r
Bias
Single-pass (REF+MS)
1.273
0.964
76.5
0.502
0..08
03
Binary+Erroors + Fine-Grained
1.375
1.065
73.0
0.444
-0.102
Single-puss (REF+MS) Binary+Errors Fine-Grained
1.816
1.367
67.6
0.476
0.762
04-MINT
1.650
1.245
66.7
0.503
0.320
Single-pass (REF+MS) Binory+Errors > Fine-Grained
1.735
1.357
66.4
0.429
0.732
RI
1.708
1.299
68.4
0.371
0.528
03+04-MINI
Binary+Emorr Fine-Grained
1.513
1.126
71.4
0.458
-0.095
Table 5: Comparison of two-step Binary+Errors - Fine-Grained pipeline versus single-pass (REF+MS) evaluation across backbones. Staged design boosts mid-tier 04-MINI but degrades strong 03 performance; bold marks the best within each model block.
Staged pipelines may improve weaker models, but not stronger ones. For staged pipelines, Table 5) presents results for Two-step (Binary+Errors + Fine- Grained) workflow. We include 03-, 04-MINI- and R 1-ased evaluators. improves performance on the 04-MINI and R1 backbone (e.g., reducing RMSE from 1.816 to 1.650 and MAE from 1.367 to 1. 1.245 for 04-MINT) but hurts the strong 03 backbone (e.g., increasing RMSE from 1.273 to 1.375 and MAE from 0.964 to 1.065).
Putting everything together: PROOFGRADER. Based on our findings, we introduce PROOF- GRADER, the evaluator that is best- best-performing most consistently across all settings. PROOF- GRADER builds on the 03 model with the REF+MS configuration and the NORM instruction set, and incorporates simple ensembling techniques.
3.5 IN-DEPTH ANALYSIS
What are the common failure modes of PROOFGRADER? To investigate failure cases, we man- ually inspected 50 solutions where out of 5 ensemble runs deviated from human scores by least 2 points. We find that over-crediting (10.8%) and under-crediting (12.2%) occur at similar rates. Over-scoring typically arises when PROOFGRADER relies surface-level heuristics: it rewards solutions that mirror rubric structure or employ sophisticated frameworks (c.g., custom transforma- tions) even when central claims false. Furthermore, it often misclassifies fatal logical errors,

---

Published as a conference paper at ICLR 2026
Best-of-N Performance across Evaluators
Best-of-N with Comparison-band based Selectors
Human Onn'
Human Gra
FrooGeader
Przefirader
hrog grnde (he! 99)
Tommamans
Freg aineed (ec)
Avcrage human score of selested prodis
Tregrannd
Average human score of selesttdd proots
Banelith
Binery (eet
3.5
3.0
3.9
2.5
2.3
2.0
10
12
14
16
10
12
16
(number Samples)
(number samples)
(a) Evaluators BoN selectors. Ensemble-base fine-grained evaluator closely tracks the Human- Oracle curve, while the binary evaluators (green lines) perform much worse.
(b) Comparison-basee selectors. evaluator performs the best. Some strategies show signs of performance degradation at larger values of while approach remains robust.
fine-grained
Figure 3: Best-of-n with different selectors. Average best-of-n score over 29 problems for 03 (generator) as n increases from 16. PROOFGRADER our ensemble evaluator: the median over five independent 03 runs using the reference solution and marking scheme.
such broken reductions, minor justification issues. Under-scoring commonly results from penalizing early missteps in otherwise correct proofs, double-counting a single flaw, or demand- ing excessive jecro-justffications. By domain, failures are most frequent in Algebra and Geometry (~25% each). See for details.
Why reference solutions and marking schemes helpful? Comparing evaluators based 03 with NONE to those given REF+MS, we find that in over 60% cases, the evaluator without context overestimates the generation's correctness, i.e., it incorrectly assigns a higher score the generation. Crucially, this overestimation is not uniform: we observe a strong correlation (r 0.699, p < 0.001) between proof quality and evaluation gap. For low-quality proofs (scored 0- 2), the no-context evaluator over-scores by an average of 1.7 points. In contrast, for high-qualiny proofs (scored 5-7), the evaluator with context information assigns higher scores by 0.8 points on average. This asymmetric pattern supports our hypothesis that, without reference solutions or marking schemes, the evaluator struggles gauge proof progress.
What if the evaluator uses a different marking scheme from human experts? In our main setup, evaluators use the same marking schemes as the human graders. To test sensitivity to the rubric, we replace these with two alternatives: (i) regenerate marking scheme using the same prompt/model (new sample), and (ii) generate a marking scheme with a different model. We then evaluate the dataset with 03 given the reference solution plus each alternative scheme. In both cases, performance degrades relative to using the original marking scheme across different metrics, suggesting that evaluator accuracy depends close alignment with the marking scheme used by human although experts do not strictly follow them. Detailed results appear in H
DOWNSTREAM UTILITY: BEST-OF-N PROOF SELECTION
A good reward model should be able to reliably identify the best response in given batch. To under- stand how this ability correlates with the calibration metrics in Scction[.22] we measure the best-of-n (BoN) performance of various evaluators. In general, higher BoN score means the evaluator more reliably selects high-quality candidates for subsequent training, guiding real downstream gains. The applications include selecting high-quality training data via rejection sampling (e.g.. distillation) (Nakano et al., 2022; Touvron et al. 2023) and providing a reward signal for Reinforcement Learn-
ing (RL) (DeepSeek-Al et al.) 2025
Yu al. 2025
8

---

Published as a conference paper at ICLR 2026
In summary, this section answers critical question: Does the superiority of our fine- aine-grinedd evalu- ators, as measured by offline metrics, translate to an improvement in a downstream selection task?
Setup. To create a testbed, we use 03 to generate 16 candidate proofs for each of 29 selected problems from 2025, resulting in 464 unique proofs. All 464 of these candidates were then scored by three human experts using the pipeline described in $2 This dataset is distinct from PROOFBENCH and serves different purpose. For each problem, responses
graded by two experts with disagreements resolved through discussion. We test a selection of the fine-grained evaluators studied previously ($4.1) and several comparison-basee selection strategies ($4.2). The performance of each selection method is measured using a best-of-n (BoN) curve. Since an exhaustive evaluation over all (19) subsets is computationally intensive, we estimate the BoN curve using Monte Carlo subsampling. For each n,, sample a large number of subsets of size without replacement. For each subset, the evaluator selects the single proof with the highest assigned score. The performance the average human score of these selected proofs, aggregated over all subsamples and all 29 problems. We also include two key baselines; an oracle baseline and a mean baseline. The HUMAN ORACLE represents the performance ceiling, calculated as the average score of the best possible selection among the sampled n candidates. The MEAN BASELINE is calculated as the cumulative average score of the sampled candidates. All evaluators and selectors use 03 as the backbone model.
4.1 THE VALUE OF ENE-GGRINNED SCORING
As shown in Figure 3a our PROOFGRADER (an ensemble of five 03 runs with REF+MS) closely tracks the human- curve, consistently selecting higher-quality proofs as n increases. At n=16, it achieves an average score of 4.14. Comparing the four different fine-grained evaluators from $ REF+MS ensemble (PROOFGRADER), REF+MS, REF, and NONE, we find the same ranking holds. Notably, NONE performs significantly worse than those using marking scheme, confirming that the marking scheme a critical component.
We further compare with binary evaluators: the 03-hased models prompted to classify each proof as "Correct" or "Incorrect" rather than assigning a 007 score. In contrast to fine- traeggraied evaluators, the binary evaluators perform much worse. This limitation comes from collapsing all "correct" (or "incorrect") proofs into a single category, losing the ability to rank solutions. When multiple correct candidates exist, it cannot distinguish adequate proof (e.g.. a 5/7) from excellent one (7/7). We thus conclude that fine mne-grained scoring preserves relative ordering, making it essential for effective reward models in mathematical reasoning.
4.2 ROBUSTNESS AGAINST COMPARISON-BASTR SELECTION STRATEGIES
Prior work (Liu et al. 2025b) explored relative comparison methods for improving best-of-n (BoN), e.g., iteratively performing pairwise comparison between generations select the best one. This is significantly more computationally expensive than using PROOFGRADER, which scores each candidate independently without pairwise evaluation. We compare PROOFGRADER against two comparison-based methods: 'ourrnaeent (all-pairs) and Knockout (singleellmmination)
Tournament. For candidates 81y..., Sp, the selector performs pairwise comparisons for every un- ordered pair (i.j). Let Way E 0, indicate whether beats sj. We form a win-rate matrix W and compute wi Σizi Way. The selected answer is arg max, w; (tie-break by head-to-head or margin if applicable). This uses (?) comparisons.
Knockout. Candidates are placed in bracket; the selector compares pairs, and the winner advances until one remains. This requires n - comparisons per bracket. Similar to other approaches, for each n, we average the scores over multiple random brackets.
Figure 3b) shows that PROOFGRADER consistently dominates all selection variants across n, indi- cating that a strong, context-rich scoring function matters more than re-querying the same signal with pairwise procedures. Iterative strategies (Tournament, Knockout) still yield clear gains over mean baseline. Tournament may continue improving beyond n=16, but its quadratic cost O (()) is substantially higher than alternatives. Finally, Tournament and Knockout can also be applied at test time to boost proof quality, the results suggest that proof generation benefits from increased test-time compute, echoing prior findings (Dekoninck al. 2025

---

Published as a conference paper at ICLR 2026
5 RELATED WORK
Benchmarks for Mathematical Reasoning. GSM8K (Cobbe et al. 2021). MATH (Hendrycks
et al. (02T), and AIME provide math reasoning benchmarks but mainly target short, closed-form answers. More recent competition-basee benchmarks: Omni-MATH (Gao et al. 2024 Olympiad- Bench (He et al. 2024). HARP (Yue et al., 2024), and MathArena (Balunović et al. 2025 are more challenging yet still emphasize answer matching, leaving proof problems underrepresented. MathArena includes proofs but focuses only on latest competitions. Meanwhile, proof genera- tion has advanced rapidly: Gemini (Luong & Lockhart, (025),, unreleased OpenAI systems, and model-agnostic verify-and-refing methods achieve IMO gold-level performance even for base mod- els (Huang Yang 2025). but evaluations still mostly rely on manual grading (Petrov et al. 2025).
Automated Evaluation for Generative Outputs. LLM-as-a-judge methods use LLMs to score open-ended responses along dimensions such as correctness. enabling scalable evaluation while reducing human annotation costs (Zheng et al., [023b] Li et al.] 2024). Recent work has further examined the reliability of LLM judges on more challenging tasks (Tan al.] 2025 Frick et al. 2024). For mathematical proofs, however, automated evaluation remains relatively underexplored. Earlier work (Welleck et al.) 2022, Frieder et al. 2023) often relies on human evaluation or lexical automatic metries, which are difficult to scale and insufficient for verifying complex, competition- level proofs. Existing approaches are also often highly specialized, such as IneqMath (Sheng et al.] 2025 for inequality proofs, or lack fine-grained evaluation; for example, the dataset of Dekoninck et al. 2025) provides only binary annotations. As a result, many studies still depend on manual evaluation for model-generated proofs (Petrov et al. 2025 Huang & Yang) 2025).
Formal Proof Generation. A complementary line work uses interactive theorem provers, where LLMs generate proofs in formal languages (e.g., Lean, Isabelle) whose correctness can be automatically checked. Key benchmarks include miniF2F (Zheng et al.) [02T). FIMO (Liu et al.) 2023). PutnamBench (Tsoukalas al.] 2024), which formalize competition problems, and Lean- Workbook (Ying et al. 2202)). a broad Lean corpus. While this approach is promising, our work focuses on informal proofs for two reasons. First, natural language remains the primary medium for mathematical communication in education and research. Second, the task of automatically translat- ing informal proofs into a formal language, i.e., autoformalization, is itself an exceptionally chal- lenging research problem (Gao et al., 2025 Liu et al. 2025a).
Summary. While prior work has established the importance of proof-based evaluation and ex- plored the systematic, empirical study of the evaluator design space for mathematical proofs, nor provided scalable methodology for creating the fine-grained, rubric-driven annotations necessary for such a study. The key factors that determine evaluator robustness remain largely uninvestigated.
paradigm, a critical gap remains. No existing work has conducted a
6 CONCLUSION
We tackle the challenge of reliably evaluating natural-language mathematical proof' by introduc- ing PROOFBENCII the first comprehensive, fine-grained proof grading dataset spanning multiple contests and years. Using PROOFBENCH, we systematically explore the evaluator design space and show that strong backbones, problem- specific marking schemes, and ensembling are important, re- sulting in PROOFGRADER, our best- perst-erformin evaluator. Finally, demonstrate practical utility by showing that using PROOFGRADER for best-of-n selection closely tracks oracle performance.
Limitations and Future Work. While our work advances reliable evaluation of natural language math proofs, several limitations remain. First, our scope, i.e., olympiad-style proofs, does not yet cover research-level problems, or educational settings; extending to these regimes is an important next step. Second, evaluator quality can likely be improved through better prompting and workflow designs. Our dataset and analyses are intended as a foundation for such work, and we encourage future work to continue improving evaluators using PROOFBENCH as a testhed. Our evaluation focuses exclusively on mathematical correctness. Other crucial aspects such as readability, clarity, and elegance, are not currently assessed, and we leave the development of metrics for these qualities as future work. Third, our strongest evaluators currently rely on closed models. Although our design is model-agnostic further improving fully open-source evaluators to match those based on closed models is an important direction. While our best-of-n experiments use the evaluator selection signal, a first step toward training-time time integration, we have not yet trained with it; incorporating into proof generator training is promising future direction.
10

---

Published as a conference paper at ICLR 2026
ACKNOWLEDGEMENTS
We thank Robin Said Sharif and Bradley Louie for their invaluable contributions to the ProofBench dataset. We also thank Jingxuan He, Zhaoyu Li, and Tony Lian for valuable discussions during the early stages of this work, well as Prasann Singhal and Aviral Kumar for their feedback earlier draft of the paper.
This work partially supported by the Google BAIR Commons Program (2025-2020 and the Gemini Academic Program Award. Sky Computing Lab is supported by gifts from Accenture, Amazon, AMD, Anyscale, Broadcom, Google, IBM, Intel, Intesa Sanpaolo, Lambda, Lightspeed, Mibura, NVIDIA, Samsung SDS, and SAP.
ETHICS STATEMENT
Our work adheres to the ICLR Code of Ethies. The primary ethical considerations for this research involve the creation and use of our dataset, PROOFBENCH, and the potential for biases in our LLM- based evaluator. The dataset was constructed using problems from publicly accessible mathematics competitions. The expert annotations, which form the core of our benchmark, were provided by qualified individuals who were fairly compensated for their time and expertise.
REPRODUCIBILITY STATEMENT
We are committed to ensuring the reproducibility our research. To this end, we will publicly release all code, data, and supplementary materials upon publication. The PROOFBENCH, includ- ing all problems, LLM--geerrted solutions, expert-annotated scores, and problem-specife marking schemes, will be made available. Our source code will include scripts to reproduce the experi- ments presented this paper, including the implementation of our evaluator, PROOFGRADERand all prompts used.
REFERENCES
Mislav Balunović, Jasper Dekoninck, Ivo Petrov, Nikola Jovanović, and Martin Vechev. Matharena: Evaluating ilms on uncontaminated math competitions, 2025. URL
org/
abs/ /20552505.2m 23281
Karl Cobbe, Vineet Kosaraju, Mohammad Bavarian, Mark Chen, Heewoo Jun, Lukasz Kaiser, Matthias Plappert, Jerry Tworek, Jacob Hilton, Reiichir Nakano, Christopher Hesse, and John Schulman. Training verifiers to solve math word problems, 2021. URL pittps://arxivv
g 1/abs/2110..0 14168
DeepSeek-AI, Daya Guo, Dejian Yang. Haowci Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang. Xiao Bi, Xiaokang Zhang, Xingkai Yu, Yu Wu, Z. F. Wu, Zhibin Gou, Zhihong Shao, Zhuoshu Li, Ziyi Gao, Aixin Liu, Bing Xue, Bingxuan Wang, Bochao Wu, Bei Feng, Chengda Lu, Chenggang Zhao, Chengqi Deng, Chenyu Zhang, Chong Ruan, Damai Dai, Deli Chen, Dongjie Ji, Erhang Li, Fangyun Lin. Fucong Dai, Fuli Luo, Guangbo Hao, Guanting Chen, Guowei Li, H. Zhang, Han Bao, Hanwei Xu, Haocheng Wang, Honghui Ding. Huajian Xin, Huazuo Gao, Hui Qu, Hui Li, Jianzhong Guo, Jiashi Li, Jiawei Wang, Jingchang Chen, Jingyang Yuan, Junjie Qiu, Junlong Li, J. Cai, Jiaqi Ni, Jian Liang, Jin Chen, Kai Dong, Kai Hu, Kaige Gao, Kang Guan, Kexin Huang, Kuai Yu. Lean Wang, Lecong Zhang, Liang Zhao, Litong Wang. Liyue Zhang, Lei Xu, Leyi Xia, Mingehuan Zhang, Minghua Zhang, Minghui Tang, Meng Li, Miaojun Wang, Mingming Li, Ning Tian, Panpan Huang, Peng Zhang, Qiancheng Wang, Qinyu Chen, Qiushi Du, Ruiqi Ge, Ruisong Zhang, Ruizhe Pan, Runji Wang, R. J. Chen, R. L. Jin, Ruyi Chen, Shanghao Lu, Shangyan Zhou, Shanhuang Chen, Shengfeng Ye, Shiyu Wang. Shuiping Yu, Shunfeng Zhou, Shuting Pan, S. S. Li, Shuang Zhou, Shaoqing Wu, Shengfeng Ye, Tao Yun. Tian Pei, Tianyu Sun, T. Wang, Wangding Zeng, Wanjia Zhao, Wen Liu, Wenfeng Liang, Wenjun Gao, Wenqin Yu, Wentao Zhang, W. L. Xiao, Wei An, Xiaodong
Liu, Xiaohan Wang, Xiaokang Chen, Xiaotao Nie, Xin Cheng, Xin I Liu, Xin Xie, Xingchao Liu,

---

Published as a conference paper at ICLR 2026
Xinyu Yang, Xinyuan Li, Xuecheng Su, Xuheng Lin, X. Q. Li, Xiangyue Jin, Xiaojin Shen, Xi- aosha Chen, Xiaowen Sun, Xiaoxiang Wang, Xinnan Song, Xinyi Zhou, Xianzu Wang, Xinxia Shan, Y. K. Li, Y. Q. Wang. Y. X. Wei, Yang Zhang, Yanhong Xu, Yao Li, Yao Zhao, Yaofeng Sun, Yaohui Wang, Yi Yu, Yichao Zhang, Yifan Shi, Yiliang Xiong, Ying He, Yishi Piao, Yisong Wang, Yixuan Tan, Yiyang Ma, Yiyuan Liu, Yongqiang Guo, Yuan Ou, Yuduan Wang, Yue Gong, Yuheng Zou, Yujia He, Yunfan Xiong, Yuxiang Luo, Yuxiang You, Yuxuan Liu, Yuyang Zhou, Y. X. Zhu, Yanhong Xu, Yanping Huang, Yaohui Li, Yi Zheng, Yuchen Zhu, Yunxian Ma, Ying Tang, Yukun Zha, Yuting Yan, Z. Z. Ren, Zehui Ren, Zhangli Sha, Zhe Fu, Zhean Xu, Zhenda Xie, Zhengyan Zhang, Zhewen Hao, Zhicheng Ma, Zhigang Yan, Zhiyu Wu, Zihui Gu, Zijia Zhu, Zijun Liu, Zilin Li, Ziwei Xie, Ziyang Song. Zizheng Pan, Zhen Huang. Zhipeng Xu, Zhongyu Zhang, and Zhen Zhang. Deepseek-rl: Incentivizing reasoning capability in Ilms via reinforce- ment learning. 2025. URL htt.:htttt:/aaae
org/ abs abw.///..111 12948
Jasper Dekoninck, Ivo Petrov, Kristian Minchev, Mislav Balunovic, Martin Vechev, Miroslav Marinov, Maria Drencheva, Lyuba Konova, Milen Shumanov, Kaloyan Tsvetkov, et al. The open proof corpus: large-scale study of Ilm-generated mathematical proofs. arXiv preprint wrXiv:2506.21622 2025.
Evan Frick, Tianle Li, Connor Chen, Wei-Lin Chiang, Anastasios N. Angelopoulos, Jiantao Jiao, Banghua Zhu, Joseph E. Gonzalez, and lon Stoica. How to evaluate reward models for rlhf, 2024. abs/ /41 O. 4472
URL httttp://aaxiv.orrt
Simon Frieder, Luca Pinchetti, Alexis Chevalier, Ryan-Rhys Griffiths, Tommaso Salvatori, Thomas Lukasiewiez, Philipp Christian Petersen, and Julius Berner. Mathematical capabilities of chatgpt, 2023. WRRLhttps: ///a//axvvv// org /2001. 13867
Bofei Gao. Feifan Song, Zhe Yang. Zefan Cai, Yibo Miao, Qingxiu Dong, Lei Li, Chenghao Ma, Liang Chen, Runxin Xu, Zhengyang Tang, Benyou Wang, Daoguang Zan, Shanghaoran Quan, Ge Zhang, Lei Sha, Yichang Zhang, Xuancheng Ren, Tianyu Liu, and Baobao Chang. Omni- math: A universal olympiad level mathematic benchmark for large language models, 2024. URL htttss://arxae org/ abs 2410. 07985
Guoxiong Gao, Yutong Wang, Jiedong Jiang, Qi Gao, Zihan Qin, Tianyi Xu, and Bin Dong. Herald: A natural language annotated lean 4 dataset. In The Thirteenth International Conference on Learning Representations, 2025. URL httpt:t/////. http//pppnneeeeeeee/ee net. wew.eee/orrrmmm-meeirr t.hhz]
Leo Gao, John Schulman and Jacob Hilton. Scaling laws for reward model overoptimization, 2022.
URL
www.ooggg/bbb//aaoee attp:/...././/......../.. 10760
Google DeepMind. Gemini 2.5 pro: our most advanced model for complex tasks. https://ce
epmi nommind.c. wod.ggoole/mien
s
2025. Accessed: 2025-11-12.
Chaoqun He, Renjie Luo, Yuzhuo Bai, Shengding Hu, Zhen Leng Thai, Junhao Shen, Jinyi Hu, Xu Han, Yujie Huang, Yuxiang Zhang, Jie Liu, Lei Qi, Zhiyuan Liu, and Maosong Sun. Olympiadbench: A challenging benchmark for promoting agi with olympiad-leve bilingual mul- timodal scientific problems, 2024. URL /tLLtttss////xii// org/ 24022 14008
Dan Hendrycks, Collin Burns, Saurav Kadavath, Akul Arora, Steven Basart, Eric Tang, Dawn Song, and Jacob Steinhardt. Measuring mathematical problem solving with the math dataset. arXiv preprint arXiv:2 103.0377. 2021.
Yichen Huang and Lin F. Yang. Gemini 2.5 pro capable of winning gold at imo 2025, 2025. URI 15855
Tianle Li, Wei-Lin Chiang, Evan Frick, Lisa Dunlap, Tianhao Wu, Banghua Zhu, Joseph E. Gon- zalez, and Ion Stoica. From crowdsourced data to high-quality benchmarks: Arena-hard and benchbuilder pipeline, 2024.
//tp///aiii/////////i//ee//eaaa/ org/ abs/ /24/ 11939
Chengwu Liu, Jianhao Shen, Huajian Xin. Zhengying Liu, Ye Yuan, Haiming Wang, Wei Ju, Chuanyang Zheng, Yichun Yin, Lin Li, et al. Fimo: A challenge formal dataset for automated theorem proving. arXiv preprini 042245530 2023.
12

---

Published as a conference paper at ICLR 2026
Qi Liu, Xinhao Zheng, Xudong Lu, Qinxiang Cao, and Junchi Yan. Rethinking and improving autoformalization: Towards a faithful metric and a dependency retrieval-basee approach. In The Thirteenth International Conference Learning Representations, 2025a. URL https: enrevi ew net. / ff forum? meet/ d=hub2At2DsQ
Yantao Liu, Zijun Yao, Rui Min, Yixin Cao, Lei Hou, and Juanzi Li. Pairjudge rm: Perform best- of-n sampling with knockout tournament, 2025b. URL ht
13007
Thang Luong and Edward Lockhart. Advanced version of gemini with deep think officially achieves gold-medal standard at the international mathematical olympiad, July 2025. URL httpp://ds:
e-think-officiialllyacheeee gold medal sataal-staddadd at -te -et-thh-interaaa tional hat.aa/eeeeemmtcllllllmm.mmmoaoa
Blog post.
Saumya Malik, Valentina Pyatkin, Sander Land, Jacob Morrison, Noah A. Smith, Hannaneh Ha-
jishirzi, and Nathan Lambert. Rewardhench Advancing reward model evaluation, 2025. URL,
attps://arze org/ attp://bs/225055 01937
Reiichiro Nakano, Jacob Hilton, Suchir Balaji, Jeff Wu, Long Ouyang, Christina Kim, Christopher Hesse, Shantanu Jain, Vineet Kosaraju, William Saunders, Xu Jiang, Karl Cobbe, Tyna Eloundou, Gretchen Krueger, Kevin Button, Matthew Knight, Benjamin Chess, and John Schulman. Webgpt:
Browser-assisted question-anssee answering with human feedback, 2022. URL bttps::/arxxii...
g 3/abs/2112.0933
OpenAl. Gpt-40 system card. Technical report, OpenAI, August 2024. URL https: op enai enai.com/gpt 4c system card. pdf Accessed: 2025-11-15.
OpenAl. o3 and o4-mini system card. Technical Report Version 2, OpenAl, April 2025. URL
http:://cccc..ppeeaaacoreeeeee22 03-and-o4-mini---
card. pdf
Accessed: 2025-11-12.
OpenAl. Gpt-5 system card. Technical report, OpenAl, August 2025. URL htttt::ss://dd
enai.
card. pdf
Accessed: 2025-11-15.
Ivo Petrov, Jasper Dekoninck, Lyuben Baltadzhiev, Maria Drencheva, Kristian Minchev, Mislav Balunović, Nikola Jovanović, and Martin Vechev. Proof or bluff? evaluating Ilms on 2025 usa math olympiad. arXiv preprint arXiv:2503.21934 2025.
Zhihong Shao, Peiyi Wang, Qihao Zhu Runxin Xu, Junxiao Song, Xiao Bi, Haowei Zhang. Mingchuan Zhang, Y. K. Li, Y. Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathe- matical reasoning in open language models, 2024. URL htths::::: :/arxivv/////vi/////a/aa org/ abs 24C2
003300
Jiay Sheng, Luna Lyu, Jikai Jin, Tony Xia, Alex Gu, James Zou, and Pan Lu. Solving inequality proofs with large language models, 2025. URL http://aavvvvo/////e org/ wwwp/og////////oo///////////eae/
abs/////////// / 220665066660 07927
Sijun Tan, Siyuan Zhuang, Kyle Montgomery, William Y. Tang, Alejandro Cuadron, Chenguang Wang, Raluca Ada Popa, and Ion Stoica. Judgebench: A benchmark for evaluating llm-based judges, 2025. httpt://s wwwp:xivv.rggeeeo
Hugo Touvron, Louis Martin, Kevin Stone, Peter Albert, Amjad Almahairi, Yasmine Babaei, Niko- lay Bashlykov, Soumya Batra, Prajjwal Bhargava, Shruti Bhosale, Dan Bikel, Lukas Blecher, Cristian Canton Ferrer, Moya Chen, Guillem Cucurull, David Esiobu, Jude Fernandes, Jeremy Fu, Wenyin Fu, Brian Fuller, Cynthia Gao, Vedanuj Goswami. Naman Goyal, Anthony Hartshorn, Saghar Hosseini, Rui Hou, Hakan Inan, Marcin Kardas, Viktor Kerkez, Madian Khabsa, Isabel Kloumann, Artem Korenev, Punit Singh Koura, Marie-Anne Lachaux, Thibaut Lavril, Jenya Lee, Diana Liskovich, Yinghai Lu, Yuning Mao, Xavier Martinet, Todor Mihaylov, Pushkar Mishra, Igor Molybog, Yixin Nie, Andrew Poulton, Jeremy Reizenstein, Rashi Rungta, Kalyan Saladi, Alan Schelten, Ruan Silva, Eric Michael Smith, Ranjan Subramanian, Xiaoqing Ellen Tan, Binh Tang, Ross Taylor, Adina Williams, Jian Xiang Kuan, Puxin Xu, Zheng Yan, Iliyan Zarov, Yuchen Zhang, Angela Fan, Melanie Kambadur, Sharan Narang, Aurelien Rodriguez, Robert Stojnic, Sergey Edunoy, and Thomas Scialom. Llama 2: Open foundation and fine-tuned chat models, 2023. URL (tl.htt::: a/axx/rriii org abs aataaba/33002 /230 09288
13

---

Published as a conference paper at ICLR 2026
George Tsoukalas, Jasper Lee, John Jennings, Jimmy Xin, Michelle Ding, Michael Jennings, Ami- tayush Thakur, and Swarat Chaudhuri. Putnambench: Evaluating neural theorem-provee on the putnam mathematical competition. Advances in Neural Information Processing Systems, 37: 11545-1 1569, 2024.
Yiping Wang. Qing Yang, Zhiyuan Zeng. Liliang Ren, Liyuan Liu, Baolin Peng, Hao Cheng, Xuehai He, Kuan Wang, Jianfeng Gao, Weizhu Chen, Shuohang Wang, Simon Shaolei Du, and Yelong Shen. Reinforcement learning for reasoning in large language models with one training example, 2025. URL pectps://arxive www.eiiw....ro...ooooo wbw.absga//oooooooooooooboooeo.s haarrggbbb/25544 20571
Sean Welleck, Jiacheng Liu, Ximing Lu, Hannaneh Hajishirzi, and Yejin Choi. Naturalprover: Grounded mathematical proof generation with language models, 2022. URL httphhtts//ee
V. w.org/abs/2200 12910
An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, Chujie Zheng, Dayiheng Liu, Fan Zhou, Fei Huang, Feng Hu, Hao Ge. Haoran Wei, Huan Lin, Jialong Tang, Jian Yang. Jianhong Tu, Jianwei Zhang, Jianxin Yang, Jiaxi Yang, Jing Zhou, Jingren Zhou, Junyang Lin, Kai Dang. Keqin Bao, Kexin Yang, Le Yu, Lianghao Deng, Mei Li, Mingfeng Xue, Mingze Li, Pei Zhang, Peng Wang. Qin Zhu, Rui Men, Ruize Gao, Shixuan Liu, Shuang Luo, Tianhao Li, Tianyi Tang, Wenbiao Yin, Xingzhang Ren, Xinyu Wang, Xinyu Zhang, Xuancheng Ren, Yang Fan, Yang Su, Yichang Zhang, Yinger Zhang, Yu Wan, Yugiong Liu, Zekun Wang, Zeyu Cui, Zhenru Zhang, Zhipeng Zhou, and Zihan org/ 2205 09388
Qiu. Qwen3 technical report, 2025, URL httpt:
Huaiyuan Ying, Zijian Wu, Yihan Geng. Jiayu Wang. Dahua Lin, and Kai Chen. Lean workbook: A large-scale lean problem set formalized from natural language math problems. Advances in Neural Information Processing Systems, 37:105848-10586, 2024.
Qiying Yu, Zheng Zhang, Ruofei Zhu, Yufeng Yuan, Xiaochen Zuo, Yu Yue, Weinan Dai, Tiantian Fan, Gaohong Liu, Lingjun Liu, Xin Liu, Haibin Lin, Zhiqi Lin, Bole Ma, Guangming Sheng, Yuxuan Tong, Chi Zhang, Mofan Zhang, Wang Zhang, Hang Zhu, Jinhua Zhu, Jiaze Chen, Jiangjie Chen, Chengyi Wang, Hongli Yu, Yuxuan Song, Xiangpeng Wei, Hao Zhou, Jingjing Liu, Ying Ma, Ya-Qin Zhang, Lin Yan, Mu Qiao, Yonghui Wu, and Mingxuan Wang. Dapo: An open-source Ilm reinforcement learning system scale, 2025. URL https:
25033 14476
Albert S. Yue, Lovish Madaan, Ted Moskovitz, DJ Strouse, and Aaditya K. Singh. Harp: A chal- http:/awwiiiaaaaaaaaaaaa/aa /ab
lenging human-annotated math reasoning benchmark, 2024. URL
s 5/2412. 08819
Kunhao Zheng, Jesse Michael Han, and Stanislas Polu. Minif2f: cross-system benchmark for formal olympiad-level mathematics. arXiv preprint arXiv:2109.001 10, 2021.
Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric Xing, Hao Zhang, Joseph E. Gonzalez, and Ion Stoica. Judging LLMMass-a-udae with MT-bench and chatbot arena. In Shirty-sevntth Conference on Neural Information Processing Systems Datasets and Benchmarks Track, 2023a. URL https:
/openreview. wtw.:/neettooommmoooooooooooo
Lianmin Zheng, Wei-Lin Chiang, Ying Sheng, Siyuan Zhuang, Zhanghao Wu, Yonghao Zhuang, Zi Lin, Zhuohan Li, Dacheng Li, Eric P. Xing. Hao Zhang, Joseph Gonzalez, and lon Stoica. Judging judge with btnbench and chatbot arena, 2023b. U httpss:/aa......../
g/ //abs/2300 2206. 05685
14

---

Published as a conference paper at ICLR 2026
A THE USE OF LARGE LANGUAGE MODELS (LLMS)
In preparing this submission, we used LLMs as general-purpose writing assistant. The human authors were responsible for the entire research process, including the initial ideation, experimental design, implementation, and data analysis. During writing, authors first creating complete draft of each section, which included all core ideas and technical details. The LLM was then used to revise this draft for clarity, conciseness, and grammatical correctness. Its role was strictly limited to improving the language and flow of the text. All scientific contributions and claims presented in this paper originate from the authors, who take full responsibility for the final content
B PROBLEMS INFORMATION
Table 6 provides short descriptions of the contests which we sourced problems from. The data information for the collected problems available in Table 7 Problem 4 from EGMO 2023 was intentionally removed because contains figure in problem text.
Contest
Description
Source
APMO
The Asia Pacific Mathematical Olympiad is a regional proof-based contest for high school
apmo-official.org
students Asia-Pacific. It features five challenging problems solved over fixed time window, proctored locally.
EGMO
The European Girls' Mathematical Olympiad is an international two-day proof contest for female students. modeled after the IMO. It promotes participation and excellence among young women in mathematics.
egmo.org
IMO
The International Mathematical Olympiad the premier global high school math competi- tion. Over two days, students tackle six proof problems that test creativity, rigor, and depth.
imm--ofiicill.org for problems and solutions from 2022 2025 and IMO 2025 problems. We use Evan Chen's Notes for IMO 2025 so- lutions.
PUTNAM
The William Lowell Putnam Mathematical Competition is a highly challenging proof exam for undergraduates in the U.S. and Canada. It consists of 12 problems emphasiz- ing ingenuity and precise argumentation.
mma.org/puttnn
TST
Team Selection Tests are national-level olympiad exams used by USA to select their IMO teams. Problems mirror international difficulty and assess readiness for global competition.
Evan Chen's Notes
USAMO
The United States of America Mathematical Olympiad is an invitational proof contest fol- lowing AMC/AIME qualification. It identifics top U.S. high school problem solvers and feeds into further training and team selection.
Evan Chen's Notes
Table Brief descriptions of core contests.
C ANNOTATION PIPELINE DETAILS
C.1 MARKING SCHEME GENERATION: EVALUATION PROCESS
We began by evaluating LLM-generated marking schemes with the objective of selecting optimal configuration for reliable marking scheme generation. Two factors were considered: the backbone L.L and the prompting strategy (instructions).
15

---

Published as a conference paper at ICLR 2026
Contest
2022
2023
2024
2025
Total
APMO
5
S
5
20
EGMO
6
IMO
6
6
6
PUTNAM
12
12
12
36
TST
6
6
18
USAMO
6
6
24
Total per year
35
40
41
29
145
Table Problem counts by contest and year.
Throughout the evaluation process, two domain experts independently graded all marking schemes 0-3 scale using the rubrie defined below. The experts compared two marking schemes at a time and rated both (the evaluation interface shown Figure
Evaluation Protocol.
Scoring Guidelines:
The rubric is completely incorrect.
1: The rubric seems reasonable, but the distinctions between scores and point allocations are not well-defined.
The rubric is mostly correct, though details could be improved (e.g., inclusion of corner cases).
The rubric is excellent-on par with those written by expert human graders.
We had the following experimental configuration:
Models: We compared two state-of-the-art models: OpenAl o3 and Gemini-2.5-Pro.
Prompts: Initial prompts were designed based on guidance from Evan Chen Chen's framework suggests organizing marking schemes into three sections: (1) list of award points (indicating what progress merits credit), (2) a list of zero-credit points (for trivial observations), and (3) list of also designed to enforce consistent output formatting.
deductions. The prompts
We compared zero-shot and few-shot prompting strategies. For few-shot prompting, examples were selected from Evan Chen's rubrics for the United States Emergent Mathematicians Olympiad (USEMO) as marking schemes from other competitions are not publicly available.
Stage 1 (Model Selection): We evaluated 18 problems, yielding 36 marking schemes (one per model). Zero-shot prompting was used for all generations. The two annotators differed by more than point in only three cases. Overall, they preferred Gemini-2.5-Pro. Based on annotator feedback, we revised the prompts accordingly.
Stage (Prompt Selection): We evaluated 36 problems, comparing zero-shot and few-shot prompt- ing strategies. Both experts rated zero-shot prompting slightly better. Specifically, Expert 1 rated zero-shot as better in 13/36 cases, worse in 10/36 cases, and equal in 13/36 cases; Expert rated zero-shot as better in 17/36 cases, worse in 8/36 cases, and equal in 1 1/36 cases. Feedback from Stage 2 was used to further refine the prompt design.
Average Rubric Quality: Of the 36 rubrics generated in Stage 2, 35 were rated 2 or by both annotators, indicating high overall quality. Note that we did not generate or evaluate rubrics for all available problems.
Final Configuration. The final configuration selected based both quantitative annotator scores and qualitative feedback. While no single setup produced perfect rubrics across all prob- lems, we chose the configuration with the best overall performance: Gemini-2.5-Pro with zero-shot prompting.
n-guidance dance -ww-uu.semmo...
https://web.evantt wtt../ccccooooeeeee.ee html
16

---

Published as a conference paper at ICLR 2026
Annotator Feedback. We include representative feedback from the annotators below provide insight into the rubric quality and areas for improvement:
Expert Annotator Comments
General observations:
Several problems included deductions for minor calculation errors, despite the prompt explicitly instructing against this practice. Due to the frequency of this issue, we did not comment on every
occurrence.
Problems repeated from previous batches retained preloaded feedback from earlier evaluations. Clearing this feedback between batches would prevent confusion about which problems have been completed versus those requiring re-evaluation.
Many problems awarded partial credit merely for stating a lemma, definition, or formula without requiring proof or demonstration of its significance. This was the most significant issue to address in future iterations.
Partial credit allocation typically followed the official solution path rather than recognizing alterna- tive approaches that yield weaker (but still meaningful) results. For example, in ASEEO-2002-PP the Al-generated rubrics allocated partial credit across steps in the official solution, whereas the official marking scheme (by Evan Chen) awarded partial credit based on the strength of justified bounds. This discrepancy arises because the model cannot anticipate altemattvve solution strategies without explicit examples. A prompt modification could encourage such flexibility- -or instance: "prove X bound [max 4] (step [additive 1J, step 2 [additive 3]) (proving weaker bound Y earns 2 points partial)."
The "additive up scoring feature in generated schemes does align well with available contest rubrics. Whether this is acceptable depends on the overall objectives of the evaluation system.
An example of marking scheme together with the problem and reference solutions is shown in Fig- ure
C.2 EVALUATION OF
PROOFS
Pilot Calibration. Using the frozen rubric generator, we produced problem-specific marking schemes and calibrated the scoring protocol. Two experts independently annotated 36 problems with 3 responses each (108 total solutions). The experts then discussed disagreements to reach con- sensus and refine their grading protocol accordingly. They will share their experience with other experts.
Annotation Process. Throughout this study, two datasets were evaluated by a team of five experts: ProofBench and the dataset used in the best-of-n experiments. For each solution, experts were provided with the problem statement, reference solutions, the corresponding marking scheme, and optional Al Al-generated judgment to inform their final grade 0-7 scale. Screenshots of the annotation interface are shown in Figures and
Double Grading.
To ensure annotation quality, more than 40% of solutions both datasets were independently graded by two experts. Specifically:
All problems from 2025 competitions, as well as all EGMO (European Girls' Mathematical Olympiad) and APMO (Asian Pacific Mathematics Olympiad) problems, were double-graded.
ProofBench:
Best-of-n datasets: For each problem, 8 out of 16 responses were double-graded
The annotation process was conducted in dedicated meeting rooms with experts working collabora- tively. The entire process was supervised by a PhD student and professor (both co-authors of this work).
Disagreement Resolution. Disagreements were flagged when expert ratings differed by more than 1 point. In such cases, the experts discussed their rationales and justifications. On the 0-7 scale,
17

---

Published as a conference paper at ICLR 2026
Problem. Let > l: 2 1 be integers. Let P(x) R[x] be polynomial of degree with repeated roots and P(O) * O. Suppose that for any real numbers da,-.. .., the product dgd1 as is zero. Prove that P(x) has nonreal root.
... ag such that dg." + +... a1
divides P(x),
Reference Solution. By considering any k + 1 roots of P. WLOG assume l + 1. Suppose P(x) (x +r). (n) has P(0) # 0. Then each polynomial (z))) P r:) of degree has coefficient.
The leading and constant coefficients each are nonzero, leaving n other coefficients. By pigeonhole, P. and P22 share a zero coefficient position, say z" for some 1 f < Y
Claim. If Pi and P2 both have x² coefficient zero, then Q(r) = (x + r3) (x + rw.) has consecutive zero coefficients by bb-1 = 0.
+ by- The x² caefficient of Pl, being zero means hence by = 1 = (using T; monzero, distinct).
Proof. By Victa, let Q(2) x"= ribs + bb-1 = r2b4 + bk-1
bn-3x=
Lemma. F()) E R[(r]] has two consecutive zero coefficients, it cannot have all distinct real roots.
Proof I (Rolle). Say x², .²* coefficients zero. If all roots real and distinct, Rolle's 's thcorem implics every derivative has this property.
But (F(t) (x) has a double root at O, contradiction.
Proof 2 (Descartes). Real roots bounded by sign changes in F(z) plus sign changes in F(-x). For consecutive nonzero coefficients *xr *x'' (i > j): if - = 1, the sign change counts once; if - 2 2, it may count twice but there's s 2 1 zero between them.
With b nonzero coefficients and runs zeros, real roots S 1-1++ I deg F. Two consecutive zeros make this striet.
Marking Scheme (max pts). Checkpoints (additive):
(1) [1pt] Problem reduction to n = k + 1 and setup. Alt: complete proof for k = 1.
(2) [2pts] Pigconhole: polynomials,
internal coefficient positions; share position.
(3) [2pts] Deduce consecutive zeros: from [ax""] P I
Pt (x++r) show bm bm-1
(4) [2pts] Prove lemma (2pts for complete Rolle or Descartes proof; 1p for partial).
Deductions: Cap 6/7 if no reduction justification; cap 5/7 if lemma flawed; cap 3/7 if stops after PHP; 1pt for minor gaps (e.g.. not using rı & r2).
Zero credit: Unjustified WLOG; merely stating theorems; specific examples only; noting P(0) *
nonzero roots.
Figure 4: Example problem (USAMO 2025 P2) with its reference solution and marking schemn..
scores naturally cluster into four bands: incorrect (0), partial progress (1-3), nearly complete (4-6), and fully correct (7). During discussion, annotators must agree on (1) which band a solution belongs to, and (2) the exact score for fully correct (7) and fully incorrect (0) solutions. For partial-credit cases (1-6), minor differences may initially arise due to inherent ambiguities natural-language proofs and subjective judgment even with marking scheme guidance, but these are resolved through further discussion. All scores in the final dataset reflect this consensus- bassed adjudication.
Annotator Assignments.
Annotation responsibilities were distributed follows:
ProofBench: Solutions were annotated by Experts A, B, and C.
Best-of-n datasets: Solutions were primarily annotated by Experts D and E, with support from Expert B.
Marking schemes: Rubrics were evaluated by Experts A and B.
D PROOFBENCH ABLATION BY COMPETITION AND YEAR
We analyze potential data contamination by comparing model performance on problems from com- petitions occurring before versus after their respective knowledge cutoff dates. As shown in Table all three models exhibit positive bias toward pre-cutoff problems: Gemini-2.5-pri (A = +1.0T, significant), OpenAl-o3 (A +0.44, moderate), and DeepSeck-R1-0528 (A +0.40, moderate).
18

---

Published as a conference paper at ICLR 2026
Math Marking Scheme Annotation Tool
Prstier Litrt-322--g
Problem
Marking Scheme
Marking Scheme
peper anangle intersects tee distect pains q). Let maitaonn AQ)
through shandfying the prope point Q).
2ADD
serpustiinal
(sodtive
langth power ralcion boking
Prove that MVB 29C.
21.G; D.0
een Checipaitte (rowr troe))
og MBB AdQ MDC AdD, or
Solution
dicuced lepttmutall. jaddtive
AAe ACP atar ARG, ane scu wakent uq calitty
"15 plg tooableinng key property that detamminas the locaton of pain Q. (max 53 This is man insigh of protless Crecittie
Main indght (chosse one, "oward the lnger unly*))
awarded one follow neth ods.
bee peper lnsa Suppoas
Prove mippo toudva inittty
-oout Geometri charactrtaation
aFD
ctiiicationn selvction Art
Proving that the reflction acroee
indernncts tie deninet paint Q.
from,
Let melzponn AQ.
Prove that M45 20C)
We chox severs offerent approoecnve
arg)
all suutions, 2 sooite the foot the abttude flom
D3 that quscrictooal
from
12 ptl Lsang qydicity eapty
perpendiaatrr trecter RC)) cornatly conduce XP- NC. (b00tive
piiking
MPP
student who estar shes these three fots witheut
Figure 5: View of Marking Evaluation Platform Setup
Al Solution Evaluation Tool
Petiore
Moudh
Supplesi en loox
Stctes
Problem
Marking Scheme
Al Solution
Human Solution
Al Grading
Evaluation
Figure View of Evaluation Platform Setup
Gemini-2.5-pro demonstrates the strongest contamination signal (14.4% performance improvement
on pre-cutoff data), which is attributable to its late cutoff date (January 1, 2025) resulting in only 20% of our dataset being clean evaluation data. Table reveals heterogeneous contamination pat- terns across competitions: while IMO shows consistent positive contamination across all models, other competitions like EGMO and APMO exhibit mixed or reverse effects, suggesting interactions between contamination and problem difficulty variations.
19

---

Published as a conference paper at ICLR 2026
Problem
Marking Scheme
Al Solution
Fectal linges dijiig in and ports snccish
mepasseniin Ciipa grate made coutiia valus tuat nst other prodee to reaty
To solee the emuution pfi th itages 2. shon adests the oe of poskin cilto snr pes leged prre diicc prosect Dolovi
etoy denee the surcet of yoo desoon of serr aesons pagr areadiee
1d iouuoo.
sou
mand
eggt Lmm Subrtttin ins thes srasiootrr give
Chodppiiie teaa"
Human Solution
"Ml af Selirm moss to stoe)
ldt peat loddeeud
Valtegiing byl
Ancwer alsesorraeennnn
thes solitora 201
migh oo
lnd aivd
arpmecr settin up couation enagee
Pin p-
adut ( (1.)))
by thoming le
12"
vSi unec thee pener comproitty 200fy
**g y2 Andjeso the cae vnice tus disend
the bo fune toreeyy
prine ledtrs the block ascord sum parai.
Loneort thr otfecnson dor
insouato
455 off
night)
dieable teightt -3 devitttee part
tuckes of nus ln and
Dorate pirt legent dioper Thon
Lauget 10-1
"i hypoot mesers intreg ofsf with tey tery sigh
"Tilk caiing dig
Sicce posko parl wree Sooee in aa anll and coutton
showing thd (u 3) th sertiens" eerp p
hove moving
dupll 498 willl quallle??
prtspardinggee Thang pand.
Al Grading
Figure 7: View of Evaluation Platform Setup
To mitigate contamination effects, we focus our primary analysis on the 29 problems from 2025 competitions (APMO, EGMO, IMO, USAMO, TST 2025), which provide clean evaluation data for all three models. While this reduces our sample size to 20% of the full dataset, it ensures fair cross-model comparison without training data leakage confounds. We report full dataset results for completeness but mark pre-cutoff data with contamination warnings. These findings highlight the need for continuously updated benchmarks using very recent competitions (within 3-6 months) and increased transparency from model developers regarding training data composition and cutoff dates.
E ADDITIONAL DETAILS FOR EVALUATION METRICS
Within-problem ranking agreement. For problem p. consider all pairs (i.j) with < j. Define exp ypp Upj and A Avvll Upi Upj- Let C and D be the numbers of concordant and discordant
pairs, respectively, and let
Texp # ((i.g): A 0},
Teval = (((,s) A.jaa 0}.
Kendall's To for problem p is
C
(p) V(C+D + D (C+
and is undefined if the denominator is zero (we omit such p from aggregation).
Macro averaging. We macro-average per- per-problem metries across problems. Writing for the set of problems with defined Tu and P = IP]:
P Σ
P
1 P p=1
1
MAE- =
MAE p
RMSE
RMSE
Bias
Biasp
P
P
p.
p=1
p=1
WTA 1)
1
Σ
WTA 1)
1
Σ
(p).
P
P
pEP
(As noted in the main text, all problems have the same response count n.)
20

---

Published as a conference paper at ICLR 2026
Year
Summary
Competition
Mean Before
Mcan After
2022
2023
2024
2025
Contam.
Clean
OpenAl-o3 (cutoff: June 1, 2024)
X 3.8
X 4.0
x 3.2
v 4.6
APMO
15
3.67
4,60
-0.93
n=5
n=5
n=5
n=5
X 3,4
X 3.5
5.2
EGMO
17
3.71
5.17
-1,46
n=5
n=6
D=6
n=
X 2.8
x 2.7
V 2.0
V 1.0
IMO
2.75
1,50
+1.25
n=6
n=
n=
n=
3.3
3,4
V 3.0
PUTNAM
24
12
3.33
3.00
+0.33
n=12
n=12
n=12
no data
x 1.7
V 1.3
V 1.2
IST
1.67
1.25
+0.42
no data
n=6
1=
n=
2.3
X 1.8
X 2.0
2.3
USAMO
18
2.06
2.33
-0.28
n=6
Total
92
53
3.02
2.59
+0.44
Gemini-2.5-pro (cutoff: January 1, 2025)
X 3.2
X 2.8
X 3.2
3.6
APMO
15
3.07
3.60
-0.53
n=
n=
n=5
n=5
3.6
X 2.8
x 3.0
1.0
EGMO
17
3.12
1.00
+2.12
n=5
n=6
n=6
n=6
x 2.5
x 2,2
x 2.0
V 1.5
IMO
2.22
1.50
+0.72
n=6
n=
n=
n=
3.1
X 3.3
x 3.2
PUTNAM
36
3.19
n=12
n=12
data
x 2.2
x 2.0
V 1.2
TST
2.08
1.17
+0.92
no data
n=6
n=
n=6
2.5
X 2.0
X 1.8
1.7
USAMO
18
2.11
1.67
40.44
n=6
Total
116
29
2.73
1.72
+1.01
DeepSeck-R1-0528 (cutoff: July 1, 2024)
x 2.6
x 2.2
x 2.2
V 1.4
APMO
2.33
1,40
+0.93
n=5
n=5
n=5
n=5
3.0
2.2
x 2.2
V 1.5
EGMO
17
2.41
1,50
+0.91
n=6
n=
n=6
X 1.5
x 1,2
V 0.8
V 0.3
IMO
1.33
0.58
+0.75
n=
n=6
n=
n=
2.8
x 2.5
V 3.4
PUTNAM
24
12
2.63
3.42
-0.79
n=12
n=12
data
X 0.7
X 0.5
V 1.0
TST
12
0.58
1.00
-0.42
no data
n=6
n=6
n=6
2.0
X 1.5
X 1.3
v 0.5
USAMO
18
1.61
0.50
+1.11
n=6
n=6
n=6
n=6
Total
98
47
1.95
1.55
+0.40
Table Contamination status by competition, year, and model. Each cell shows mean expert rating (1-7 scale) and problem count. x potentially contaminated (before cutoff), v = clean (after cutoff), no data. Summary columns show contamination effect (A = before after).
F EVALUATION ON WEAKER, OPEN-SOURCE MODELS
We collected expert gradings on solutions from two weaker models (Qwen3-4B and DeepSeek- 0528- 5528-Qwen3-88
selected set of 36 problems from 2024 and 2025 competitions. Both models are among the best math reasoning models of the same scale. Here we provide the results on the generators (Table IT) and selected evaluators (Tabl 12
21

---

Published as a conference paper at ICLR 2026
Contaminated (#)
Clean (#)
Mean Before
Mean After
Model
Cutoff Date
A
OpenAl-o3
June 2024
(63%)
53 (37%)
3.02
2.59
+0.44
Gemini-2.5-pm 2.5-pro
Jan 1, 2025
116 (80%)
29 (20%)
2.73
1.72
+1.01
DeepSock -lick-RR--oo 0520
July 1, 2024
98 (68%)
47 (32%)
1.95
1.55
+0,40
Á = Mcan difference (contaminated - clcan); positive values indicate contamination.
Expert ratings on 1-7 scale; dataset contains 145 problems 3 solutions 435 total.
Table Contamination analysis summary across three models. All three show positive bias toward pre-cutoff data, with Gemini-2.5-ppm exhibiting the strongest effect.
Confest
OpenAI-o3
Gemini-2.5-pro
DeepSeek-R1-6es
АPMO
-0.93
-0.53
+0.93
EGMO
-1.46
+2.12
+0,91
IMO
+1.25
+0.72
+0.75
PUTNAM
+0.33
-0.79
TST
+0.42
+0.92
-0.42
USAMO
-0.28
+0.44
+1.11
Overall
+0.44
+1.01
+0.40
values: strong contamination (>1.0), moderate (0.3 1.0), no contamination reverse effect (<0..)
Table 10: Contest-specife contamination effects (A) across models. Red indicates stronger perfor- mance on pre-cutoff data (contamination), green indicates better performance on post-cutoff data.
PROOFGRADER'S emrr rates actually significantly lower here than those reported in the main paper. This is because weaker models mostly produce incorrect (0-point) proofs, making grading much easier. Since grading weaker models is generally easier, chose the strongest available model as generators in PROOFBENCH. BENCH. This allows the benchmark to better challenge evaluators by requiring them distinguish between partially correct and nearly-complete solutions, and detect subtle errors in reasoning steps.
Generator
Average (out of 7)
O-point solutions
Qwen3-4B
0.92
70%
DeepSeek-R1-OS5 R--osee-----5-2---0- --22---23---
0.78
72%
Table 11: Weaker generator performance on selected problems.
G WEAKER MODELS AS EVALUATORS
We have conducted additional experiments with leading open-source models at different capability levels: Dwen3-235B-A220 (Thinking) and Llama-3.1-70B. Instructt
Unfortunately, these models demonstrate substantially weaker per- formance evaluators compared to frontier proprietary models. Given that these represent some of the strongest available open-source models their respective families, evaluating smaller variants (e.g., 7B 14B models) would likely yield even weaker results. These findings suggest that current open-source models significantly lag behind proprictary models in fine- fine-grained grained mathematical proof evaluation.
Results are shown in Table 13
22

---

Published as a conference paper at ICLR 2026
Evaluator
MAE
RMSE
1T
03 ensemble (Ref+MS) ProofGrader
0,431
0.521
93.1%
03 (Ref+MS)
0.486
0.559
95.8%
o3 (None)
1.764
1.892
59.7%
CrepSeck-RI(ReFH..
0.750
0.929
81.9%
Caanseek-RI(None
3.653
3.823
11.1%
Gpt-4o (Ref+MS)
2.458
2.669
26.4%
Gpt-4o (None)
3.931
4.056
5.6%
Table Evaluator performance metrics on weaker generators.
Model
Context
MAE
RMSE
Bias
WTA(<1)
Ref+MS
3.212
3.679
3.156
31.0%
Llama-3.1-70
MS
3.189
3.385
3.150
27.9%
B-Instruct
Ref
3.194
3.661
3,096
31.2%
None
3,945
4.404
3.898
26.1%
Ref+MS
1.531
2.007
0.724
65.3%
Qwen3-235B
MS
1.351
1.727
0.041
66.8%
-222B
Ref
1.860
2.068
1,425
45.3%
None
2.631
3.070
2.359
40.6%
Table 13: Model performance comparison across different contexts for two additional models: 1ama--.1-700-Insse Instructt and Qwen3-235B-A225
H IN-DEPTH ANALYSES
What are the common failure modes of PROOFGRADER? After examining PROOFGRADER'S outputs, we find that cases of over-crediting and under-crediting by more than one point are relatively 12.2% Across generators, PROOFGRADER makes the most errors o3-
balanced (10.8% generated solutions 28.9% 9% of the solutions, compared to 23.3% for GEMINI and 16.9% for GEMINI. Since PROOFGR ADER itself is based on 03, this suggests a degree of within-generatoo bias. By problem type, PROOFGRADER ADER fails more frequently on Algebra and Geometry problems (each accounting for ~5% of failure cases) than on other domains. For qualitative analysis, we manually examined 50 solutions for which two or more ensemble runs of PROOFGRADER deviated from expert scores by least two points. This reveals several common failure modes:
Overcrediting:
PROOFGRADER sometimes assigns high scores to solutions whose structure closely mirrors the rubric (sections, lemmas, final condition) even when central mathematical claim is false, superficial alignment masks fatally incorrect core argu- ment.
Appearance-of-copleess
Case Study: o3 APMO-20000 2025-2. The solution performs several correct manipulations but in- correctly rewrites a key condition so that a range of (a, b) values claimed to always satisfy the constraint, though that is false.
Fatal gaps treated as minor omissions. When a proof relies on a false universal claim or broken reduction, PROOFGRADER often interprets this as "missing justification" rather than fatal error, granting partial credit even though the entire method collapses.
Case Study: APMO 2024/3. R1 claims " "f(s, t) is always nonnegative", but direct coun- terexamples show fs, t) < 0. This invalidates the whole reduction.
Overtrust in sophisticated but incorrect frameworks. For solutions that use polished frame- works (coordinates, height functions, custom transformations), PROOFGRADER tends reward the global structure and technical vocabulary without verifying key validity conditions, leading substantial overeredit for incomplete invalid arguments.
23

---

Published as a conference paper at ICLR 2026
Case Study: Gemini APMO-2023-5. Gemini constructs an elaborate height-function argument but never verifies that paths do not cross or that the constructed ordering is actually consistent, which is required for the proof.
Undercrediting:
Penalizing early missteps despite correct final proof. LLMs often explore an incorrect approach before restarting with valid proof; humans grade the final argument, but PROOF- GRADER aggregates all attempts and heavily penalizes early errors, leading to near-zero scores even when the final proof is fully correct.
Case Study: RI APMO 2023/2. RI initially writes incorrect divisor equations and claims "larger & gives no solution." Then it restarts and produces a valid classification.
Double-penalizing a single flaw. A single conceptual error can both prevent multiple check- points from firing and trigger a global "major error" deduction, so partially correct solutions with substantial progress can be driven all the way to 0/7.
Case Study: RI PUTNAM 2022 B4. The solution analyzes several structural cases correctly but ends with an incorrect final expression that contradicts its earlier reasoning.
Overstrict demand for micro-jsstifications. Omitted trivial steps or minor slips (e.g.. a mis- labeled point) can cause PROOFGRADDE mark long downstream chains as unproven, heavily undergrading solutions whose main ideas and overall argument would receive high partial credit from human graders.
Case Study: o3 USAMO 2023/1. The solution has a valid coordinate approach but misla- bels a point, causing PROOFGRADER to treat all downstream angle and collinearity relations as missing justification.
Geometry Instability. Geometry problems are particularly brittle: long dependency chains (sim- ilarity - ratios + concurrencyccycliitt)) mean a single incorrect or missing step can either be wrongly ignored (leading to overcredit, e.g., treating a non-circle-preservvee valid) or over-amplified (leading to undercredit when a routine angle equality is left implicit), pro- ducing highly unstable scores on geometric proofs (e.g., o3. APMO 2024/1 vs. o3. EGMO 2025/4).
transformation as
Why are reference solutions and marking schemes helpful? Comparing evaluators based on 03 with NONE to those given REF+MS, we find that in over 60% cases, the evaluator without context overestimates the generation's 's correctness, i.e., it incorrectly assigns a higher score to the generation. Crucially, this overestimation is not uniform: we observe a strong correlation (r = 0.699, p < 0.001) between proof quality and evaluation gap. For low-quality proofs (scored 0- 2), the no-context evaluator over-scores by an average of 1.7 points. In contrast, for high-quality proof' (scored 5-7), the evaluator with context information assigns higher scores by 0.8 points on average. This asymmetric pattern supports our hypothesis that, without reference solutions or marking schemes, the evaluator struggles gauge proof progress.
This effect is exacerbated when the evaluator cannot fully solve the problem, a case that constitutes the majority of our dataset (as shown FFiuuee 2p. When we examine problems that 03 cannot solve well (scoring < 2 when acting as prover), we find that the evaluator without context over-scores by 1.4 points on average. For problems that 03 can solve (scoring 2 5), the evaluator with context scores higher by 0.9 points. This demonstrates that the evaluator's difficulty in solving a problem directly impairs its ability to assess partial progress on that problem without reference.
Case study. On Putnam-2022-Bs (generator: 03), the evaluator with context identified critical logical flaw ("log-conaae concavityy inequality fails when la, > 1") and assigned point, while the no- context evaluator deemed the proof "essentially correct" and awarded points. Manual inspection of the 20 cases with largest disagreements (AA) 2 4) reveals that 80% involve proofs with sophisti- cated presentation but fundamental logical errors, supporting the view that reference solutions help evaluators distinguish between fluent exposition and mathematical correctness.
Sensitivity to Marking Schemes. Table 14 reports results for 03 evaluators under REF+MS,
comparing three marking-scheme variants: (i) the original schemes used by human experts, (ii)
24

---

Published as a conference paper at ICLR 2026
Model Marking Scheme
RMSEJ
MAET
WTAg1 (%61
Kendall-r
Biass
Original
1.273
0.964
76.5
0.502
-0.088
New marking scheme (GEMINI)
1.467
1.156
70.0
0.515
0.219
New marking scheme (03)
1.525
1.196
70.4
0.460
0.020
Table 14: Marking Scheme Sensitivity. We evaluate the single-past 03 evaluator under REF+MSwith three marking-scheer schemee sets sets-ori (human), regenerated (same model/prompt), and 033-generaeed (same prompt). The original human schemes perform best.
schemes regenerated by the same model with the same prompt, and (iii) schemes generated by 03 itself with the same prompt. The original human pooandpr schemes yield the strongest performance.
I GENERATOR PROMPT
Default
Your task is to write proof solution to the following problem. Your proof will graded by judges for correctness and completeness. When you write your proof, follow these guidelines:
You are creating proof, not a proof outline. Each step should be carefully explained and documented. If not properly explained, the judge will assume that you cannot explain it, and therefore decrease your grade.
You can are well-known. As a rule of thumb: if the result has a name and is famous enough to have Wikipedia page or something similar to describe it, it is allowed. Any result from papers that would not be taught: in high school low-level bachelor courses in mathematics should not be used. Any use of such results will inmediately give you zero grade.
general theorems and lemmas, but only if they
Do not skip computation steps in your proof. Clearly explain what transformations were done and why they are allowed in each step of calculation.
Your proof should be self-contained. If you
not sure about specific step, do not know how to prove an intermediate result, clearly state this. It is much preferable to indicate your uncertainty rather than making incorrect statements or claims.
FORMATTING GUIDELINES:
You should write Markdown with LaTeX math. Do NOT use code fences (no "*)
You should use correct LaTeX notation to write equations and mathematical symbols. You should encompass these equations correct delimiters ("\) and "\\)" for inline math, "\\"" and "\\]" for block math) to enhance the clarity of your proof. **Do not use any unicode characters.
For multi-line derivations, wrap an aligned block INSIDE display math.
Do not use other LaTeX ronments or packages.
PROBLEM: (problem)
25

---

Published as a conference paper at ICLR 2026
J MARKING SCHEME GENERATION PROMPT
Marking Scheme (without examples)
You experienced y1ypia grader. *Treat the efficial solution fully correct and authoritative; do not claim contains errors or gaps.* Your task is to write a complete, grader-fr zubric for the problem and official solution below. The rubric must map student's proof to integer score from **0 to 7**.
### INSTRUCTIONS
Produce the marking scheme in **exactly** the following three sections.
1. *Checkpeints (max 7 pts +
Break the solution into logically independent checkpoints with vxinteger** point values.
Allocate **>= 4 pts.* to the main idea/critical steps; **<= pts** routine work.
If two itens are mutually exclusive (soive the *same* logical gap), **nes*** them and write **laward the larger only*...
Parallel solution paths (non-additive) If the official solution (or student submission) admits more than one legitimate approach, write **parallel checkpoint chains** labeled \Chain A / Chain B ... (idea: ...)".
**Start this section with bold rule:*. **Score
exactly ene chain take the **maximum** subtotal
among chains; do **not** add points across chains.**
Within a chain, checkpoi nts may be (idd For steps **shared across chains* (e.g., 1enna usable by multiple approaches), place then. under \Shared prerequisites" group with **) k]**, and state **)count at most once regardless of chain."*.
For every bullet (or group), append either **\ [add ** [max *]** to make the scoring rule unambiguous.
Finish with a one-line ** Votal (max "** check that is consistent with the non-addi non-additivity rule.
Never demand cosmetic labels or specific variable names unless essential to the logic.
2. zero-crredit items**
list common arguments observations that *xearn 0 points** (e.g., conjectures without proof especially geometry, routine restatements of the problem, or dead-ends).
*Deductiinss**
Bullet each typical mistake with a **flat. penalty (*+ (2**, or +</cap at x/7"**),
Apply **at most the single largest** deduction; never
reduce score below
Target legic gaps, invalid clairs, circular reasoning, or contradictions. Cosmetic slips (notation, aritametic, wording) do +*not** trigger deductions unless they break
26

---

Published as a conference paper at ICLR 2026
validity.
If student gives **multiple distinct proofs**, **grade the best ene only** (no stacking). . If proofs contain excontradictory claims*e, apply an appropriate deduction (e.g., **cap at 5/7+*).
##f IMPORTANT REQUTREMENTS
Use **concise se bul lets. no prose exposition of the official solution.
**Arithmetic sanity checks:** per-chain checkpoint sums and |max kl
caps must make it impossible to exceed ***** overall; at least one chain must allow a perfect **7/7** Do **not* introduce, \fix," or critique the official solution.
Avoid frem-fragmnnting: do not split routine algebra into separate 1-pt bullets.
* Keep notation consistent with the official solution; define any new symbols you introduce.
### PROBLEM
(problem)
### OFFICIAL SOLUTION
(solution)
Marking Scheme (with examples)
You experienced Olympiad grader.
Your task is to write a complete, grader-friendly subric for the problem and official solution given below.
*Treat the efficial solution fully correct and authoritative; do not claim it contains errors gaps.*
The rubric must map a student's ' proof to an integer score from to 7.
### INSTRUCTIONS
Produce the marking scheme in **exactly** the following three sections.
1. Checkpoints (max 7 pts total)
Break the sclution into logically independent checkpoints. Assign each checkpoint an integer value.
Allocate >- pts total to the main part of the proof;
<= 3 pts total to routine work.
If two items are mutually exclusive (solve the same gap), nest them and waate the larger only"**, For every bullet, append either [additive] or [max k] to make the scoring rule unambiguous.
Finish the section with a one-line \Total (nax 7) check. If the official solution mentions more than one legitimate path, give either (a) parallel checkpoint chains (b) catch-all checkpoint worth up to 7 pts for completely correct alternative proot that uses the same underlying idea.
Never demand cosmetic labels or specific variable naming unless
27

---

Published as a conference paper at ICLR 2026
they are essential to the logic.
2. Zero-credit items
List common arguments or observations that look related but **aarn 0 points**. Include conjectures stated with no proof (esp. geonetry), routine restatements, or dead-end explorations.
Deductions
Bullet each typical mistake with a flat penalty:
-1, -2, or ceap at x/7". Apply at most the single Largest deduction; never reduce score below D.
Fenalties should target logic gaps, invalid claims, or circular reasoning. Ccsmetic slips (notation, arithmetic, wording) never trigger deductions unless they break validity.
### IMPORTANT REQUIREMENTS
Use concise bullet points; no prose exposition of the official solution.
Arithmetic sanity checks: checkpoint points - exclusivity rules must to 7. The rubric should self-evident to grader with no caleulator.
to not introduce, Afix, or critique any part of the official solution.
Avoid over-fragmenting: do not split routine algebra manipulation into 3+ separate 1-pt bullets.
Keep notation consistent with the official solution; you intucduce new symbols, define then.
Here is an example problem from past math competition, along with human-written solutions and the corresponding marking scheme. Please study the problem and solution carefully, and use them to understand how the marking scheme was constructed.
## Problem
A positive integer n is called beautiful it, for every integer <= <= 10000, the base-b
representation of n contains the consecutive digits 2, 0, 2, 3 (in this order, from left to right).
Determine whether the set of all beautiful integers is finite.
### Soluticn AI (5)
such that for every (,=4,, \idots\), the number ((L(K)) contains (2023_[bFV) in every base (4 \ieq \ieq k\). This will solve the problem because (NN_(1000)), N_(10001), Aldots)) will be the requested infinite set.
For the base case, take For the inductive step, here is one of many valid zecipes. We are going select
[[(k)=N \edot (k \ell) \J
where the ingredients (e, \ell, e\) are selected to satisfy:
\begin(itemize)
\item \(eil\ is the product of all primes at most MKV) which are relatively prime to ((K)) (in particular,
28

---

Published as a conference paper at ICLR 2026
Vloperatorname (ged) (k, \el1)=1\) );
\item (c\) is large enough that for each 5b=4,5, Aldots, k\), the largest power of (bV) dividing \ik (o Nedot N_(k-1)\);
is greater than
\item (cl) is chosen to satisfy the modular congruence lend(itemize)
\I
a ledot \ell"(e) Aequiv (3(3) x-121+2 k+3 Aquad Weef (\bmed k" ("14)
A]
which pessible since ((/operatorname(ged)) Wieft (k" (4), \ell" (ell////gggttt///..
With these ingredients, for all the smaller bases \ (4 \ldots, k-1V, the ending of ((_(K]) in base- (bb) is the same as in (XL(K-1) (since \(k (e) is multiple of large enough power
(bb)) ). On the other hand, we've embedded (2203_ into the base- MKY) representation of \ \NLik-L))) because the coefficients of (kk (e+3), (*t2),, (e(1),, k(je/\) in the (k\) representation are exactly (2,, 211,
### Marking Scheme
1. Checkpoints (max 7 pts total)
Merely claiming there is sone congruence of sone sort is not sufficient to pass the benchmark. For solutions that fail achieve this benchmark, the following partial credits are available but not additive: point for showing that the existence of single beautiful number implics the existence of infinitely many, e.g. by adding large powers of 2023!.
point for serious induction attempt or construction but which botches the main difficulty mentioned above.
points for a solution that additionally has the idea in the indirect censtruction solution of ensuring compatibility by picking certain integer parameter $t_i Vin \i0, \edots, b.k 1 in consecutive range for sufficiently large sks. points if they are completely correct.
2. Zero-credit items
points for yes/no answer alone.
points for just mentioning induction. points for base cases like b = 4.
points for a solution that only works on coprime moduli. This includes, e.g. showing there is number which has 2023b for every base <= <= 2023 which is the power of a prine (that is, $b Vin (44, 5, 7, 8, 9, 11, 13,
20111;5).
3. Deducticns
-1 point for minor completely emitting the base case of the induction;
such
{ using an integer parameter which is not large enough as stated but could easily be changed to be large enough.
-2 points for more serious but non-central. flaw in of the steps of inductive approach.
Below is the problem with its correct solution need to read and generate the marking scheme for.
HEF PROBLEM
<insert problen. statement>
### OFFICIAL SOLUTION
29

---

Published as a conference paper at ICLR 2026
<insert full solution>
K
EVALUATOR PROMPTS
Below we list prompts used in our evaluation. Each prompt shown verbatim.
With Reference Solution and Marking Scheme
You are an *expert math proof grader**. You are judging the correctness of an LiM-generated proof for a math problem.
### Input
Your input will consist of:
**Pobblem statement**; mathematical problem that the proof is attempting solve.
**Reference Solutionxx: A correct solution or proof provided for reference. This is w*not necessarily the only valid solution If the problem requires final numeric aigebraic answer, this section contains the correct answer, which should be the only accepted final answer (thouga alternative reasoning paths are valid). +*Marking Scheme**: A problem-specific grading rubric (0(7 scale) with checkpeints, zero-credit items, and deductions. **Treat this scheme as advisory guidance, not script... Use it anchor scoring, but *ado not require* the proof to follow the order, lemmas, or technique its reasoning is nathematically sound.
**Pro Sclution=*: The proof that you need to evaluate. This proof may centain errors, omissions, unclear steps. The proof was generated by another language model.
## Task
Analyze the proof carefully.
**Core principles (in order of precedence) :**
1) **Mathematical validity= of the proof's reasoning and conclusion.
2) **Problem constraints=* (e.g., unique required final value; forbidden toels if stated).
3) ..Avissry mapping to the marking scheme*. (checkpoints/ deductions), allowing different orders and techniques.
4) **Reference solutionx> as anchor for sufficiency, not exclusivity.
*+Alternative-apprracc policy:**
It the precf uses different but valid method, **map its steps to equivalent rubric checkpoints** (same logical role) and award peints accordingly.
**0 not penalize** solely for re-ordering steps, using different lemmas, or giving a correct shorteut, vunlessa* the problem forbids it.
Apply zero-credit items/deductions **only when the underlying issuc actually occurs** in the given proof's approach; **do not auto-penalizo*. for omitting a rubric step that is unnocossary under the alternative method.
Avoid dcuble-countine solve the same logical gap, *xaward the larger only*s. the final numeric/algebrati answer wrong where uniqueness is required, award only partial credit justified by correct intermediate reasoning.
mutually exclusive itens; if two items
30

---

Published as a conference paper at ICLR 2026
Riigor and evidence:**
Award credit for intermediate claims **only if adequately justified** within the proof (not merely asserted).
If step is plausible but under-justified, award *xconservative
partial credit** and note what is missing.
**What to produce:**
Identify legical errors, incorrect steps, or unclear reasoning.
Give a **sccre between and 7** with **detailed assessment
**Within the assessment text**, show clearly how the score was
derived:
Which rubric checkpoints (or their **mapped equivalents**)
were earned and the points you awarded.
Any zcre-credit items or deductions you applled (and why)
How these add up to the final integer score in [0-7].
### Output Format
Respond with **only** well-formed XMI using the structure below. Do not include any extra text Karkdown.
**Requiremetts:**
>sscore> must be an integer in [0, 7].
*<assessment>' must be eddetailed analysis.. that explains your reascning step-by-step and provides clear *rationale for the score** Reference specific claims/lines if present. Include the scoring breakdown *vin prose** here (earned checkpoints or mapped equivalents, deductions, and subtotal final score). "<errors>" must be list of specific issues (empty if score 7).
Example output:
<score>0</score>
<assessment>1hhe proof shows good understanding ng of the main idea, but has some unclear reasoning and minor mistakes.. .aatees.....saee..... </asssessmntt> <errors>
1. specific error 1,
2. specific
</crrors>
**Problem Statement** (problem)
*eeference Solution** thuman_solution
*arrknn Scheme** (markinggschheme
**Proof Sclution** (solution]
Basic Evaluation Template
You are an *exxort math proof grader**. You are judging the correctness of an LIM-generated proof for a math problem.
### Input
Your input will consist of:
31

---

Published as a conference paper at ICLR 2026
Prooblmm statement**: mathematical problem that the proof is attempting to solve.
**Proof Sclutionex: The proof that you need to evaluate. This proof may contain errors, onissions, or unclear steps. The proof was generated by another language model.
### Task
Analyze the proof carefully.
Identify legical errors, incorrect steps, unclear reasoning. Give an **integer** score between and with brief overall assessment.
##F Output Format
Respond with **only+* well-formed XML using the structure below. Do not include any extra text or Markdown.
**Requiremntts:.
'<score>' must be an integer in 10, Tl.
'<assessment>> must be **detailed analysis** that explains your reasoning step-by-step and provides clear *xrationale for the score... Reference specific claims/lines if present.
'<errors>' must be list specific issues (enpty if score 7)
Example output:
<score>0</score>
<assesement>The proof shows good understanding of the main idea, but has some unclear reasoning and minor mistakes... bateees....sssseeeee </assesement> <errors>
1. speci fic error 2,
2. specific
</errors>
### Scoring Guidelines (0-7 scale)
+**** Completely incorrect; proof is irrelevant, nonsensical, or shows no understanding.
++1-2++: Very poor; major logical flaws, does not solve the problem, but may contain fragments of relevant reasoning.
**3-4x*: Partial progress; captures some correct reasoning or key ideas, but has significant Logical errors, missing steps, or incomplete arguments that make the proof invalid everall.
**5-6**: Largely correct; the preef is overall valid and reaches the correct conclusion. Contains only **minor issues** (e.g., small calculation mistakes, notation slips, or slightly unclear wording) that do not undermine correctness.
.*7**: Fully correct; the proof is complete, logically sound, and clearly presented with substantive errors.
++Problem Statement** (problem)
**Proof Sclution** (solution]
32

---

Published as a conference paper at ICLR 2026
With Reference Solution
You are an **xpert math proof grader**. You are judging the correcthess of an LiM-geneertte proof for math problem.
### Input
Your input will consist of:
Problem statement*::
mathematical problen that the proof
a attempting to solve.
A correct solution or proof provided for reference. This is **not necessarily the only valid solutionxs. If the problem requires final numeric algebraic answer, this section contains the correct answer, which should be the only accepted final answer (thouga alternative reasoning paths are valid). +*Proof Sclution=*; The procf that you need to evaluate. This proof may contain errors, omissions, unclear steps. The proof was generated by another language model.
Reference Solution+::
### Task
Analyze the proof carefully.
Compare the proof against the reference solution where relevant. Identify legical errors, incerrect steps, or unelear reasoning.
Give sccre between 0 and with brief overall assessment.
### Output Format
Respond with **only+* well-formed XXI using the structure below. Do not include any extra text Karkdown.
'<score>' must be an integer in [0, 7].
><assessment>> must be iddetailed anslysis.. that explains your reasoning step-by-step and provides clear vvrationae for the score**. Reference specific claims/lines if present.
"Kerors>>" must be list of specific issues (emрty if score 7).
Example output:
<score>0</accre>
<assessment>Thhe proof shows good understandi ng of the main idea but has some unclear reasoning and minor mistakes.. .aares....aassssss </assessment> <errors>
1. specific error 1,
2. specific error 2,
</errors>
### Scoring Guidelines (0-7 scale)
**0**: Completely incorrect; proof is irrelevant, nonsensical, shows understanding.
+*1-2**: Very poor; major logical flaws, does not solve the problem, but may contain fragments of relevant reasoning.
+*3-4**: Partial progress; captures some correct reasoning or key ideas, but has logical errors, missing steps, or incomplete arguments that make the proof invalid overall.
**5-6**: Largely correct; the proof is overall valid and reaches the correct conclusion. Contains only **minor issues** (e.g., small calculation mistakes, notation slips, or slightly unclear wording) that do not undermine correctness.
33

---

Published as a conference paper at ICLR 2026
**7**: Fully correct; the proof is complete, logically sound, and clearly presented with no substantive errors.
**Froblem Statement** (problem)
**Reference Sclution* (human_solution)
**Proof Solutien** (solution]
With Reference Solution and Marking Scheme (Strict)
You **expert math proof grader**. You are judging the correctness of an LIM-generated proof for a math problem.
### Input
Your input will consist of:
Problem Statement**: A mathematical problem that the proof is at tempting to solve.
**Reerence Solutionex:
A correct solution proof provided for necessarily the only valid solutionxx.
reference. This is the problem requires final numeric or algebraic anawer, this section contains the correct answer, which should be the only accepted final answer (though alternstive reasoning paths are valid). M*Maringg Scheme**: A problem-specific grading rubric (0-7 scale) with checkpcints, zero-credit items, and deductions. follow this scheme when assigning points.
must
Proo Sclution+*: The proof that you need to evaluate. This proof may centain errors, omissions, or unclear steps. The proof generated by another language model.
### Task
Analyze the proof carefully.
Compare the proof against the reference solution and the marking scheme.
Award points according to the marking scheme's checkpoints, zero-credit items, and deductions.
Identify logical errors, incorrect steps, or unclear reasoning.
Give a score between 0 and with a bricf overall assossment.
Show clearly how the score was derived:
Which checkpoints
carned (with awarded points).
Any zero-credit items or deductions applied.
How the subtotal leads to the final score (0-7).
### Output Fornat
Respond with **onyy+* well-formed XMI using the structure below. Do not include any extra text or Markdown.
Reqquirements.
'<score> must an integer in [0, 7]
*<assessment>> must be s*detailed anslysis.. that explains your reascning step-by-step and provides a clear vezationale for the score**. Reference specific claims/lires if present.
'errrrs>'' must be 1ist of specific issues (enpty if score 7)
34

---

Published as a conference paper at ICLR 2026
Example output:
<score>0</scoro>
<assesement>The proof shows good understanding of the main idea but has some unclear reasoning and minor mistakes... </assessment> <errors>
1. specific error 1, 2. specitic error
</errors>
Prroblem Statement** (problem)
**Reference Sclution** (human_soluticn)
+Marking Scheme** (marking_scheme)
**Proof Sclutionks Isolutiont
With Reference Solution and Marking Scheme (most basic)
You are expert grader for math proofs. Judge the proof's mathematical correctness based the reference solution and the marking scheme, return an integer score between and
INPUTS:
Problem Statement
Reference Sclution (correct but not exclusive)
Marking Scheme (0-7) with checkpoints and deductions use as guidance, not script
Proof Solution (from an LLM)
OUTPUT (XML enly; no extra text): <score> (integer 0/7ores (assesment>>stee-byyeee ratienale with scoring breakdown in prose] </assessment>
<errors> [numbered 1ist of speci fic issues; empty if none] </errors>
**Problem Statement** (problem)
Referencc Sclution** (human_soluticn)
**Marking Scheme** [marking_scheme)
**Proof Sclution** Isolution)
With Reference Solution and Marking Scheme (basic)
You are an expert grader for math proofs.
INPUTS:
35

---

Published as a conference paper at ICLR 2026
Problem Statement
Reference Sclution (correct but not exclusive)
Marking Scheme (0-7) with checkpoints and deductions guidance, not script
Proof Solution (from an LLM)
TASK:
Judge the preei's mathematical correctness. Prefer validity problem constraints marking scheme aligament reference solution. If the proot uses a different valid method, map its steps to equivalent marking scheme checkpoints and award points. If unique final answer is wrong, give partial credit only for justified intermediate reasoning.
OUTPUT (XML only; no extra text): <score> <score> (integer 0-7]</score>
<assessment> (step-by-step rationale with scoring breakdown in prose] </asscssment> <errors> [numbered list of specific issues; empty if none] </errors>
Probbem Statement** (problem)
*Referrnnce Solution** (human_solution)
Marking Scheme** (marking_scheme)
**Proof Solution** (solution)
With Marking Scheme (no reference solution)
You **epprrt math proof grader**. You judging the correctness of an LIM-generated proof for a math problem.
FF Input
Your input will consist of:
Problem Statement*:: A mathematical problen that the proof is attempting te solve.
**Marking Scheme**: problem-specific grading rubric (0-7 scale) with checkpeints, zero-credit itens, and deductions. You must follow this scheme when assigning points.
**Proot Sclution**: The proct that you need to evaluate. This proof may contain errors, omissions, unclear steps. The proof was generated by another language model.
### Task
Analyze the proof carefully.
Follow the marking schome exactly: award chockpoints, apply zero-credit itens, and apply any deductions/capy as specified.
Identify legical errors, incorrect steps, unclear reasoning.
Give score between 0 and with brief overall assessment.
Show clearly how the score was derived:
Which checkpoints were earned (with awarded points).
Any zere-credit items or deductions applied.
36

---

Published as a conference paper at ICLR 2026
How the subtotal leads to the final score (0-7).
### Output Format
Respond with **only+* well-formed XMI using the structure below. Do not include any extra text or Markdown.
**Requi rements:**
"<score>" must. be an integer in [0, 7].
'<assessment>> must be exdetailed analysis.v that explains your reasoning step-by-step and provides clear vrrationale for the score**. Reference specific claims/lines if present.
'cerrors> must be list specific issues (empty if score 7)
Example output:
<score>0</score>
<assessment>The proof shows good understanding of the main idea, but has some unclear reasoning and minor mistakes... mistakes...</asseeee.. </assessmentt> <errors>
1. specific error 2. specitic error 2,
</errors>
**Problem Statement** (problem)
*-aarking Scheme** [marking_scheme)
**Proof Sclution** (solution]
With Reference Solution and Marking Scheme (more detailed)
You are an **xxprrt math proof grader**, You are judging the correctness of an IIM-generated proof for a math problem.
FFF Input
Your input will consist of:
**Problem Statement*x;
mathematical problen that the proof is
attempting to solve.
**Reference Solutionxx: A correct solution or proof provided for reference. This is **not necessarily the only valid solution**. If the problem requires final numeric or algebraic answer, this section contains the correct answer, which should be the only accepted final answer (theugh alternative reasoning paths M*Maring Scheme**: A problem-specific grading rubric (0-7 scale) with checkpoints, zero-credit items, and deductions. You must follow this scheme when assigning points.
valid).
**Proof Sclution**: The proof that you need to evaluate. This proof may contain errors, omissions, or unclear steps. The proof was generated by another language model.
### How to Use the Marking Scheme (mandatory)
Checkpoints parsing & awarding
Treat each checkpoint exactly as written. Respect its tag: ladditivel: award all applicable items in that bullet/ group.
37

---

Published as a conference paper at ICLR 2026
[max :]: award up to points from the itens in that bullet/grene (choose the best-matching ones; do not exceed k). items nested with \award the larger only", and than one applics, award only
larger point value.
If the scheme presents parallel checkpoint chains (alternative legitimate paths), score the single chain combination that yields the highest valid total without viclating exclusivity [max k] caps. Do not double-coune equivalen steps across mutually exclusive paths.
If a catch-all checkpoint is provided for Fully correct alternative proof using the same underlying idea, you may award up to its stated maximum only the student's argument is complete and logically valid for that idea.
2. Zero-credit items
If the proef relies any listed zero-credit arguments, award for those parts. Do not add points for restatements, conjectures without proof (especially in geometry), or dead-ends.
3. Deductiens (apply most one)
Ident fy applicable deduction ons and apply only y the single largest (e.g., -1, -2, or cap at x/7).
Apply cap by truncating the post-checkpoint subtotal to before finalizing the score.
Never reduce the score below 0. Cosmetic slips (notation, arithmetic,
wording) do not trigger deductions unless they break validity.
4. Final answer consistency (when applicable)
If the reference solution gives definitive final answer, the candidate sclution's s final answer must be wcorrect/equivalense If not, follew the marking scheme's pwnckpoinns/deductiionnn typically, wrong final
prevents awarding the \conelusioa" checkpoint.
5. Arithmetic & bounds
Checkpoint awards are integers. Subtotal <- 7 by construction. After applying the single largest deduction/cap, the final score is an integer [0, 7].
### Task
Analyzc the proof carefully.
Compare the proof against the reference solution and the marking scheme.
marking scheme's checkpoints, zero-credit items, and deductions.
Award points according
* Identify logical errors, incorrect steps, or unclear reasoning.
Give scere between 0 and 7 with brief overall assessment.
Show clearly how the score was derived:
which checkpoints were earned (with awarded points).
Any zerc-credit items or deductions applied.
How the subtotal leads to the final score (0-7).
### Output Format
Respond with **only** well-formed XXI using the structure below. Do not include any extra text or Markdown.
Requi rements:**
38

---

Published as a conference paper at ICLR 2026
<score>> must be an integer in [0, 7].
><assessment>" must be *xdetailed analysis* that explains your reasoning step-by-step and provides clear vvrationale for the score.*. Reference specific claims/lines present. '<errors> must be 1ist of specific issues (empty if score 7).
Example output:
<score>0</accre>
<assessment>Ihe proof shows a good understanding of the main idea, but has some unclear reasoning and minor mistakes.. </assessment> <errors>
1. specific error 1,
2. specific error 2,
</errors>
**Problem Statement** (problem)
Reffrrence Sclution* (human_solution)
Marking Scheme** sharking_scheme|
**Proof Solutions* [solution]
39


Reviews:
[{"review_id": "TAq6T2iuEB", "reviewer": "Reviewer_HNs6", "summary": "This paper introduces ProofBench, a dataset of 131 competition math problems with 393 expert-graded LLM solutions, and systematically studies design choices for automated proof evaluators. The authors propose ProofGrader, which achieves RMSE of 1.093 against expert scores and demonstrates practical utility in best-of-n selection tasks.", "questions": "Q1. Since the best-of-n experiments are supposed to establish the predictive generalization power of ProofBench for use as a reward model, shouldn’t the ground truth annotations for the proofs used in the experiment be annotated by different people than those used to annotate the examples in ProofBench? A difficulty in designing a benchmark for evaluators is that the bias in the annotations themselves need to be accounted for, i.e, the paper needs to demonstrate that the possibly imperfect annotator preferences used in ProofBench are sufficient for generalization to general aesthetic preferences in the math community (regarding competition style proofs).\n\nQ2. Similarly to Q1, in the best-of-n experiments, shouldn't the set of model generations being evaluated by the candidate evaluators be generated by models that are different to the three specific models used to generate the outputs in the benchmark? Could the authors provide justification why the current methodology is sufficient to demonstrate the general utility of ProofBench for selecting evaluators meant to evaluate generations from other models? Currently, it seems like ProofBench is useful for selecting evaluators for proofs generated by o3, Gemini, and DeepSeek-R1, but no indication of general ability.\n\nQ3. This approach seems very committal to a specific frozen mark scheme. Since the labor intensive annotation process is predicated on a particular MS, what happens if the mark scheme needs to be changed? Do we need to re-annotate each time? Could the authors provide justification why using a particular frozen mark scheme for the annotation process is sufficiently general to avoid re-annotation?", "limitations": "", "rating": 4, "confidence": 3, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "S1: The paper tackles an important problem for mathematical reasoning research. Reliable proof evaluation is a critical bottleneck for training and assessing LLMs on mathematical reasoning tasks, and the lack of scalable alternatives to human grading or formal verification makes this work timely and valuable.\n\nS2: The systematic methodology using problem-specific marking schemes as an anchor is well-motivated. The two-stage annotation process (generating marking schemes, then grading with them as guidance) provides a principled way to maintain consistency while allowing flexibility for alternative solution approaches.\n\nS3: The experimental design is comprehensive and well-structured. The ablation studies clearly isolate the impact of different design choices (backbone model, context components, instructions, workflows), providing actionable insights about what matters for evaluator performance.\n\nS4: The best-of-n experiment (Section 6) effectively demonstrates practical utility beyond correlation metrics. Showing that ProofGrader closes 90% of the gap between a naive binary evaluator and the human oracle provides evidence of real-world value for downstream applications like RL training.\n\nS5: The decision to use fine-grained (0-7) rather than binary scoring is validated empirically. Figure 2 clearly shows that binary evaluators fail to distinguish among correct solutions, while fine-grained scoring enables effective ranking.", "weaknesses": "W1: ProofBench is only shown to show predictive power (via MSE on the benchmark) over whether an evaluator is good at grading outputs of three specific models (o3, Gemini 2.5 Pro, DeepSeek-R1), all of which are precisely the models whose proofs are used as the annotated examples for computing the MSE. There is no evaluation of how well ProofGrader generalizes to solutions from weaker models, different model families, or human-written proofs, which limits our understanding of its robustness. The paper should have tested whether evaluators with low MSE on ProofBench have high agreement with human annotators on grading proofs generated by models that are not one of those three models, in order to demonstrate general utility.\n\nW2: Inter-annotator reliability is insufficiently reported. While the paper mentions that two experts underwent calibration and double-scored 20% of items, the actual agreement metrics (e.g., correlation, exact agreement rate, within-1 agreement) are not provided. Since the significance of the contributions hinges on the correctness of the human annotations, this needs to be emphasized in the main text.\n\nW3: Error analysis is absent. The paper does not systematically examine where ProofGrader fails or succeeds, what types of errors it makes (over-crediting vs. under-crediting), or which problem types are most challenging. Understanding failure modes would be valuable for future work and practical deployment.\n\nW4: Computational costs and efficiency are not discussed. For practical deployment, especially in RL training scenarios where evaluators may need to score thousands of candidate solutions, the cost (in terms of API calls, latency, and financial expense) compared to simpler baselines would be relevant information.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "8bR6jZs7qY", "reviewer": "Reviewer_LGPu", "summary": "This paper addresses the challenge of reliably evaluating natural language mathematical proofs generated by large language models. The authors propose a systematic methodology for developing automated evaluators that assign fine-grained scores on a 0-7 scale, rather than binary correct/incorrect judgments. They introduce PROOFBENCH, an expert-annotated dataset containing 393 LLM-generated solutions to 131 competition math problems, along with problem-specific marking schemes. Through systematic experimentation, they develop PROOFGRADER, an ensemble-based evaluator that achieves strong alignment with expert judgments (RMSE of 1.093) and demonstrates practical utility as a reward model for best-of-n selection tasks.", "questions": "1. How sensitive are the results to the quality of the automatically generated marking schemes? Have you conducted experiments with human-written marking schemes for comparison?\n2. How well do these evaluator design principles transfer to other mathematical domains beyond competition problems (e.g., research-level proofs, educational contexts)?\n3. Can you provide more detailed analysis of when and why the evaluator fails? What types of mathematical reasoning or proof structures are most challenging?\n4. What are the computational costs of your best evaluator compared to simpler alternatives? How does this scale with problem complexity?\n5.What is the inter-annotator agreement between your experts, and how does this compare to the agreement between experts and your automated evaluator?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 3, "presentation": 3, "contribution": 3, "strengths": "1 The work tackles an important gap in mathematical proof evaluation with a systematic approach. While building on existing LLM-as-a-judge paradigms, the application to fine-grained mathematical proof evaluation with problem-specific marking schemes is novel.\n2. The experimental design is thorough and methodical. The expert annotation process is well-designed with appropriate quality controls. The systematic ablation studies provide clear insights about what factors matter for evaluator performance.\n3. The paper is well-organized and clearly written. The motivation is compelling, methodology is systematic, and results are presented comprehensively with good visualizations.\n4. Addresses a real bottleneck in mathematical reasoning research. PROOFBENCH provides a valuable resource for the community, and the insights about evaluator design will inform future work. The demonstration of practical utility in best-of-n selection shows real-world applicability.", "weaknesses": "1. The dataset contains only 393 solutions across 131 problems from competition mathematics. This is relatively small for drawing broad conclusions about evaluator design, and competition problems may not represent the full spectrum of mathematical reasoning tasks.\n2, The approach relies heavily on LLM-generated marking schemes, which could introduce systematic biases or limitations. The quality of these schemes fundamentally constrains the evaluation quality, but this dependency is not thoroughly analyzed.\n3. All experiments use the same expert annotators and marking scheme generation process. It's unclear how well the findings generalize to different mathematical domains, difficulty levels, or evaluation standards.\n4. The paper doesn't compare against other potential evaluation approaches beyond varying LLM configurations. For instance, how does this approach compare to simpler heuristic methods or other structured evaluation frameworks?", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "H0uHn63MJA", "reviewer": "Reviewer_zjS9", "summary": "This paper tackles the critical bottleneck of evaluating natural language math proofs from LLMs with PROOFBENCH, a new expert-annotated dataset of LLM-generated proofs graded on a 0–7 scale using detailed marking schemes. Based on a systematic study of evaluator design, they developed PROOFGRADER, an evaluator that achieves high alignment with human experts. Moreover, they show in a Best-of-N task where PROOFGRADER, as a reward model, closes over 90% of the performance gap between a naive binary evaluator and a human oracle.", "questions": "1. Does the evaluator show a \"self-enhancement bias\"? For instance, does the O3-backbone evaluator systematically over-score proofs generated by O3? A heatmap of bias (Generator vs. Evaluator) would be insightful.\n2. The paper shows that strong models (like O3) are strong evaluators. What about the other dynamics? How well do weak models evaluate strong models, and vice versa? Understanding this is important for understanding the robustness of \"LLM-as-a-judge\" and its potential for \"weak to strong generalization\".\n3. Is there a risk that generator-LLMs could hack the evaluator to get a high score?", "limitations": "", "rating": 6, "confidence": 4, "soundness": 4, "presentation": 2, "contribution": 4, "strengths": "1. The paper tackles the crucial and timely problem of scalable, reliable proof evaluation.\n2. PROOFBENCH represents a substantial and meticulous human annotation effort.\n3. The BoN experiments demonstrate the effectiveness of the methods.", "weaknesses": "1. The paper relies heavily on aggregate metrics (RMSE, etc.). It would be better to include some case studies and error analyses.\n2. The paper mentions MathArena but doesn't adequately compare PROOFBENCH to MathArena's manual annotation efforts.\n3. The backbone models are mainly proprietary models. The analysis would be more comprehensive if it evaluated some open-source models (e.g., Llama and Qwen series) to look into their capabilities as evaluators.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "KrqxuRAjeH", "reviewer": "Reviewer_EDhE", "summary": "This paper evaluates the feasibility and effectiveness of LLMs as judges for the continuous-scale grading of natural language solutions to mathematical problems. The authors present a pipeline for 1) automatically generating grading rubrics, 2) manually verifying LLM-generated solutions, and 3) investigating various aspects of an LLM-as-a-judge system. This process resulted in the `ProofBench` dataset of 393 expertly graded solutions, used for evaluating the backbone model and prompting style of an LLM judge. The work also presents `ProofGrader`: the best-performing combination of a judgment ensemble using the o3 model, with a marking scheme and potential solutions as additional reference information. As a proof of concept for `ProofGrader`'s utility, the authors show that the system can be used as a solution selector in a best-of-8 setting, achieving a score that approaches the human oracle's performance.", "questions": "1. Can the authors address all the concerns listed in the **Weaknesses** section?\n2. The authors describe the marking scheme generation methodology in Section 3.1 and later in Appendix A.3. However, the description lacks sufficient detail. Can the authors clarify:\n    - The model families they tested for rubric generation?\n    - What the prompts (with and without examples) entailed?\n    - How the annotators interacted with the initially generated rubrics, e.g., what were their instructions, how was consensus achieved, and what was the extent of disagreement prior to adjudication?\n    - What was the average rubric quality rating in the final iteration?\n    - How was the best configuration selected, was it based solely on the average score?\n3. The authors have measured the bias of the graders with respect to the human grades. However, when breaking down by model, [1] and [2] show a clear positive bias toward a model's own solutions. Can the authors report similar metrics and discuss the implications?\n4. In what realistic setting can the authors' framework from Section 6 be applied (refer to comments in W2.3)?\n5. When evaluating different provers, the authors have constrained themselves to using a score-based selection system. How does this compare to using a tournament-style approach?\n6. The best-of-n evaluation was done on 29 selected problems. How were these problems selected and what was their difficulty distribution?\n7. The authors claim in 3.2.3 that Staged Evaluation is \"particularly effective for improving the performance of weaker backbone models.\" This is a very strong claim, given that this observation is only seen for the `o4-mini` model. Can the authors consider running additional experiments to support this statement or temper the claim to reflect the limited evidence?\n8. For 2/3 models in 5.2.2, the *Strict* setting yields more accurate judgement than the *Norm* one. Do the authors have any qualitative explanations for this?\n\n## Current rating\n\nI have given this paper a score of **4: Borderline Reject**. The contribution is valid, important, and potentially impactful to the field. However, the lack of transparency on some aspects, particularly reproducibility, prevents me from assigning a higher score. I would be happy to raise my score if the authors address the majority of my concerns during the rebuttal and discussion period.\n\n### References\n\n[1] Dekoninck et al. The open proof corpus: A large-scale study of llm-generated mathematical proofs. arXiv preprint arXiv:2506.21621, 2025.\n\n[2] Petrov et al. Proof or bluff? evaluating llms on 2025 usa math olympiad. arXiv preprint arXiv:2503.21934, 2025.", "limitations": "", "rating": 4, "confidence": 5, "soundness": 2, "presentation": 2, "contribution": 3, "strengths": "1. The topic of the paper is clearly well-motivated, relevant, timely, impactful, and provides opportunities for further developments in the field\n2. The paper is overall well-written and conveys the high-level idea well.\n3. The authors have investigated several factors affecting the performance of an LLM-as-a-judge, identifying the backbone model and a well-defined marking scheme as the most significant factors for its performance. This provides readers with clear guidance on the information necessary for achieving accurate automatic grading.\n4. This work provides the currently largest dataset of expert-annotated solutions graded on a continuous scale, covering a wide range of challenging recent problems suitable for further LLM-as-a-judge validation.\n5. The best evaluated settings for the LLM-as-a-judge are shown to also correlate with a better performance as a best-of-n selector. This is a very desirable result, showing that the comparisons performed in the analysis are valid on downstream tasks.\n6. The authors provide the prompts necessary for running the LLM-as-a-judge, aiding reproducibility.\n7. The annotator calibration phase is a valuable step for minimizing error and noise in the final dataset.", "weaknesses": "For this section, I have labelled each comments as either:\n - *Critical*: These weaknesses have significantly impacted the score, and addressing/not addressing them could positively or negatively affect my final recommendation.\n- *Important*: Addressing these weaknesses would, in my opinion, significantly strengthen the paper's quality and/or clarity.\n- *Minor*: These are nitpicks that, while valuable to address, have not impacted the score of this assessment.\n\n1. Reproducibility\n    - (Critical) The authors claim `ProofBench` as one of their core contributions. However, despite promising to open-source the dataset upon publication, I see no reason why this was not done as part of the supplementary material. Not providing a core contribution of the paper for peer review significantly hinders the process. Upon release, the authors should also ensure they include an appropriate license, given the nature of the source materials.\n    - (Important) The annotation pipeline, described in A.3, is missing a substantial amount of details. Further elaboration can be found in the **Questions** section.\n\n2. Methodology\n    - (Critical) The authors have not reported the reliability of their human grading. They describe having performed double-grading on 20% of the solutions but have not reported any inter-annotator agreement statistics. In particular, they mention that they \"adjudicate all flagged disagreements,\" however, it is not clear what threshold for a disagreement constitutes a flag, how often flags occurred, or how they resolved these inconsistencies. The perceived reliability of the remaining 80% of grades is highly dependent on clarifying this process.\n    - (Critical) Generating rubrics is an incredibly challenging task in practice. This paper involves an automated system that is difficult to verify without significant manual intervention. Details about how this process was refined are lacking. Furthermore, no discussion is presented on how the annotators verified that these rubrics adhered to a standard for high-quality marking schemes. For example, the rubric in Appendix A.6 gives a total of 3 points for initial observations that seem relatively trivial compared to the rest of the proof. While my interpretation of this rubric is a personal opinion, I believe the authors should clarify how they ensured that the rubrics adhere to a high standard of quality, reflecting authentic evaluation practices.\n    - (Important) The authors claim that in Section 6 they investigate the judging framework as a reward model. However, the described setting appears to lack a clear, realistic application. In particular:\n\n        * If used within a solver's selection system, as described in the paper, such applications often aim to solve a problem without access to a reference solution. In that case, the best result seems to be `o3`, at around 3 average points, which is considerably lower than the human oracle's 4.21.\n        * If used as a reward model for training, as proposed in Sections 1 and 7, the presented setups are all too expensive to be scalable to a full RL (or other) pipeline.\n \n      The authors should clarify what a potential use case for this result can be.\n    - (Minor) The paper makes no distinction between results on undergraduate- and high-school-level problems, and whether this is a relevant factor.\n\n3. Dataset\n    - (Important) The dataset consists of problems from 2022-2025 from popular competitions (IMO, USAMO, Putnam). The earlier years precede the knowledge cutoff dates for the models tested. The authors should discuss whether test-set contamination has impacted the results and, if so, how significant the effect is.\n    - (Important) The authors claim to have sourced their problems and solutions from official sources. However, to the best of my knowledge, the USAMO and USATST do not publicly release their competition materials. The authors should clarify this point in their rebuttal.\n\n4. Writing and Clarity\n    - (Minor) The work never explicitly states which configuration constitutes `ProofGrader`. While it can be inferred from the results, it would be best if the authors defined this in the earlier sections of the paper.\n    - (Minor) Most models presented in the paper are not cited according to best practices. Standard practice is to cite the official model cards from the providers, if one exist.\n    - (Minor) In Section 5.3, the authors refer to an \"ensemble\" of evaluators. This term is usually reserved for a collection of **different** models or algorithms applied to the same task, rather than for multiple samples from a single algorithm.", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "", "claims_and_evidence": "", "methods_and_evaluation_criteria": "", "theoretical_claims": "", "experimental_designs_or_analyses": "", "relation_to_broader_scientific_literature": "", "essential_references_not_discussed": "", "other_strengths_and_weaknesses": "", "other_comments_or_suggestions": "", "questions_for_authors": "", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Decision: Accept (Poster)