Skip to content
Preprint

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

Jul 2026 · 0 citations · 40 references
Computer Science

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.

View source

Similar papers

Open access Jul 2026

Empirical Analysis of Chain-of-Thought and Solver-Augmented Large Language Models for Deductive Reasoning

These results indicate that while CoT-augmented LLMs achieve strong performance on deductive reasoning tasks up to five hops, solver augmentation remains valuable for deeper multihop deduction and for applications requiring robust and verifiable reasoning.

Ya Wang, Raja Havish Seggoju, A. Paschke · 0 citations
Preprint Jul 2026

ITPEval: Benchmarking Formal Translation Across Interactive Theorem Provers

ITPEval is presented, the first benchmark for evaluating automated formal proof translation across four major ITPs (Lean 4, Rocq, Isabelle, and HOL Light), spanning two distinct logical foundations and itpeval, a unified multi-ITP verification infrastructure with state-isolated warm backends that preserve per-artifact native checking semantics.

Jiayi Wu, Robert Joseph George, Anima Anandkumar · 0 citations
Preprint Aug 2026

ClosureBench: A Constructive Benchmark for Compositional Graph Reasoning

ClosureBench is introduced, a constructive benchmark for compositional graph-relational reasoning with programmatically verified ground truth with programmatically verified ground truth: each task's reference answer is computed by executing a program in the Ein tensor-logic language, ensuring machine-verified correctness.

S. Goria · 0 citations
Jun 2026

Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics

This work introduces *Theo*, an agentic autoformalization framework powered by general coding LLMs, and successfully formalizes their main theorems and proofs and validate the generated formalizations with human experts.

Arshia Soltani Moakhar, Iman Gholami, Max Springer et al. · 2 citations
Review Jul 2026

From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontier

It is argued that the next leap in AI4Math systems requires a decisive shift from predefined problem-solvers to research agents that can address frontier mathematical challenges with rigorous formal mathematical reasoning, highlighting core limitations of existing systems in serving as mathematical research agents.

E. Jiang, Xiao Liang, Yikai Zhang et al. · 1 citation