Source-linked AI summary
Towards Robust Mathematical Reasoning
Thang Luong, Dawsen Hwang, Hoang H. Nguyen, Golnaz Ghiasi, Yuri Chervonyi, Insuk Seo, Junsu Kim, Garrett Bingham, Jonathan Lee, Swaroop Mishra, Alex Zhai, Clara Huiyi Hu, Henryk Michalewski, Jimin Kim, Jeonghyun Ahn, Junhwi Bae, Xingyou Song, Trieu H. Trinh, Quoc V. Le, Junehyuk Jung
TL;DR
Existing mathematical reasoning evaluations can be too easy or depend on short-answer matching, which may not reflect robust multi-step reasoning. IMO-Bench addresses this with vetted IMO-level benchmarks for short answers, proofs, and grading, with frontier models struggling and automated graders correlating strongly with expert evaluations.
Problem
Existing evaluations may rely on limited techniques or final-answer matching, leaving robust multi-step reasoning insufficiently assessed.
Method
IMO-Bench provides three vetted benchmarks covering short-answer matching, full-proof correctness, and proof verification at International Mathematical Olympiad level.
Results
65.7% on advanced IMO-ProofBench versus 23.3% for the best non-Gemini model, while automated graders achieved near-human answer accuracy and strong correlation with expert proof scores.
Takeaways & Limitations
IMO-Bench separates short-answer success from correct mathematical reasoning and offers scalable evaluation tools while retaining human expertise as the high-stakes standard.
Takeaways & Limitations
Public release creates a long-term data-contamination risk because models may memorize benchmark answers rather than demonstrate genuine reasoning.
Abstract
from arXiv · showhide
Finding the right north-star metrics is highly critical for advancing the mathematical reasoning capabilities of foundation models, especially given that existing evaluations are either too easy or only focus on getting correct short answers. To address these issues, we present IMO-Bench, a suite of advanced reasoning benchmarks, vetted by a panel of top specialists and that specifically targets the level of the International Mathematical Olympiad (IMO), the most prestigious venue for young mathematicians. IMO-AnswerBench first tests models on 400 diverse Olympiad problems with verifiable short answers. IMO-Proof Bench is the next-level evaluation for proof-writing capabilities, which includes both basic and advanced IMO level problems as well as detailed grading guidelines to facilitate automatic grading. These benchmarks played a crucial role in our historic achievement of the gold-level performance at IMO 2025 with Gemini Deep Think (Luong and Lockhart, 2025). Our model achieved 80.0% on IMO-AnswerBench and 65.7% on the advanced IMO-Proof Bench, surpassing the best non-Gemini models by large margins of 6.9% and 42.4% respectively. We also showed that autograders built with Gemini reasoning correlate well with human evaluations and construct IMO-GradingBench, with 1000 human gradings on proofs, to enable further progress in automatic evaluation of long-form answers. We hope that IMO-Bench will help the community towards advancing robust mathematical reasoning and release it at https://imobench.github.io/.
1. Introduction
Existing mathematical reasoning benchmarks can be too easy, saturating, or dependent on short-answer matching, so IMO-Bench targets robust reasoning at IMO difficulty through answer and proof evaluations.
- Motivation: Many existing benchmarks rely on limited techniques or final-answer matching, which may not distinguish guessing from robust reasoning.The paper identifies saturation and insufficiently deep, multi-step reasoning as key concerns.
- Benchmark suite: IMO-Bench targets rigorous multi-step and novel reasoning at the level of the International Mathematical Olympiad.Its problems were vetted by IMO medalists and mathematicians.
- Benchmark suite: IMO-AnswerBench contains 400 diverse Olympiad problems with verifiable answers, while IMO-ProofBench evaluates complete proofs across basic and advanced difficulty levels.The benchmarks cover varied topics and include grading guidelines for consistent evaluation.
- Results: 65.7% on advanced IMO-ProofBench exceeded the best non-Gemini model’s 23.3% according to human evaluations, while automated graders correlated highly with expert evaluations.The reported correlation supports using automated grading as a scalable complement.
2. IMO-AnswerBench
IMO-AnswerBench uses 400 diverse, robustified Olympiad problems spanning four categories and multiple difficulty levels, with language-model answer verification designed to tolerate semantic variation.
- Problem Selection: 400 problems span Algebra, Combinatorics, Geometry, and Number Theory across pre-IMO, IMO-Easy, IMO-Medium, and IMO-Hard levels.The benchmark contains 100 problems per category.
- Problem Selection: Number Theory and Combinatorics have the most topics, while Geometry emphasizes angle and sidelength computation.The distribution reflects both broad topic coverage and the short-answer format.
- Problem Robustification: Problems are reformulated to produce clear, nontrivial short answers while reducing ambiguity during solving and verification.Some proof-heavy problems undergo an additional reformulation step.
- Problem Robustification: Paraphrasing, renamed objects, modified numerical values, distractors, and equivalent reformulations are used to reduce memorization.The transformations can alter expressions or objectives while preserving the underlying problem structure.
- Answer autograder: AnswerAutoGrader uses Gemini 2.5 Pro to extract final answers and assess correctness against ground truths, supporting flexible answer formats.Its performance is reported as nearly identical to human evaluators.
3. Going Beyond Short Answers with IMO-ProofBench
IMO-ProofBench addresses the limits of short-answer evaluation by requiring valid mathematical arguments across basic and advanced IMO-level problems, with human and automated grading procedures.
- Motivation: Correct short answers can conceal flawed reasoning, and many IMO problems lack short answers, motivating proof-based evaluation.Guessing a final answer can be easier than deriving it rigorously.
- Benchmark design: IMO-ProofBench contains 60 proof-based problems, and models receive credit only for correct and relevant reasoning steps.The benchmark mirrors IMO-style problems and assesses comprehensive mathematical arguments.
- Benchmark design: The basic subset covers pre-IMO to IMO-Medium difficulty, while the advanced subset contains 30 highly challenging problems up to IMO-Hard level.The advanced collection includes novel problems designed to simulate complete IMO examinations.
- Evaluation: The grading framework uses four primary ratings, while human experts may assign any integer score from 0 to 7 for greater nuance.The simplified rubric includes Correct, Almost, Partial, and Incorrect.
- Evaluation: ProofAutoGrader uses Gemini 2.5 Pro with the problem, candidate solution, reference solution, and grading guidelines, but human experts remain the gold standard.The paper describes automated proof evaluation as intricate and not a perfect substitute for experts.
4. IMO-GradingBench
IMO-GradingBench contains 1000 human-graded proof examples framed as four-way classification, with grade distributions that track problem difficulty.
- Dataset construction: IMO-GradingBench contains 1000 examples pairing problem statements and proposed solutions with human-assigned grades on a 0–7 scale.The evaluation maps scores to Correct, Almost, Partial, and Incorrect labels and balances the categories roughly equally.
- Evaluation format: The benchmark converts fine-grained IMO scores into four labels: Correct, Almost, Partial, and Incorrect.This framing reduces noise from precise point-level scoring.
- Difficulty calibration: As intended difficulty rises from IMO-easy to IMO-hard, correct and almost solutions decrease while incorrect and partial solutions increase.The reported distribution aligns the human grades with the assigned difficulty levels.
- Difficulty calibration: Figure 3 shows grade distributions for IMO-GradingBench across IMO-Hard, IMO-Medium, and IMO-Easy problems.The figure organizes solutions by difficulty level and grade category.
5. Results
IMO-Bench results show strong performance by Gemini Deep Think on short-answer and proof tasks, while advanced proof writing remains difficult and automated grading is promising but imperfect.
- IMO-ProofBench: 89.0% on basic IMO-ProofBench was achieved by Gemini Deep Think (IMO Gold), while most other models scored below 60%.Scores were based on expert grading of complete proofs.
- IMO-ProofBench: Advanced proof performance varied sharply by problem source, with Grok 4 (heavy) scoring 76.2% on USAMO 2025 but 11.1% on novel problems.Gemini Deep Think (IMO Gold) scored 69.0% on USAMO and 61.1% on novel sets, indicating more general capabilities.
- Automated grading: ProofAutoGrader correlated with human grades at Pearson coefficients of 0.96 on basic and 0.93 on advanced problems.On 170 internal systems, the correlation was lower but still reasonable at 0.87.
- Automated grading: ProofAutoGrader occasionally misses high-level logical errors or penalizes unconventional correct solutions, so human verification remains necessary.The paper recommends using it to augment rather than replace human evaluation.
- IMO-GradingBench: IMO-GradingBench remained challenging under minimal context, whereas reference solutions and grading guidelines enabled robust aggregate rankings with ProofAutoGrader.The benchmark’s best accuracy was 54.0%, while Gemini Deep Think (IMO Gold) achieved the best MAE at 18.4%.
6. Related Work
Related work has expanded mathematical reasoning benchmarks toward harder Olympiad-level tasks, robustness testing, long-form reasoning, and process supervision.
- Harder benchmarks: Olympiad Bench and Omni-MATH evaluate Olympiad-level questions across diverse domains, while Humanity’s Last Exam spans many knowledge domains.Other benchmarks target long-form puzzles, hard mathematics, formal proofs, reward models, or applied mathematics.
- Robustness evaluation: Robustness benchmarks test whether models overfit by perturbing existing questions and measuring performance drops.SVAMP, Putnam-AXIOM, and MATH-Perturb report reduced performance after perturbations.
- Reasoning processes: Process supervision offers an alternative robustness strategy by supervising reasoning from start to finish rather than only the final outcome.The cited approach improved performance on the MATH dataset.
7. Conclusion
The paper introduces IMO-Bench and validated automated graders to evaluate robust mathematical reasoning beyond short-answer correctness, while retaining human expertise for high-stakes proof evaluation.
- Contributions: IMO-Bench combines IMO-AnswerBench for short answers, IMO-ProofBench for full proof correctness, and IMO-GradingBench for proof verification.Together, the benchmarks target answer matching, proof construction, and solution grading.
- Findings: The benchmarks show that frontier models struggle on IMO-Bench and that correct short answers do not necessarily indicate correct mathematical reasoning.This conclusion is stated across the three benchmark types.
- Automated grading: AnswerAutoGrader reached 98.9% near-human accuracy, while ProofAutoGrader correlated 0.93–0.96 with expert scores.Human expertise remains the gold standard for high-stakes evaluation.
- Implications: The released suite is intended to shift evaluation from answer-getting toward deep, verifiable, and robust reasoning processes.The authors aim for IMO-Bench to measure and drive progress toward more advanced and reliable AI.
Limitations
IMO-Bench is constrained by evaluation cost and future data contamination. Robustification makes problems harder than their original versions, while the benchmark spans four categories and includes varied Olympiad topics.
- Evaluation Cost: Evaluation requires costly human verification because ProofAutoGrader correlates strongly with human scores but is not a perfect substitute.Automatic grading can introduce noise, so definitive assessments still require experts who are costly and difficult to source.
- Future Data Contamination: Public release creates a risk that future training data will absorb IMO-Bench problems and solutions, enabling memorization rather than genuine reasoning.The authors identify preventing this benchmark decay as a significant field-wide challenge.
- Benchmark Scope: 400 problems are divided evenly across Algebra, Combinatorics, Geometry, and Number Theory in IMO-AnswerBench.Each category contains exactly 100 problems.
- Benchmark Scope: IMO-Bench emphasizes Olympiad topics and problem-solving techniques beyond the coverage of prior benchmarks.Examples include inequalities, functional equations, graph theory, tiling, combinatorial geometry, and modular analysis.
- Interpretation: Strong model performance would indicate both high competence and broad knowledge coverage because some problems require particular solution strategies.The authors frame this as an implication of the benchmark’s varied contest levels and topics.
- Robustification: 11.2% is the reported maximum performance gap between original and robustified problems for o4-mini (high reasoning).Models perform significantly better on the original problems, indicating that robustification creates a substantial challenge.
A.4. Towards Consistent Problem Statements and Answer Evaluation
The benchmark reformulates Olympiad problems to make statements easier to interpret and answers uniquely verifiable. These changes target ambiguity, notation errors, answer guessing, and evaluation difficulty.
- Problem Statements: Problem statements are redesigned to avoid misinterpretation and unintended outputs when models solve complex Olympiad problems.The authors add several strategies on top of robustification to improve interpretability.
- Unique Answers: Unique numerical outputs replace hard-to-verify solution sets or tuples, often by asking for sums or other non-trivial functions of many inputs.Examples include computing a sum instead of characterizing all solution tuples.
- Problem Statements: Answer simplification and more specific wording address confusion from complex notation and special characters, including angle-degree notation.Geometry questions explicitly specify degrees to prevent radians-versus-degrees confusion.
- Binary Answers: Binary existence questions are reformulated as requests for the smallest positive integer satisfying the property, preserving difficulty while reducing answer guessing.The original answer “It exists” is replaced by a non-binary numerical target.
- Answer Evaluation: AnswerAutoGrader checks mathematical equivalence between extracted model answers and golden answers rather than grading reasoning steps.Its rules cover algebraic, numerical, and set/list equivalence, with no partial credit for incomplete answers.
- Answer Evaluation: The grader uses a strict two-part output protocol requiring analysis tags followed by only a boxed Correct or Incorrect grade.A worked example classifies an empty set as Incorrect against a non-empty interval union.
B. IMO-ProofBench
IMO-ProofBench includes robustified examples presented in Table 10. The supplied passage identifies the table but does not describe its examples or evaluation outcomes.
- Examples: Table 10 presents robustified examples of IMO-ProofBench.The passage provides no further description of the examples or their results.
B.2. Proof Evaluation Guidelines for IMO-ProofBench
IMO-ProofBench evaluates complete proof writing under rigorous Olympiad standards, using structured grading criteria and an iterative self-verification pipeline. Examples show that correct short answers can conceal incomplete proofs, unsupported assumptions, or guesses.
- Proof evaluation: Proof evaluation verifies whether each logical step is valid, but informal proofs introduce subjectivity when judging whether claims are sufficiently justified.Olympiad grading nevertheless typically remains consistent because rubrics specify partial results and common solution approaches.
- Solution generation: A pipeline repeatedly self-verifies and bug-fixes candidate solutions, returning one after five successful checks or exiting after ten consecutive verification failures.It runs up to 30 iterations and 100 parallel runs; two advanced problems produced no returned solution.
- Observed proof failures: Correct final answers may still receive little or no proof credit when the argument assumes unproved restrictions or guesses solutions from small cases.One example checks only linear functions, while another guesses polynomial forms without proving correctness or completeness.
- Observed proof failures: No tested model earned even a partial score on a standard pre-IMO symmetric inequality or found the invariant for a standard easy combinatorics problem.The examples illustrate failures on problems described as among the easiest high-school competition inequalities and easy invariance problems.
- Grading rubric: Scores use a 0–7 scale, with full credit requiring a complete, correct, rigorous proof and lower scores reflecting minor gaps, substantial progress, or fundamental flaws.Discarded incorrect attempts do not reduce full credit when the final proof is complete and correct.
- Grading procedure: The evaluation prompt supplies the problem, reference solution, specific guidelines, and proposed solution before requiring step-by-step analysis and a single parsed score.Specific grading guidelines take precedence over the general rubric, especially for partial credit.
B.6. Limitations of ProofAutoGrader
ProofAutoGrader supports scalable proof evaluation with structured prompts and categorical labels, but its assessments remain vulnerable to systematic over- and under-penalization. Human grade distributions also vary across problems rather than remaining uniform.
- Autograder limitations: ProofAutoGrader tends to overestimate scores, miss high-level logical errors, and over-penalize minor formatting issues or unconventional correct solutions.These systematic errors limit the reliability of automatic proof assessment despite high correlation with human grades.
- Autograder limitations: The grader can overlook deceptive logical inconsistencies, including invalidly inferring one inequality from two unrelated upper bounds.Such errors may appear plausible but can invalidate an entire proof.
- Autograder limitations: ProofAutoGrader may mark an almost-correct novel solution wrong when its key lemma omits a condition, although human graders award substantial partial credit.In one case, adding a fixed-slope condition made the lemma valid and led human graders to assign 6 out of 7 points.
- Grade distribution: Grade distributions are not uniform across problems, reflecting differences in problem difficulty and the score patterns proof-evaluation models will encounter.Figure 6 presents the aggregate grade distribution for the benchmark.
- Evaluation settings: The vanilla grading setting asks a model to analyze a proposed solution and output one of four labels: incorrect, partial, almost, or correct.The final label is constrained to the last response word for extraction.