# Reliable Fine-Grained Evaluation of Natural Language Math Proofs

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

## Key facts

- Cited by 18 papers in the map (data through 14 Oct 2026).
- Placed in Mathematical reasoning, one of 17 directions in LLM reasoning.
- Builds on 26 of its 36 references that are in the map.
- First posted on arXiv 14 Oct 2025.

## Placed in

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

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

- [Training Verifiers to Solve Math Word Problems](https://mlsanity.com/paper/2110.14168/) (2021)
- [DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Models](https://mlsanity.com/paper/2402.03300/) (2024)
- [Judging LLM-as-a-Judge with MT-Bench and Chatbot Arena](https://mlsanity.com/paper/2306.05685/) (2023)
- [Measuring Mathematical Problem Solving With the MATH Dataset](https://mlsanity.com/paper/2103.03874/) (2021)
- [Learning to summarize from human feedback](https://mlsanity.com/paper/2009.01325/) (2020)
- [OlympiadBench: A Challenging Benchmark for Promoting AGI with Olympiad-Level Bilingual Multimodal Scientific Problems](https://mlsanity.com/paper/2402.14008/) (2024)
- [Scaling Laws for Reward Model Overoptimization](https://mlsanity.com/paper/2210.10760/) (2022)
- [Prometheus: Inducing Fine-grained Evaluation Capability in Language Models](https://mlsanity.com/paper/2310.08491/) (2023)
- [From Crowdsourced Data to High-Quality Benchmarks: Arena-Hard and BenchBuilder Pipeline](https://mlsanity.com/paper/2406.11939/) (2024)
- [MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics](https://mlsanity.com/paper/2109.00110/) (2021)
- [JudgeBench: A Benchmark for Evaluating LLM-based Judges](https://mlsanity.com/paper/2410.12784/) (2024)
- [MathArena: Evaluating LLMs on Uncontaminated Math Competitions](https://mlsanity.com/paper/2505.23281/) (2025)
- [Reinforcement Learning for Reasoning in Large Language Models with One Training Example](https://mlsanity.com/paper/2504.20571/) (2025)
- [Mathematical Capabilities of ChatGPT](https://mlsanity.com/paper/2301.13867/) (2023)
- [PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition](https://mlsanity.com/paper/2407.11214/) (2024)
- [Lean Workbook: A large-scale Lean problem set formalized from natural language math problems](https://mlsanity.com/paper/2406.03847/) (2024)
- [How to Evaluate Reward Models for RLHF](https://mlsanity.com/paper/2410.14872/) (2024)
- [Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad](https://mlsanity.com/paper/2503.21934/) (2025)
- [NaturalProver: Grounded Mathematical Proof Generation with Language Models](https://mlsanity.com/paper/2205.12910/) (2022)
- [Herald: A Natural Language Annotated Lean 4 Dataset](https://mlsanity.com/paper/2410.10878/) (2024)
- [FIMO: A Challenge Formal Dataset for Automated Theorem Proving](https://mlsanity.com/paper/2309.04295/) (2023)
- [The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofs](https://mlsanity.com/paper/2506.21621/) (2025)
- [HARP: A challenging human-annotated math reasoning benchmark](https://mlsanity.com/paper/2412.08819/) (2024)
- [Solving Inequality Proofs with Large Language Models](https://mlsanity.com/paper/2506.07927/) (2025)
- [Using Natural Language Explanations to Rescale Human Judgments](https://mlsanity.com/paper/2305.14770/) (2023)
- [Temporal Consistency for LLM Reasoning Process Error Identification](https://mlsanity.com/paper/2503.14495/) (2025)

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

- [Beyond Benchmarks: MathArena as an Evaluation Platform for Mathematics with LLMs](https://mlsanity.com/paper/2605.00674/) (2026)
- [Hard2Verify: A Step-Level Verification Benchmark for Open-Ended Frontier Math](https://mlsanity.com/paper/2510.13744/) (2025)
- [Scaling Generative Verifiers For Natural Language Mathematical Proof Verification And Selection](https://mlsanity.com/paper/2511.13027/) (2025)
- [Do We Need Frontier Models to Verify Mathematical Proofs?](https://mlsanity.com/paper/2604.02450/) (2026)
- [QED-Nano: Teaching a Tiny Model to Prove Hard Theorems](https://mlsanity.com/paper/2604.04898/) (2026)
- [Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness](https://mlsanity.com/paper/2605.10379/) (2026)
- [FormalTCS: Benchmarking End-to-End Frontier Formal Theoretical Computer Science Research of Large Language Models](https://mlsanity.com/paper/2608.20153/) (2026)
- [ProofVerifier: A Scalable, Diversity-Driven Framework for Natural-Language Proof Verification](https://mlsanity.com/paper/2602.02377/) (2026)
- [Judging What We Cannot Solve: A Consequence-Based Approach for Oracle-Free Evaluation of Research-Level Math](https://mlsanity.com/paper/2602.06291/) (2026)
- [MA-ProofBench: A Two-Tiered Evaluation of LLMs for Theorem Proving in Mathematical Analysis](https://mlsanity.com/paper/2606.13782/) (2026)
- [ReasFlow: Assisting Reasoning-Centric Scientific Discovery in Applied Mathematics via a Knowledge-Based Multi-Agent System](https://mlsanity.com/paper/2607.14178/) (2026)
- [Cost-Effective Automated Judging of Natural-Language Mathematical Proofs](https://mlsanity.com/paper/2608.00004/) (2026)
- [ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics](https://mlsanity.com/paper/2606.10479/) (2026)
- [FaithSieve: Fine-Grained Evaluation of Math Proofs with Faithful Formal Evidence](https://mlsanity.com/paper/2608.26310/) (2026)
- [TCSAlgBench: Benchmarking Automated Proving for Research-Level Theoretical Computer Science](https://mlsanity.com/paper/2609.35606/) (2026)
- [Splicing Hints into Reasoning Traces: Learning from Demonstrator Failures](https://mlsanity.com/paper/2610.13996/) (2026)
- [TeachGrade: Training-Free Short Answer Scoring with Teacher Evidence](https://mlsanity.com/paper/2610.14900/) (2026)
- [One-Sided Verification Under Limited Expert Review](https://mlsanity.com/paper/2610.18089/) (2026)

## Abstract (arXiv)

Recent advances in large language models (LLMs) for mathematical reasoning have largely focused on tasks with easily verifiable final answers while generating and verifying natural language math proofs remains an open challenge. We identify the absence of a reliable, fine-grained evaluator for LLM-generated math proofs as a critical gap. To address this, we propose a systematic methodology for developing and validating evaluators that assign fine-grained scores on a 0-7 scale to model-generated math proofs. To enable this study, we introduce ProofBench, the first expert-annotated dataset of fine-grained proof ratings, spanning 145 problems from six major math competitions (USAMO, IMO, Putnam, etc) and 435 LLM-generated solutions from Gemini-2.5-Pro, o3, and DeepSeek-R1. Using ProofBench as a testbed, we systematically explore the evaluator design space across key axes: the backbone model, input context, instructions and evaluation workflow. Our analysis delivers ProofGrader, an evaluator that combines a strong reasoning backbone LM, rich context from reference solutions and marking schemes, and a simple ensembling method; it achieves a low Mean Absolute Error (MAE) of 0.926 against expert scores, significantly outperforming naive baselines. Finally, we demonstrate its practical utility in a best-of-n selection task: at n=16, ProofGrader achieves an average score of 4.14/7, closing 78% of the gap between a naive binary evaluator (2.48) and the human oracle (4.62), highlighting its potential to advance downstream proof generation.