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

International Mathematical Olympiad problems require complete, rigorous proofs of novel problems, under a selection process designed to avoid anything too similar to known problems. Independent grading by MathArena found that leading models in mid-2025 scored 31.6% (Gemini 2.5 Pro), 21.4% (Grok-4) and 38.1% (GPT-5) of the points on IMO 2025, even when each model chose its best answer out of 32 attempts.

This paper argues that the models have more ability than single attempts show, and that a structured loop can draw it out. The pipeline uses one model in every role. Step 1 generates a solution with a prompt that stresses rigor and allows the model to report partial results instead of guessing. Step 2 asks the model to review and improve its own work, which the authors describe as giving it a second budget of reasoning tokens. Step 3 runs the same model as a verifier with a strict grading prompt: it must check every step and list each issue as a critical error or a justification gap. Step 4 optionally reviews the bug report to remove false alarms. Step 5 asks the model to correct the solution using the report, and the loop returns to verification. A solution is accepted when it passes verification five times in a row and rejected after repeated major issues.

With any of the three models the pipeline produced proofs for Problems 1 to 5 and failed Problem 6, a combinatorics problem on a 2025 by 2025 grid; the authors identify the flaw in the failed attempt. Early versions used general hints for Problems 1 and 2 (induction, analytic geometry); later versions solved them without hints at higher cost. The full proofs are printed in the appendix as evidence.

MathArena later ran the authors' public code with Gemini 2.5 Pro on the IMC 2025 university competition, held after the code was released, and scored it 94.5%, compared with 57.7% for the model alone.

The pattern transfers. Generate, critique against a strict rubric, repair and accept only after repeated clean checks is a design you can apply to contracts, financial models, code changes and reports. The paper's prompts are a good template: a verifier that must classify every issue, quote where it occurs and is forbidden from fixing what it finds.

Acceptance rules matter more than prompts. The pipeline accepts only after five consecutive clean verifications. That rule is what turns a fallible checker into a usable gate, as long as its misses are independent. When the same model writes and checks, some of its blind spots are shared, and repeating the check does not remove them. A different model or a deterministic check (tests, a solver, a calculation) as one of the verifiers is the stronger design.

Report cost and attempts. The paper runs the pipeline "some number of times" and does not say how many, or how many tokens were spent per problem. A customer comparing this approach with a single call needs both: success rate and cost per accepted output.

Separate the evaluator from the system. The strongest evidence here is the independent IMC run, not the authors' own IMO claims. For any loop that grades its own work, insist on an outside check on a sample.

Verifier bug reports are useful output. Even when the loop fails, the list of critical errors and gaps tells a reviewer where to look. In professional workflows that can be more valuable than the final draft.