Let's start with a seemingly simple question:
"Please prove the Pythagorean theorem."
If you ask ChatGPT, it may produce a plausible-looking explanation, complete with a diagram. But if you follow up with: "Is every step of your proof strictly grounded in mathematical axioms? Is the notation used correctly? Is the logical chain complete?"—things get complicated.
This is precisely the fundamental challenge AI faces in mathematical reasoning today: generating an answer that looks right is easy; generating a rigorously correct mathematical object is extremely hard.
The latest research from Meta FAIR (yes, the team behind LLaMA) has built a mathematical reasoning benchmark suite called Principia. Their findings are sobering: even today's most powerful models—Qwen3-235B and OpenAI's o3—struggle on this benchmark.
---
1. Why Does Reasoning over Mathematical Objects Matter?
The Uniqueness of Mathematics
Mathematics is different from other domains. In general text generation, "approximately correct" is often good enough. In mathematics, however, small errors compound catastrophically. A single wrong symbol or a skipped logical step can collapse an entire proof.
The endpoint of mathematical reasoning is not an "answer" but a rigorously formalized mathematical object—a proof, a formula derivation, a geometric construction, or a sequence of symbolic computations. Such objects must satisfy:
- Syntactic correctness: notation follows formal conventions
- Semantic correctness: every step has strict mathematical justification
- Completeness: the logical chain from premises to conclusion has no gaps
- Algebraic derivations: equation solving, inequality proofs
- Geometric constructions: compass-and-straightedge geometric proofs
- Calculus operations: rigorous derivations of limits, derivatives, integrals
- Discrete mathematics: combinatorial proofs, graph theory propositions
- Check syntactic correctness (proper symbol usage)
- Validate the logical chain (whether each step follows from the previous one)
- Compare against reference answers (for equivalence)
- Qwen3-235B: the flagship of the Qwen series
- OpenAI o3: OpenAI's strongest reasoning model
- Symbol misuse: confusing similar symbols (e.g., mixing up ∂ and d)
- Logical jumps: omitting crucial derivation steps—what's "obviously" true isn't obvious
- Missing boundary conditions: ignoring special cases or constraints
- Circular reasoning: unintentionally using the conclusion as a premise
- Compared to baseline models, accuracy in mathematical object generation improves by an order of magnitude
- Formal derivation ability improves substantially while preserving numerical computation ability
- Cross-format generalization: models trained on Principia also improve on traditional numeric benchmarks (like GSM8K)
- Title: Reasoning over mathematical objects: on-policy reward modeling and test time aggregation
- Authors: Pranjal Aggarwal, Marjan Ghazvininejad, Seungone Kim, Ilia Kulikov, Jack Lanchantin, Xian Li, et al.
- Institution: Meta FAIR
- arXiv: 2603.18886
- Published: 2026-03-20
Limitations of Current Evaluation
Existing math benchmarks (like GSM8K and MATH) share a fundamental problem: they are too simplified. Most only require a model to output a final numeric value or pick a correct option. This bypasses the core of mathematical reasoning—formal derivations.
It's like judging a chef solely by a photo of the finished dish, without tasting the food, checking ingredient freshness, or evaluating the cooking process.
---
2. Principia: An Ambitious Effort to Fill the Evaluation Gap
To solve this, the research team built the Principia suite, consisting of three core components:
1. A Specialized Training Dataset
The team constructed large amounts of high-quality mathematical object derivation data. These are not simple "question-answer" pairs but complete derivation trajectories—step-by-step demonstrations of how to build a target mathematical object from initial conditions.
2. Rigorous Benchmarks
Principia tests cover multiple mathematical domains:
Every test item requires the model to output a complete derivation, not just a final answer.
3. Automatic Verification System
To automatically evaluate model outputs, the team developed specialized verifiers that:
---
3. Sobering Experimental Results
The team tested multiple state-of-the-art language models on Principia, revealing an uncomfortable reality.
Even Strong Models "Fall Off the Cliff"
Even today's most powerful models:
performed far below expectations on Principia. They can handle simple numerical computation, but when faced with tasks requiring rigorous formal derivations, error rates rise sharply.
Specific failure modes include:
Limitations of Existing Training Paradigms
The team's analysis identified the root causes of poor mathematical object reasoning in limitations of training data and methods:
1. Data scarcity: high-quality derivation data is rare on the web; most training data consists of "question-answer" pairs without complete derivations
2. Reward misalignment: in reinforcement learning, models are rewarded for "getting the right answer," not "deriving correctly." This teaches models to "guess answers" rather than "reason rigorously"
3. Format mismatch: the simplified formats of existing benchmarks (numeric answers, multiple choice) fail to reflect the true difficulty of reasoning over mathematical objects
---
4. On-Policy Judge Training: A New Way Forward
To tackle these challenges, the team proposed an innovative solution: On-Policy Judge training.
What Is On-Policy Judge Training?
Traditional reinforcement learning typically uses a fixed reward function. But in mathematical reasoning, defining a perfect reward function is nearly impossible—how do you automatically judge whether a mathematical proof is correct?
The team's approach: train a dedicated "judge model" to assess derivation quality.
This judge takes a derivation as input and outputs a quality score. Crucially, the judge is continuously trained on data generated by the current policy model (on-policy), rather than a fixed external dataset.
The Training Pipeline
1. Generation: the policy model produces many derivation attempts 2. Verification: automatic verifiers check correctness, giving binary feedback (right/wrong) 3. Judge training: this feedback trains the judge model to predict whether derivations are correct 4. Policy update: the judge's scores serve as reward signals for optimizing the policy model via reinforcement learning
This cycle iterates continuously, with the policy model and judge model mutually improving.
Validation
Experimental results show On-Policy Judge training delivers significant performance gains:
---
5. Test-Time Compute Scaling: Letting AI "Think More"
Beyond training innovations, the team also explored test-time compute scaling.
The Core Idea
When humans face difficult math problems, they often try multiple approaches, compare different solution paths, and pick the most reliable one. AI can do the same.
The team adopted a generate-and-aggregate framework: 1. Multi-path generation: the model produces multiple independent derivation attempts 2. Quality assessment: the trained judge model evaluates each attempt 3. Aggregation and selection: based on the judge's scores, the most reliable derivation is chosen, or the strengths of multiple derivations are combined
Compute-Performance Trade-off
Experiments show that increasing test-time computation (generating more candidates, performing more evaluations) yields continuous accuracy improvements. This provides empirical support for inference-time scaling—sometimes, letting the model "think a bit longer" is more effective than simply scaling up the model.
---
6. What This Research Means
A Reassessment of AI's Mathematical Ability
The Principia research shows our evaluation of AI's mathematical capabilities may be too optimistic. The simplified formats of existing benchmarks mask the true reasoning challenges. Stricter, more comprehensive benchmarks are needed going forward.
Implications for Training Paradigms
The success of On-Policy Judge training shows that teaching AI to "self-evaluate" is key to improving reasoning. This may not be unique to mathematics—it could apply to other domains requiring rigorous reasoning (programming, legal analysis, scientific derivation).
The Importance of Test-Time Compute
The research also reminds us that training and inference complement each other. Sometimes, rather than training a bigger model, it's better to give existing models more compute at inference time. This offers a new approach for AI deployment in resource-constrained settings.
---
7. Limitations and Future Directions
Current Limitations
1. Limited coverage: Principia currently focuses mainly on elementary mathematics; higher mathematics (algebraic geometry, number theory) is not yet well covered 2. Imperfect verifiers: automatic verifiers still have limits; some complex mathematical objects are hard to verify automatically 3. High compute cost: On-Policy Judge training and test-time aggregation both require substantial computational resources
Future Directions
The team proposed several directions worth exploring: 1. Integration with formal proof assistants: combining with Lean, Coq, and similar tools for fully rigorous mathematical verification 2. Cross-domain transfer: exploring how mathematical reasoning training transfers to other STEM fields (physics, chemistry, biology) 3. Human-AI collaboration: developing AI-assisted mathematical research tools where AI and human mathematicians work together
---
Conclusion
Mathematics is hailed as "the queen of the sciences" because it provides the most rigorous, precise form of knowledge. Enabling AI to master mathematical reasoning is not just a technical challenge—it is an exploration of the nature of AI intelligence itself.
The Principia research tells us: the road to true mathematical intelligence is still long. Current large language models perform impressively but have clear weaknesses in rigorous formal reasoning.
The good news: through innovative training methods (like On-Policy Judge) and inference strategies (like test-time aggregation), we are steadily closing the gap.
Perhaps in the near future, AI will not only help us compute but also help us prove theorems and discover new mathematical structures. That would be another milestone in the history of artificial intelligence.
---
Paper information: