Cost-Effective Automated Judging of Natural-Language Mathematical Proofs

# Cost-Effective Automated Judging of Natural-Language Mathematical Proofs
Source: [https://arxiv.org/html/2608.00004](https://arxiv.org/html/2608.00004)
###### 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, three cheap judges \(GPT\-OSS\-120B, DeepSeek\-V4\-Flash, Gemma\-4\-31B\) agree with human pass/fail decisions at rates statistically indistinguishable from Claude Opus 4\.7 and Gemini 3\.1 Pro, at up to100×100\\timeslower cost\. We had expected a majority vote of the three to be the best budget option; it matched the frontier but did not improve on its strongest member\. Extending to the full 1000\-instance benchmark and exploring consensus rules, we found that requiring unanimous agreement \(all\-three\-pass\) reaches the highest pass\-agreement and precision and, on four replicate runs, the smallest run\-to\-run spread\. The headline finding is that cheap judges are competitive with the frontier at one to two orders of magnitude lower cost; as a deployable default we recommend all\-three\-pass, with the caveat that this rule was identified post\-hoc and warrants independent replication\.

LLM\-as\-a\-judge, mathematical reasoning, natural language proof grading, cost\-efficiency, open\-weight models

## 1Introduction

Benchmarks for AI mathematical reasoning increasingly include problems whose solutions are full natural\-language proofs rather than short final answers, and scoring those proofs is a bottleneck\. Formal verification with proof assistants such as Lean\(de Moura and Ullrich,[2021](https://arxiv.org/html/2608.00004#bib.bib1)\)gives trustworthy guarantees and has reached IMO\-medal performance with AlphaProof\(Hubertet al\.,[2025](https://arxiv.org/html/2608.00004#bib.bib2)\)\. Extending it to the breadth of research mathematics, through autoformalization and self\-evolving provers, is an active frontier; until that coverage arrives, most proofs are still graded in natural language, as the 2025 IMO gold\-medal results from frontier models were\.

While the model under study can change between experiments, the judge must be reliable and held fixed across an entire study, so its cost is a tax on the whole research effort, and frontier judges are expensive\. The same cost recurs inside self\-improving systems, where a loop that generates, critiques, and revises proofs needs a judgment at every step, so an expensive judge limits how much such a system can iterate\. This motivates a concrete question:*is there a cheap judge a budget\-constrained researcher can trust for proof grading?*

We study this judging task onIMO\-GradingBench\(Luonget al\.,[2025](https://arxiv.org/html/2608.00004#bib.bib3)\), the grading split of IMO\-Bench: 1,000 instances, each pairing an Olympiad problem and a reference solution with a candidate proof and an expert human grade on the standard 0–7 IMO scale\. The judge reads the problem, reference, and candidate, and predicts the grade\. We are deliberately narrow in scope; this is a study of*judging*, not*solving*, on problems that come with a reference proof and a human grade \(not reference\-free verification\)\.

Our prior expectation, following the Panel\-of\-LLM\-evaluators result\(Vergaet al\.,[2024](https://arxiv.org/html/2608.00004#bib.bib4)\), was that a \(majority\-vote\) consensus of several cheap models would be the safest choice, as offsetting biases should cancel\. We tested this: the consensus performed well, but it did not beat the strongest individual model within it\. The more useful and general finding is that the cheap tier as a whole is competitive: cheap open\-weight judges match frontier baselines \(Claude Opus 4\.7, Gemini 3\.1 Pro\) on pass/fail agreement with human graders at acost of 1–2 orders of magnitude lowerin our setup\. In a post\-hoc rule search on the full benchmark we found that the unanimous variant \(all\-three\-pass\) of the same trio outperformed both cheap and frontier judges \(on pass\-agreement, precision, and stability\) and is the configuration we recommend pending replication\.

## 2Related Work

LLM\-as\-a\-judge\(Zhenget al\.,[2023](https://arxiv.org/html/2608.00004#bib.bib5)\)is now the standard tool but is known to exhibit position, verbosity, and self\-preference biases and to be sensitive to prompt design\(Guet al\.,[2024](https://arxiv.org/html/2608.00004#bib.bib6)\)\. For proofs specifically, frontier models often fail to produce valid arguments even when their final answers are correct\(Petrovet al\.,[2025](https://arxiv.org/html/2608.00004#bib.bib7)\), motivating dedicated grading benchmarks such as the Open Proof Corpus\(Dekonincket al\.,[2025](https://arxiv.org/html/2608.00004#bib.bib8)\)and IMO\-GradingBench\(Luonget al\.,[2025](https://arxiv.org/html/2608.00004#bib.bib3)\)\. Cost has received less attention:Vergaet al\.\([2024](https://arxiv.org/html/2608.00004#bib.bib4)\)show that small\-model panels can outperform a single large judge at roughly7×7\\timeslower cost on QA and chatbot tasks\.

Two concurrent works frame our contribution\.Maet al\.\([2026](https://arxiv.org/html/2608.00004#bib.bib9)\)search the evaluator design space and reach expert\-level agreement by combining a strong reasoning backbone with reference solutions, marking schemes, and ensembling; we ask whether the backbone itself must be strong and find that, for reference\-based pass/fail grading, it need not be\.Naiket al\.\([2026](https://arxiv.org/html/2608.00004#bib.bib10)\)study the closest reference\-*free*version of our question and report cheap judges trailing the frontier by∼10%\{\\sim\}10\\%in accuracy \(and∼25%\{\\sim\}25\\%in self\-consistency\), a gap that prompt ensembling narrows\. In our reference\-*based*setting \(judging against ground\-truth solutions\), the accuracy gap closes entirely\. This is consistent with the reference solution doing work the judge would otherwise have to do\. We do not measure self\-consistency, which remains open\.

## 3Problem Setting

We consider grading instances of the form*\(problem, ground\-truth solution, candidate solution, human score\)*\. A judge reads the first three and outputs a score; we compare its score to the human’s\. The decision that matters most for downstream use is thepass/fail boundary: did the candidate proof meet the bar \(a score of≥6\\geq 6on the 0–7 IMO scale\)? Our primary metric ispass\-agreement: the fraction of instances where the judge’s pass/fail decision matches the human’s\. We report precision, recall, and F1 at that boundary, and Spearman rank correlation with the human score as a secondary, ordinal measure \(appropriate for the coarse\{0,1,6,7\}\\\{0,1,6,7\\\}output\)\. We also report per\-grading cost\.

## 4Methodology

#### Data and sampling\.

From IMO\-GradingBench’s 1,000 instances \(spanning 30 IMO\-style problems\), we draw two disjoint random samples of 200 by uniform selection without replacement: a*prior*\(exploratory\) sample with seed 42, used for exploration and for selecting the consensus trio, and a*validation*sample with seed 7, drawn from the remaining 800 instances, used as a clean held\-out test\. Section[6\.1](https://arxiv.org/html/2608.00004#S6.SS1)additionally reports results over the complete 1,000\-instance benchmark\. All headline results are on the validation sample unless noted otherwise\.

#### Judge prompt and scoring buckets\.

Every judge uses the same prompt and is instructed to emit a score in\{0,1,6,7\}\\\{0,1,6,7\\\}\(incorrect / partial / almost / correct\); our parser accepts any integer 0–7, and a handful of off\-bucket scores \(4 across all runs, under 0\.1%\) occurred and are scored as parsed\. This four\-bucket scheme follows the public grading prompt released with IMO\-GradingBench\(Luonget al\.,[2025](https://arxiv.org/html/2608.00004#bib.bib3)\), which we lightly adapt so that our judges are scored under an established, externally defined rubric rather than one of our own design\. Pass/fail and all confusion\-matrix metrics use the raw human score, so a human\-4 graded as 6 by a judge is correctly counted as a false positive\. The benchmark also ships a per\-problem marking scheme; we do not provide it to the judge\.

#### Judges and reasoning settings\.

We evaluate three cheap open\-weight models \(GPT\-OSS\-120B,DeepSeek\-V4\-Flash, andGemma\-4\-31B\) and two frontier baselines,Claude Opus 4\.7andGemini 3\.1 Pro\. The three cheap models were chosen for their cost\-accuracy tradeoff and offsetting calibration biases \(Gemma over\-credits, DeepSeek\-V4\-Flash under\-credits\), the intended ingredient for a majority vote\. These bias signs hold across our replicate runs \(Section[6\.2](https://arxiv.org/html/2608.00004#S6.SS2)\), so the trio’s diversity is a property of the models, not of any single run\.*For each model we use the strongest reasoning configuration it exposes\.*These settings are not normalized and are not directly comparable across providers: GPT\-OSS\-120B runs at effortxhigh, Gemma\-4\-31B and Gemini\-3\.1\-Pro with reasoning activated \(listed as efforthigh\), while Claude Opus 4\.7 \(adaptive thinking\) and DeepSeek\-V4\-Flash \(default\) self\-regulate their reasoning, so we report them at their default\. The “Reasoning” column in each table names the per\-model setting\.

#### Consensus rule\.

The cheap consensus is the majority pass/fail vote of the three cheap models\. We also report a*continuous*consensus score \(the mean of member scores\) only for completeness: because averaging the bucketed\{0,1,6,7\}\\\{0,1,6,7\\\}outputs produces intermediate values that no single judge can emit, the consensus Spearmanρ\\rhois not comparable to single\-judge correlations, and we therefore omit it \(shown as “—”\) throughout\. Majority vote was the pre\-specified consensus rule; alternate variants \(pairs, all\-three\-pass\) were added during the full\-benchmark analysis in Section[6\.1](https://arxiv.org/html/2608.00004#S6.SS1)after observing that the vote did not improve over its strongest member on validation\.

#### Providers, coverage, and re\-runs\.

The cheap open\-weight judges are served through OpenRouter by a shifting pool of third\-party providers at varying quantizations; we did not pin a provider, so a single judge’s pass\-agreement can move by a few points between runs \(quantified in Section[6\.2](https://arxiv.org/html/2608.00004#S6.SS2)\)\. For a reproducible number, pin a provider and log the served\-provider field; the frontier baselines are first\-party, single\-provider, and stable\. Under2%2\\%of judge calls failed to return a parseable score on the first attempt \(transient rate limits, or reasoning that exceeded the 32k\-token output ceiling without concluding\); we re\-ran these \(runaways usually converged on a retry\) and never substituted fabricated scores\. Final coverage is 1000/1000 for each cheap judge and 200/200 for each frontier baseline\. All per\-instance scores and standalone code \(standard library only\) that regenerates every table and figure are in the supplementary materials\.

## 5Results

Table[1](https://arxiv.org/html/2608.00004#S5.T1)reports the validation results, sorted by pass\-agreement, with95%95\\%bootstrap confidence intervals \(1000 resamples\)\. This is our primary comparison: the only setting in which all five judges, frontier and cheap, are run head\-to\-head\. Figure[1](https://arxiv.org/html/2608.00004#S5.F1)shows the same comparison as a forest plot\.

Table 1:Validation results \(n=200n=200; metrics over valid responses\)\. Reasoning names each model’s maximum/natural setting \(see Section[4](https://arxiv.org/html/2608.00004#S4)\); the consensus Spearmanρ\\rhois omitted \(“—”\) as it is not comparable to single\-judge correlations\.![Refer to caption](https://arxiv.org/html/2608.00004v1/x1.png)Figure 1:Pass/fail agreement with humans \(95% CI\) for all six systems \(the five judges and the cheap consensus\) on the validation sample \(n=200n=200\), sorted by point estimate, with per\-200\-call cost at right \(frontier costs boxed\)\. Every cheap judge’s interval overlaps the leader’s estimate \(dashed line\), at one to two orders of magnitude lower cost than the frontier baselines\.#### The cheap tier is competitive with the frontier\.

The confidence intervals for the top five systems \(all but Gemma\) overlap substantially\. GPT\-OSS\-120B has the highest point estimate, but it is best read as the front\-runner of a cluster, not a clear winner: pairwise, it is statistically indistinguishable from Claude Opus 4\.7 \(P≈0\.76P\\approx 0\.76of being higher on a resample\) and only weakly separated from Gemma\. Our sample does not support a claim that any single model is best\. It does support the claim that the cheap cluster sits inside the frontier’s interval: three open\-weight judges, each costing under $1 per 200 gradings, match two models costing $28–32 for the same work\.

#### The consensus did not beat its best member\.

The majority vote matched Opus on pass\-agreement, but its agreement \(0\.8550\.855\) and F1 \(0\.7790\.779\) fell below those of its strongest single member, GPT\-OSS\-120B \(0\.8750\.875,0\.8060\.806\), at roughly five times the cost \($1\.73 vs $0\.32\)\. Combining a strong model with two weaker ones diluted rather than improved the result\. We return in Section[6\.1](https://arxiv.org/html/2608.00004#S6.SS1)to whether a different consensus rule over the same trio fares better\.

#### The price gap is dramatic\.

GPT\-OSS\-120B grades at $0\.0016 per instance, about100×100\\timescheaper than Claude Opus 4\.7\($0\.162\) and∼90×\{\\sim\}90\\timescheaper than Gemini 3\.1 Pro at high reasoning \($0\.143\)\. Every cheap judge in Table[1](https://arxiv.org/html/2608.00004#S5.T1)is one to two orders of magnitude cheaper than either frontier baseline, with no consistent accuracy penalty on the pass/fail decision\. This is the practical headline\.

#### Where the frontier still leads\.

The frontier keeps an edge on rank correlation with the human score: Opus \(0\.7150\.715\) and Gemini \(0\.7040\.704\) sit above the cheap judges \(0\.620\.62–0\.680\.68\)\. The margin is modest \(Gemma reaches0\.6760\.676\), but for applications that need a graded quality signal rather than a pass/fail gate, a frontier judge is still the safer choice\. Appendix[B](https://arxiv.org/html/2608.00004#A2)visualizes this split\.

#### All of this is relative\.

In absolute terms no judge here is highly reliable: single\-judge precision and F1 sit in the0\.60\.6–0\.80\.8range, and because only∼30%\{\\sim\}30\\%of instances are passes, the high pass\-agreement rates are less impressive than they appear \(a fail\-everything baseline already scores0\.7150\.715\)\. Pushing precision into the mid\-0\.800\.80s takes the unanimous consensus rules of Section[6\.1](https://arxiv.org/html/2608.00004#S6.SS1)\.

Reasoning effort turns out to be a model\-specific lever: raising Gemini to high reasoning does not change its agreement, while it matters a great deal for GPT\-OSS\-120B; we report this comparison in Appendix[A](https://arxiv.org/html/2608.00004#A1)\.

## 6Additional Results

The two studies below extend the primary comparison\. Neither changes the headline, and both are run on the cheap tier only \(the frontier baselines are validation\-only, for budget\); we present them as supporting evidence\.

### 6\.1The full benchmark \(n=1000n=1000\)

We graded all three cheap judges over thecomplete 1000\-instance benchmark\(prior \+ validation \+ the remaining 600\) for a more stable estimate and to explore consensus configurations beyond the pre\-specified majority vote\.

Table 2:Full benchmark \(n=1000n=1000\), 95% bootstrap CIs \(2000 resamples\)\. Pairs and “all\-three” use the unanimous\-pass rule \(a candidate passes only if all listed members pass\); consensus Spearmanρ\\rhois omitted \(“—”; see Section[4](https://arxiv.org/html/2608.00004#S4)\)\.Three observations\. First,the single\-model leader changes with scale: GPT\-OSS\-120B led on the 200\-instance validation sample, but on the full benchmark DeepSeek\-V4\-Flash is the strongest single judge \(0\.8730\.873vs0\.8420\.842\), direct evidence that 200 instances cannot separate the leaders \(Figure[2](https://arxiv.org/html/2608.00004#S6.F2)\)\. Second,the choice of consensus rule trades precision against recall: the unanimous all\-three\-pass rule reaches the highest pass\-agreement \(0\.8790\.879\) and precision \(0\.8550\.855\), while majority vote is the most recall\-heavy \(0\.9120\.912\)\. Third,every confidence interval still overlaps, consistent with the validation finding that no single configuration is separable\.

![Refer to caption](https://arxiv.org/html/2608.00004v1/x2.png)Figure 2:The strongest single judge flips between the 200\-instance validation sample and the full 1000\-instance benchmark \(GPT\-OSS↔\\leftrightarrowDeepSeek\); the 95% CIs overlap throughout, so 200 instances cannot separate the leaders\.The choice of consensus rule is effectively a precision/recall dial \(Figure[3](https://arxiv.org/html/2608.00004#S6.F3)\)\. Unanimous rules, such as both\-pass pairs \(e\.g\., DeepSeek \+ GPT\-OSS\) or all\-three\-pass, suppress false positives by passing a candidate only when members agree, which is the right profile when wrongly passing a flawed proof is costly; majority vote instead maximizes recall\. The strictness of a pair is driven by its most conservative member: any pairing that includes the under\-crediting DeepSeek\-V4\-Flash inherits high precision, and adding the over\-crediting Gemma to an already\-strict pair changes little\.

![Refer to caption](https://arxiv.org/html/2608.00004v1/x3.png)Figure 3:Consensus rule as a precision/recall dial on the full benchmark \(n=1000n=1000\); dashed lines are iso\-F1 contours\. Majority vote sits at high recall, while the unanimous rules \(both\-pass pairs and all\-three\-pass\) move toward high precision\.
### 6\.2Run\-to\-run variance \(validation, four runs\)

How stable are these numbers across repeated runs? We re\-ran the cheap tier on the same 200\-instance validation sample three more times, with no fixed random seed, giving four independent runs per system \(including the original\)\. Table[3](https://arxiv.org/html/2608.00004#S6.T3)reports pass\-agreement for each run, with the mean and standard deviation; Figure[4](https://arxiv.org/html/2608.00004#S6.F4)plots the per\-run points and their spread\.

Table 3:Run\-to\-run pass\-agreement on validation \(n=200n=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=191n=191–199199\): self\-maj\. passes if≥2\\geq 2of 3 runs pass, self\-all\-3 if all 3 pass\. Consensus\-of\-consensus cells are blank \(“—”\)\.![Refer to caption](https://arxiv.org/html/2608.00004v1/x4.png)Figure 4:Run\-to\-run pass\-agreement across four independent runs \(n=200n=200\)\. Faded points are individual runs; solid points are mean±\\pmstd\. All\-three\-pass is both the highest and the tightest; single cheap judges drift more than the consensus rules\.Three points\. First,the unanimous all\-three\-pass rule is the best configuration on this sample on both counts: the highest mean \(0\.9020\.902\) and the smallest spread \(std0\.0090\.009\)\. Second,the majority vote is steadier than its individual members\(std0\.0140\.014, versus0\.0220\.022–0\.0240\.024for GPT\-OSS and DeepSeek\)\. Third, the single\-judge numbers move enough to matter:GPT\-OSS’s headline0\.8750\.875is the top of its0\.830\.83–0\.880\.88range, not a fixed value, while DeepSeek is the most reliable single judge \(mean0\.8810\.881\), matching the full\-benchmark result in Section[6\.1](https://arxiv.org/html/2608.00004#S6.SS1)\. We do not claim consensus always reduces variance: Gemma alone is the steadiest single judge \(std0\.0110\.011\), edging out even the majority vote\.

This variance comes from how the models are served, not from the models changing\. Each call to GPT\-OSS\-120B or DeepSeek\-V4\-Flash is routed to one of several third\-party providers, and different providers run the model at different numerical precisions \(quantization\), so identical requests can return slightly different scores\. Gemma is served almost entirely \(∼93%\{\\sim\}93\\%\) by a single provider, which is likely why its spread is small\. The frontier baselines run on their own providers and are stable \(a 20\-problem re\-run of Opus produced no pass/fail changes\), so the run\-to\-run movement is specific to the cheaply\-hosted open judges and does not affect the head\-to\-head comparison in Section[5](https://arxiv.org/html/2608.00004#S5)\. It does mean that any single cheap\-judge number should be read as one draw from a few\-point band, which is a further reason to prefer the steadier consensus rules\.

The two rightmost columns of Table[3](https://arxiv.org/html/2608.00004#S6.T3)turn that variance to advantage by applying the consensus rules to a single model’s own three runs\. For the recall\-biased judges this helps: requiring all three GPT\-OSS runs to pass lifts agreement from a single\-run mean of0\.8510\.851to0\.8880\.888, and Gemma from0\.8100\.810to0\.8490\.849, because the run\-to\-run noise produces occasional spurious passes that a unanimity rule filters out, lifting GPT\-OSS’s precision from0\.720\.72to0\.780\.78and giving it its highest F1 \(0\.810\.81\)\. DeepSeek, already balanced, does not surpass its best single run \(0\.9050\.905\)\. This is the same precision\-for\-recall trade as the cross\-model rules in Section[6\.1](https://arxiv.org/html/2608.00004#S6.SS1), amplified because successive runs are often served by different providers; in effect, running one cheap model three times and requiring unanimity recovers much of the multi\-model consensus benefit \(GPT\-OSS self\-all\-3 reaches0\.8880\.888, approaching the cross\-model all\-three\-pass at0\.9020\.902\)\. This is why we recommend all\-three\-pass as the default budget judge: within noise of every alternative on agreement, but the most precise and the most stable, and cheap enough that the single\-model variant is a viable fallback when three judges is too many calls\.

## 7Limitations

Sample size and intervals\.Even on the full benchmark, the leading systems’ confidence intervals overlap and we cannot resolve a single best judge\. The 30\-problem pool means problem\-level effects are real, and our bootstrap intervals resample instances independently, so they do not account for this clustering by source problem; problem\-level \(cluster\) bootstrap intervals would be somewhat wider\.

Run\-to\-run variance \(cheap tier\)\.Single cheap judges vary by∼2\{\\sim\}2points \(std\) across runs due to OpenRouter provider routing \(Section[6\.2](https://arxiv.org/html/2608.00004#S6.SS2)\); we did not pin providers for the headline runs\. We did not replicate the frontier baselines beyond a 20\-problem Opus drift screen \(0/20 flips\), which suggests they are stable\.

Budget\-constrained search\.We could not afford a broad sweep, and frontier baselines were not run on the full benchmark\. Most notably, we did*not*evaluate GPT\-5\.5 Pro at xhigh reasoning: at roughly $180 per million output tokens \(more than7×7\\timesthe price of Claude Opus 4\.7\) a single full run was out of budget\.

Contamination\.Training\-data leakage is unlikely to explain the result, at least for our strongest cheap judge: GPT\-OSS\-120B was released on 2025\-08\-05, three months*before*IMO\-GradingBench \(2025\-11\-03\), so it cannot have trained on the benchmark’s graded instances\. Models released afterward \(including Gemma\-4 and DeepSeek\-V4\) could in principle have seen it, but grading a candidate against a provided reference solution is a distinct task from having encountered the problem, and the benchmark includes problems written specifically for it\.

Post\-hoc rule selection\.All\-three\-pass was identified through rule search on the full benchmark rather than pre\-specified; the precision and stability advantages we report come from the same data the rule was selected on\. Independent replication would strengthen the recommendation\.

Judging, not solving\.These results speak to judge reliability against ground\-truth proofs and human scores\. They say nothing about a model’s ability to*produce*proofs\.

Scope\.Findings are specific to IMO\-style competition mathematics with a ground\-truth reference and a human grade\. We do not claim they transfer to reference\-free verification or to other domains\.

## 8Conclusion

For grading AI\-generated natural\-language proofs on a budget, cheap open\-weight judges are a credible choice: they match frontier judges on pass/fail agreement with human graders at about1%1\\%of the cost, which also makes them cheap enough to run repeatedly inside a self\-improving loop\. The intuition that a consensus of cheap models would be the best option was not borne out \(the majority vote did not beat its strongest member\), but the broader result is more valuable and more robust: the cheap tier as a whole competes at the frontier, and the consensus rule offers a precision/recall dial and the most stable behavior across runs\. For a deployable baseline we would recommend all\-three\-pass: across our configurations it has the highest precision and the smallest run\-to\-run spread \(although a single cheap model run three times under a unanimity rule recovers much of the same benefit\)\. We deliberately stop short of crowning a single model; our intervals do not support it, and the leader shifts between the validation sample and the full benchmark\.

These conclusions are preliminary\. The clear next step is a more comprehensive evaluation, with more replicates per judge \(and pinned providers\) and a wider set of models run across the entire benchmark by researchers with a larger budget\. We expect the central finding \(that very cheap judges are competitive\) to hold, though we would not be surprised to learn that they underperform GPT\-5\.5 Pro \(xhigh\) or Gemini 3\.1 DeepThink\.

## Impact Statement

This paper studies how to evaluate AI\-generated mathematical proofs cheaply and reliably\. Lowering the cost of trustworthy automated grading can broaden participation in math\-reasoning research to groups without large compute budgets\. A risk of any automated judge is over\-reliance on its pass/fail decisions; we emphasize that these judges are imperfect, are validated only on IMO\-style problems with a ground\-truth reference, and are not a substitute for human review in high\-stakes settings\.

## References

- L\. de Moura and S\. Ullrich \(2021\)The Lean 4 theorem prover and programming language\.InAutomated Deduction – CADE 28,Lecture Notes in Computer Science, Vol\.12699,pp\. 625–635\.Cited by:[§1](https://arxiv.org/html/2608.00004#S1.p1.1)\.
- J\. Dekoninck, I\. Petrov, K\. Minchev, M\. Balunović, M\. Vechev, M\. Marinov, M\. Drencheva, L\. Konova, M\. Shumanov, K\. Tsvetkov, N\. Drenchev, L\. Todorov, K\. Nikolova, N\. Georgiev, V\. Kalinkova, and M\. Ismoldayev \(2025\)The open proof corpus: a large\-scale study of LLM\-generated mathematical proofs\.arXiv preprint arXiv:2506\.21621\.Cited by:[§2](https://arxiv.org/html/2608.00004#S2.p1.1)\.
- J\. Gu, X\. Jiang, Z\. Shi, H\. Tan, X\. Zhai, C\. Xu, W\. Li, Y\. Shen, S\. Ma, H\. Liu, S\. Wang, K\. Zhang, Y\. Wang, W\. Gao, L\. Ni, and J\. Guo \(2024\)A survey on LLM\-as\-a\-Judge\.arXiv preprint arXiv:2411\.15594\.Cited by:[§2](https://arxiv.org/html/2608.00004#S2.p1.1)\.
- T\. Hubert, R\. S\. Mehta, L\. Sartran, M\. Z\. Horváth, G\. Žužić, E\. Wieser, A\. Huang, J\. Schrittwieser, Y\. Schroecker,et al\.\(2025\)Olympiad\-level formal mathematical reasoning with reinforcement learning\.Nature\.Note:AlphaProofExternal Links:[Document](https://dx.doi.org/10.1038/s41586-025-09833-y)Cited by:[§1](https://arxiv.org/html/2608.00004#S1.p1.1)\.
- T\. Luong, D\. Hwang, H\. H\. Nguyen, G\. Ghiasi, Y\. Chervonyi, I\. Seo, J\. Kim, G\. Bingham, J\. Lee, S\. Mishra, A\. Zhai, H\. Hu, H\. Michalewski, J\. Kim, J\. Ahn, J\. Bae, X\. Song, T\. H\. Trinh, Q\. V\. Le, and J\. Jung \(2025\)Towards robust mathematical reasoning\.InProceedings of the 2025 Conference on Empirical Methods in Natural Language Processing \(EMNLP\),Suzhou, China,pp\. 35418–35442\.Note:Introduces IMO\-Bench, including IMO\-GradingBench and the four\-bucket grading promptCited by:[§1](https://arxiv.org/html/2608.00004#S1.p3.1),[§2](https://arxiv.org/html/2608.00004#S2.p1.1),[§4](https://arxiv.org/html/2608.00004#S4.SS0.SSS0.Px2.p1.1)\.
- W\. Ma, A\. Cojocaru, N\. Kolhe, B\. Louie, R\. S\. Sharif, H\. Zhang, V\. Zhuang, M\. Zaharia, and S\. Min \(2026\)Reliable fine\-grained evaluation of natural language math proofs\.InInternational Conference on Learning Representations \(ICLR\),Note:Introduces ProofBench and ProofGraderCited by:[§2](https://arxiv.org/html/2608.00004#S2.p2.2)\.
- A\. Naik, G\. Shabadi, R\. Alur, and M\. Naik \(2026\)Do we need frontier models to verify mathematical proofs?\.arXiv preprint arXiv:2604\.02450\.Cited by:[§2](https://arxiv.org/html/2608.00004#S2.p2.2)\.
- I\. Petrov, J\. Dekoninck, L\. Baltadzhiev, M\. Drencheva, K\. Minchev, M\. Balunović, N\. Jovanović, and M\. Vechev \(2025\)Proof or bluff? evaluating LLMs on 2025 USA math olympiad\.arXiv preprint arXiv:2503\.21934\.Cited by:[§2](https://arxiv.org/html/2608.00004#S2.p1.1)\.
- P\. Verga, S\. Hofstätter, S\. Althammer, Y\. Su, A\. Piktus, A\. Arkhangorodsky, M\. Xu, N\. White, and P\. Lewis \(2024\)Replacing judges with juries: evaluating LLM generations with a panel of diverse models\.arXiv preprint arXiv:2404\.18796\.Cited by:[§1](https://arxiv.org/html/2608.00004#S1.p4.1),[§2](https://arxiv.org/html/2608.00004#S2.p1.1)\.
- L\. Zheng, W\. Chiang, Y\. Sheng, S\. Zhuang, Z\. Wu, Y\. Zhuang, Z\. Lin, Z\. Li, D\. Li, E\. P\. Xing, H\. Zhang, J\. E\. Gonzalez, and I\. Stoica \(2023\)Judging LLM\-as\-a\-Judge with MT\-Bench and Chatbot Arena\.InAdvances in Neural Information Processing Systems 36 \(NeurIPS\), Datasets and Benchmarks Track,Cited by:[§2](https://arxiv.org/html/2608.00004#S2.p1.1)\.

## Appendix AReasoning Effort Is a Model\-Specific Lever

Because Table[1](https://arxiv.org/html/2608.00004#S5.T1)reports Gemini 3\.1 Pro at high reasoning, we can read the effect of reasoning effort directly\. To check whether reasoning*budget*, rather than model identity, drives judge quality, we additionally ran Gemini 3\.1 Pro at its default setting for a within\-model comparison \(Table[4](https://arxiv.org/html/2608.00004#A1.T4)\)\.

Table 4:Gemini 3\.1 Pro: default vs\. high reasoning \(n=200n=200\)\. “Agree” is pass\-agreement,ρ\\rhois Spearman, and cost is per 200 gradings\.Raising Gemini’s reasoning roughly fourfold left its pass\-agreementunchanged\(0\.8400\.840in both cases; a paired bootstrap finds no detectable difference, and ten individual decisions flipped but canceled out\), while quadrupling its cost\. By contrast, reasoning effort matters a great deal for GPT\-OSS\-120B: on the exploratory sample its pass\-agreement rises from0\.720\.72at minimal effort to0\.840\.84atxhigh\(its validationxhighrun,0\.8750\.875, is the one reported in Table[1](https://arxiv.org/html/2608.00004#S5.T1)\)\. Claude Opus 4\.7 uses adaptive thinking and does not accept a manual reasoning budget, so its reported result already reflects whatever thinking it elects to do\. The conclusion is that reasoning effort is a model\-specific lever, not a universal one: large for GPT\-OSS\-120B, negligible for Gemini\.

## Appendix BPass/Fail vs\. Rank Correlation

Figure[5](https://arxiv.org/html/2608.00004#A2.F5)plots the two axes against each other: pass/fail agreement with humans, the decision practitioners gate on, and Spearman rank correlation with the human score, a graded\-quality signal\. The split matches Section[5](https://arxiv.org/html/2608.00004#S5): the cheap judges stay competitive on pass/fail, while the two frontier models lead on rank correlation by a modest margin\. DeepSeek\-V4\-Flash is the exception that does well on both, consistent with its standing as the most reliable cheap judge in Section[6](https://arxiv.org/html/2608.00004#S6)\. This lead is measured on the validation sample only: on the full benchmark the cheap judges’ rank correlation rises to0\.700\.70–0\.740\.74\(Table[2](https://arxiv.org/html/2608.00004#S6.T2)\), matching the frontier’s validation values, so—as with the pass/fail leader \(Section[6\.1](https://arxiv.org/html/2608.00004#S6.SS1)\)—the gap may be a small\-sample effect\. We did not run the frontier baselines on the full benchmark, so a matched full\-benchmark correlation comparison is not available\.

![Refer to caption](https://arxiv.org/html/2608.00004v1/x5.png)Figure 5:Pass/fail agreement \(x\) versus Spearman rank correlation with the human score \(y\) on the validation sample \(n=200n=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\.