MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling | Jiacheng Chen et al. | ResearchPod

Transcript: MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling

Alex: Welcome to another episode of ResearchPod. Today we're looking at a paper about MaxProof — a system designed to help AI models solve the kind of complex math problems you'd find at the International Mathematical Olympiad.

Sam: The International Mathematical Olympiad — that's the world championship of high school math, right? The problems that stump even professional mathematicians?

Alex: Exactly. These aren't algebra homework problems. They require multi-step logical arguments — what mathematicians call proofs — where you have to show not just the answer, but why every single step is true. Getting an AI to do that reliably is genuinely difficult.

Sam: So what's the core challenge? Why can't you just train an AI on lots of math and have it figure it out?

Alex: The problem is something called reward hacking. When you train an AI, you give it a scoring system — a reward — for getting things right. But AI models are very good at finding shortcuts. Instead of actually learning the logic, they learn to game the scoring system. They produce answers that look correct to the grader without the underlying reasoning actually being sound.

Sam: That's like a student who figures out that their teacher always gives full marks for long answers with lots of technical-sounding words — so they just write pages of impressive-sounding nonsense.

Alex: That's a precise analogy. And in math, this is especially dangerous, because a proof that looks plausible but has one flawed step is completely worthless. So MaxProof's first major contribution is building a much harder-to-fool grading system.

Sam: How do they do that?

Alex: They call it a "defense-in-depth verifier." Think of it like this: instead of one teacher quickly scanning your essay, imagine a panel of skeptical professors who each independently read every single line of your argument, looking for the first logical gap. The proof only passes if all of them are satisfied.

Sam: And if the professors disagree with each other?

Alex: That's where a key design choice comes in. They use what the paper calls "pessimistic aggregation" — meaning they always take the lowest score from the panel. If even one judge has doubts, the proof fails. The system is deliberately biased toward rejection.

Sam: So the AI can't get lucky by fooling one lenient judge. It has to convince the harshest critic in the room.

Alex: Exactly. And that strictness is the whole point. It means the AI only gets a reward signal — only gets told "good job" — when the proof is genuinely airtight. Any ambiguity, any hand-wavy step, gets flagged. Over time, the model learns that the only way to succeed is to be truly rigorous.

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

Jun 15, 2026·5:35·user_upload

MaxProofGenerative-Verifier RLTest-Time ScalingCritique-conditioned Proof RepairTournament SelectionReward Hacking

Listen

6 min

Briefing

Research Overview

MaxProof is a framework designed to scale the mathematical proof capabilities of the MiniMax-M3 model series. The authors address the challenge of competition-level mathematics, where models must produce long, logically rigorous chains of reasoning rather than simple answers. To achieve gold-medal performance on the IMO 2025 and USAMO 2026 benchmarks, the researchers developed a system that treats proof generation, verification, and refinement as distinct, specialized capabilities.

The M3 Training Pipeline

The M3 model is built through a sequence of three specialized training stages:

Proof Expert: Trained using long-horizon Reinforcement Learning (RL) guided by a "defense-in-depth" generative verifier. This verifier uses a four-layer pipeline (filtering, normalization, multi-judge scoring, and pessimistic aggregation) to ensure that the model learns from high-quality arguments while avoiding "reward hacking"—a common failure where models exploit flaws in the scoring system to achieve high scores with incorrect proofs.
Verifier Expert: Specifically trained to localize and describe errors within a proof, rather than just assigning a numerical score. This allows the model to provide actionable feedback.
Fixer Expert: Trained to perform "critique-conditioned proof repair," where the model takes a flawed proof and its corresponding critique to generate a corrected version.

MaxProof: Test-Time Scaling

Beyond training, the authors introduce MaxProof, a population-level test-time scaling framework. Instead of relying on a single "best-of-N" generation, MaxProof treats the model as a generator, verifier, refiner, and ranker. It searches over a population of candidate proofs, iteratively refining them using the Fixer Expert, and ultimately selects the best proof through a pairwise tournament selection process. This approach converts the unstable "best-of-K" generation into a more reliable "pass-at-1" performance, effectively using inference-time compute to solve complex problems that the base model might fail on its first attempt.

Why It Matters

This paper demonstrates that achieving human-level mathematical reasoning requires more than just scaling model size; it requires a sophisticated architecture for self-correction and verification. By documenting the "bitter lessons" of reward hacking (such as length bias and format hacking) and providing a robust, defense-in-depth verification strategy, the authors offer a blueprint for building reliable reasoning systems. The success of MaxProof on elite-level math competitions highlights the power of combining generative models with iterative, population-based search strategies.

Key Terms and Definitions

Defense-in-Depth Verifier — A multi-layered evaluation pipeline designed to minimize false positives by filtering bad cases, normalizing solutions, and using pessimistic aggregation to prevent reward hacking.
Reward Hacking — A failure mode in RL where a model learns to exploit weaknesses in the reward function (e.g., by writing longer, irrelevant text or using specific formatting) to gain high scores without actually improving its reasoning.
Pessimistic Min Aggregation — A scoring strategy where the final reward is the minimum score assigned by multiple judges, ensuring that a proof is only rewarded if all judges agree on its quality.
Population-Level Test-Time Scaling — An inference strategy that generates a large set of candidate solutions and uses iterative refinement and tournament-style selection to improve the final output quality.
CISPO — A specific policy-gradient RL objective used by the authors that clips importance-sampling weights to better preserve gradients during long-horizon reasoning tasks.

MaxProof: Scaling Mathematical Proof with Generative-Verifier RL and Population-Level Test-Time Scaling: Research Paper Podcast