PaperlayerView exact revision on arXiv

Source-linked AI summary

Winning Gold at IMO 2025 with a Model-Agnostic Verification-and-Refinement Pipeline

Yichen Huang, Lin F. Yang

arXiv:2507.15855v4cs.AI

TL;DR

LLMs perform well on many mathematical benchmarks but struggle with Olympiad problems requiring novel, rigorous proofs. The paper develops a model-agnostic verification-and-refinement pipeline and evaluates it with three leading models. It solves 5 of 6 IMO 2025 problems, while remaining limited by a consistent failure on Problem 6 and by verifier errors.

  • Problem

    Olympiad-level problems require difficult, novel, multi-step reasoning and complete rigorous proofs, exposing weaknesses in current LLM mathematical reasoning.

  • Method

    The paper uses a model-agnostic pipeline that generates solutions, performs self-improvement, verifies them through bug reports, and iteratively refines or accepts them.

  • Results

    5 out of 6 IMO 2025 problems were solved, approximately 85.7% accuracy, versus best-of-32 baselines of 31.6% for Gemini 2.5 Pro, 21.4% for Grok-4, and 38.1% for GPT-5.

  • Takeaways & Limitations

    The results indicate that methodology for harnessing base models can substantially improve automated reasoning on complex Olympiad mathematics.

  • Takeaways & Limitations

    The pipeline failed on IMO 2025 Problem 6 across all three base models, and its verifier can make mistakes without quantitative effectiveness results.

Abstract

from arXiv · show

The International Mathematical Olympiad (IMO) is widely regarded as the world championship of high-school mathematics. IMO problems are renowned for their difficulty and novelty, demanding deep insight, creativity, and rigor. Although large language models perform well on many mathematical benchmarks, they often struggle with Olympiad-level problems. Using carefully designed prompts, we construct a model-agnostic, verification-and-refinement pipeline. We demonstrate its effectiveness on the recent IMO 2025, avoiding data contamination for models released before the competition. Equipped with any of the three leading models -- Gemini 2.5 Pro, Grok-4, or GPT-5 -- our pipeline correctly solved 5 out of the 6 problems ($\approx$85.7% accuracy). This is in sharp contrast to their baseline accuracies: 31.6% (Gemini 2.5 Pro), 21.4% (Grok-4), and 38.1% (GPT-5), obtained by selecting the best of 32 candidate solutions. The substantial improvement underscores that the path to advanced AI reasoning requires not only developing more powerful base models but also designing effective methodologies to harness their full potential for complex tasks.

1 Introduction

The IMO tests difficult, novel mathematical reasoning through rigorous proofs, exposing weaknesses in current LLMs. The paper presents a model-agnostic refinement pipeline and reports strong results across leading models and an independent benchmark.

  • Motivation: IMO problems combine exceptional difficulty, rigorous proof requirements, and systematic novelty, making them a demanding benchmark for genuine mathematical reasoning.The competition spans algebra, combinatorics, geometry, and number theory across two 4.5-hour sessions.
  • Motivation: Current state-of-the-art models often fail to produce sound, rigorous Olympiad proofs, committing logical fallacies or relying on superficial heuristics.Recent USAMO 2025 and IMO 2025 evaluations found that models consequently failed to win even a bronze medal.
  • Positioning: The approach remains in the natural-language paradigm, producing human-readable proofs rather than Lean-verified formal proofs.The paper positions readability as useful for mathematicians to understand, critique, and build upon AI reasoning.
  • Contribution: The paper constructs a model-agnostic verification-and-refinement pipeline evaluated with Gemini 2.5 Pro, Grok-4, and GPT-5 on IMO 2025.Using recent competition problems helps mitigate data-contamination concerns for models released before the event.
  • Results: 5 out of 6 IMO 2025 problems were solved, approximately 85.7% accuracy, compared with best-of-32 baselines of 31.6% for Gemini 2.5 Pro, 21.4% for Grok-4, and 38.1% for GPT-5.The baseline figures come from an independent MathArena evaluation using 32 generated solutions per problem and model selection.
  • External validation: An independent IMC 2025 evaluation reported 94.5% accuracy for the Gemini agent, versus 57.7% for Gemini 2.5 Pro alone.The agent ranked #3 among 434 human participants, while the base model ranked #92, on the more knowledge-intensive benchmark.

2 Methods

The pipeline repeatedly generates, improves, verifies, and selectively accepts mathematical solutions. Its verifier classifies errors and gaps, while repeated checks and review are intended to make refinement robust to verifier mistakes.

  • 2.1 Pipeline: The pipeline generates an initial solution, performs self-improvement, verifies it, reviews the bug report optionally, and iteratively corrects or accepts the result.The high-level procedure contains six steps, ending in acceptance or rejection.
  • 2.1 Pipeline: Multiple independent or serial runs are used to obtain a correct solution, with the model allowed either to produce one or report failure.The procedure can be run some number of times in parallel or serially.
  • 2.2 Solver: Self-improvement addresses the limited reasoning budget of single queries, which can be exhausted before a typical IMO problem is solved.Gemini 2.5 Pro permits up to 32,768 thinking tokens, and Step 1 almost always uses that budget.
  • 2.3 Verifier: The verifier checks solutions step by step and classifies issues as critical errors or major and minor justification gaps.Critical errors are demonstrably false claims or clear logical fallacies; major unrepairable gaps can invalidate an entire proof.
  • 2.3 Verifier: Bug reports explain detected issues so the solver can repair errors or fill gaps, while optional review can remove issues reported incorrectly.The solver is also instructed to review each bug-report item and revise when it disagrees.
  • 2.3 Verifier: Critical errors are seldom missed, but the verifier can report noncritical issues and make mistakes, so the pipeline relies on repeated verification.A solution is accepted only after passing five verification runs.

3 Experiment Setup

The pipeline uses solver and verifier prompts to produce rigorous mathematical solutions, review them step by step, and refine them while explicitly handling errors and justification gaps.

  • Solver instructions: The solver is instructed to provide a complete, step-by-step proof with every statement logically justified.The required output excludes internal commentary, alternative approaches, and failed attempts.
  • Solver instructions: The model must review its method sketch and detailed solution before finalizing the response.The self-correction check requires a clean, rigorous argument in which every statement contributes directly to the final proof.
  • Verifier instructions: The verifier generates an explained bug report that guides correction, with an optional review step for deleting false issue reports.Critical errors invalidate the current line of reasoning, whereas justification gaps are assumed true temporarily before subsequent steps are checked.
  • Verifier instructions: The required verification output contains a summary with a final verdict and findings, followed by a detailed step-by-step verification log.Findings must quote the relevant location and classify each issue as a Critical Error or Justification Gap.

4 Results and Discussion

Across IMO 2025 and the IMC 2025, the pipeline generated rigorous solutions and substantially outperformed baseline generation, while one difficult combinatorial problem remained unsolved across all three models.

  • Performance on IMO 2025: 5 out of 6 IMO 2025 problems were solved by the pipeline with Gemini 2.5 Pro, Grok-4, and GPT-5.Complete verbatim proofs from each model are provided in Appendix A.
  • Performance on IMO 2025: Problem 6 remained unsolved across all three base models because the attempted lower-bound proof relied on an incorrect premise about tile placement.The flawed premise claimed every tile lies entirely to the left or right of two uncovered squares, but a tile can span both regions across different rows.
  • Performance on IMO 2025: 31.6% for Gemini 2.5 Pro, 21.4% for Grok-4, and 38.1% for GPT-5 were the IMO 2025 baseline accuracies under best-of-32 selection, versus approximately 85.7% with the pipeline.The comparison is presented as evidence that iterative refinement addresses limitations of single-pass generation.
  • Discussion: The verifier-guided loop was essential for eliciting rigorous and trustworthy arguments from the models.The authors connect this result to converting powerful models’ latent capabilities into sound mathematical proofs.
  • Generalization to Undergraduate Mathematics: 94.5% accuracy placed the independently evaluated Gemini agent at rank #3 among 434 IMC 2025 human participants, versus 57.7% and rank #92 for base Gemini 2.5 Pro.The IMC provides a benchmark requiring complete rigorous proofs in undergraduate mathematics.
  • Generalization to Undergraduate Mathematics: The IMC evaluation supports applicability beyond IMO-style problems and mitigates data-contamination concerns because the competition followed the code’s public release.The evaluation was conducted independently by MathArena using the public implementation.

5 Outlook

The paper proposes extending the pipeline with more powerful model variants and with collaboration among multiple models, but current access and evaluation controls constrain these directions.

  • Future model variants: More powerful variants such as Gemini 2.5 Pro Deep Think, Grok-4 Heavy, and GPT-5 Pro were not used because they lack API availability and controllable web search.Without disabling web search, fair evaluation is prevented for problems whose solutions are available online.
  • Future model variants: The authors identify integrating these variants through an API with necessary controls as a next step for automated mathematical reasoning.The proposed direction is explicitly described as computationally intensive.
  • Multi-model collaboration: A proposed multi-model framework would use different leading LLMs collaboratively for solution generation, iterative refinement, and verification.The current implementation instead uses one base LLM as both solver and verifier.

Archival Note

The paper records its evolution from Gemini-only experiments to hint-free, three-model results and preserves solution materials, including a geometric coverage problem and its stated conclusion.

  • Archival Note: The research was developed incrementally across arXiv versions, with its evolution documented for transparency.The archival record distinguishes earlier Gemini-only work from the present expanded version.
  • Archival Note: Version 3 produced hint-free Gemini 2.5 Pro solutions for Problems 1 and 2 at higher computational cost.Only the hints were removed from the prompt, confirming that the pipeline could solve these problems from first principles.
  • Archival Note: Version 4 applied the pipeline to Grok-4 and GPT-5 and generated hint-free solutions for all five solvable problems.This generalization motivated changing the paper title to reflect the pipeline’s broad applicability.
  • Archival Note: Appendix A contains complete hint-free solutions from all three models, while Appendix B archives the original hint-based Gemini solutions for Problems 1 and 2.The appendix text states that only minor formatting corrections were made and that wording, mathematical steps, and logic were unchanged.
  • Problem 1: For the sunny-lines problem, the paper defines sunny lines as those not parallel to the x-axis, y-axis, or x+y=0.The problem asks for possible counts of sunny lines among n distinct lines covering a triangular lattice-point set.
  • Problem 1: The constructions exhibit k = 0, k = 1, and k = 3, while k = 2 is ruled out for n = 3.The impossibility proof uses the fact that a sunny line contains at most two points of P3 and analyzes the non-sunny line.
  • Problem 1: For n ≥4, any n-line cover must contain x = 1, y = 1, or x+y = n+1.This key lemma supports the induction that preserves the possible-value set across n.
  • Problem 1: For every n ≥3, the stated possible values of k are {0, 1, 3}.The argument establishes K3 = {0, 1, 3} and then uses K_n = K_{n−1} for n ≥4.

A.1.2 Solution by Grok-4

The proof establishes by induction that the possible numbers of sunny lines covering S_n are exactly {0, 1, 3} for every n ≥3.

  • Base case: The base case S_3 admits exactly k = 0, 1, and 3 sunny lines.Constructions establish achievability, while a case analysis rules out k = 2.
  • Inductive step: For n ≥4, any cover must contain a full boundary side among x = 1, y = 1, or x + y = n + 1.Without a full side, n lines cover at most 2n boundary points, fewer than the 3n −3 boundary points.
  • Inductive step: Removing a full boundary side reduces the uncovered region to S_n−1 and preserves the number of sunny lines among the remaining lines.The construction can therefore be repeated inductively.
  • Constructions: All three values remain achievable for every n by recursively extending the base configurations with non-sunny boundary sides.The recursive constructions produce k = 0, 1, and 3.

A.1.3 Solution by GPT-5

The proof reduces covers of S_n to three-line covers of S_3 by repeatedly removing forced non-sunny boundary sides, then transfers the base-case classification to all n ≥3.

  • Boundary lemma: A boundary-counting lemma forces every cover of S_m by m lines, for m ≥4, to include x = 1, y = 1, or x + y = m + 1.The triangle boundary has 3m −3 lattice points, while non-side lines cover at most 2m of them.
  • Peeling: Iterative peeling removes at least n −3 non-sunny boundary sides and leaves three lines covering a translate of S_3.Translations preserve slopes and therefore preserve sunny versus non-sunny status.
  • Base case: The only sunny pairs among points of S_3 are three disjoint pairs, and no sunny line contains three points.Their slopes are 1, −1/2, and −2.
  • Base case: Three-line covers of S_3 realize t ∈{0, 1, 3}, while exactly two sunny lines are impossible.Together these propositions classify the base case completely.
  • Conclusion: Therefore, every n-line cover of S_n has k ∈{0, 1, 3}, and explicit constructions achieve each value.The constructions cover the final columns using either zero, one, or three sunny lines.

A.2.1 Proof by Gemini 2.5 Pro

The coordinate proof places the circle centers on the x-axis, derives the relevant circumcenter and orthocenter relations, and verifies the tangency condition algebraically.

  • Coordinate setup: Choosing MN as the x-axis and AB as the perpendicular radical axis gives A = (0, a), B = (0, −a), M = (m, 0), and N = (n, 0).The circle equations imply a^2 = r^2 −m^2 = R^2 −n^2.
  • Coordinates of P and H: The circumcenter P of triangle ACD is obtained from the perpendicular bisectors, while the orthocenter H of triangle PMN satisfies x_H = x_P.The proof also relates the altitude through M to line AD.
  • Coordinates of E and F: The second intersections E and F of AP with the two circles are computed by substituting the line equation into each circle equation.Both coordinates depend on the slope k_AP and the corresponding center coordinate.
  • Circumcircle of BEF: The circumcenter O_ω of triangle BEF satisfies relations obtained from the perpendicular bisector of EF and equal distances to B and E.These relations support the later distance calculation.
  • Tangency verification: The algebra proves T_1 = rR/a and T_1^2 = T_2, exactly matching the squared-distance tangency criterion.Consequently, the line through H parallel to AP is tangent to the circumcircle of triangle BEF.

A.2.2 Proof by Grok-4

A second coordinate proof parameterizes the intersections and the line AP, derives the circumcenter and radius of triangle BEF, and shows that the line through H parallel to AP has equal distance from that center.

  • Coordinate setup: The circles are placed with centers M = (0, 0) and N = (d, 0), while their intersections are A = (m, h) and B = (m, −h).The intersection coordinates satisfy m = (d^2 + r^2 −R^2)/(2d).
  • Construction of P and AP: The points C and D lie on the x-axis in the required order, and the circumcenter P of ACD has x-coordinate p = (d + R −r)/2.This determines the slope parameter s of AP.
  • Intersections and identities: The second intersections E and F are expressed using line parameters u and v, and an auxiliary polynomial identity establishes the key relation Q(p) = 0.The identity supports subsequent center and tangency calculations.
  • Circumcenter of BEF: The circumcenter of triangle BEF has x-coordinate d/2 and y-coordinate (d/2 −m)/s −h.These coordinates follow from the perpendicular bisectors of BE and BF.
  • Tangency: The circumradius equals the distance from the circumcenter to the line through H parallel to AP, proving tangency.The proof explicitly concludes that the line is tangent to the circumcircle of BEF.

A.2.3 Proof by GPT-5

The proof develops geometric identities for the tangency claim and analyzes bonza functions through prime divisibility and congruences, ultimately obtaining the sharp bound c = 4.

  • Geometric setup: The coordinate setup places A at the origin and MN on the horizontal line y = s, with M = (m,s), N = (n,s), and U = n − m ≠ 0.The vector a = AP and its 90° rotation b provide the basis for subsequent calculations.
  • Geometric setup: The circumcircle of BEF exists exactly when the x-coordinate of AP is nonzero.When this coordinate vanishes, E and F coincide; otherwise B, E, and F are noncollinear.
  • Tangency proof: The constructed orthocenter H is characterized by intersecting the vertical altitude through P with the altitude through M perpendicular to PN.The relation td = p_x − m determines the parameter used to express H.
  • Tangency proof: The distance calculation and key identity show that the line through H parallel to AP is tangent to the circumcircle of triangle BEF.The final equality is stated to hold identically.
  • Bonza functions: For bonza functions, prime divisibility forces congruence rigidity, while primes absent from function values satisfy f(q) = 1.The classification reduces the possible prime sets to ∅, {2}, or all primes.
  • Bonza functions: c = 4 is the smallest universal constant because every bonza function satisfies f(n) ≤ 4n and an explicit function attains equality at n = 4.The bound is also achieved for n = 4, 8, 16, … by the exhibited construction.

A.3.3 Solution by GPT-5

The solution classifies bonza functions using prime-divisibility lemmas and separates the identity branch from a 2-adic branch, yielding the sharp bound f(n) ≤ 4n.

  • Structural lemmas: Every bonza function satisfies f(1) = 1, and each prime divisor of f(n) must divide n.These facts follow by applying the divisibility condition at carefully chosen pairs of arguments.
  • Structural lemmas: An odd prime value forces f(b) ≡ b (mod p) for every b, while primes outside the value set satisfy f(q) = 1.This creates strong congruence constraints across the entire function.
  • Classification: If an odd prime occurs as a value, infinitely many odd primes occur and the function is the identity f(n) = n.The proof constructs infinitely many such primes and applies the congruence condition to each fixed n.
  • Classification: In the complementary branch, f(n) = 1 for odd n, every value is a power of 2, and v_2(f(n)) ≤ v_2(n) + 2 for even n.Consequently, f(n) ≤ 2^(v_2(n)+2) ≤ 4n.
  • Sharpness: The extremal construction is bonza and reaches f(n) = 4n for n = 2^s with s ≥ 2, proving that the optimal constant is 4.The conclusion states that f(n) ≤ 4n for every bonza function and that 4 is best possible.

A.4.2 Solution by Grok-4

The sequence problem is analyzed through the sum of the three largest proper divisors, showing that valid infinite orbits eventually stabilize and classifying their possible starting values.

  • Setup: For N with at least three proper divisors, the three largest proper divisors are N/d_2, N/d_3, and N/d_4.Here d_1 < d_2 < … < d_k = N are the divisors in increasing order.
  • Fixed points: The fixed points are exactly the integers divisible by 6 but divisible by neither 4 nor 5.For such N, the three largest proper divisors are N/2, N/3, and N/6.
  • Orbit behavior: Every valid infinite sequence eventually reaches and remains at a fixed point, because non-fixed steps cannot occur indefinitely.The only increasing transitions are the specified 13/12 and 31/30 cases, while trajectories outside the fixed-point regime decrease.

A.4.3 Solution by GPT-5

The divisor-sum analysis establishes the structure and classification of valid infinite sequences, while the supplied final passages introduce the separate inekoalaty game and its parameter-dependent winning-strategy question.

  • Divisor map: For multiples of 6, the map f is determined by divisibility by 4 and 5, yielding the three values 13N/12, 31N/30, or N.The cases depend on whether 4 divides N and whether 5 divides N.
  • Necessary conditions: Odd terms and even terms not divisible by 3 cannot occur in a valid infinite sequence, so every term is divisible by 6.The exclusions rely on strict descent and the resulting parity or divisibility contradictions.
  • Stabilization: No term is divisible by 5, and only finitely many transitions multiply by 13/12; therefore the sequence stabilizes at a fixed point.The fixed point has 6 | N, 4 ∤ N, and 5 ∤ N.
  • Classification: The valid initial values are exactly a_1 = 2^(2t+1)3^b m with t ≥ 0, b ≥ t + 1, and gcd(m,30) = 1.The sequence performs exactly t non-fixed transitions before becoming constant.
  • Inekoalaty game: The inekoalaty game alternates choices by Alice on odd turns and Bazza on even turns under a cumulative square constraint, and asks which λ values give either player a winning strategy.If a player cannot choose a suitable number, the opponent wins; an endless game gives neither player a win.

A.5.1 Solution by Gemini 2.5 Pro

The solution analyzes the threshold cases for λ by bounding the defensive function and comparing Alice’s and Bazza’s strategies. It concludes that Alice wins above the threshold, Bazza wins below it, and the boundary case is a draw.

  • Bazza’s defense: Bazza’s best defense maximizes F by choosing even-turn moves that saturate the quadratic constraint and equalize the relevant variables.The maximization uses monotonicity and equality in Cauchy–Schwarz.
  • Alice’s strategy: Alice can force a win when λ exceeds the critical threshold by choosing a sufficiently large target turn and zeros beforehand.Her winning condition is max(F) < λ(2m −1), and the preliminary zero moves remain valid.
  • Bazza’s winning case: Bazza wins below the threshold because Alice’s optimal survival strategy eventually requires a negative move.Choosing zero on earlier odd turns minimizes the accumulated sum, yet at the decisive turn the admissibility bound forces x2m−1 < 0.
  • Boundary case: At the boundary value, neither player has a winning strategy, and the game can continue indefinitely.Bazza’s defense prevents Alice from satisfying her winning condition, while Alice’s zero strategy prevents Bazza from forcing her loss.

A.5.2 Solution by Grok-4

The solution establishes the same three-way classification of λ using induction on the accumulated even-turn quantities. It constructs winning strategies on either side of the threshold and proves indefinite play at equality.

  • Alice’s victory: Alice has a winning strategy if and only if λ is above the critical value.She plays zeros until a suitable odd turn, then chooses a move that makes Bazza’s next response impossible.
  • Draw: At equality, neither player has a winning strategy and the game continues indefinitely.Alice’s zero moves prevent Bazza from forcing an odd-turn loss, while Bazza’s greedy strategy prevents Alice from forcing an even-turn loss.
  • Bazza’s response: Bazza’s greedy response keeps Q within its legal bound while maximizing the accumulated sum S.The induction shows the maximal even-turn sum is attained when Alice’s prior odd moves are zero and Bazza uses the prescribed response.
  • Bazza’s victory: For λ below the threshold, Alice eventually gets stuck on an odd turn while Bazza continues to move.The zero strategy is Alice’s best hope for survival, but its admissibility bound fails at a sufficiently large turn.

A.5.3 Solution by GPT-5

The solution formalizes the game with cumulative sums and proves bounds by Cauchy–Schwarz and induction. These lemmas yield the threshold classification and, separately, a 2025 grid-tiling result of 4048 tiles.

  • Game classification: Bazza wins below the threshold because Alice eventually has no legal odd-turn move.The proof uses the lower bound on accumulated sums under Bazza’s response strategy.
  • Game classification: Alice wins above the threshold by playing zero on earlier odd turns and then using a decisive odd move.Lemma C shows that the decisive move can force Q2k−1 > 2k, leaving Bazza no legal response.
  • Game classification: At the threshold, both players can avoid losing, so the game is a draw.Alice uses zero odd moves, while Bazza follows Lemma A and remains legal at every even turn.
  • Grid tiling: 4048 tiles are necessary and sufficient for the 2025 × 2025 grid problem.The construction and lower bound both give 2N −2 tiles, which equals 4048 when N = 2025.

B Hint-Based Solutions from Initial Experiments

The hint-based solutions reduce the sunny-line problem to a boundary-free core case, prove the core impossibilities, and extend the constructions to every n ≥3. They also set up an analytic coordinate system for a separate geometry solution.

  • Problem setup: The sunny-line problem asks which values of k can occur when n distinct lines cover Sn.Sunny lines exclude slopes 0, ∞, and −1.
  • Reduction: A principal-boundary-line reduction maps a covering of Sn to one of Sn−1 without changing the number of sunny lines.Repeated application reduces any configuration to a smaller core problem with no principal boundary line.
  • Core impossibility: The core analysis rules out k = 2 for sufficiently large core size through permutation constraints and a final contradiction.The argument first forces j = k −1, then contradicts the allowed range of σ(2).
  • General constructions: For every n ≥3, constructions realize exactly k ∈ {0, 1, 3} sunny lines.Vertical, mixed, and diagonal-based constructions cover Sn with respectively zero, one, and three sunny lines.
  • Analytic geometry: The geometry solution chooses axes along the line of centers and common chord to express the circles analytically.The intersections are placed on the y-axis and the centers on the x-axis.
Loading 2507.15855v4…