Technical Summary: IMProofBench

Problem Statement

Current benchmarks for evaluating Large Language Models (LLMs) on mathematics are insufficient for assessing research-level capabilities. Existing datasets primarily focus on high-school or undergraduate competition problems (e.g., AIME, MATH), which are increasingly solvable by state-of-the-art models and fail to test genuine proof-writing abilities. Furthermore, benchmarks targeting advanced mathematics, such as FrontierMath and Humanity's Last Exam (HLE), often restrict evaluation to final-answer correctness. This limitation allows models to employ shortcuts or guess correct answers without constructing logically sound arguments, thereby overlooking the critical skill of generating rigorous mathematical proofs. There is a lack of a standardized, private benchmark that evaluates LLMs on research-level proof generation within a realistic, tool-augmented environment.

Methodology

Benchmark Construction (IMProofBench)

IMProofBench is a private benchmark comprising 77 peer-reviewed problems developed in collaboration with over 44 professional mathematicians. The problem creation pipeline involves:

• Authorship: Problems are authored by researchers within their specific areas of expertise, ranging from graduate-level oral exam questions to open research problems.
• Peer Review: Each submission undergoes a rigorous review process by a core team member and an external expert in the relevant field to ensure mathematical correctness, appropriate difficulty, and clarity.
• Structure: Each problem consists of a main proof-writing task and follow-up subquestions with unique, automatically gradable answers. This dual structure supports both human expert evaluation of the proof and automated quantitative analysis of final answers.
• Dynamic Nature: The benchmark is designed as a continuous platform. Problems are added on a rolling basis, and authors are encouraged to retire problems if they become solvable due to new research, ensuring the benchmark remains unsaturated.

Evaluation Framework

The evaluation simulates a realistic research environment using an agentic framework built on the Inspect framework. Models operate with access to:

• Computational Tools: Python (NumPy, SciPy, SymPy), Bash (Arch Linux), and specialized mathematical software including SageMath, GAP, Maxima, PARI/GP, and Singular.
• Literature Search: Web search capabilities to locate relevant theorems, papers, or data (e.g., OEIS).
• Interaction: Models engage in multi-turn interactions, utilizing a submit tool to distinguish reasoning steps from final outputs.

Grading Process

Evaluation occurs in two stages:

1. Automated Grading: Follow-up subquestions are graded by comparing model outputs against ground-truth answers.
2. Human Expert Grading: The main proof is evaluated by the problem's author using a 0–3 scale:
   • 0/3: No progress.
   • 1/3: Minor progress (limited advancement).
   • 2/3: Major progress (substantial work completed).
   • 3/3: Complete solution.
     Graders also annotate specific error types (logical mistakes, hallucinations, calculation errors, conceptual misunderstandings) and achievement indicators (understanding, correct results, insights, usefulness). To prevent bias, model identities are hidden during grading.

Key Contributions

1. IMProofBench: A private, evolving benchmark specifically designed for research-level mathematical proof generation, developed through direct collaboration with the mathematical community.
2. Systematic Analysis: A comprehensive evaluation of state-of-the-art LLMs on proof generation, judged by human experts, moving beyond simple final-answer accuracy.
3. Qualitative Insights: A detailed analysis of model strengths and failure modes, highlighting the gap between final-answer accuracy and genuine proof-writing capability, as well as the models' interaction with research tools.

Experimental Results

Performance Overview

The authors evaluated 10 LLMs on the proof-based portion of the benchmark:

• Top Performers: GPT-5.4 achieved the highest performance, producing complete solutions (3/3) for 49% of tasks. GEMINI-3.1-PRO followed closely at 46%.
• Lower Performers: CLAUDE-OPUS-4.6 provided complete solutions for only 32% of tasks.
• Open Problems: Among the 23 open research questions in the benchmark, GPT-5 solved one in December 2025.

Final-Answer vs. Proof Generation

On the subset of 45 questions with follow-up subquestions, GPT-5.4 scored 75% on final-answer accuracy. The correlation between subquestion scores and human-graded proof progress was 0.51, suggesting that while final-answer accuracy is a useful proxy, it lacks the nuance required to evaluate the quality of the reasoning process.

Error and Tool Analysis

• Error Types: Logical errors were the most common failure mode (e.g., unfounded assumptions), particularly in CLAUDE-OPUS-4.6 (40% of responses). Hallucinations of non-existent theorems were also observed.
• Tool Usage: Models varied significantly in tool usage. GEMINI-3.1-PRO made nearly four times as many tool calls as other models but used the fewest output tokens.
• Ablation Study: An ablation on the agentic setup revealed that tool access generally improved performance (e.g., +14.4% for GROK-4), though some models (e.g., GEMINI-2.5-PRO) saw slight decreases, likely due to suboptimal tool selection (e.g., overusing code interpreters for mathematical reasoning).

Qualitative Observations

• Literature Knowledge: Leading models demonstrated strong familiarity with specialized mathematical literature but struggled with obscure sources like private lecture notes.
• Hallucination and Confidence: Models frequently hallucinated results to force an answer and rarely abstained from providing a solution, even when stuck. They often presented flawed arguments with high confidence.
• Insight: Despite errors, models frequently provided insights and partial progress that could be useful to human researchers, with GPT-5.4 offering meaningful contributions in approximately 60% of attempts.

Significance and Claims

The paper claims that IMProofBench addresses a critical gap in AI evaluation by shifting focus from competition-style problems to research-level proof generation. The authors assert that:

1. Current Capabilities: State-of-the-art LLMs can already solve a meaningful subset of research-level problems, indicating their potential as mathematical collaborators.
2. Limitations: Current models remain imperfect, prone to logical errors and hallucinations, and often lack the ability to distinguish between a correct final answer and a valid proof.
3. Evaluation Necessity: The benchmark demonstrates that final-answer metrics are insufficient for measuring mathematical capability; human expert evaluation of the reasoning process is essential.
4. Future Direction: The work establishes a framework for continuous, dynamic evaluation of LLMs in realistic research settings, facilitating the study of how AI can be effectively integrated into mathematical workflows.

The authors maintain a modest stance, noting that the benchmark is currently in active development with a limited number of problems (77), but argue that even this scale provides valuable insights into the trajectory of AI in mathematical research.