Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness
Not on the map. Why?
Abstract (arXiv)
Large language models (LLMs) have become capable mathematical problem-solvers, often producing correct proofs for challenging problems. However, correctness alone is not sufficient: mathematical proofs should also be clear, concise, insightful, and transferable to other problems. While this proof quality is subjective and depends on the reader and context, many of its components are concrete and broadly valued. In this work, we identify such components and introduce ProofRank, a benchmark curated from challenging mathematical competitions. ProofRank evaluates several scalable proxies of proof quality: (i) conciseness, measuring whether proofs avoid unnecessary steps; (ii) computational ease, measuring the extent to which a proof relies on tedious calculations; (iii) cognitive simplicity, measuring how accessible the used proof techniques are; (iv) diversity, measuring how varied a model's proofs for a single problem are; and (v) adaptivity, measuring whether a model can follow a specified proof technique. Across models, we find substantial differences in proof quality that are not captured by correctness-only benchmarks. We also observe significant trade-offs between proof-quality metrics and correctness, suggesting that future evaluations of mathematical reasoning should measure how useful LLM-generated proofs are.
Key facts. Cited by 3 papers in the map (data through 14 Oct 2026). Builds on 44 of its 55 references that are in the map. First posted on arXiv 11 May 2026.
Builds on
44 of 55 references.
References · 44
- 2023Judging LLM-as-a-Judge with MT-Bench and Chatbot Arenacited by 8,626
- 2025gpt-oss-120b & gpt-oss-20b Model Cardcited by 1,386
- 2025DeepSeek-V3.2: Pushing the Frontier of Open Large Language Modelscited by 815
- 2026GLM-5: from Vibe Coding to Agentic Engineeringcited by 587
- 2026Kimi K2.5: Visual Agentic Intelligencecited by 501
- 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 391
- 2024Justice or Prejudice? Quantifying Biases in LLM-as-a-Judgecited by 368
- 2025MathArena: Evaluating LLMs on Uncontaminated Math Competitionscited by 297
- 2024Judging the Judges: A Systematic Study of Position Bias in LLM-as-a-Judgecited by 269
- 2023Mathematical Capabilities of ChatGPTcited by 268
- 2024Self-Preference Bias in LLM-as-a-Judgecited by 258
- 2024WildBench: Benchmarking LLMs with Challenging Tasks from Real Users in the Wildcited by 218
32 more
- 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 192
- 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 165
- 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 154
- 2025AbstentionBench: Reasoning LLMs Fail on Unanswerable Questionscited by 145
- 2023Verbosity Bias in Preference Labeling by Large Language Modelscited by 91
- 2025Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiadcited by 74
- 2025Towards Robust Mathematical Reasoningcited by 73
- 2023Evaluating Language Models for Mathematics through Interactionscited by 70
- 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 60
- 2026Step 3.5 Flash: Open Frontier-Level Intelligence with 11B Active Parameterscited by 36
- 2025The Open Proof Corpus: A Large-Scale Study of LLM-Generated Mathematical Proofscited by 30
- 2025BrokenMath: A Benchmark for Sycophancy in Theorem Proving with LLMscited by 27
- 2025FATE: A Formal Benchmark Series for Frontier Algebra of Multiple Difficulty Levelscited by 27
- 2025Brains vs. Bytes: Evaluating LLM Proficiency in Olympiad Mathematicscited by 24
- 2025Hard2Verify: A Step-Level Verification Benchmark for Open-Ended Frontier Mathcited by 22
- 2025Solving Inequality Proofs with Large Language Modelscited by 21
- 2025Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Modelscited by 20
- 2025Reliable Fine-Grained Evaluation of Natural Language Math Proofscited by 18
- 2025IMProofBench: Benchmarking AI on Research-Level Mathematical Proof Generationcited by 13
- 2025ProofOptimizer: Training Language Models to Simplify Proofs without Human Demonstrationscited by 11
- 2026Self-Preference Bias in Rubric-Based Evaluation of Large Language Modelscited by 11
- 2026LemmaBench: A Live, Research-Level Benchmark to Evaluate LLM Capabilities in Mathematicscited by 10
- 2025ReliableMath: Benchmark of Reliable Mathematical Reasoning on Large Language Modelscited by 8
- 2026SorryDB: Can AI Provers Complete Real-World Lean Theorems?cited by 8
- 2026TaoBench: Do Automated Theorem Prover LLMs Generalize Beyond MathLib?cited by 6
- 2024Lattice-Valued Bottleneck Dualitycited by 5
- 2026Interactive Benchmarkscited by 5
- 2026FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?cited by 5
- 2025RefGrader: Automated Grading of Mathematical Competition Proofs using Agentic Workflowscited by 4
- 2026QEDBENCH: Quantifying the Alignment Gap in Automated Evaluation of University-Level Mathematical Proofscited by 4
- 2025From Euler to AI: Unifying Formulas for Mathematical Constantscited by 2
- 2025Putnam-like dataset summary: LLMs as mathematical competition contestantscited by 2
Built on by
Citing papers per year: 2026: 3.
3 papers.
- 2026Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalizationcited by 4
- 2026SABER-Math: Automated Benchmark for Information Retrieval Evaluation in Mathematicscited by 1
- 2026AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verificationcited by 0
- 2026AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification13 Jul 2026
- 2026SABER-Math: Automated Benchmark for Information Retrieval Evaluation in Mathematics29 Jun 2026
- 2026Sorries Are Not the Hard Part: An Expert-Review Case Study of a Semi-Autonomous Formalization11 Jun 2026
Similar, not cited
Close in wording, no citation either way
- 2025RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematics
- 2026Mask-Proof: An LLM-based Automated Data Curation Pipeline on Mathematical Proofs
- 2025ProofCompass: Enhancing Specialized Provers with LLM Guidance
- 2026Evaluating Research-Level Math Proofs via Strict Step-Level Verification
- 2025Putnam-AXIOM: A Functional and Static Benchmark for Measuring Higher Level Mathematical Reasoning in LLMs
- 2024Not All Votes Count! Programs as Verifiers Improve Self-Consistency of Language Models for Math Reasoning
- 2026Do We Need Frontier Models to Verify Mathematical Proofs?
- 2026ALPS: Measuring Valid Creativity in Large Language Models with Mathematical Construction