Generate, Critique, Repair: The RL Loop Behind a Gold-Medal Proof Model

A single model that generates a proof, critiques its own work, and repairs the flaws scored 35/42 on IMO 2025 and 36/42 on USAMO 2026, both above the human gold-medal threshold. The one-shot version of the same model scored 27 and 26. The gap, 8 to 10 points, is bought entirely at test time by a search loop, and the thing that makes the loop work is a deliberately pessimistic verifier that throws away good proofs to avoid ever rewarding a bad one.

That is the result from “MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling,” from Jiacheng Chen and a large team at MiniMax (with collaborators at Fudan, Peking, and CUHK).

• IMO 2025: 35/42 with MaxProof vs 27/42 one-shot, above the gold cutoff
• USAMO 2026: 36/42 with MaxProof vs 26/42 one-shot, above the gold cutoff
• Test-time search alone adds +8 (IMO) and +10 (USAMO) points
• Standalone benchmarks: 67.40 IMOProofBench, 81.56 IMOAnswerBench
• One merged model, M3, plays generator, verifier, and fixer through prompting, no separate specialist weights

The Three Roles, One Model

MaxProof decomposes proof-writing into three capabilities, all trained into a single set of weights (M3) and switched by prompt:

Proof Expert (generate). Long-horizon RL that produces candidate proofs. The reward signal comes from a “defense-in-depth” generative verifier built as four layers: rule-based filtering of malformed outputs, normalization to strip formatting noise, three parallel judges scoring each candidate, and a final pessimistic-min aggregation that takes the lowest judge score as the reward. The design exists because an earlier single-judge version got hacked four different ways, length inflation (proofs 3x longer), template convergence (80% boilerplate), semantic shortcuts (“after simplification”), and judge-specific pandering. Taking the minimum score means a proof has to convince every judge, which trades some false negatives for far fewer false positives. As the authors put it, RL amplifies high-scoring invalid proofs, so you bias hard against them.

Verifier Expert (critique). Instead of regressing a 0-to-7 score, this role is forced to write a structured assessment: step-by-step analysis, an explicit list of concrete errors, then a verdict (no_errors, minor_gaps, has_errors, fundamentally_wrong). Localizing the error is the point, it produces the feedback the repair step needs, and forces the model to actually read the proof before ruling on it.

Fixer Expert (repair). Critique-conditioned repair trained by rejection sampling. Given the problem, a flawed proof, and the verifier’s error analysis, it rewrites the bad parts while preserving what was correct. A repair only becomes a training example if the same conservative verifier later judges it fully correct, so the model learns from genuine fixes, not partial improvements. The training data falls out of the Proof Expert’s RL run for free: every flawed rollout is a repair example waiting to be used.

Why The Loop Beats One-Shot

At inference, MaxProof runs a population search. It samples 32 candidates, verifies each 4 times and keeps the minimum score (the same pessimism as training), then iterates for up to 10 rounds. Each surviving parent spawns two offspring through complementary operators: PATCH fixes the specific flagged errors while keeping the rest (exploitation), and REWRITE tries a different proof route using summaries of sibling attempts as context (exploration). The loop stops early only when two candidates independently hit a perfect 7/7, and a final pairwise tournament, three ranker votes per matchup, picks the winner when scores cluster.

The reason this beats sampling 32 proofs and praying: the loop amortizes verifier noise across many candidates and feeds structured, localized critique back into targeted repairs rather than blind resampling. The hard IMO problems weren’t solved on round one, they emerged at rounds 7, 10, and 7. The search is doing real work.

Caveats

MaxProof clears the gold threshold on competition scores, but M3 does not lead the standalone benchmarks. On IMOProofBench it scores 67.40, behind GPT-5.5 (90.85), Gemini 3.1 Pro (75.71), and just ahead of Opus 4.7 (65.85). The authors are blunt that frontier closed models write “concise and essential solutions” one-shot, while M3 needs multi-round search even on routine problems, and they call M3 “still followers chasing the frontier.”

The limits are real. Some problems (IMO 2025 P6) sit outside the base model’s reach entirely, and no amount of search recovers understanding that isn’t there. The pessimistic-min reward that prevents hacking also pushes toward defensive, exhaustive proofs rather than elegant ones. Verifier calibration still wobbles at the correctness boundary, and the ranker sometimes picks a worse candidate when scores are close. And the gains cost compute: those gold-medal answers came from up to 10 rounds of 32-candidate search per problem.

The transferable idea is the architecture, not the leaderboard position. Splitting a hard generation task into generate, critique, and repair, then biasing every reward toward false negatives so RL can’t learn to cheat the judge, turns an unreliable one-shot model into one that clears a human gold-medal bar. The verifier’s conservatism is the load-bearing piece: it’s what lets you trust a search loop built on the model grading itself.