# Cost-Effective Automated Judging of Natural-Language Mathematical Proofs

arXiv: https://arxiv.org/abs/2608.00004 · HTML: https://mlsanity.com/paper/2608.00004/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 7 of its 15 references that are in the map.
- First posted on arXiv 29 May 2026.

## Placed in

- LLM reasoning / [Mathematical reasoning](https://mlsanity.com/lr/mathematical-reasoning/)

## Builds on (most cited first, 7 of 7)

- [A Survey on LLM-as-a-Judge](https://mlsanity.com/paper/2411.15594/) (2024)
- [Replacing Judges with Juries: Evaluating LLM Generations with a Panel of Diverse Models](https://mlsanity.com/paper/2404.18796/) (2024)
- [Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad](https://mlsanity.com/paper/2503.21934/) (2025)
- [Towards Robust Mathematical Reasoning](https://mlsanity.com/paper/2511.01846/) (2025)
- [The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs](https://mlsanity.com/paper/2506.21621/) (2025)
- [Reliable Fine-Grained Evaluation of Natural Language Math Proofs](https://mlsanity.com/paper/2510.13888/) (2025)
- [Do We Need Frontier Models to Verify Mathematical Proofs?](https://mlsanity.com/paper/2604.02450/) (2026)

## Built on by (most cited first, 1 of 1)

- [RAIM: Robust Aggregation of Inexpensive Models for Hallucination Detection](https://mlsanity.com/paper/2609.39229/) (2026)

## Abstract (arXiv)

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× 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.