AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification

• URL: http://arxiv.org/abs/2607.11849v1
• Date: Mon, 13 Jul 2026 17:38:22 GMT
• Title: AdvancedMathBench: A Benchmark Suite for Advanced Mathematical Proof Generation and Verification
• Abstract summary: Large language models (LLMs) have achieved remarkable performance on high-school and olympiad-style mathematics.<n>Existing benchmarks fall short in both scope and evaluation granularity.<n>We introduce AdvancedMathBench, a benchmark suite designed to evaluate advanced mathematical reasoning capabilities.
• Score: 41.90353470982016
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Large language models (LLMs) have achieved remarkable performance on high-school and olympiad-style mathematics, yet their capabilities on advanced mathematics remain poorly understood. Existing benchmarks, however, fall short in both scope and evaluation granularity: they provide limited disciplinary coverage and often rely on final-answer correctness or coarse judgments, leaving the validity of the reasoning process inadequately assessed. To bridge this gap, we introduce AdvancedMathBench, a benchmark suite designed to evaluate advanced mathematical reasoning capabilities. Its core proof-generation benchmark, ProverBench, contains 296 problems spanning undergraduate and doctoral qualifying-exam levels. To provide reliable evaluation of the proofs, we develop a dedicated automatic verification pipeline trained on large-scale expert annotations to produce both correctness verdicts and fine-grained assessments of proof errors, which exhibits strong agreement with human experts on held-out proof trajectories. We further introduce VerifierBench, consisting of 888 model-generated proof trajectories paired with expert ground truth, to evaluate whether models can correctly judge proof validity and provide sound verification rationales. Experiments show that AdvancedMathBench remains challenging for frontier models. On proof generation, the best-performing model, GPT-5.5-xhigh, achieves only 75.8 and 66.1 on the UGD and QE splits, respectively, indicating substantial room for improvement on advanced mathematical proof construction. On proof verification, the best model attains a Balanced F1 of only 65.1, and models generally exhibit low true negative rates, suggesting that critical error detection remains a major bottleneck.

Related papers

• ComBench: A Benchmark for Rigorous Proof Reasoning and Constructive Realization in Olympiad-Level Combinatorics [95.15900681087088]
  We introduce ComBench, an Olympiad-level benchmark for diagnosing and the reasoning capabilities of large language models.<n>ComBench contains 100 human-annotated competition-level problems organized around two complementary settings.<n>Experiments show that the strongest model reaches 65.4% overall Avg. and 75.3% overall Best@4.
  arXiv  Detail & Related papers  (2026-06-09T06:50:15Z)
• FormalRewardBench: A Benchmark for Formal Theorem Proving Reward Models [0.0]
  We introduce textbfFormalRewardBench, the first benchmark for evaluating reward models in formal theorem proving with Lean 4.<n>Our results reveal that frontier LLMs achieve the highest performance (59.8%%) while specialized theorem provers perform the worst (24.4%)<n>We release textbfFormalRewardBench publicly to encourage more research on developing reward models in formal mathematics.
  arXiv  Detail & Related papers  (2026-05-11T07:51:15Z)
• LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches [61.30693283718321]
  We present LiveMathematicianBench, a dynamic multiple-choice benchmark for research-level mathematical reasoning.<n>By grounding evaluation in newly published theorems, it provides a realistic testbed beyond memorized patterns.<n>It employs a proof-sketchguided distractor pipeline that uses high-level proof strategies to construct plausible but invalid answer choices.
  arXiv  Detail & Related papers  (2026-04-02T08:22:17Z)
• FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified? [0.04324039930655099]
  We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs.<n>Each task pairs a natural-language problem with a Lean4 formal statement, and a model must output a Lean proof accepted by the Lean 4 checker.<n>We evaluate a range of frontier models with an agentic harness, and find that the best-performing foundation model achieves 33.5% accuracy.
  arXiv  Detail & Related papers  (2026-03-27T21:14:53Z)
• Reliable Fine-Grained Evaluation of Natural Language Math Proofs [30.992321135182905]
  We propose a systematic methodology for developing evaluators that assign fine-grained scores on a 0-7 scale to model-generated math proofs.<n>We introduce ProofBench, the first expert-annotated dataset of fine-grained proof ratings, spanning 145 problems from six major math competitions.<n>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.
  arXiv  Detail & Related papers  (2025-10-14T02:59:07Z)
• Reasoning or Memorization? Unreliable Results of Reinforcement Learning Due to Data Contamination [67.67725938962798]
  Pre-training on massive web-scale corpora leaves Qwen2.5 susceptible to data contamination in widely used benchmarks.<n>We introduce a generator that creates fully clean arithmetic problems of arbitrary length and difficulty, dubbed RandomCalculation.<n>We show that only accurate reward signals yield steady improvements that surpass the base model's performance boundary.
  arXiv  Detail & Related papers  (2025-07-14T17:55:15Z)
• Mathematical Proof as a Litmus Test: Revealing Failure Modes of Advanced Large Reasoning Models [11.250861762443801]
  We introduce the RFMDataset (Reveal Failure Modes), a collection of 200 diverse mathematical proof problems.<n>We thoroughly evaluate advanced models' performance on it.<n>Our analysis uncovers 10 fine-grained error types, which shows fundamental limitations in current large reasoning models.
  arXiv  Detail & Related papers  (2025-06-20T16:14:18Z)
• Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad [4.573289946657861]
  We evaluate reasoning models on six problems from the 2025 USAMO.<n>Only Gemini-2.5-Pro achieves a non-trivial score of 25%.<n>Our results suggest that current LLMs are inadequate for rigorous mathematical reasoning tasks.
  arXiv  Detail & Related papers  (2025-03-27T19:21:05Z)
• Lean-STaR: Learning to Interleave Thinking and Proving [53.923617816215774]
  We present Lean-STaR, a framework for training language models to produce informal thoughts prior to each step of a proof.<n>Lean-STaR achieves state-of-the-art results on the miniF2F-test benchmark within the Lean theorem proving environment.
  arXiv  Detail & Related papers  (2024-07-14T01:43:07Z)
• PRover: Proof Generation for Interpretable Reasoning over Rules [81.40404921232192]
  We propose a transformer-based model that answers binary questions over rule-bases and generates the corresponding proofs. Our model learns to predict nodes and edges corresponding to proof graphs in an efficient constrained training paradigm. We conduct experiments on synthetic, hand-authored, and human-paraphrased rule-bases to show promising results for QA and proof generation.
  arXiv  Detail & Related papers  (2020-10-06T15:47:53Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.