Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad

Ivo Petrov; Jasper Dekoninck; Lyuben Baltadzhiev; Maria Drencheva; Kristian Minchev; Mislav Balunović; Nikola Jovanović; Martin Vechev

Source-linked AI summary

Proof or Bluff? Evaluating LLMs on 2025 USA Math Olympiad

Ivo Petrov, Jasper Dekoninck, Lyuben Baltadzhiev, Maria Drencheva, Kristian Minchev, Mislav Balunović, Nikola Jovanović, Martin Vechev

arXiv:2503.21934v5Mar 27, 2025cs.CL

TL;DR

Numerical-answer benchmarks do not establish whether LLMs can produce rigorous proofs, leaving their performance on complex mathematical reasoning uncertain. The paper evaluates eight state-of-the-art models on six 2025 USAMO problems using repeated generations and expert human grading, finding that performance remains very poor and revealing recurring reasoning failures and training-related artifacts.

Problem
Numerical-answer benchmarks for competitions such as AIME and HMMT do not evaluate the rigorous proof-based reasoning required for many mathematical tasks.
Method
The study evaluates eight state-of-the-art LLMs on six proof-based USAMO 2025 problems using repeated solutions, anonymization, and expert human grading.
Results
Only GEMINI-2.5-PRO scored above 5%, achieving an average score of 24.4% across all problems; the highest average score of any other model was below 5%.
Takeaways & Limitations
Current LLMs remain inadequate for rigorous olympiad-level mathematical reasoning and require substantial improvement in proof-generation capabilities.

Abstract

from arXiv · show

Recent math benchmarks for large language models (LLMs) such as MathArena indicate that state-of-the-art reasoning models achieve impressive performance on mathematical competitions like AIME, with the leading model, Gemini-2.5-Pro, achieving scores comparable to top human competitors. However, these benchmarks evaluate models solely based on final numerical answers, neglecting rigorous reasoning and proof generation which are essential for real-world mathematical tasks. To address this, we introduce a comprehensive evaluation of full-solution reasoning for challenging mathematical problems. Using expert human annotators, we evaluated several state-of-the-art reasoning models on the six problems from the 2025 USAMO within hours of their release. Our results reveal that all tested models struggled significantly: only Gemini-2.5-Pro achieves a non-trivial score of 25%, while all other models achieve less than 5%. Through detailed analysis of reasoning traces, we identify the most common failure modes and find several unwanted artifacts arising from the optimization strategies employed during model training. Overall, our results suggest that current LLMs are inadequate for rigorous mathematical reasoning tasks, highlighting the need for substantial improvements in reasoning and proof generation capabilities.

1 INTRODUCTION

Existing benchmarks show strong numerical-answer performance but do not test rigorous proofs, leaving current reasoning models’ ability on complex mathematical questions uncertain. This study evaluates natural-language proofs on 2025 USAMO problems and finds substantial difficulty.

Numerical-answer competitions such as AIME and HMMT show strong LLM performance but do not require rigorous proof-based reasoning.
Current proof benchmarks either depend on formal verification or cover only limited proof types, while prior full-solution evaluation considered older models and potentially contaminated problems.
The study conducts the first evaluation of LLM natural-language proofs on challenging, proof-based problems from the 2025 USAMO.
Less than 25% was the best-performing model’s average score, while evaluated LLMs exhibited flawed logic, unjustified assumptions, and insufficient creativity.
The findings underscore substantial limitations in current LLMs’ ability to generate rigorous mathematical proofs.

2 METHODOLOGY

The evaluation uses six proof-based USAMO 2025 problems, repeated model generations, anonymized PDF solutions, expert double grading, and standardized partial-credit schemes. Judges also categorized first reasoning failures and logged noteworthy behavioral trends.

2.1 PROBLEM SELECTION AND PREPARATION: Six uncontaminated USAMO 2025 proof problems were selected because they require challenging, detailed solutions for full credit.
2.1 PROBLEM SELECTION AND PREPARATION: Each model solved every problem four times after receiving prompts for comprehensive proofs formatted in LATEX.
2.2 GRADING PROCEDURE: Four expert judges independently evaluated assigned solutions, using instructions and a trial run to support consistent grading.
2.2 GRADING PROCEDURE: Each problem was independently graded by two evaluators, reducing personal bias through a double-grading process modeled on IMO evaluation.
2.2 GRADING PROCEDURE: Standardized problem-specific grading schemes were built from verified community solutions, with each solution scored out of seven points and partial credit available.
2.2 GRADING PROCEDURE: Judges recorded the justification for each partial-credit award while reviewing solutions against the pre-established schemes.
2.3 FAILURE ANALYSIS: Prominent failures were defined as the first incorrect or inadequately explained reasoning and classified as logic, assumption, creativity, or algebra/arithmetic errors.
2.3 FAILURE ANALYSIS: Noteworthy behaviors and trends were systematically logged to identify recurring pitfalls and areas for improvement in model reasoning.

3 RESULTS

The evaluation tested eight reasoning models on 2025 USAMO proofs and found a substantial gap between numerical-answer performance and rigorous proof generation. Gemini-2.5-Pro was the only model above 5%, while automated graders systematically overestimated solution quality.

3.1 MAIN RESULTS: Eight state-of-the-art reasoning models were evaluated on all six 2025 USAMO problems.Each problem was scored out of 7 points, and average scores were computed across four evaluation runs.
3.1 MAIN RESULTS: 24.4% was Gemini-2.5-Pro’s average score across all problems, the only model above 5%.It produced a solution scoring at least 6/7 in six of 24 attempts.
3.1 MAIN RESULTS: Below 5% was the highest average score achieved by every other model, revealing a substantial limitation on rigorous USAMO reasoning.Among nearly 175 solutions from other models, the only perfect score was one GROK 3 attempt on Problem 1.
3.2 FAILURE MODES: Flawed logic was the most common failure category, including unjustified steps, incorrect rationale, and treating crucial proof steps as trivial.O3-MINI frequently skipped essential proof steps despite being among the strongest reasoning models.
3.2 FAILURE MODES: Models generally performed strongly on algebraic and arithmetic computations, although R1 showed notably more errors in these areas.The models performed symbolic manipulations without external computational support.
3.3 AUTOMATED GRADING: Neither O3-MINI nor CLAUDE 3.7 graded solutions accurately; both consistently overestimated quality by awarding credit for incorrect reasoning.The resulting score inflation reached a factor of up to 20.
3.3 AUTOMATED GRADING: Automated scores were lower for FLASH-THINKING and GROK 3 and higher for QWQ, likely reflecting differences in solution multiplicity and clarity.The authors hypothesize that chaotic or multiple solutions confused judges, whereas simpler attempts were easier to evaluate.

4 QUALITATIVE DISCUSSION

The qualitative analysis identifies recurring reasoning artifacts beyond incorrect answers, including answer-boxing, unsupported pattern generalization, fabricated citations, and major variation in clarity. These behaviors reflect mismatches between training incentives and the demands of rigorous proof writing.

Answer Boxing: Answer-boxing often appeared even when USAMO problems did not require a final boxed answer.In Problem 5, QWQ incorrectly insisted the answer was 2 after dismissing non-integer solutions, despite correctly deducing that all even numbers satisfied the conditions.
Generalizing Patterns: Models frequently generalized patterns from small numerical cases without proving that those patterns held generally.This heuristic may help with numerical answers but is fundamentally flawed for rigorous proofs.
Non-Existent Citations: GEMINI-2.5-PRO frequently generated citations to unverifiable or nonexistent theorems and lemmas, especially on difficult problems.All four generations for Problem 6 included citations the evaluators could not verify or locate.
Solution Structure and Clarity: Solution clarity varied substantially: O3-MINI and O1-PRO were generally coherent, whereas FLASH-THINKING and QWQ often produced chaotic responses.GEMINI-2.5-PRO also sometimes boxed entire proofs or exposed thought-process material in final answers.

5 CONCLUSION

The study evaluated eight state-of-the-art LLMs on USAMO 2025 problems and found substantial weaknesses in rigorous mathematical reasoning and proof generation.

Eight state-of-the-art LLMs were evaluated on problems from the USAMO 2025 competition.The evaluation examined mathematical reasoning on high-level olympiad problems.
The best-performing model achieved an average accuracy below 25%.The study reports this result alongside critical failure modes and training-related artifacts.
Reasoning-trace analysis identified flawed logic, unjustified assumptions, and significant artifacts arising from model-training optimization strategies.These failures were observed in the context of rigorous mathematical reasoning required by high-level olympiad competitions.
The findings highlight substantial limitations in current LLM proof generation capabilities.The authors frame these limitations as requiring substantial improvements in proof generation.

A ADDITIONAL EXPERIMENTAL DETAILS

This section documents the evaluation setup, including model configurations, prompts, grading procedures, example schemes, and the six USAMO 2025 problems.

Model Hyperparameters: The evaluation used default or specified reasoning settings, temperature, sampling parameters, and token limits for the tested models.O3-MINI and O1-PRO used high reasoning settings; CLAUDE 3.7 and FLASH-THINKING used a 32000-token reasoning limit, while R1 and QWQ used temperature 0.6 and top-p 0.95.
Prompt: Models were prompted to provide thorough, step-by-step proofs that human judges would assess for accuracy, correctness, and rigor.The prompt explicitly warned against skipping important proof steps and requested LaTeX formatting.
Judge Prompt: Solutions were graded by an expert-mathematician judge according to problem-specific scoring schemes and required rigorous proof steps.The schemes assigned points to concrete components such as closed forms, transformations, bounds, and finishing arguments.
USAMO Problems: The six problems span combinatorial allocation, base-2n digit representations, polynomial roots, geometric games, triangle geometry, and binomial sums.The listed problems require proofs rather than only numerical answers.

C.1.1 EXAMPLE OF LOGICAL ERROR

An example logical error occurs when CLAUDE 3.7 extends a result proved for one index to all indices without justification.

Example of Logical Error: CLAUDE 3.7 generalizes over all indices after proving a statement for only one index.The passage explicitly characterizes this as a leap in logic.
Example of Logical Error: The argument considers two choices for s_k and derives corresponding expressions for σ_j.These choices are s_k = r_m and s_k = r_l, producing σ_j = T_j + r_m · T_{j−1} and σ_j = T_j + r_l · T_{j−1}.
Example of Logical Error: If both expressions vanish for the same index, distinct roots imply T_{j−1} = 0.The argument uses r_m ≠ r_l to obtain this consequence.
Example of Logical Error: Continuing the implication would force all T_j to zero, contradicting T_0 = 1.This contradiction supports the existence of a choice of s_k for which all σ_j are nonzero.

C.1.2 EXAMPLE OF CREATIVITY ERROR

The creativity-error example contrasts models’ incorrect claim that Bob wins with the paper’s stated result that Alice has an optimal strategy.

Example of Creativity Error: On the two-player Alice–Bob game, O3-MINI and most other models argued that Bob should win from the beginning.The passage states that this conclusion is incorrect.
Example of Creativity Error: The problem can be proven to have an optimal strategy for Alice.This directly contradicts the models’ repeated conclusion about Bob’s victory.
Example of Creativity Error: The stated proof strategy instead shows that Bob can place cities so the road network fails at least one of Alice’s two winning conditions.Alice wins only if the network is connected and has no crossing roads.

C.1.3 EXAMPLE OF ASSUMPTION ERROR

The example illustrates an incorrect geometric assumption: O3-MINI implicitly treated C as external to the circumcircle of AFP, although that condition is false.

C.1.3 EXAMPLE OF ASSUMPTION ERROR: O3-MINI incorrectly assumed that C is external to the circumcircle of AFP.The assumption was not stated explicitly and undermined the geometric reasoning.

C.1.4 EXAMPLE OF ALGEBRAIC/ARITHMETIC ERROR

The examples show arithmetic mistakes and invalid combinatorial reasoning, including an incorrect divisibility calculation and misapplied matching arguments.

C.1.4 EXAMPLE OF ALGEBRAIC/ARITHMETIC ERROR: 3,395,016 is divisible by 8, contradicting R1’s incorrect sum calculation.The example identifies the correct value and its divisibility explicitly.
C.1.4 EXAMPLE OF ALGEBRAIC/ARITHMETIC ERROR: 1,894,391 / 8 = 236,798.875 is not an integer, so k = 4 fails for n = 7.Testing n through 6 suggested integrality, but n = 7 provides a counterexample.
C.1.4 EXAMPLE OF ALGEBRAIC/ARITHMETIC ERROR: The matching setup requires disjoint choices A_i, but the stated neighborhood bound only gives |N(X)| ≤ n|X|.The text explicitly notes that this is not Hall’s theorem directly and requires further investigation.
C.1.4 EXAMPLE OF ALGEBRAIC/ARITHMETIC ERROR: The flow approach is left incomplete because the construction does not establish the required max flow or valid conclusion.The response itself says further investigation is needed to construct the correct argument.

C.3 QWQ BOXES AN INTEGER

The examples show models forcing mathematical solutions into inappropriate answer formats and making unsupported generalizations, while one polynomial argument reaches the stated conclusion through contradiction.

C.3 QWQ BOXES AN INTEGER: QWQ treated the solution set of all positive even integers as requiring one integer answer.The correct solution is all even positive integers, not merely the minimal value 2.
C.3 QWQ BOXES AN INTEGER: The boxed-answer convention encouraged reporting 2 even though the complete answer is every positive even integer.The passage distinguishes the expected minimal boxed answer from the mathematically complete solution.
C.3 QWQ BOXES AN INTEGER: FLASH-THINKING tested one explicit polynomial before generalizing its conclusion to all polynomials.This is identified as an unsupported transition from a special case to a universal claim.
C.3 QWQ BOXES AN INTEGER: For P(x) with roots 1, 2, ..., n, the divisor Q(x)=(x−1)(x−2)···(x−k) has every coefficient nonzero.The elementary symmetric polynomials of the positive roots are positive, so each coefficient is nonzero.
C.3 QWQ BOXES AN INTEGER: This divisor contradicts the assumed zero coefficient-product condition, proving that P(x) has a nonreal root.The contradiction refutes the assumption that all roots of P(x) are real.
C.3 QWQ BOXES AN INTEGER: GEMINI-2.5-PRO also boxed an entire proof rather than presenting a clear final result.The example identifies this as part of broader clarity and structure problems.