PaperlayerView exact revision on arXiv

Source-linked AI summary

Challenging the Boundaries of Reasoning: An Olympiad-Level Math Benchmark for Large Language Models

Haoxiang Sun, Yingqian Min, Zhipeng Chen, Wayne Xin Zhao, Ji-Rong Wen

arXiv:2503.21380v3cs.CL

TL;DR

Existing math benchmarks provide limited challenge, verification, contamination control, and multilingual coverage for advanced reasoning models. OlymMATH addresses these gaps with a bilingual Olympiad-level suite combining rule-based numerical evaluation and Lean 4 formal verification. Experiments show substantial difficulty, cross-language performance gaps, and heuristic guessing behaviors, while the released resources support further analysis.

  • Problem

    Existing benchmarks leave challenge, contamination control, multilingual coverage, and the combination of outcome and process verification incompletely addressed.

  • Method

    OlymMATH provides 350 bilingual problems: 200 computational items with sympy-verifiable numerical answers and 150 Lean 4 formalizations, curated from printed publications and verified by experts.

  • Results

    Advanced models achieve low performance on OlymMATH-HARD and OlymMATH-LEAN, with consistent English–Chinese gaps and observed heuristic guessing behaviors.

  • Takeaways & Limitations

    OlymMATH supports comprehensive evaluation of answer correctness and reasoning rigor while enabling research on multilingual reasoning and process-level reward modeling.

  • Takeaways & Limitations

    The benchmark covers only English and Chinese, uses text-based problems, and does not yet precisely quantify heuristic shortcuts in natural-language evaluation.

Abstract

from arXiv · show

The rapid advancement of large reasoning models has saturated existing math benchmarks, underscoring the urgent need for more challenging evaluation frameworks. To address this, we introduce OlymMATH, a rigorously curated, Olympiad-level math benchmark comprising 350 problems, each with parallel English and Chinese versions. OlymMATH is the first benchmark to unify dual evaluation paradigms within a single suite: (1) natural language evaluation through OlymMATH-EASY and OlymMATH-HARD, comprising 200 computational problems with numerical answers for objective rule-based assessment, and (2) formal verification through OlymMATH-LEAN, offering 150 problems formalized in Lean 4 for rigorous process-level evaluation. All problems are manually sourced from printed publications to minimize data contamination, verified by experts, and span four core domains. Extensive experiments reveal the benchmark's significant challenge, and our analysis also uncovers consistent performance gaps between languages and identifies cases where models employ heuristic "guessing" rather than rigorous reasoning. To further support community research, we release 582k+ reasoning trajectories, a visualization tool, and expert solutions at https://github.com/RUCAIBox/OlymMATH.

1 Introduction

OlymMATH addresses the need for reliable, verifiable, and sufficiently challenging math benchmarks by combining numerical-answer and formal-proof evaluation in a bilingual Olympiad-level suite.

  • Benchmark motivation: Reliable LLM reasoning assessment requires unambiguous problems, low contamination risk, and verifiable evaluation.Numerical-answer benchmarks scale through rule-based checking but assess only outcomes, whereas theorem-proving benchmarks verify reasoning processes but require specialized formalization.
  • OlymMATH: The benchmark is designed to jointly address quality, verifiability, contamination, and multilingual evaluation gaps.Its motivation follows directly from the limitations identified in existing numerical-answer and formal-proof benchmarks.
  • Benchmark motivation: Existing benchmarks remain limited by small or insufficiently difficult Olympiad collections, judge hallucination, incomplete solutions, contamination risks, and English-centric coverage.These limitations affect both numerical-answer and formal-proof paradigms and are not straightforwardly solved by recombining existing resources.
  • OlymMATH: OlymMATH introduces a rigorously curated bilingual benchmark with 350 unique Olympiad-level problems organized into three subsets.The supplied passage introduces the benchmark and its scale; the detailed subset composition appears in later construction passages.

OlymMATH-EASY / HARD

OlymMATH-EASY and OlymMATH-HARD use bilingual computational problems with rule-based numerical verification, while OlymMATH-LEAN adds Lean 4 process-level verification. Experiments show substantial difficulty for advanced models and reveal limitations in reasoning behavior.

  • OlymMATH-EASY / HARD: OlymMATH-EASY and OlymMATH-HARD contain 100 computational problems each with bilingual versions and sympy-verifiable numerical answers.The numerical-answer design supports precise, objective, and rule-based assessment.
  • OlymMATH-LEAN: OlymMATH-LEAN provides 150 bilingual problems formalized in Lean 4 for automated and rigorous theorem-proving evaluation.Lean verification evaluates formal proof correctness rather than relying on an LLM judge.
  • Dataset scope: OlymMATH comprises 350 problems spanning four major mathematical fields and includes expert-verified problems sourced from printed publications.The released materials also include expert solutions and reasoning trajectories for community research.
  • Evaluation results: 19.5%, 31.2%, and 58.4% accuracy were achieved by DeepSeek-R1, o3-mini, and Gemini 2.5 Pro Exp, respectively, on OlymMATH-HARD (EN).These results indicate that Olympiad-level mathematics remains difficult for advanced reasoning models.
  • Reasoning patterns: Models often use heuristic guessing that fails on OlymMATH problems, including an incorrect symmetry assumption on a complex optimization problem.The example illustrates the benchmark’s ability to expose reasoning shortcuts rather than only final-answer errors.

2 Related Work

Existing natural-language and formal-mathematics benchmarks provide important foundations but remain constrained by scale, contamination, judge reliability, language coverage, or proof-verification scope. OlymMATH is positioned as a larger, manually curated bilingual alternative for Olympiad-level evaluation.

  • Natural Language Math Benchmarks: GSM8K and MATH established scalable numerical-answer evaluation, but slow-thinking models have largely saturated these benchmarks.Their rule-based format remains influential for mathematical reasoning research.
  • Natural Language Math Benchmarks: AIME offers greater difficulty but its small scale weakens statistical reliability and leaves less headroom for rapidly improving models.The passage notes that a single problem can materially change measured accuracy.
  • Natural Language Math Benchmarks: Omni-MATH, PolyMath, and related collections face contamination risks from web crawling, public competitions, or existing datasets, while proof-based problems may require LLM-as-judge evaluation.These design choices can reduce the dependability of benchmark comparisons.
  • Natural Language Math Benchmarks: OlymMATH offers 200 challenging Olympiad-level computational problems with manual curation from printed publications, bilingual versions, and larger scale.These features target contamination reduction, statistical reliability, and broader evaluation coverage.
  • Formal Language Math Benchmarks: Formal theorem-proving benchmarks evaluate how models derive solutions by requiring machine-checkable proofs, complementing final-answer assessment.The related-work discussion identifies miniF2F and other formal benchmarks as the relevant process-level evaluation paradigm.

3 Benchmark Construction

OlymMATH integrates numerical-answer and Lean formal-proof evaluation in a bilingual framework, with construction choices targeting comprehensive assessment and reduced contamination. Its leakage analysis and multi-stage verification support benchmark reliability.

  • Benchmark design: OlymMATH integrates 200 natural-language numerical-answer problems with 150 Lean 4 formalizations in one bilingual benchmark.The design assesses both outcome correctness and reasoning rigor rather than relying on either paradigm alone.
  • Contamination analysis: The 350 problems were curated from printed resources and intentionally excluded online repositories to minimize prior digital exposure.This construction contrasts with benchmarks sourced from well-known competitions and online repositories.
  • Contamination analysis: Leakage risk is estimated by comparing n-gram accuracy on original problems with three LLM-rewritten versions using the normalized difference δ.Relative δ comparisons across benchmarks are required because its absolute value depends on the rewriting model.
  • Contamination analysis: OlymMATH exhibits lower δ values than PolyMath per language, indicating lower contamination risk.The comparison is reported in the leakage-analysis results and caption.
  • Verification: Each EASY and HARD problem was reviewed by at least two expert reviewers, while LEAN items underwent multiple independent checks and Lean-server verification.The review process covered problem solutions, translation accuracy, statement precision, and formal solution rigor.
  • Problem composition: The benchmark spans algebra, geometry, number theory, and combinatorics.These are the four high-school Olympiad mathematical fields used to classify OlymMATH problems.

EASY HARD LEAN

OlymMATH spans four mathematical domains and combines bilingual computational evaluation with Lean-based formal verification. Its design emphasizes objective answer checking, challenging multi-answer reasoning, and expert-verified translation.

  • Category distribution: Algebra, geometry, number theory, and combinatorics form OlymMATH’s four core categories.The category distribution covers topics including inequalities, solid and analytic geometry, Diophantine equations, graph theory, and permutations.
  • Benchmark subsets: OlymMATH-EASY and OlymMATH-HARD contain computational problems, while OlymMATH-LEAN provides 150 Lean 4 formalizations for process-level verification.The computational subsets target standard and advanced reasoning, respectively.
  • Answer verification: Computational answers are restricted to real numbers and intervals, enabling objective SymPy-based and Lean server verification.Ambiguous formats such as set operations, variables, complex numbers, and text are excluded.
  • Reasoning demands: Multiple-answer problems require models to summarize all possible outcomes, testing whether they account for complete solution sets.Examples include reporting sums or sums of squares across potential answers.
  • Bilingual construction: Chinese-origin problems receive English translations through model-assisted refinement and verification by two expert annotators.The pipeline targets mathematical accuracy and linguistic fluency, and Lean problems also include bilingual natural-language statements.

4 Experiments

The experiments evaluate leading reasoning models on bilingual numerical-answer subsets using repeated sampling, consensus metrics, and objective verification. Results show substantial difficulty and a consistent advantage for English over Chinese evaluation.

  • Experimental setup: The evaluation covers representative open-source reasoning models and reports OlymMATH results for English and Chinese versions.The main text presents representative models, with full results deferred to the appendix.
  • Experimental setup: 64 responses are generated per problem for most models, while resource-intensive models receive 8 samples because of computational constraints.Pass@1 averages sampled-response accuracy, whereas consensus metrics use majority voting.
  • Bilingual comparison: Figure 2 compares Pass@1 on English and Chinese problems against a parity line, with points above the line favoring English.Solid circles represent local dense models colored by size, while diamonds represent MoE or closed-source models.
  • Evaluation results: 31.2% and 58.4% are achieved by OpenAI o3-mini (high) and Gemini 2.5 Pro Exp, respectively, on OlymMATH-HARD (EN).The authors interpret these results as evidence of the benchmark’s high overall difficulty.

OlymMATH-HARD OlymMATH-EASY

OlymMATH evaluates numerical-answer and formal-proof reasoning through difficulty comparisons, sampling-based robustness, bilingual analysis, and Lean verification. Results show substantial difficulty, English advantages, heuristic failures, and low formal-proof success.

  • Bilingual performance: All models tend to perform better on English than Chinese versions, potentially because English corpora dominate pre-training data.The bilingual comparison identifies a consistent cross-lingual reasoning gap.
  • Sampling robustness: Increased sampling raises the 7B model from 11.1% Pass@1 to 74.0% Pass@64 on EN-HARD, but Cons@64 remains 22.0%.The gap indicates that correct solutions may be found across attempts without reliable consistency.
  • Cross-benchmark difficulty: The benchmark comparison establishes the difficulty hierarchy HARD ≫ EASY ≈ AIME24 > OlympiadBench, while OlymMATH-HARD remains more challenging than Omni-MATH.OlymMATH-EASY produces nearly identical DeepSeek-R1 scores to AIME24: 79.8% versus 79.6%.
  • Reasoning patterns: Heuristic strategies can fail on OlymMATH-HARD: a symmetry assumption produced 3081 instead of the correct 2625.The benchmark is designed so that difficult reasoning steps are hard to bypass through empirical guessing.
  • Formal verification: OlymMATH-LEAN requires machine-verifiable Lean 4 proofs, complementing numerical evaluation by enforcing rigorous step-by-step reasoning.Formal verification is presented as a way to detect reasoning gaps that final-answer checks may miss.
  • Lean evaluation: OlymMATH-LEAN scores remain around 10% versus around 80% on miniF2F; DeepSeek Prover V2 7B reaches 6.40% Pass@1, while Kimina Prover 8B reaches 14.00% Pass@32.Geometry performs best across subjects, whereas combinatorics is most difficult; extraction, compilation, and server errors further affect results.

5 Conclusion

OlymMATH unifies bilingual natural-language evaluation and formal theorem proving in a 350-problem Olympiad-level benchmark. Experiments show substantial challenges for state-of-the-art models, cross-lingual performance gaps, and heuristic guessing behaviors, while released resources support further research.

  • OlymMATH is a 350-problem bilingual benchmark combining numerical-answer evaluation with Lean-based formal theorem proving.Its EASY and HARD subsets support scalable outcome evaluation, while LEAN supports rigorous process-level verification.
  • The benchmark exposes substantial challenges for state-of-the-art models, consistent cross-lingual performance gaps, and heuristic guessing that bypasses rigorous reasoning.
  • OlymMATH-LEAN may support process-level reward models using formal proofs as ground-truth labels for reasoning rigor.The proposed direction includes penalizing unjustified heuristic shortcuts during reinforcement learning training.
  • The release of 582k reasoning trajectories and the OlymMATH-demo tool enables community analysis of reasoning patterns without new model evaluations.

Limitations

The benchmark’s scope is limited by its language coverage, text-only problem format, qualitative treatment of heuristic shortcuts, and the possibility of future data leakage.

  • Language coverage: The benchmark evaluates reasoning in English and Chinese, leaving other languages unexplored.Extending the benchmark to additional languages is proposed for broader multilingual assessment.
  • Input modality: The current benchmark focuses on text-based problems, with geometry reformulated into natural-language descriptions rather than retaining original diagrams.Adding original diagrams and figures would support evaluation of multimodal vision-language models.
  • Reasoning analysis: The proportion of heuristic shortcuts in natural-language evaluation is not yet precisely quantified.The paper identifies guessing through qualitative case studies and leaves scalable shortcut metrics for future work.
  • Contamination: No static benchmark can permanently avoid data leakage after public release.The authors state that their methodology delays contamination compared with web-sourced benchmarks but cannot eliminate it permanently.

A.1 Usability and Accessibility

OlymMATH provides an interactive tool and released data for inspecting model reasoning, while its Lean formalization workflow iteratively validates compilable problem statements and proofs.

  • Usability and accessibility: OlymMATH-demo compares two LLMs on the same rendered problem, visualizes per-problem accuracy, and exposes individual reasoning samples.The tool also provides reference answers, correctness information, extracted answers, and token counts.
  • Usability and accessibility: The visualization tool includes standard solutions for difficult problems and supports local deployment for error diagnosis and model development.These features make individual failures and challenging areas easier to inspect.
  • Lean formalization workflow: The Lean formalization agent reads a mathematical problem and proof, creates a one-sorry formalization and a complete solution, and refines both through lean-server validation.The workflow requires compilation without errors for the formalization and without errors or warnings for the complete solution.
  • Demonstrations and case studies: The demonstrations include geometry, sequence, and functional-equation examples, plus a case where o3-mini found a correct answer without rigorously solving the problem.The examples illustrate both benchmark problem types and the targeted analysis of reasoning behavior.
Loading 2503.21380v3…