Cost-Effective Automated Judging of Natural-Language Mathematical Proofs

Grading natural-language mathematical proofs is a recurring cost in evaluating math-reasoning systems, and frontier LLM judges are expensive. This paper investigates whether cheap open-weight models can serve as reliable judges given a candidate proof, a ground-truth proof, and a human-grading rubric, finding that cheap judges are competitive with the frontier at one to two orders of magnitude lower cost.

How it works

The study focuses on grading instances from IMO-GradingBench (Luong et al., 2025), which pairs 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 proof to predict the grade. The primary metric used is pass-agreement: the fraction of instances where the judge’s pass/fail decision matches the human’s (Page 3).

The researchers evaluated three cheap open-weight models (GPT-OSS120B, DeepSeek-V4-Flash, and Gemma-4-31B) against two frontier baselines (Claude Opus 4.7 and Gemini 3.1 Pro) on a 200-instance validation sample (Page 1). The cheap models were chosen for their cost-accuracy tradeoff and offsetting calibration biases (Gemma over-credits, DeepSeekV4-Flash under-credits), the intended ingredient for a majority vote (Page 4). For each model, the researchers used the strongest reasoning configuration it exposes (Page 4).

Methodology and Metrics

The primary metric is pass-agreement at the boundary: did the candidate proof meet the bar (a score of ≥ 6 on the 0–7 IMO scale)? (Page 3). Secondary ordinal measures include precision, recall, and Spearman rank correlation with the human score (Page 3). The study compares five systems: three cheap judges, two frontier baselines, and a cheap consensus rule defined as the majority pass/fail vote of the three cheap models (Page 4).

The judges were instructed to emit a score in the bucket set: emit a score in [0, 1, 6, 7] (incorrect / partial / almost / correct) (Page 4). The comparison is conducted across different settings; for instance, Gemini 3.1 Pro was tested at both its default setting and high reasoning configuration to show that reasoning effort is a model-specific lever, not a universal one (Page 6).

Key Findings on Performance

The headline finding is that cheap judges are competitive with the frontier at one to two orders of magnitude lower cost (Page 1). The consensus rule did not outperform its strongest member; the majority vote did not beat its strongest member (Page 5). However, extending the analysis to the full 1000-instance benchmark, requiring unanimous agreement (all-three-pass) reaches the highest pass-agreement and precision and, on four replicate runs, the smallest run-to-run spread (Page 1).

The cheap tier is competitive with the frontier; cheap openweight judges match frontier baselines (Claude Opus 4.7, Gemini 3.1 Pro) on pass/fail agreement with human graders at a cost of 1–2 orders of magnitude lower in our setup (Page 1). While the consensus did not beat its best member, the unanimous rule reaches the highest pass-agreement (0.879) and precision (0.855) compared to majority vote, which is the most recall-heavy (0.912) (Page 6).

Stability and Recommendation

The analysis of run-to-run variance showed that the unanimous all-three-pass rule is the best configuration on this sample on both counts: the highest mean (0.902) and the smallest spread (std 0.009) (Page 6). The paper recommends all-three-pass, with the caveat that this rule was identified post-hoc and warrants independent replication (Page 1). This configuration is favored because it offers the highest precision and the smallest run-to-run spread (Page 6).

REFERENCES

de Moura, L. and Ullrich, S. The Lean 4 theorem prover and programming language. In Automated Deduction – CADE 28, volume 12699 of Lecture Notes in Computer Science, pp. 625–635. Springer, 2021.

Dekoninck, J., Petrov, I., Minchev, K., Balunovic, M., Vechev, ´ M., Marinov, M., Drencheva, M., Konova, L., Shumanov, M., Tsvetkov, K., Drenchev, N., Todorov, L., Nikolova, K. and Ismoldayev, M. The open proof corpus: A large-scale study of LLM-generated mathematical proofs. arXiv preprint arXiv:2506.21621, 2025.

Hubert, T., Mehta, R. S., Sartran, L., Horvath, M. Z., ´ Zuˇ ziˇ c,´ G., Wieser, E., Huang, A., Schrittwieser, J., Schroecker, Y. et al. Olympiad-level formal mathematical reasoning with reinforcement learning. Nature, 2025. doi: 10.1038/s41586-025-09833-y.

Luong, T., Hwang, D., Nguyen, H. H., Ghiasi, G., Chervonyi, Y., Seo, I., Kim, J., Bingham, G., Lee, J., Mishra, S. Zhai A. Hu H. Michalewski H. Kim J. Ahn J. Bae J. Song X Trinh T H Le Q V and Jung J Towards robust mathematical reasoning. In Proceedings of the 2025 Conference on Empirical Methods in Natural Language Processing (EMNLP), pp. 35418–35442, Suzhou, China, 2025. Association for Computational Linguistics.

Ma, W., Cojocaru, A., Kolhe, N., Louie, B., Sharif, R. S., Zhang H., Zhuang V., Zaharia M. and Min S. Reliable fine-grained evaluation of natural language math proofs. In International Conference on Learning Representations (ICLR), 2026.

Naik, A., Shabadi, G., Alur, R. and Naik, M. Do we need frontier models to verify mathematical proofs? arXiv preprint arXiv:2604.02450, 2026.

Petrov, I., Dekoninck, J., Baltadzhiev, L., Drencheva, M., Minchev, K., Balunovic, M., Jovanovi c N. and Vechev M. Proof or bluff? evaluating LLMs on 2025 USA math olympiad. arXiv preprint arXiv:2503.21934, 2025.

Verga, P., Hofstatter, S., Althammer, S., Su, Y., Piktus, A., ¨ Arkhangorodsky, A., Xu, M., White N. and Lewis P. Replacing judges with juries: Evaluating LLM generations with a panel of diverse models. arXiv preprint arXiv:2404.18796, 2024.

Zheng, L., Chiang, W.-L., Sheng, Y., Zhuang, S., Wu, Z., Zhuang Y., Lin Z., Li Z., Li D., Xing E. P. Zhang H. Gonzalez J. E. and Stoica I Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena. In Advances in Neural Information Processing Systems 36 (NeurIPS), Datasets and Benchmarks Track, 2023.

A Reasoning Effort Is a Model-Specific Lever A. Reasoning Effort Is a Model-Specific Lever Because Table 1 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). Raising Gemini’s reasoning roughly fourfold left its passagreement unchanged (0.840 in both cases; a paired bootstrap finds no detectable difference, and ten individual decisions flipped but canceled out), while quadrupling its cost.

B. Pass/Fail vs. Rank Correlation B. Pass/Fail vs. Rank Correlation 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.

C.

1. Improve cost-effective proof grading by deploying an all-three-pass consensus rule across cheap models, as it reaches the highest pass-agreement and precision on the full benchmark, which is recommended as a default for production systems.

2. Enhance the reliability of budget-constrained reasoning loops by using a single model run three times under an unanimity rule, which recovers much of the multi-model consensus benefit, leading to higher agreement (e.g., GPT-OSS self-all-3 reaches 0.888).

3. Develop a decision gate that balances precision and recall by using consensus rules as a precision/recall dial on the full benchmark, allowing researchers to select between high recall (majority vote) and high precision (unanimous rules) depending on whether wrongly passing a flawed proof is more costly.

4. Create an adaptive reasoning budget for cheap models by recognizing that reasoning effort is a model-specific lever, where raising Gemini's reasoning does not change its agreement, suggesting optimization should focus on models like GPT-OSS-120B where effort significantly drives quality.