PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Lingkai Kong, Zijian Wu, Yuzhe Gu, Haiteng Zhao, Wenyong Huang, Shuang Sun, Zhicheng Xiong, Xiaotian Zhang, Shuya Zhao, Yan Wang, Disheng Xu, Wenwei Zhang, Kai Chen

arXiv:2607.11849v1cs.CL

TL;DR

Advanced mathematical proof capabilities of language models remain poorly understood because answer-centric benchmarks inadequately assess rigorous reasoning. AdvancedMathBench evaluates proof generation and verification, finding that frontier models still struggle substantially with both tasks.

  • Problem

    Existing mathematics benchmarks provide limited evidence about advanced proof reasoning because they emphasize final answers or coarse judgments over rigorous intermediate claims.

  • Method

    AdvancedMathBench combines curated proof-generation and proof-verification benchmarks with automatic, expert-annotated assessment of correctness, errors, and verification rationales.

  • Results

    Frontier models struggle on both tasks: GPT-5.5-xhigh scores 64.5 on UG and 48.9 on QE, while DeepSeek-V4-Pro reaches 65.1 Meta-Verification Balanced F1.

  • Takeaways & Limitations

    Advanced proof evaluation should assess complete reasoning and error detection, since models often over-accept plausible but invalid proofs.

Abstract

from arXiv · show

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.

1. Introduction

AdvancedMathBench addresses gaps in advanced-mathematics evaluation by testing both natural-language proof generation and proof-trajectory verification. Its results show that frontier models still struggle, particularly with harder qualifying-exam-level proofs.

  • Motivation: Advanced mathematics remains less understood for LLMs because it requires rigorous intermediate claims rather than only final-answer prediction.Mathematical proof offers a natural stress test for evaluating whether models can construct rigorous reasoning trajectories.
  • Motivation: Existing benchmarks have limited advanced-mathematics coverage and often rely on final-answer checking or coarse solution matching that cannot establish proof validity.Coverage remains limited across undergraduate, graduate, and research-level mathematics.
  • Benchmark design: AdvancedMathBench evaluates complementary capabilities through ProverBench for proof generation and VerifierBench for proof verification.The suite focuses on constructing complete natural-language proofs and assessing the validity of proof trajectories.
  • Results: 64.5 on the UG split and 48.9 on the more challenging QE split were achieved by GPT-5.5-xhigh on ProverBench.Several other frontier models exhibit substantially larger drops when moving to QE-level proofs.

2. Related Work

Prior mathematical benchmarks have progressed from arithmetic and competition problems toward university- and expert-level reasoning, while proof and process-verification research has emphasized complete arguments and step-level reliability. AdvancedMathBench extends these directions to advanced natural-language proofs by evaluating validity judgments, error detection, and rationale agreement with experts.

  • Mathematical Reasoning Benchmarks: Mathematical benchmarks have expanded from arithmetic word problems and competition mathematics to university-level and expert-level problem solving.GSM8K and MATH established multi-step reasoning testbeds, while OlympiadBench and Omni-MATH increased difficulty through olympiad-level coverage.
  • Natural-Language Proof: Natural-language proof generation requires logically sufficient, conceptually coherent, and checkable arguments rather than merely correct answers.NaturalProofs and NaturalProver studied corpora, retrieval, proof completion, and grounded proof generation, highlighting the need to retrieve, cite, and organize mathematical knowledge.
  • Process Verification: Process verification evaluates intermediate reasoning reliability instead of only final-answer correctness.PRM800K introduced step-level human feedback, while ProcessBench, OPV-Bench, and Hard2Verify framed evaluation around error-step identification or first-error localization.
  • Process Verification: AdvancedMathBench applies process verification to advanced natural-language proofs by requiring binary validity judgments and verification rationales.Its evaluation measures rationale agreement with expert judgment through a meta-verifier, testing rejection of invalid proofs, identification of critical gaps, and reliable verification analysis.

3. AdvancedMathBench

AdvancedMathBench evaluates advanced proof generation and verification through process-level assessment, using a multi-stage curation pipeline to retain substantive proof tasks and expert-reviewed trajectories. It comprises ProverBench for complete natural-language proof generation and VerifierBench for validity judgments, rationales, and error localization.

  • Benchmark construction: A multi-stage curation pipeline combines broad mathematical sourcing, structured parsing, task filtering, uncertainty-based difficulty screening, and expert quality control.The pipeline removes answer-centric, noisy, ambiguous, contaminated, overly simple, and ill-posed samples while retaining proof-based reasoning tasks.
  • Benchmark construction: Problems are sourced from undergraduate examinations, doctoral qualifying examinations, mathematics contests, and textbook exercises across multiple mathematical sub-disciplines.These sources target undergraduate curricula, advanced qualifying-exam reasoning, contest proof techniques, and textbook-based conceptual breadth.
  • Benchmark construction: Verifier uncertainty is defined as the entropy of repeated verification outcomes and is used to identify challenging problems and plausible but error-prone proof trajectories.Several top-tier LLMs generate trajectories, while Intern-S2-Preview-35B independently verifies each trajectory multiple times.
  • ProverBench: 200 UG problems cover core undergraduate subjects, while 45 QE problems emphasize more advanced qualifying-exam-level topics in ProverBench.Models must produce complete step-by-step natural-language proofs, which are evaluated by an expert-aligned automatic verification pipeline rather than reference-solution template matching.
  • VerifierBench: 888 problem-proof-ground-truth triples comprise VerifierBench, where models judge validity, explain their judgments, and localize proof errors.Expert annotation uses full-chain analysis rather than first-error-only labeling because later substantive failures can determine global proof validity.

4. Automatic Verification Pipeline

The pipeline provides expert-aligned, process-level verification for diverse model-generated proofs, using augmented and repaired trajectories, expert-guided training, and pessimistic multi-pass aggregation. On 94 held-out examples, it achieves a Rough F1 of 82.1, exceeding GPT-5.5-xhigh’s 70.6 baseline.

  • Pipeline design: The expert-aligned pipeline evaluates diverse model-generated proofs at scale, including proofs that deviate from reference solutions.It is designed for rigorous process-level verification rather than only reference-solution matching.
  • Training data: Additional LLM-generated and iteratively revised trajectories are selected with verifier uncertainty and expert annotation to create informative training cases.The trajectory pool includes outputs from GPT-5.5 and DeepSeek-V4-Pro, alongside the original benchmark labels.
  • Training data: Proof repair augments positive examples to counter the negative-example skew of high-risk annotations and reduce rejection bias.Expert correction suggestions guide models to revise erroneous proofs before the repaired proofs are verified.
  • Verifier training: The verifier is trained with GRPO from Intern-S2-Preview-35B, using a meta-verifier reward based on agreement with expert ground truth.Rewards are 1.0 for EXACT_MATCH, 0.5 for BASIC_MATCH, 0.25 for POOR_MATCH, and 0 for WRONG_POLARITY.
  • Evaluation: 82.1 Rough F1 is achieved on 94 held-out examples, exceeding the GPT-5.5-xhigh baseline of 70.6.The pipeline uses pessimistic verification with 8 parallel passes, accepting a proof only when all 8 passes judge it correct.

5. Experiments and Results

Experiments show that advanced proof generation is difficult, especially on doctoral-level QE problems, while proof verification is limited by over-acceptance of invalid arguments. The proposed verification pipeline improves expert-aligned performance, with reward design and positive-sample augmentation producing substantial gains.

  • ProverBench: GPT-5.5-xhigh leads ProverBench with 64.5 on UG and 48.9 on QE, while performance is substantially lower than on HMMT and USAMO.The results indicate that advanced proof generation remains challenging and that answer-centric or competition-style benchmarks may expose fewer weaknesses.
  • ProverBench: QE performance falls sharply across models, including Claude-Opus-4.8 from 59.0 to 40.0, Gemini-3.1-Pro-Preview from 46.5 to 17.8, and Kimi-K2.6 from 48.0 to 20.0.DeepSeek-V4-Pro is more stable, reaching 40.0 on QE and matching Claude-Opus-4.8 despite lower UG performance.
  • VerifierBench: Moving from Rough to Meta-Verification lowers average TNR by 12.3 and average Balanced F1 by 9.0, showing that validity polarity alone overestimates verification ability.GPT-5.5-high drops from 76.0 to 63.6 Balanced F1, while GLM-5.2 drops from 73.9 to 63.3.
  • VerifierBench: Models more often accept valid proofs than reject invalid ones, with gpt-oss-120b and Intern-S2-Preview-35B exceeding 95 Meta-Verification TPR but reaching only 32.0 and 30.7 TNR.Claude-Opus-4.8 similarly reaches 93.8 TPR but only 35.0 TNR, highlighting invalid-proof rejection as the main bottleneck.
  • Verification Pipeline: The final verification pipeline achieves 82.1 Rough Balanced F1 and 73.9 Meta-Verification Balanced F1, outperforming GPT-5.5-xhigh at 70.6/61.6 and DeepSeek-V4-Pro at 69.9/63.0.Meta-Ver-RL raises Rough Balanced F1 from 66.4 to 69.0 and Meta-Verification Balanced F1 from 59.5 to 62.6; positive-sample augmentation raises Meta-Ver TPR from 56.8 to 81.4 and Meta-Ver Balanced F1 from 60.5 to 72.2.

6. Conclusion

AdvancedMathBench evaluates advanced proof generation and verification at the process level, showing that frontier LLMs remain far from saturating advanced mathematical reasoning. It also exposes over-acceptance of plausible but invalid proofs and motivates expert-aligned, rationale-aware verification.

  • Conclusion: AdvancedMathBench evaluates advanced mathematical proof generation and verification under process-level assessment, rather than relying only on plausible conclusions.Its findings emphasize that proof judgment should withstand expert-aligned verification.
  • Conclusion: Current models tend to over-accept plausible but invalid proofs, so binary validity judgments can overestimate verification quality.Ignoring rationales and error localization contributes to this overestimation.
  • Conclusion: The automatic verification pipeline combines expert annotations, rationale-aware rewards, positive proof repair, and pessimistic verification to provide a scalable judge for generated proofs.The pipeline is presented as a response to verification failures that binary judgments alone do not capture.

A. Benchmark Details · A.1. Subject Distributions · A.2. ProverBench Examples

The benchmark-details section includes subject distributions for ProverBench’s UG and QE splits, with percentages computed within each split, and gives a proof example involving the condition AB = 0.

  • A.1. Subject Distributions: ProverBench reports subject distributions separately for its UG and QE splits.The distributions are presented in Table 4.
  • A.1. Subject Distributions: The percentages in the subject-distribution table are computed within each split.This normalization applies to both the UG and QE splits.
  • A. Benchmark Details: The benchmark-details block includes a dedicated subsection on subject distributions.This subsection is identified as A.1. Subject Distributions.
  • A.2. ProverBench Examples: One ProverBench example states that AB = 0 if and only if tr(AB) = 0.The example presents an equivalence between a matrix-product condition and its trace condition.
  • A.2. ProverBench Examples: The example is formulated as a necessary-and-sufficient condition.Its “if and only if” structure links the two displayed conditions.

A.3. VerifierBench Example · B. Prompts

The VerifierBench example illustrates how a proof can contain a fatal global-minimization gap alongside a recoverable local sign issue. Its meta-verification prompt then evaluates verifier outputs strictly against human ground truth using structured error matching, false-positive analysis, and graded XML feedback.

  • A.3. VerifierBench Example: The example asks to formulate a variational proof that circles minimize perimeter among smooth simple closed curves enclosing fixed area.The setup introduces a curve C, bounded interior Ω, fixed area A, and perimeter L.
  • A.3. VerifierBench Example: The proof parametrizes the curve regularly and uses arc-length tangent and Frenet formulas to conclude that stationary curves have constant curvature.The method proceeds through a smooth 2π-periodic parametrization, perimeter functional, unit tangent, and signed curvature.
  • A.3. VerifierBench Example: The conclusion claims that Lagrange multipliers force a minimizer to have constant curvature and therefore be a circle achieving perimeter 2√πA₀.It also states equality in the isoperimetric inequality holds only for circles up to rigid motions.
  • A.3. VerifierBench Example: The reviewer identifies Step 9 as a fatal error because the proof assumes a stationary point is a global minimum without first proving existence of a global minimizer.Step 5 is labeled recoverable because of a minor normal-vector and curvature sign-convention mismatch.
  • B.3. Meta-Verification Prompt: The meta-verification prompt compares a verifier’s XML output with human ground truth, using the problem, optional reference solution, structured proof, verification output, and GT labels.It explicitly instructs the evaluator not to re-grade the proof independently.
  • B.3. Meta-Verification Prompt: The prompt infers the verifier’s overall status primarily from whether <errors> is empty, while <assessment> explains identified issues and <reviewer_comment> supplies the oracle’s substantive reasoning.A fatal error breaks global correctness, whereas recoverable errors are local, minor, and fixable.
  • B.3. Meta-Verification Prompt: A verifier issue matches GT only when its step, reason, and grounding align with the labeled proof error; unmatched or unsupported claims are false positives, and omitted or mislocated issues are misses.Exact wording is unnecessary, but the underlying issue must materially match GT.
  • B.3. Meta-Verification Prompt: The evaluator assigns EXACT_MATCH, BASIC_MATCH, POOR_MATCH, or WRONG_POLARITY based on fatal-error detection, recoverable-error completeness, false positives, and overall alignment with GT.When a fatal error exists, only recoverable errors before the first fatal error affect completeness; the required output is well-formed XML with explicit step indices.

B.1. Proof Generation Prompt … C.2. Annotation Principles

The benchmark uses tightly specified prompts for generating detailed mathematical proofs and verifying their correctness, rigor, and errors. Annotation likewise prioritizes independent mathematical judgment of complete proofs, including validity, constraints, and sufficient justification.

  • B.1. Proof Generation Prompt: Proof-generation prompts require fully documented proofs rather than outlines, with every step carefully explained.They warn that insufficient explanation lowers the grade.
  • B.1. Proof Generation Prompt: Proof-generation instructions require self-contained reasoning, explicit computation steps, and disclosure of uncertainty instead of unsupported claims.General results are allowed only when they are sufficiently well-known; advanced unpublished results can receive zero credit.
  • B.1. Proof Generation Prompt: Proof outputs must use step tags, return only the proof, and follow prescribed mathematical formatting conventions.The formatting instructions specify LaTeX delimiters, prohibit Unicode characters, and require boxed final answers when applicable.
  • B.2. Proof Verification Prompt: Verification prioritizes mathematical validity and problem constraints, using a reference solution as an anchor for sufficiency rather than as the only valid approach.Alternative valid methods, reordered steps, different lemmas, and correct shortcuts should not be penalized unless forbidden.
  • B.2. Proof Verification Prompt: Verifiers must identify errors and unjustified leaps, assess correctness and rigor in detail, and classify proofs as fully correct, partially correct, or incorrect.Claims are accepted only when adequately justified, with under-justified but plausible steps judged conservatively.
  • B.2. Proof Verification Prompt: Verifier outputs require well-formed XML containing a detailed assessment, specific errors, and the earliest erroneous or unjustified step.The first-error-step field is set to -1 when no error exists and is otherwise the index of the earliest problem.
  • C.1. Annotation Interface: Annotation instances provide problems, optional official solutions, model proofs, and auxiliary verification traces, but annotators must rely on their own mathematical judgment.Annotators judge the full proof rather than only its final conclusion, applying validity, constraint-respect, and logical-completeness principles.

C.3. Error Categories

The benchmark classifies proof failures into fatal and recoverable errors based on whether they invalidate the global reasoning chain or can be repaired locally. Uncertain cases are flagged for discussion and adjudication.

  • Error Categories: Fatal errors invalidate the global reasoning chain or prevent the proof from establishing its conclusion.Examples include invalid theorem applications, essential unjustified implications, proving only one direction of an equivalence, and treating necessary conditions as sufficient.
  • Error Categories: Recoverable errors are local issues repairable through a minor correction or additional justification.
  • Error Categories: Uncertain error classifications are flagged for further discussion and adjudication.

C.4. Annotation Fields · C.5. Label Semantics

The annotation protocol records proof-trajectory fields using zero-based step indices and combines fatal and recoverable error labels to determine proof validity. It supports both global validity judgments and fine-grained verification of local mathematical issues.

  • C.4. Annotation Fields: Annotators complete the protocol fields for each proof trajectory, with all step indices referring to zero-based model-generated proof positions.
  • C.5. Label Semantics: The expert label is determined jointly by the fatal-error and recoverable-error annotations.
  • C.5. Label Semantics: A proof is fully correct only when First Fatal Error Step is −1 and Recoverable Error Steps is also −1.
  • C.5. Label Semantics: Any fatal error makes the proof invalid regardless of whether later steps are correct.
  • C.5. Label Semantics: Recoverable errors mark local defects that belong in the reviewer comment and meta-verification target but do not necessarily invalidate the global proof.
  • C.5. Label Semantics: The first fatal error marks where global validity is lost, whereas recoverable-error steps identify local issues before that fatal cutoff.
  • C.5. Label Semantics: The protocol enables coarse validity evaluation alongside fine-grained meta-verification of proof errors.
  • C.5. Label Semantics: Reviewer comments explain the mathematical issue, allowing verifier evaluation to assess semantic error identification rather than only error-polarity prediction.
Loading 2607.11849v1…