PaperlayerView exact revision on arXiv

Source-linked AI summary

LiveMathematicianBench: A Live Benchmark for Mathematician-Level Reasoning with Proof Sketches

Linyang He, Qiyao Yu, Hanze Dong, Baohao Liao, Xinxing Xu, Micah Goldblum, Jiang Bian, Nima Mesgarani

arXiv:2604.01754v1cs.CLcs.AIcs.LG

TL;DR

Existing mathematics benchmarks are limited by synthetic or historically sourced tasks and contamination, motivating more realistic evaluation of research-level reasoning. LiveMathematicianBench builds a dynamic post-cutoff arXiv benchmark with logical taxonomy and proof-aware question design; results show substantial model difficulty, sharper declines under substitution-resistant evaluation, and gains from proof-sketch access.

  • Problem

    Existing mathematics benchmarks are often synthetic, competition-based, historically sourced, or vulnerable to contamination, limiting evidence about research-level mathematical reasoning.

  • Method

    LiveMathematicianBench uses post-cutoff arXiv theorems, a thirteen-category logical taxonomy, proof-sketch-guided distractors, and dual-mode evaluation.

  • Results

    Gemini-3.1-pro-preview achieves the highest aggregate accuracy, while category-level performance varies across logical forms and substitution-resistant questions produce substantially lower scores.

  • Takeaways & Limitations

    The benchmark provides a diagnostic, less contamination-prone testbed for tracking structure-specific strengths, weaknesses, and use of proof-level guidance in research-level reasoning.

Abstract

from arXiv · show

Mathematical reasoning is a hallmark of human intelligence, and whether large language models (LLMs) can meaningfully perform it remains a central question in artificial intelligence and cognitive science. As LLMs are increasingly integrated into scientific workflows, rigorous evaluation of their mathematical capabilities becomes a practical necessity. Existing benchmarks are limited by synthetic settings and data contamination. We present LiveMathematicianBench, a dynamic multiple-choice benchmark for research-level mathematical reasoning built from recent arXiv papers published after model training cutoffs. By grounding evaluation in newly published theorems, it provides a realistic testbed beyond memorized patterns. The benchmark introduces a thirteen-category logical taxonomy of theorem types (e.g., implication, equivalence, existence, uniqueness), enabling fine-grained evaluation across reasoning forms. It employs a proof-sketch-guided distractor pipeline that uses high-level proof strategies to construct plausible but invalid answer choices reflecting misleading proof directions, increasing sensitivity to genuine understanding over surface-level matching. We also introduce a substitution-resistant mechanism to distinguish answer recognition from substantive reasoning. Evaluation shows the benchmark is far from saturated: Gemini-3.1-pro-preview, the best model, achieves only 43.5%. Under substitution-resistant evaluation, accuracy drops sharply: GPT-5.4 scores highest at 30.6%, while Gemini-3.1-pro-preview falls to 17.6%, below the 20% random baseline. A dual-mode protocol reveals that proof-sketch access yields consistent accuracy gains, suggesting models can leverage high-level proof strategies for reasoning. Overall, LiveMathematicianBench offers a scalable, contamination-resistant testbed for studying research-level mathematical reasoning in LLMs.

1 Introduction

Existing mathematics benchmarks are often synthetic, competition-oriented, historically sourced, or vulnerable to contamination, limiting their assessment of research-level reasoning. LiveMathematicianBench addresses this gap with post-cutoff research theorems, a thirteen-type logical taxonomy, and proof-sketch-guided evaluation.

  • Motivation: Existing benchmarks often emphasize calculation-heavy competition problems rather than open-ended reasoning through abstractions, hypotheses, and conceptual frameworks.This mismatch limits their representation of authentic mathematical research.
  • Motivation: Data contamination can inflate benchmark scores by enabling memorization of solution templates instead of first-principles derivation.Performance may drop when questions are rephrased or numerical values change.
  • Benchmark design: LiveMathematicianBench uses dynamically sourced post-cutoff arXiv theorems to evaluate research-level mathematical reasoning with reduced contamination risk.The benchmark is designed to expand evaluation beyond statement-level recognition toward strategy-level reasoning.
  • Benchmark design: Its thirteen-category taxonomy covers logical structure, qualitative analysis, and generalization, including equivalence, implication, inequalities, asymptotic bounds, universal quantifiers, and bijections.Questions are tailored to the underlying logical form.
  • Benchmark design: Proof sketches expose high-level proof structure for targeted question construction and dual-mode evaluation with or without strategic guidance.This design probes structural understanding rather than theorem retrieval alone.

2 Methods

The benchmark pipeline converts arXiv papers into calibrated research-level multiple-choice questions through theorem extraction, logical classification, proof-sketch use, and adversarial distractor design. It also adds substitution-resistant items to require reasoning beyond mechanical option checking.

  • Pipeline: The seven-stage pipeline retrieves papers, extracts LATEX, extracts and classifies theorems, generates questions, filters trivial stems, calibrates hardness, and evaluates models.Human validation is performed at every stage.
  • Pipeline: Papers are retrieved from target-month math.* submissions published strictly after a model’s training cutoff to reduce contamination risk.The retrieval process records paper identifiers, links, and titles.
  • Theorem processing: Theorem processing combines rule-based extraction with an agentic fallback, then normalizes LATEX and resolves references into a self-contained theorem representation.The rule-based path prioritizes primary theorem environments, while the fallback handles unconventional formatting.
  • Question construction: Proof sketches are generated for each theorem to guide adversarial distractor generation and enable sketch-aware evaluation.The sketches capture high-level strategy without full formal detail.
  • Question construction: Thirteen logical categories drive tailored question stems that isolate features such as quantifier scope, sharp bounds, dependence, existence versus uniqueness, and asymptotic regime.The generator defines paper-specific objects or notation inline to keep questions self-contained.
  • Question construction: Distractors are generated from proof-sensitive failure modes including controlled perturbation, semantic weakening, semantic strengthening, and property confusion.An adversarial revision pass removes options that can be rejected through surface-level cues.
  • Substitution-resistant design: Substitution-resistant items replace the correct option with a meta-option requiring identification of a valid distractor and determination that a strictly stronger result holds.This adds a deductive step beyond mechanical substitution or elimination.

3 Benchmark

The hard split contains 177 theorems spanning diverse logical structures, with implication and universal statements most common, followed by existence and inequality/bound problems. Category composition changes across months while retaining diversity.

  • Hard-split composition: 177 theorems comprise the hard split, and individual theorems may receive multiple logical-category labels.Counts therefore represent category memberships rather than unique questions.
  • Hard-split composition: Implication and universal statements are the most common categories, followed by existence and inequality/bound problems.The distribution indicates broad coverage rather than concentration on one theorem template.
  • Hard-split composition: Monthly benchmark composition changes from November 2025 through February 2026 while preserving category diversity.The month-level breakdown tracks category memberships over time.

4 Evaluation Results

Evaluation shows that LiveMathematicianBench remains difficult for frontier models, with substantial variation across logical categories and sharp sensitivity to answer-choice design. Proof-sketch access consistently improves accuracy.

  • Overall performance: 43.5% overall accuracy is the best result, achieved by Gemini-3.1-pro-preview, while GPT-5.4 (high) reaches 41.8%.The strongest systems remain far from saturation.
  • Category-wise and monthly variation: Model strengths vary by logical form: Gemini-3.1-pro-preview is particularly competitive on equivalence and classification/bijection, whereas GPT-5.4 variants are stronger on implication, universal, and inequality/bound items.Monthly performance is also unstable across benchmark slices.
  • Substitution-resistant evaluation: Substitution-resistant accuracy falls below original-choice accuracy across all evaluated systems, with Gemini-3.1-pro-preview dropping from 67.4% to 17.6%.The 17.6% result is below the 20% random-guess baseline, whereas GPT-5.4 retains 29.4%–30.6% on the substitution-resistant subset.
  • Proof-sketch access: 11.9 percentage points and 13.6 percentage points are the gains for GPT-5.4 (high) and Gemini-3.1-pro-preview (high), respectively, when proof sketches are provided.GPT-5.4 (high) rises from 41.8% to 53.7%, while Gemini-3.1-pro-preview (high) rises from 43.5% to 57.1%.
  • Proof-sketch access: Proof sketches provide strategic information that helps models disambiguate closely related answer choices and identify load-bearing parts of an argument.This result indicates that sketches add information beyond a redundant theorem restatement.

5 Endnote and Discussion

The discussion positions LiveMathematicianBench as a diagnostic, scalable alternative to static or manually authored benchmarks. Its substitution-resistant and proof-sketch protocols probe structural comprehension and strategy use beyond answer derivation.

  • Discussion: Logical-form performance differences support using the taxonomy as a diagnostic axis alongside aggregate leaderboard scores.The benchmark can reveal structure-specific strengths and weaknesses that aggregate accuracy alone does not show.
  • Discussion: The benchmark is less vulnerable to rapid saturation and contamination because it is built from recent post-cutoff arXiv papers.This supports tracking progress in research-level mathematical reasoning over time.
  • Discussion: Substitution-resistant questions require models to recognize a weakened true option while inferring that a stronger statement follows from the hypotheses.The design therefore probes movement beyond recognition toward a limited form of mathematical conjecturing.
  • Discussion: Proof-sketch access improves the two highest-scoring models and tests whether they can use strategic guidance without full derivational detail.The authors connect this behavior to proof-guided reasoning, tool use, and interactive mathematical exploration.
  • Related work: Prior benchmarks face trade-offs among contamination risk, sample size, scalability, and coverage of research-level reasoning.First Proof has only ten problems, FrontierMath requires substantial human authoring, and RealMath covers a narrower set of automatically verifiable theorem types.
  • Related work: Unlike manually authored benchmarks, LiveMathematicianBench draws from a continuously growing stream of recent arXiv papers, enabling a scalable and refreshable pipeline.It also uses logical categories and proof-sketch-guided distractors to probe plausible but invalid reasoning directions.
  • Validation: The released set contains 177 benchmark items reviewed for theorem fidelity, self-containedness, answer uniqueness, and distractor quality.Intermediate pipeline outputs were also audited through stratified reviews across logical categories.
  • Validation: Human validation combines prompt design and expert review to ensure distractors are demonstrably false and MCQs are valid.The appendix illustrates this process through an existential-universal theorem example with labeled distractor perturbations.

C Detailed Logical Taxonomy of Theorem Categories

The taxonomy classifies theorems by logical form rather than mathematical topic, enabling structured analysis of reasoning types. One category is algorithmic or constructive theorems, which assert that an object can be explicitly or efficiently computed.

  • Taxonomy framework: The taxonomy focuses on theorem logical form independently of mathematical topic or context, with each category paired with a canonical form and example.This supports diagnosis across distinct mathematical domains.
  • Algorithmic / Constructive: Algorithmic or constructive theorems assert that an algorithm computes a function or that an object can be explicitly constructed.The representative example is a polynomial-time algorithm for maximum matching in any bipartite graph.

LIVEMATHEMATICIANBENCH Example

The benchmark examples test whether models can identify precise theorem conclusions across diverse research mathematics, including finite-state periodicity, asymptotic bounds, geometric equality cases, and existence results. Proof sketches expose the strategic mechanisms behind these conclusions, such as finite-state transducers, prime bucketing, and geometric stability arguments.

  • Fibonacci and finite-state example: Finite-state reasoning yields that S(M) is either finite or ultimately periodic, with procedures for deciding finiteness and computing relevant periodicity information.The proof sketch uses multiplication transducers, length-M windows, and an automaton checking forbidden-factor avoidance.
  • Fibonacci and finite-state example: The Fibonacci example defines Zeckendorf digits by ε_k = 1 and ε_iε_i+1 = 0, then forms a padded reversed encoding eZ(N) for factor-avoidance questions.The generated question asks which conclusion about S(M) follows from this encoding and the finite-state construction.
  • Proof-sketch guidance: Proof sketches connect benchmark questions to high-level strategies, including finite-state dynamical systems, prime bucketing, geometric control of maximizing slices, and forcing constructions.These sketches are used alongside theorem statements and generated questions to test structural understanding across mathematical domains.
  • Theorem-conclusion examples: The finite-state, cubic-field, and geometric examples require distinguishing theorem conclusions such as periodicity, uniform existence, and equality characterization rather than merely recalling isolated formulas.The supplied examples include an equality statement identifying the Clifford torus and a family of continuum-many pairwise non-isomorphic McDuff-superrigid groups.
  • Cubic-field example: The cubic-field theorem guarantees at least cX^(1−κ−ε) suitable integers d ≤ X for sufficiently large X, with class-number and discriminant-count conditions.For each relevant shift d+i, any cubic field with the prescribed signed discriminant has class number greater than H, while at least k such fields occur across the interval.

LIVEMATHEMATICIANBENCH Example 8 (Question & Answers)

Example 8 tests whether models can identify the strongest theorem statement about σ-complete ultrafilters and a quantitative bound for surface crossing numbers. It also presents a scalar-curvature nonexistence theorem whose proof uses relative higher-index methods.

  • Ultrafilters: The ultrafilter question asks which consistency statement follows from the existence of a measurable cardinal, using the Lipschitz and Ketonen orders.
  • Surface crossing number: The fundamental inequality bounds surface crossing number using knot complexity, tunnel number, and the Heegaard deficiency of the ambient surface.
  • Surface crossing number: The proof sketch derives the lower bound through inequalities relating surface crossing, ascending, and bridge numbers, then establishes asymptotic optimality using iterated connected sums.
  • Theorem taxonomy: The benchmark classifies nonexistence theorems as claims that no object satisfies a specified property.
  • Scalar curvature: The scalar-curvature theorem excludes complete positive-scalar-curvature metrics on M#N and forces non-negative-scalar-curvature metrics there to be Ricci-flat.
  • Scalar curvature: The corresponding proof uses Dirac operators, a relative higher-index theorem, and explicit K-theory computations.

LIVEMATHEMATICIANBENCH Example 10 (Question & Answers)

Example 10 asks for the strongest metric conclusion under the rational strong Novikov conjecture, while the surrounding examples illustrate existence, uniqueness, universal, and proof-strategy categories. The proof approach combines linearized well-posedness, iteration, convergence, bootstrapping, and boundary analysis.

  • Example 10: Under the stated asphericity, spin, and rational strong Novikov assumptions, the connected sum admits no complete positive-scalar-curvature metric, while every complete non-negative-scalar-curvature metric is Ricci-flat.
  • Theorem taxonomy: The benchmark taxonomy defines uniqueness as existence of exactly one object satisfying a property.
  • Proof sketch: The proof strategy establishes linearized well-posedness, constructs a convergent iterative scheme, and uses bootstrapping to reach the final conclusion.
  • Proof sketch: Boundary interactions are handled using adapted coordinates and geometric analysis of characteristic curves near the singular set and boundary.
  • Universal theorem: The hyperbolic-lattice theorem states that every hyperbolic lattice of rank at least 46 has trivial exceptional lattice.

LIVEMATHEMATICIANBENCH Example (Theorem & Sketch)

Example 13 asks models to identify the strongest universal graph-theoretic theorem statement. The theorem uses probabilistic methods and hypergraph containers in constructing graphs with a Ramsey property while avoiding a larger clique.

  • Theorem: For every k ≥2, there is a graph G such that K_k is not a subgraph of G but G arrows K_{k−1}.
  • Proof sketch: The proof combines probabilistic methods with the hypergraph container framework and ideas from Bollobás–Erdős.

D Benchmark Composition Across Construction Stages

Figure 6 tracks benchmark size through monthly construction stages, from the full generated candidate pool to filtered and calibrated released splits. The pipeline reduces candidates through explicit quality, stem-nontriviality, and hardness procedures.

  • Construction stages: Figure 6 compares the complete post-generation pool, the rubric-filtered subset, and the final Hard split across construction stages for each month.
  • Construction stages: The described pipeline consistently reduces the candidate pool through structured filtering rather than ad hoc pruning.

E Evaluation Implementation Details

The released evaluators provide backend-specific inference entry points while sharing a common evaluation pipeline, deterministic option handling, scoring logic, and resumable result serialization.

  • Backend support: The repository provides separate evaluators for Azure OpenAI, Claude through Anthropic, and models served through an OpenAI-compatible vLLM endpoint.Backend-specific command-line options support provider credentials, timeouts, debugging, sampling, and reasoning controls.
  • Benchmark inputs: Each benchmark item contains a question stem, one correct choice, four distractors, and auxiliary metadata, while evaluation consumes the finalized multiple-choice fields.Source theorem context, sketches, and other record-level annotations remain in the benchmark files but are not used by the released evaluation scripts.
  • Prompt construction: The scripts deterministically shuffle five answer choices, relabel them A–E, and prompt models to provide a boxed final answer.The shuffle uses a per-item seed based on the global seed and dataset index.
  • Evaluation modes: All models were evaluated without sketches, while sketch-aware evaluation was additionally run for only the strongest models because of budget constraints.The dual-mode comparison therefore covers a limited subset of models in the sketch-aware condition.
  • Scoring: Answer extraction prioritizes the last boxed label A–E and falls back to short or standalone capital-letter responses when no boxed answer appears.The evaluators apply this parsing logic to generated response text, with Claude responses first separated into text and other response components.
  • Execution and outputs: The evaluators support parallel inference, repeated sampling, token accounting, fault-tolerant resumption, and JSON result serialization across backends.Claude and vLLM completion counts include reasoning tokens when metadata is available, and resume mode reruns unanswered or failed items only.

F Additional Evaluation Results

Proof sketches improve accuracy in both ordinary and substitution-resistant settings, but the size of the gain varies by model and choice style.

  • Sketch-aware gains: Proof sketches improve performance on both original-choice and substitution-resistant questions, with model-dependent gains.GPT-5.4 benefits more on the original-choice subset, whereas Gemini-3.1-pro-preview shows especially large gains on substitution-resistant items.

F.2 Cost Analysis

The cost analysis compares model accuracy with completion-token usage and finds that GPT-5.4 offers a strong accuracy–cost frontier relative to higher-token alternatives.

  • Accuracy–cost frontier: GPT-5.4 leads the accuracy–cost frontier rather than the highest-token models.Qwen and Kimi use substantially more tokens without matching GPT-5.4 or Gemini in accuracy.
  • Accuracy–cost frontier: GPT-5.4 (high) reaches 41.8% accuracy with about 7.0k tokens, while GPT-5.4 (medium) reaches 41.2% with about 3.8k tokens.Both settings remain close to Gemini-3.1-pro-preview in accuracy while using fewer completion tokens.
  • Model efficiency: Open-weight and alternative frontier systems occupy distinct efficiency niches, with Qwen3.5-397B-A17B and Kimi-K2.5 showing mid-tier accuracy at higher token budgets.GPT-oss-120b generates even more tokens without reaching the top closed-model accuracy band.
  • Model efficiency: The results suggest that research-level mathematical reasoning gains cannot be reduced to allocating more inference tokens alone.The analysis attributes the remaining efficiency differences to architectural and training differences affecting conversion of tokens into correct mathematical judgments.
Loading 2604.01754v1…