Pith. sign in

REVIEW 3 major objections 4 minor 10 references

Cheap open-weight language models match frontier judges on pass/fail grading of natural-language math proofs, at up to 100x lower cost.

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-04 04:52 UTC pith:GTLGACFW

load-bearing objection Cheap judges may indeed be competitive, but the 'statistically indistinguishable' claim rests on underpowered n=200 data and overstates what the paper shows; worth refereeing with a required statistical revision. the 3 major comments →

arxiv 2608.00004 v1 pith:GTLGACFW submitted 2026-05-29 cs.CL cs.AIcs.LG

Cost-Effective Automated Judging of Natural-Language Mathematical Proofs

Benjamin Grayzel This is my paper
classification cs.CL cs.AIcs.LG
keywords LLM-as-a-judgeproof gradingIMO-GradingBenchpass/fail agreementopen-weight modelscost-effective evaluationconsensus rulesmathematical reasoning
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper asks whether cheap open-weight language models can judge natural-language math proofs as reliably as expensive frontier models, when each judge is given a reference solution and a human-grading rubric. It reports that, on a 200-instance sample of the IMO-GradingBench benchmark, three cheap models agree with human pass/fail decisions at rates statistically indistinguishable from two frontier baselines, at roughly one to two orders of magnitude lower cost. The authors expected a majority vote of the three cheap models to be the best budget option, but it did not beat its strongest member; instead, a unanimous all-three-pass rule agreed with humans even more often and had the smallest run-to-run spread, though this rule was selected after seeing the data. The paper is deliberately narrow, covering only IMO-style problems with ground-truth references and human scores, not proof generation or reference-free verification.

Core claim

On the 200-instance validation sample, GPT-OSS-120B, DeepSeek-V4-Flash, and Gemma-4-31B each agreed with human pass/fail decisions within the confidence intervals of the frontier leaders Claude Opus 4.7 and Gemini 3.1 Pro, with per-grading costs of $0.0016 to $0.0036 versus roughly $0.14–$0.16. The pre-specified majority vote of the three matched but did not exceed its strongest member (0.855 vs 0.875 pass-agreement). Over the full 1000-instance benchmark, the unanimous all-three-pass rule reached the highest pass-agreement (0.879) and precision (0.855) and, across four replicate runs, the smallest run-to-run spread (std 0.009). The paper stops short of naming a single best judge: confidence

What carries the argument

The judge prompt is a four-bucket IMO scoring scheme ({0,1,6,7}) with pass defined as a score of ≥6; each judge receives the problem, a ground-truth reference solution, and the candidate proof, so it never verifies a proof from scratch. The evaluation relies on bootstrap 95% confidence intervals for pass-agreement and on a panel of three cheap open-weight models chosen for offsetting calibration biases (one over-credits, one under-credits). Consensus rules—majority vote versus unanimous all-three-pass—act as a precision/recall dial, with the unanimous rule suppressing false passes at the cost of recall.

Load-bearing premise

The headline claim rests on treating overlapping 95% bootstrap confidence intervals from a 200-instance sample (with only about 30% passes) as evidence that cheap judges are statistically indistinguishable from frontier judges, without a paired test or a pre-specified equivalence margin; the study has low power to detect a real 5–10 point gap.

What would settle it

Run all five judges on the full 1000-instance benchmark with pinned providers and repeated runs, then compare pass-agreement with a paired test against a pre-specified equivalence bound (e.g., cheap judges within ±5 points of the best frontier judge). If a frontier judge is more than 5 points better on the full set, the claim that cheap judges carry no accuracy penalty fails.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • Budget-constrained labs can use cheap open-weight judges instead of frontier models for pass/fail gating of IMO-style proofs, cutting grading cost by roughly two orders of magnitude.
  • Self-improving loops that generate, critique, and revise proofs can afford many more judge calls per experiment, enabling more iterations at the same budget.
  • The all-three-pass rule (or running one cheap model three times and requiring unanimity) suppresses false passes, which matters when wrongly passing a flawed proof is costly.
  • Frontier judges still show a modest edge in rank correlation with human scores on the validation sample, so applications needing a graded-quality signal rather than a pass/fail gate may still prefer them.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The close agreement in this reference-based setting, contrasted with the roughly 10% gap reported for reference-free verification by concurrent work, suggests the ground-truth reference is doing much of the judging work; a direct ablation (judge with vs. without the reference) would quantify that contribution.
  • The run-to-run variance from un-pinned third-party providers means any single cheap-judge score should be read as a band, not a point; pinning providers could make cheap judges both more reliable and easier to replicate.
  • The self-all-3 result (one model run three times under unanimity nearly matching the cross-model consensus) implies the ensemble benefit here is largely variance reduction rather than error-canceling diversity; this could be tested by comparing the two on a fresh, larger sample.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

3 major / 4 minor

Summary. The paper studies whether cheap open-weight LLMs can grade natural-language mathematical proofs against a reference solution and human rubric at the pass/fail boundary, using 200 instances from IMO-GradingBench as a validation sample and 1,000 instances for an extended cheap-tier analysis. It compares three cheap judges (GPT-OSS-120B, DeepSeek-V4-Flash, Gemma-4-31B) with two frontier baselines (Claude Opus 4.7, Gemini 3.1 Pro) on pass-agreement, precision/recall/F1, Spearman correlation, and cost. The author reports that cheap judges are competitive with frontier models at 1–2 orders of magnitude lower cost, that majority voting does not beat its strongest member, and that a post-hoc unanimous 'all-three-pass' rule achieves the highest precision and stability. The paper is unusually candid about limitations: the validation sample is small, the bootstrap ignores clustering by source problem, the all-three-pass rule was selected post-hoc, and frontier baselines were not run on the full benchmark.

Significance. If the central finding holds after closer statistical scrutiny, the practical contribution is substantial: automated proof grading is a recurring cost in math-reasoning evaluation, and reducing that cost by one to two orders of magnitude without losing pass/fail agreement would benefit budget-constrained researchers and enable more iteration in self-improving systems. The paper also ships reproducible assets (code, per-instance scores, prompts) and reports a wide range of metrics. Its transparency about post-hoc rule selection, provider-dependent variance, and contamination is exemplary. The main weakness is that the headline 'statistically indistinguishable' claim rests on overlapping confidence intervals from n=200, with no equivalence test, no paired analysis, and no cluster bootstrap; the paper's own Figure 2 shows that 200 instances cannot separate leaders. A more cautious equivalence statement would make the contribution sound and still valuable.

major comments (3)
  1. [Abstract; §5, Table 1; §6.1, Figure 2] The central claim of the abstract is not supported by the reported statistics. Overlapping 95% bootstrap intervals on n=200 do not establish equivalence; the paper itself shows (Figure 2) that an 8-point gap (GPT-OSS vs Gemma) has overlapping intervals and that the leader flips when the cheap tier is run on n=1000. No paired test (e.g., McNemar) or pre-specified equivalence margin is given; the 'P≈0.76' in §5 is a bootstrap proportion, not a test. Since the frontier baselines were not run at n=1000, the headline comparison rests entirely on this low-power sample. Please add a paired analysis and a stated equivalence margin, report cluster-bootstrap intervals by source problem, and reword the abstract to say the study 'cannot detect' a difference rather than 'statistically indistinguishable.'
  2. [Table 1; Figure 1; §5] The statement that all three cheap judges are 'statistically indistinguishable' from the frontier conflicts with Table 1: Gemma-4-31B's interval [0.740, 0.850] excludes GPT-OSS's point estimate 0.875 and is centered roughly 6–8 points lower than the frontier estimates. Figure 1's caption claims 'every cheap judge's interval overlaps the leader's estimate,' but the text (§5) correctly says 'all but Gemma.' This inconsistency should be fixed, and the abstract should not count Gemma among the judges that match the frontier.
  3. [Abstract; §6.1; §7] The recommendation of all-three-pass as the deployable default is based on a rule selected post-hoc on the same full benchmark from which its precision/stability numbers are computed. The authors are transparent about this in §7, but the abstract's phrasing ('as a deployable default we recommend all-three-pass') outweighs the caveat. Since the rule was not pre-specified and receives no independent validation, the recommendation should be clearly labeled a preliminary hypothesis; alternatively, the authors could validate it on a new held-out sample (e.g., a further split of the 1,000 instances).
minor comments (4)
  1. [Figure 1 vs §5] The caption of Figure 1 says 'every cheap judge's interval overlaps the leader's estimate,' but Table 1 shows Gemma's interval does not include 0.875. Please align the caption with the text in §5 ('all but Gemma').
  2. [§6.2, Table 3] Table 3 reports pass-agreement for self-majority and self-all-3, but not the precision/F1 values that the text cites for GPT-OSS (e.g., precision 0.72 to 0.78, F1 0.81). Adding these columns would make the table self-contained.
  3. [§4, data collection] Re-running failed judge calls (under 2%) may introduce selection bias if failures correlate with instance difficulty. Please report per-model failure rates and, if possible, a sensitivity analysis treating failed calls as incorrect.
  4. [Appendix B / §5] The claim that the frontier's rank-correlation lead 'may be a small-sample effect' is plausible but unquantified. A paired bootstrap of the Spearman difference, or a confidence interval for the difference, would strengthen the discussion.

Circularity Check

0 steps flagged

No circularity: the central claim is an empirical held-out comparison; the post-hoc all-three-pass rule is transparently labeled, not presented as a prediction.

full rationale

This paper makes no mathematical derivation that could reduce to its inputs; it is an empirical evaluation of LLM judges on IMO-GradingBench. The headline cheap-vs-frontier comparison is run on a held-out validation sample (seed 7, disjoint from the exploratory sample), against external human grades and an externally defined four-bucket rubric, so no fitted parameter is later renamed as a prediction. The paper explicitly flags the one in-sample selection: Section 7 states that 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' and calls for independent replication. This is honest labeling of a post-hoc finding, not a circular step. The 'statistically indistinguishable' wording rests on overlapping bootstrap CIs at n=200; the paper itself concedes that '200 instances cannot separate the leaders' (Figure 2) and that bootstrap intervals ignore 30-problem clustering. Those are evidential-power limitations, not definitional equivalences. No load-bearing self-citation or imported uniqueness/ansatz appears; prior work (Verga et al.) motivates an expectation that was tested and abandoned because the data did not support it. Accordingly, no circular step is present.

Axiom & Free-Parameter Ledger

3 free parameters · 3 axioms · 0 invented entities

The central claim is an empirical comparison; its main external inputs are the benchmark's human labels, the choice of models and consensus rule, and the serving infrastructure. The paper is transparent about the post-hoc rule and clustering issue, but these choices still condition the numbers.

free parameters (3)
  • Cheap-judge trio membership = GPT-OSS-120B, DeepSeek-V4-Flash, Gemma-4-31B
    The three cheap models were chosen for cost-accuracy tradeoff and offsetting calibration biases, and the exploratory sample (seed 42) was used to select the consensus trio; this makes the validation comparison only partially independent for the model set.
  • All-three-pass consensus rule = unanimous pass on trio
    Identified through post-hoc rule search on the full 1000-instance benchmark (Section 6.1); its reported precision/stability advantages are in-sample and explicitly require independent replication (Section 7).
  • Per-model reasoning settings = GPT-OSS xhigh; DeepSeek default; Gemma high; Gemini high; Opus adaptive
    Chosen as each model's strongest/natural configuration; not normalized across providers, so cost and accuracy comparisons conflate model identity, reasoning budget, and serving conditions.
axioms (3)
  • domain assumption Human expert grades in IMO-GradingBench are treated as ground truth for the pass/fail label (score ≥6 = pass).
    All agreement metrics are computed against these human decisions; no inter-annotator reliability is reported (Section 3).
  • domain assumption The 200 validation instances are independent; problem-level clustering by the 30 source problems is ignored in all reported confidence intervals.
    Paper states the bootstrap resamples instances independently and that cluster-bootstrapped intervals would be wider (Section 7).
  • domain assumption OpenRouter-served open-weight models at varying quantization faithfully represent each named model.
    Run-to-run variance is attributed to provider routing and quantization; the paper does not pin providers or verify which quantization is served per call (Section 6.2).

pith-pipeline@v1.3.0-alltime-deepseek · 9524 in / 12639 out tokens · 128543 ms · 2026-08-04T04:52:03.414693+00:00 · methodology

0 comments
read the original 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 to $100\times$ lower 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.

Figures

Figures reproduced from arXiv: 2608.00004 by Benjamin Grayzel.

Figure 1
Figure 1. 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 = 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. did not pin a provider, so a single jud… view at source ↗
Figure 2
Figure 2. Figure 2: The strongest single judge flips between the 200-instance validation sample and the full 1000-instance benchmark (GPT-OSS ↔ DeepSeek); the 95% CIs overlap throughout, so 200 instances cannot separate the leaders. configurations beyond the pre-specified majority vote. Three observations. First, the single-model leader changes with scale: GPT-OSS-120B led on the 200-instance valida￾tion sample, but on the fu… view at source ↗
Figure 4
Figure 4. Figure 4: Run-to-run pass-agreement across four independent runs (n = 200). Faded points are individual runs; solid points are mean ± std. All-three-pass is both the highest and the tightest; single cheap judges drift more than the consensus rules. most reliable single judge (mean 0.881), matching the full￾benchmark result in Section 6.1. We do not claim consensus always reduces variance: Gemma alone is the steadies… view at source ↗
Figure 5
Figure 5. Figure 5: 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: the cheap judges stay competitive on pass/fail, while the two frontier models lead on rank correlation by a modest mar￾gin. DeepSeek-V4-Flash is the exception that does well on both, consistent w… view at source ↗

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

10 extracted references · 4 linked inside Pith

  1. [1]

    Automated Deduction -- CADE 28 , series =

    de Moura, Leonardo and Ullrich, Sebastian , title =. Automated Deduction -- CADE 28 , series =. 2021 , publisher =

    2021

  2. [2]

    and Sartran, Laurent and Horv

    Hubert, Thomas and Mehta, Rishi S. and Sartran, Laurent and Horv. Olympiad-level formal mathematical reasoning with reinforcement learning , journal =. 2025 , doi =

    2025

  3. [3]

    Luong, Thang and Hwang, Dawsen and Nguyen, Hoang H. and Ghiasi, Golnaz and Chervonyi, Yuri and Seo, Insuk and Kim, Junsu and Bingham, Garrett and Lee, Jonathan and Mishra, Swaroop and Zhai, Alex and Hu, Huiyi and Michalewski, Henryk and Kim, Jimin and Ahn, Jeonghyun and Bae, Junhwi and Song, Xingyou and Trinh, Trieu Hoang and Le, Quoc V. and Jung, Junehyu...

    2025

  4. [4]

    Replacing Judges with Juries: Evaluating

    Verga, Pat and Hofst. Replacing Judges with Juries: Evaluating. arXiv preprint arXiv:2404.18796 , year =

    Pith/arXiv arXiv

  5. [5]

    and Zhang, Hao and Gonzalez, Joseph E

    Zheng, Lianmin and Chiang, Wei-Lin and Sheng, Ying and Zhuang, Siyuan and Wu, Zhanghao and Zhuang, Yonghao and Lin, Zi and Li, Zhuohan and Li, Dacheng and Xing, Eric P. and Zhang, Hao and Gonzalez, Joseph E. and Stoica, Ion , title =. Advances in Neural Information Processing Systems 36 (NeurIPS), Datasets and Benchmarks Track , year =

  6. [6]

    arXiv preprint arXiv:2411.15594 , year =

    Gu, Jiawei and Jiang, Xuhui and Shi, Zhichao and Tan, Hexiang and Zhai, Xuehao and Xu, Chengjin and Li, Wei and Shen, Yinghan and Ma, Shengjie and Liu, Honghao and Wang, Saizhuo and Zhang, Kun and Wang, Yuanzhuo and Gao, Wen and Ni, Lionel and Guo, Jian , title =. arXiv preprint arXiv:2411.15594 , year =

    Pith/arXiv arXiv

  7. [7]

    Proof or Bluff? Evaluating

    Petrov, Ivo and Dekoninck, Jasper and Baltadzhiev, Lyuben and Drencheva, Maria and Minchev, Kristian and Balunovi. Proof or Bluff? Evaluating. arXiv preprint arXiv:2503.21934 , year =

    Pith/arXiv arXiv

  8. [8]

    The Open Proof Corpus: A Large-Scale Study of

    Dekoninck, Jasper and Petrov, Ivo and Minchev, Kristian and Balunovi. The Open Proof Corpus: A Large-Scale Study of. arXiv preprint arXiv:2506.21621 , year =

    arXiv

  9. [9]

    International Conference on Learning Representations (ICLR) , year =

    Ma, Wenjie and Cojocaru, Andrei and Kolhe, Neel and Louie, Bradley and Sharif, Robin Said and Zhang, Haihan and Zhuang, Vincent and Zaharia, Matei and Min, Sewon , title =. International Conference on Learning Representations (ICLR) , year =

  10. [10]

    arXiv preprint arXiv:2604.02450 , year =

    Naik, Aaditya and Shabadi, Guruprerana and Alur, Rajeev and Naik, Mayur , title =. arXiv preprint arXiv:2604.02450 , year =

    Pith/arXiv arXiv