Technical Summary: Not All Proofs Are Equal: Evaluating LLM Proof Quality Beyond Correctness

Problem Statement

While Large Language Models (LLMs) have demonstrated significant capability in generating correct mathematical proofs, current evaluation benchmarks focus almost exclusively on correctness. This singular focus overlooks critical dimensions of proof quality that are essential for mathematical utility, such as clarity, conciseness, insight, and transferability. A proof can be formally correct yet be overly verbose, rely on tedious brute-force calculations, utilize obscure techniques inaccessible to the intended audience, or fail to adapt to specific methodological constraints. Furthermore, existing benchmarks often treat all correct proofs as equally valuable, failing to capture the substantial stylistic and structural variations between them. The challenge lies in defining and measuring these subjective qualities in a scalable, automated manner without relying on expensive or inconsistent human evaluation.

Methodology: PROOFRANK

To address these gaps, the authors introduce PROOFRANK, the first benchmark designed specifically to evaluate scalable proxies of proof quality in LLM-generated mathematics. The benchmark consists of 382 challenging, final-answer competition problems spanning algebra, geometry, combinatorics, calculus, and number theory. The use of final-answer problems allows for scalable correctness verification while still requiring rigorous written proofs.

The evaluation framework relies on pairwise comparisons of correct solutions to avoid the difficulty of assigning absolute scores across diverse problems. Correctness is treated as a prerequisite; models are only compared on problems where both produce valid solutions. PROOFRANK evaluates five complementary metrics, categorized into two types:

1. Proof-Level Metrics (Comparing individual proofs)

• Conciseness: Measured via compressibility. A strong reasoning model attempts to shorten a proof while preserving logical equivalence. The metric is the ratio of the original text length to the shortened length. Lower ratios indicate higher conciseness (more redundant text removed).
• Computational Ease: Assesses the extent to which a proof relies on tedious algebra, enumeration, or case-checking. An LLM judge compares pairs of proofs to determine which requires less "time-to-follow" due to notation density and explicit computation.
• Cognitive Simplicity: Measures the accessibility of the proof techniques used. It evaluates the complexity of the core ideas, the sophistication of the tools (e.g., niche theorems vs. standard methods), and the difficulty of integrating multiple concepts.

2. Problem-Level Metrics (Comparing model behavior across multiple attempts)

• Diversity: Quantifies a model's ability to produce distinct valid approaches to the same problem. Solutions are clustered by technique (using LLM-generated summaries), and diversity is measured by the entropy of the model's distribution over these clusters.
• Adaptivity: Evaluates whether a model can produce a correct proof while adhering to a specified technique requested in the prompt. This tests the model's ability to follow constraints and explore specific mathematical pathways.

Ranking System: Pairwise outcomes are aggregated into model-level ratings using a Bradley-Terry model, producing Elo-style scores. This approach mitigates biases inherent in absolute scoring and handles incomplete comparison graphs where models do not solve every problem.

Key Contributions

1. Scalable Proof-Style Metrics: The authors define and implement a suite of five metrics (conciseness, computational ease, cognitive simplicity, diversity, adaptivity) that serve as concrete, measurable proxies for subjective proof quality.
2. PROOFRANK Benchmark: The introduction of a comprehensive benchmark comprising 382 competition-level problems, curated to evaluate LLMs beyond mere correctness.
3. Empirical Evaluation of Frontier Models: A systematic evaluation of 10 state-of-the-art models (including GPT-5.4, Gemini-3.1-Pro, Kimi-K2.5, etc.), revealing distinct strengths and weaknesses that are invisible to correctness-only benchmarks.

Experimental Results

The evaluation reveals substantial differences in proof quality across models that are not captured by accuracy alone:

• GPT-5.4 Dominance: GPT-5.4 leads the benchmark, achieving the highest accuracy (86.4%) and top performance on three of the five quality metrics (Computational Ease, Cognitive Simplicity, and Adaptivity).
• Trade-offs and Divergence: There is a low correlation between accuracy and quality metrics. For instance, GLM-5 achieves reasonable accuracy (49.1%) but performs below average on all quality metrics. Conversely, QWEN3.5-397B scores highly on Computational Ease (avoiding brute-force methods) but has the lowest accuracy among evaluated models, highlighting a trade-off between elegance and correctness.
• Model-Specific Weaknesses: GEMINI-3.1-PRO performs particularly poorly on conciseness, with solutions averaging 3.5 times more verbose than necessary. KIMI-K2.5-THINK is the most concise model but ranks lowest in Cognitive Simplicity.
• Prompting Effects: Experiments show that conciseness is partially controllable via prompting. However, forcing conciseness often leads to significant drops in accuracy (e.g., ~15% drop for Kimi and DeepSeek), suggesting that style optimization is not a "free" improvement and requires careful balancing.
• Correctness Filtering Necessity: When correctness filtering is removed, rankings shift dramatically. Models that produce simple but incorrect arguments (e.g., STEP-3.5-FLASH) artificially inflate their quality scores, underscoring that quality evaluation must be predicated on correctness.

Significance and Claims

The paper claims that PROOFRANK provides a necessary expansion of the evaluation landscape for mathematical reasoning in LLMs. By moving beyond binary correctness, the benchmark reveals that models possess distinct "proof personalities"—some are rigorous but verbose, others are elegant but prone to error, and some are adaptable while others are rigid.

The authors argue that these findings are critical for practical applications:

• Educational and Research Utility: In educational settings, a proof's clarity and insight are as important as its correctness. In research, the ability to generate diverse or adaptable proofs can aid in exploring new mathematical avenues.
• Model Selection: The non-trivial trade-offs between accuracy and quality metrics suggest that users should select models based on specific needs (e.g., prioritizing computational ease for verification or diversity for brainstorming) rather than relying solely on accuracy scores.
• Future Directions: The work suggests that future evaluations of mathematical reasoning must measure the usefulness of generated proofs, acknowledging that a correct proof is not inherently a good proof if it fails to communicate insight or transfer to other contexts.

The paper remains modest regarding its limitations, acknowledging that proof quality is inherently subjective and that their metrics are proxies rather than absolute measures. It relies on LLM judges, which introduces potential biases, though extensive validation experiments suggest these proxies are robust and align reasonably well with human judgments on specific dimensions like computational ease and cognitive simplicity.