Cost-Effective Automated Judging of Natural-Language Mathematical Proofs

Benjamin Grayzel

cs.CLMay 29, 2026

Cost-Effective Automated Judging of Natural-Language Mathematical Proofs

Authors: Benjamin Grayzel

Organizations: Department of Computer Science, Dartmouth College, Hanover, NH, USA.

Abstract

Grading natural-language mathematical proofs is a recurring cost in evaluating math-reasoning systems, and frontier LLM judges are expensive. We ask whether cheap open-weight models can serve as reliable judges given a candidate proof, a ground-truth proof, and a human-grading rubric. On a 200-instance validation sample of IMO-GradingBench, two of three cheap judges (GPT-OSS-120B, DeepSeek-V4-Flash) and their three-model consensus are statistically no worse than the frontier (Claude Opus 4.7, Gemini 3.1 Pro) on agreement with human pass/fail decisions, at 4-100 $\times$ lower cost. On the full 1000-instance benchmark, the choice of consensus rule over the three judges is a precision/recall dial: unanimous (all-three-pass) rules reach the highest precision (0.855), majority vote the highest recall (0.912); across four replicate runs the unanimous rule is also the steadiest. No rule won outright; the dial replicated on a held-out 600-instance split and on the independent ProofBench. In this domain, cheap judges are competitive with the frontier at one to two orders of magnitude lower cost, and unanimity is the right setting when false positives are costly.

Figures & tables

Judge	Reasoning	Pass-agree [95% CI]	4-run	$\kappa$	F1	Spearman $\rho$	Cost / 200
GPT-OSS-120B	xhigh	0.875 [0.830, 0.920]	0.851	0.716	0.806	0.623	$0.32
DeepSeek-V4-Flash	default	0.860 [0.815, 0.905]	0.881	0.664	0.763	0.660	$0.70
Cheap consensus (trio)	—	0.855 [0.805, 0.905]	0.874	0.673	0.779	0.654	$1.73
Claude Opus 4.7	adaptive	0.855 [0.805, 0.900]	—	0.680	0.785	0.715	$32.45
Gemini 3.1 Pro	high	0.840 [0.790, 0.890]	—	0.645	0.761	0.704	$28.61
Gemini 3.1 Pro	default	0.840 [0.790, 0.890]	—	0.655	0.771	0.714	$7.07

Table 1: Validation results (

n=200

), sorted by pass-agreement of the original run. 4-run is the mean pass-agreement over four independent runs (Appendix C ); frontier baselines were run once.

\kappa

is Cohen’s kappa at the pass boundary; precision, recall, and confusion matrices are in the supplementary material.

Figure 1: Pass/fail agreement with humans (95% CI,

n=200

) with per-200-call cost at right (frontier costs boxed). Every cheap judge but Gemma-4-31B has an interval overlapping the leader’s estimate, at one to two orders of magnitude lower cost than the frontier baselines.

System	Pass-agree [95% CI]	$\kappa$	Prec.	Rec.	F1	Spearman $\rho$
DeepSeek-V4-Flash	0.873 [0.852, 0.893]	0.717	0.815	0.812	0.814	0.732
GPT-OSS-120B ( xhigh )	0.842 [0.820, 0.864]	0.668	0.716	0.889	0.793	0.704
Gemma-4-31B ( high )	0.801 [0.776, 0.826]	0.604	0.640	0.953	0.766	0.741
Majority vote (trio)	0.863 [0.842, 0.883]	0.711	0.744	0.912	0.819	0.765
All-three-pass	0.879 [0.860, 0.898]	0.725	0.855	0.777	0.814	0.733
Fail-everything	0.659 [0.629, 0.689]	0.000	—	0.000	0.000	—

Table 2: Full benchmark (

n=1000

), 95% bootstrap CIs; both-pass pairs are in Table 9 .

Appendix figures & tables11 assets

Supplementary material from the paper’s appendix.

Appendix

Setting	Reason. tok.	Agree	F1	$\rho$	Cost
Default	${\sim}2{,}400$	0.840	0.771	0.714	$7.07
High	${\sim}10{,}400$	0.840	0.761	0.704	$28.61

Appendix

Table 3: Gemini 3.1 Pro: default vs. high reasoning (

n=200

). “Agree” is pass-agreement,

\rho

is Spearman, and cost is per 200 gradings.

System	orig	rep1	rep2	rep3	mean	std	Self-maj.	Self-all-3
DeepSeek-V4-Flash	0.860	0.861	0.898	0.905	0.881	0.024	0.901	0.895
GPT-OSS-120B xhigh	0.875	0.863	0.829	0.835	0.851	0.022	0.847	0.888
Gemma-4-31B high	0.795	0.820	0.810	0.814	0.810	0.011	0.824	0.849
Majority vote (trio)	0.855	0.875	0.890	0.875	0.874	0.014	—	—
All-three-pass	0.895	0.895	0.903	0.915	0.902	0.009	—	—

Appendix

Table 4: Run-to-run pass-agreement on validation (

n=200

). orig – rep3 are four independent runs; mean and std are over those four. Self-maj. and self-all-3 apply the consensus rules to one model’s own three replicates (rep1–3), over the problems where all three are valid (

n=191

–

199

): self-maj. passes if

\geq 2

of 3 runs pass, self-all-3 if all 3 pass.

Figure 2: Run-to-run pass-agreement across four independent runs (

n=200

). Faded points are individual runs; solid points are mean

\pm

std. All-three-pass is both the highest and the tightest; single cheap judges drift more than the consensus rules.

System	Pass-agree	$\kappa$	Prec.	Rec.	F1
DeepSeek-V4-Flash	0.878	0.737	0.843	0.824	0.833
GPT-OSS-120B ( xhigh )	0.837	0.664	0.729	0.887	0.800
Gemma-4-31B ( high )	0.807	0.622	0.662	0.973	0.788
DeepSeek + GPT-OSS	0.873	0.723	0.861	0.783	0.820
DeepSeek + Gemma	0.878	0.737	0.843	0.824	0.833
GPT-OSS + Gemma	0.868	0.724	0.786	0.882	0.832

Appendix

Table 5: Held-out remaining 600 instances (human pass base rate 221/600). The fail-everything baseline scores 0.632 with

\kappa=0

System	Pass-agree	$\kappa$	Prec.	Rec.	F1
GPT-OSS-120B ( xhigh )	0.883	0.684	0.681	0.862	0.761
DeepSeek-V4-Flash	0.878	0.609	0.781	0.606	0.683
Gemma-4-31B ( high )	0.903	0.730	0.741	0.851	0.792
DeepSeek + GPT-OSS	0.887	0.626	0.846	0.585	0.692
DeepSeek + Gemma	0.897	0.656	0.877	0.606	0.717
GPT-OSS + Gemma	0.917	0.754	0.815	0.798	0.806

Appendix

Table 6: ProofBench replication (

n=435

; expert pass base rate

0.216

). Same rule definitions as Table 2 .

Disputed set	$n$	Sides with judges	Sides with human
False positives (judges pass, human fails)	25	10 (40%)	15 (60%)
False negatives (judges fail, human passes)	15	8 (53%)	7 (47%)
Combined	40	18 (45%)	22 (55%)

Appendix

Table 7: Blind GPT-5.5 adjudication of sampled all-three-pass–vs–human disagreements.

Reference	System	Instance	Cluster	4-run, cluster
Opus	GPT-OSS	$+0.020$ $[-0.020,+0.060]$ ✓	$+0.020$ $[-0.024,+0.068]$ ✓	$-0.005$ $[-0.043,+0.034]$ ✓
	DeepSeek	$+0.005$ $[-0.035,+0.045]$ ✓	$+0.005$ $[-0.037,+0.052]$ ✓	$+0.027$ $[-0.013,+0.072]$ ✓
	Trio	$+0.000$ $[-0.030,+0.035]$ ✓	$+0.000$ $[-0.039,+0.043]$ ✓	$+0.019$ $[-0.015,+0.057]$ ✓
	Gemma	$-0.060$ $[-0.095,-0.030]$	$-0.060$ $[-0.090,-0.030]$	$-0.046$ $[-0.086,-0.006]$
Gem. high	GPT-OSS	$+0.035$ $[-0.010,+0.080]$ ✓	$+0.035$ $[-0.015,+0.089]$ ✓	$+0.010$ $[-0.039,+0.058]$ ✓
	DeepSeek	$+0.020$ $[-0.020,+0.060]$ ✓	$+0.020$ $[-0.025,+0.068]$ ✓	$+0.042$ $[+0.001,+0.086]$ ✓

Appendix

Table 8: Paired difference in validation pass-agreement (system

-

frontier), 90% CIs. ✓: no worse than the frontier (lower bound above

-0.05

). Gem. high/def.: Gemini 3.1 Pro at high/default reasoning.

System	Pass-agree [95% CI]	$\kappa$	Prec.	Rec.	F1	Spearman $\rho$
DeepSeek + GPT-OSS	0.878 [0.859, 0.897]	0.723	0.852	0.777	0.813	0.733
DeepSeek + Gemma	0.877 [0.857, 0.897]	0.725	0.824	0.812	0.818	0.738
GPT-OSS + Gemma	0.866 [0.845, 0.886]	0.712	0.765	0.877	0.817	0.744

Appendix

Table 9: Both-pass pairs, full benchmark (

n=1000

), 95% bootstrap CIs. Consensus

\rho

uses the minimum member score (Appendix A ).

Figure 3: Consensus rule as a precision/recall dial on the full benchmark (

n=1000

); dashed lines are iso-F1 contours. Majority vote sits at high recall; the unanimous rules move toward high precision.

Figure 4: The strongest single judge flips between the validation sample and the full benchmark; every interval overlaps.

Figure 5: Pass/fail agreement (x) versus Spearman rank correlation with the human score (y) on the validation sample (

n=200

). Cheap open-weight judges (circles) stay competitive on the pass/fail decision; the frontier baselines (diamonds) lead on rank correlation by a modest margin.

Explore similar work

QEDBENCH: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofs
Feb 24, 2026Santiago Gonzalez, Alireza Amiri Bavandpour, Peter Ye +48Mathematical Reasoning Benchmarks LLM Evaluation
Evaluation of LLMs for Mathematical Formalization in Lean
Jun 4, 2026Tyson Klingner, Drew Bladek, Escher Crawford +6LLM Evaluation Lean Theorem Proving
Math AI Lab, University of Washington, Seattle, WA, USA. · Math AI Lab, University of Washington, Seattle, WA
Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness
May 11, 2026Ivo Petrov, Jasper Dekoninck, Dimitar I. Dimitrov +1Mathematical Reasoning Benchmarks LLM Evaluation
1INSAIT, Sofia University "St. Kliment Ohridski" · 2ETH Zurich

Feb 24, 2026, cs.LGJ/K move · Enter open · S save

QEDBENCH: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofs

Santiago Gonzalez, Alireza Amiri Bavandpour, Peter Ye, Edward Zhang+47

Mathematical Reasoning Benchmarks LLM Evaluation LLM-as-a-Judge Language Model Bias Evaluation Automated Grading

Open paper AskPDF arXiv

As Large Language Models (LLMs) saturate elementary benchmarks, the research frontier has shifted from generation to the reliability of automated evaluation. We demonstrate that standard "LLM-as-a-Judge" protocols suffer from a systematic Alignment Gap when applied to upper-undergraduate to early graduate level mathematics. To quantify this, we introduce QEDBench, the first large-scale dual-rubric alignment benchmark to systematically measure alignment with human experts on university-level math proofs by contrasting course-specific rubrics against expert common knowledge criteria. By deploying a dual-evaluation matrix (7 judges x 5 solvers) against 1,000+ hours of human evaluation, we reveal that certain frontier evaluators like Claude Opus 4.5, DeepSeek-V3, Qwen 2.5 Max, and Llama 4 Maverick exhibit significant positive bias (up to +0.18, +0.20, +0.30, +0.36 mean score inflation, respectively). Furthermore, we uncover a critical reasoning gap in the discrete domain: while Gemini 3.0 Pro achieves state-of-the-art performance (0.91 average human evaluation score), other reasoning models like GPT-5 Pro and Claude Sonnet 4.5 see their performance significantly degrade in discrete domains. Specifically, their average human evaluation scores drop to 0.72 and 0.63 in Discrete Math, and to 0.74 and 0.50 in Graph Theory. In addition to these research results, we also release QEDBench as a public benchmark for evaluating and improving AI judges. Our benchmark is publicly published at https://github.com/qqliu/Yale-QEDBench.

Abstract

Explore similar work

QEDBENCH: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofs

Evaluation of LLMs for Mathematical Formalization in Lean

Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness