Cost-Effective Automated Judging of Natural-Language Mathematical Proofs

automated proof judgingconsensus rulescost-efficient aiimo-gradingbenchllm evaluationmajority votingnatural-language proofs

Cost-Effective Automated Judging of Natural-Language Mathematical Proofs


Author: Benjamin Grayzel

Submitted: May 29, 2026

Subjects: Computation and Language (cs.CL); Artificial Intelligence (cs.AI); Machine Learning (cs.LG)

arXiv ID: 2608.00004


Abstract


Grading natural-language mathematical proofs is a recurring cost in evaluating math-reasoning systems, and frontier LLM judges remain prohibitively expensive. This paper investigates whether cheap open-weight models can serve as reliable judges when provided with a candidate proof, a ground-truth proof, and a human-grading rubric. On a 200-instance validation sample of IMO-GradingBench, three cost-efficient judges—GPT-OSS 120B, DeepSeek-V4 Flash, and Gemma-4 31B—achieved human pass/fail agreement rates statistically indistinguishable from frontier models (Claude Opus 4.7 and Gemini 3.1 Pro), at up to 100× lower cost. Contrary to our initial hypothesis that a majority vote of the three cheap judges would outperform individual models, the ensemble matched but did not exceed its strongest member. Extending to the full 1,000-instance benchmark, we explored consensus rules and found that requiring unanimous agreement (all-three-pass) yielded the highest pass-agreement and precision, along with the smallest run-to-run variance across four replicate runs. The headline finding is that cheap judges are competitively accurate at one to two orders of magnitude lower cost, making them a practical default. However, we recommend the all-three-pass rule with caution, as it was selected post-hoc and requires independent replication.


1. Introduction


The evaluation of mathematical reasoning in AI systems increasingly relies on judging natural-language proofs, a task that is both labor-intensive and costly. While frontier large language models (LLMs) offer high accuracy as judges, their expense limits scalability, particularly for researchers with constrained budgets. This study investigates a cost-effective alternative: leveraging open-weight, smaller models as automated proof judges. By benchmarking three affordable models against frontier counterparts on the IMO-GradingBench dataset, we assess their reliability and explore aggregation strategies to optimize performance.


2. Methodology


We evaluated three cheap open-weight models—GPT-OSS 120B, DeepSeek-V4 Flash, and Gemma-4 31B—as automated judges. Each model was given a candidate proof, a ground-truth proof, and a human-designed rubric, and tasked with providing a pass/fail decision. For comparison, we used two frontier models: Claude Opus 4.7 and Gemini 3.1 Pro. The evaluation was conducted on a 200-instance validation sample, followed by a full 1,000-instance benchmark. We implemented various consensus rules, including majority voting and unanimous agreement (all-three-pass), to combine the outputs of the three cheap judges.


3. Results


On the validation sample, the three cheap judges achieved pass/fail agreement with human graders at rates statistically indistinguishable from the frontier models. Notably, this performance came at up to 100× lower cost. When we combined the three cheap judges via majority voting, the ensemble’s accuracy matched the frontier models but did not surpass its strongest individual member (GPT-OSS 120B). On the full benchmark, the all-three-pass rule—requiring all three models to agree on a pass—produced the highest pass-agreement and precision, with the smallest variation across four replicate runs.


4. Discussion


Our findings demonstrate that cheap open-weight models can serve as reliable, cost-effective judges for natural-language mathematical proofs. The all-three-pass rule, which minimizes false positives, is particularly well-suited for high-stakes evaluations where precision is critical. However, its post-hoc selection introduces potential bias, and we advocate for independent replication to confirm its superiority. As AI models continue to evolve, these cost-efficient judging strategies could democratize access to robust evaluation frameworks in mathematical reasoning research.


5. Conclusion


Frontier LLMs are no longer the sole option for accurate automated judging. Cheap open-weight models, when properly aggregated, offer comparable reliability at a fraction of the cost. We recommend the all-three-pass rule as a default deployment choice, contingent on further validation. Future work should explore broader datasets and adaptive consensus rules to enhance robustness.




Comments: 7 pages, 5 figures, 4 tables

Cite as: arXiv:2608.00004 [cs.CL]

DOI: 10.48550/arXiv.2608.00004

via ArXiv CL+LG

Related