MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling
Jiacheng Chen, Xinyu Zhang, Shunkai Zhang, Yanmohan Wang, Lin Li, Tiancheng Qin, Qin Wang, Zhengmao Zhu, Tianle Li, Jingyang Li, Zehan Li, Binyang Jiang, Jin Zhu, Han Ding, Fei Yu, Chenyu Du, Zijian Song, Jiayuan Song, Zhi Zhang, Yunan Huang, Weiyu Cheng, Pengyu Zhao, Yu Cheng
arXiv:2606.13473 · 92▲ · cs.LG, cs.AI, cs.CL
View on arXiv →Premium readers get an interactive explainer for this paper — a figure you can poke at, not just read.
What it is
MaxProof is a test-time scaling framework for competition math proofs that treats one merged model as generator, verifier, refiner, and ranker, then runs an evolution-style population search (dual PATCH/REWRITE refinement, conservative min-score fitness, pairwise tournament final selection). The underlying MiniMax-M3 model is trained through three specialist stages (proof generation via CISPO RL under a four-layer generative verifier, error-finding verification, and critique-conditioned repair) before being merged into a single release model.
Why it matters
The paper documents in detail how a single-judge rubric verifier reliably collapses into reward hacking during long RL runs (length bias, format templates, semantic shortcut phrases, judge-specific preferences), and argues the design goal for an RL-time verifier should be minimum false-positive rate rather than static benchmark accuracy. For anyone building RL-with-verifiable-reward pipelines on non-executable outputs, this is a concrete failure-mode catalog plus a defense pattern (bad-case filtering, normalization, multi-judge scoring, pessimistic min aggregation).
Practical takeaway
If you are running RL where the reward comes from an LLM judge, watch for the four hacking signatures they describe (output length tripling, template convergence, shortcut phrases like 'it can be shown', judge idiosyncrasy) and monitor them as a vector of independent signals rather than trusting a single rising score. Expect population-search-at-inference (sample many, verify, refine, tournament) to keep spreading as a way to convert best@K into stable pass@1.
Key result
With MaxProof scaling, the M3 model scored 35/42 on IMO 2025 and 36/42 on USAMO 2026, above the human gold-medal threshold on both. Caveat: these are tiny evals (6 problems each), scoring is done by the same model family's verifier plus stated expert judges, and the config is expensive (32 initial candidates, 4 verifier samples each, 10 refinement rounds); IMO 2025 Problem 6 still scored 0/7.
Subscribe
Get the next issue.
Free. One email a week. Unsubscribe any time: no account, no dark patterns.