Agents2025~115 minarXiv:2512.10739

Long-horizon Reasoning Agent for Olympiad-Level Mathematical Problem Solving

Songyang Gao, Yuzhe Gu, Zijian Wu +18Dec 11, 2025cs.CL

🎯 Pitch

A gold-medal-level math AI scores 102/126 on the official Chinese Mathematical Olympiad under human expert judgment by breaking through the context-length ceiling that cripples even advanced models on IMO problems: instead of one impossibly long chain of thought, it maintains a compact memory of proven lemmas across multiple reasoning rounds, effectively expanding its working space 8×.

1. Executive Summary

This paper introduces Intern-S1-MO, a long-horizon math agent that solves Olympiad-level mathematical problems by conducting multi-round hierarchical reasoning through an LRM-based multi-agent system comprising reasoning, summary, and verification components. Evaluated on Intern-S1 across benchmarks including IMO2025, AIME2025, HMMT2025, CNMO2025, and CMO2025, the system maintains a compact memory of lemmas to extend effective reasoning context roughly 8× beyond the 64K token limit of conventional LRMs, while the companion OREAL-H framework provides online reinforcement learning with conjugate reward modeling from a process verifier to bootstrap reasoning ability. Intern-S1-MO achieves 26 out of 35 points on IMO2025 non-geometry problems—matching silver medalist performance—and scores 102 out of 126 on CMO2025 under official human-judged conditions, establishing that systematic lemma-based memory management combined with hierarchical RL enables gold medal-level Olympiad reasoning, though the gains are concentrated on problems amenable to structured decomposition rather than those requiring idiosyncratic insight constructions.

2. Context and Motivation

The Core Problem: Context Length Is the Bottleneck for Olympiad-Level Reasoning

The fundamental problem this paper addresses is that large reasoning models (LRMs) cannot think long enough to solve ultra-hard mathematical problems. This is not a capability gap in the colloquial sense—the models possess the requisite knowledge—but rather a hardware-imposed constraint on reasoning depth: state-of-the-art reasoning models typically support a maximum context length of only 64K or 128K tokens, which the authors argue is insufficient for problems like those in the International Mathematical Olympiad (IMO) that require sustained, multi-step deduction.

The paper quantifies this mismatch in Figure 1(a), showing that as problem difficulty increases, both the average human thinking time and the model's token consumption per problem grow exponentially. This is the paper's central observation: LRMs have been getting better at reasoning, and the natural response to harder problems has been to allocate more "thinking budget"—longer chain-of-thought traces, more trial-and-error exploration—but this trend is on a collision course with physical context-length ceilings. The authors frame the dilemma explicitly:

"hardware and data limitations have made unlimited scaling of context length infeasible"

What makes this gap particularly acute for Olympiad-level mathematics is the nature of the reasoning itself. Unlike AIME-level problems, which can often be solved through pattern recognition, heuristic retrieval, or relatively linear chains of deduction, IMO problems require constructing novel proof paths, synthesizing auxiliary lemmas, and exploring multiple reasoning branches before converging on a valid solution. This is not simply a matter of generating more tokens—it requires the model to maintain a coherent logical state across extended exploration, accumulating partial progress (e.g., establishing a necessary inequality, proving a sub-case) and building upon it in subsequent reasoning steps. A single-pass model, even with a long context window, may exhaust its budget on unproductive exploration without the architectural support to organize and reuse intermediate discoveries.

Why This Problem Matters: Practical and Theoretical Significance

The context-length bottleneck has implications at multiple levels:

For mathematical AI research. The IMO represents a pinnacle of human deductive reasoning, and achieving gold medal performance has been a long-standing benchmark for AI systems. Prior to this work, proprietary systems from DeepMind and OpenAI had reported impressive IMO results, but as the authors note, "the research community lacks access to their methodologies and models." By developing an open framework that achieves silver medal performance on IMO 2025 and gold medal on CMO 2025 (102/126, exceeding the gold threshold of 78), Intern-S1-MO provides a reproducible roadmap for the research community. The significance is not merely benchmarking—it demonstrates that structured, multi-agent architectures can push LRMs beyond their single-pass limits.

For the broader scaling narrative. The paper engages with a critical question in the current LLM landscape: is progress on hard reasoning problems primarily a function of scaling model size, or can architectural innovations extend the reach of existing models? The exponential growth curves in Figure 1(a) suggest that brute-force context scaling faces diminishing returns—hardware improvements are linear or sub-exponential, while the token demands of harder problems grow exponentially. This creates what the authors call a "mismatch between the existing capacity limits and practical demands," motivating a search for "cost-effective paradigm[s] to meet context requirements." The paper positions itself as an alternative to the default assumption that bigger models with longer contexts are the only path forward.

For deployment pragmatics. Even if context lengths could be extended indefinitely (e.g., to 512K or 1M tokens), doing so through naive single-pass generation would be computationally wasteful. The authors' approach of maintaining a compact lemma memory effectively achieves roughly 8× the reasoning depth of a 64K context model while avoiding the quadratic attention cost of extremely long sequences. This efficiency argument has direct practical relevance for organizations building mathematical reasoning systems.

Where Prior Approaches Fall Short

The paper identifies several categories of prior work and systematically explains their limitations for IMO-level reasoning:

Single-Round Reasoning with Extended Context

The dominant paradigm in current LRMs—exemplified by models like o3, Gemini 2.5 Pro, and DeepSeek-R1—is to solve problems in a single reasoning pass, even if that pass includes internal iterations, self-correction, or backtracking. The authors acknowledge that these models can achieve impressive results (Table 1 shows baseline scores of 82.5–92.5 on HMMT2025 and 83–92.5 on AIME2025), but they identify a fundamental structural limitation:

"these approaches still confine problem-solving to a single reasoning cycle (even with internal iterations) rather than building cumulatively upon prior reasoning trajectories, which limits their capacity to leverage historical explorations for further in-depth deduction."

The key distinction is between iterative refinement within a single context and hierarchical accumulation across multiple rounds. A model that backtracks and revises within a 64K context window is still operating under a hard token limit; once that budget is exhausted, it must produce an answer regardless of whether the reasoning is complete. The paper observes that this creates a "premature conclusion bias"—when reasoning budgets run out, "models tend to rush toward incomplete or incorrect final answers instead of acknowledging partial progress." In contrast, Intern-S1-MO's multi-round architecture allows each round to make partial progress (proving a lemma, solving a sub-case) and explicitly records that progress for the next round, effectively decoupling the total reasoning depth from any single context window.

Formal Language-Based Search Methods

An important line of work uses formal proof assistants (e.g., Lean, Isabelle) to perform exhaustive or guided search over proof spaces, storing intermediate results in structured repositories. The paper cites Seed-Prover, DeepSeek-Prover-V2, and related approaches as showing "some promise." However, the authors identify three practical limitations:

Computational overhead: "the proof verification and state traversal demand extensive iterations, leading to high computational and search overhead." Formal verification is exact but expensive—each proof step must be checked against the formal system's rules, and the search space can be combinatorially large even with learned heuristics.
Translation costs: "formal systems require translating informal descriptions into formal logic, introducing additional costs." Natural language math problems must be formalized before the system can operate on them, and solutions must be "de-formalized" for human consumption—a non-trivial process that can introduce errors or lose nuance.
Human-interaction barriers: The formalization requirement "hinder[s] the interaction between AI and humans," since the intermediate reasoning is not in natural mathematical language but in formal logic, making it difficult for human mathematicians to inspect, understand, or collaborate with the system.

Intern-S1-MO operates entirely in natural mathematical language (with LaTeX formatting), using learned verifiers rather than formal proof checkers. This is both a strength (flexibility, human interpretability) and a limitation (no ironclad correctness guarantees), and the paper navigates this tradeoff by investing heavily in verifier quality and ensemble verification.

Prompt-Based Self-Reflection and Multi-Agent Interaction

Several works have explored using prompt engineering to induce self-reflection in LLMs, where the model identifies flaws in its own intermediate steps and refines its output. Huang & Yang (2025) applied this approach with Gemini 2.5 Pro for IMO problems. The paper acknowledges these efforts but identifies two critical weaknesses:

Dependence on meticulously crafted prompts: These methods "often depend on meticulously crafted prompts and, at times, hints provided by humans." The performance gains are brittle—they work when the prompt template matches the problem structure but may fail on problems with different characteristics.
Lack of training integration: "training math agents—where exploration and reflection are optimized through learning signals—remains an emerging area." Prompt-based approaches are post-hoc engineering on frozen models; they do not improve the underlying model's ability to decompose problems, extract lemmas, or verify reasoning. The paper's OREAL-H framework addresses this directly by using online RL to train the agent components to perform their roles more effectively.

Additionally, works on multi-agent LLM training (e.g., MALT) and parallel decoding/tree search (e.g., Tree-of-Thoughts, MCTS-based methods) are cited as expanding the search landscape but "often lack depth and struggle to effectively decompose complex problems." The paper's hierarchical decomposition—where the reasoner proposes partial solutions, the summarizer extracts lemmas, and the verifier checks them—is presented as a more structured alternative that mirrors how human mathematicians actually work.

RL for Mathematical Reasoning: Sparse Rewards and Limited Agentic Behavior

The paper provides a targeted critique of reinforcement learning approaches for math agents (Section 2.2):

Outcome-based rewards are too sparse. Most existing RL for mathematical reasoning uses final-answer correctness as the only reward signal. While methods like ARTIST, ToRL, and rStar2-Agent have shown emergent agentic behaviors (adaptive tool use, self-correction), the paper argues that this sparse signal is insufficient for training agents that engage in "strategic planning or deep exploration." On IMO-level problems, the path from problem statement to final answer involves many intermediate decisions—which lemma to prove, which case to analyze, whether to continue exploring or commit to an answer—and outcome-only rewards provide no guidance on these intermediate choices.

Existing agents lack cumulative memory. The paper's most pointed critique is that current math agents "lack summarization and cross-episode awareness. While approaches like TTRL and Satori introduce basic reflection or meta-actions, they operate within isolated reasoning episodes and do not support cumulative knowledge transfer across inferences." This is the architectural gap that Intern-S1-MO's lemma memory directly addresses: the system maintains a structured repository of proven intermediate results that persists across reasoning rounds, allowing each new round to build on the accumulated discoveries of previous rounds rather than starting from scratch.

Process-aware RL is limited to verifiable domains. The paper notes that process-aware RL and verifier-guided training (e.g., Prover-Verifier Games) typically require "intermediate supervision with predefined rules or code execution, and are not well-suited for complex reasoning scenarios." In mathematical proof, there is no execution environment to verify intermediate claims—correctness is a matter of logical entailment, which is precisely what makes formal verification expensive and natural-language verification challenging. The paper's use of a learned process verifier (OPV) that judges the rigor of natural language proofs represents an attempt to provide process-level feedback without the overhead of formal verification.

How This Paper Positions Itself

Intern-S1-MO positions itself at the intersection of several research threads, synthesizing them into a unified framework:

From the multi-agent and hierarchical reasoning literature, it borrows the structure of decomposing complex problems into sub-tasks handled by specialized components (reasoner, summarizer, verifier) but moves beyond prompt engineering by training these components through the OREAL-H RL framework.

From the search and exploration literature, it adopts the idea of maintaining a repository of intermediate results (analogous to the state storage in formal proof search) but operates in natural mathematical language rather than formal logic, using learned verifiers to assess correctness.

From the RL-for-reasoning literature, it inherits the outcome-reward paradigm but extends it with process-level feedback from a verifier and round-level credit assignment through the lemma dependency graph, addressing the sparse-reward problem that limits prior approaches.

From the scaling laws and test-time compute literature (the context of the prior sections of this analysis), it extends the notion of test-time scaling from single-pass generation to hierarchical multi-round reasoning with explicit memory management, demonstrating that architectural innovation can achieve what raw context scaling cannot.

The paper's core claim is not that any individual component (lemma memory, process verification, multi-round reasoning) is novel in isolation, but rather that the integration of these components into a trainable, self-improving system represents a qualitative advance over prior work. The ablation study (Table 2) is designed to support this claim by showing that each component adds incremental value, with the full system (including OREAL-H training) substantially outperforming the initial "single-round with agents" baseline—improving CNMO2025 from 178.0 to 232.4 and HMMT2025 from 70.8 to 95.0.

A subtle but important positioning choice: the paper does not claim to have solved the context-length problem in general. The system extends effective reasoning depth by roughly 8× (from 64K to approximately 512K tokens per problem), but it does not provide unbounded reasoning. The authors are explicit about this limitation in the conclusion, noting that the "remaining deficit largely stems from problems requiring highly idiosyncratic transformations or 'spark-of-insight' constructions that elude systematic search." This honesty about boundary conditions strengthens the paper's credibility—it is not promising a universal solution, but rather a systematic approach that pushes the frontier substantially while acknowledging where it still falls short.

3. Technical Approach

3.1 Reader Orientation

Intern-S1-MO is a multi-agent system where a Large Reasoning Model (LRM) solves ultra-hard math problems by breaking them into smaller, manageable chunks across multiple rounds of reasoning, rather than trying to produce a complete solution in a single marathon thinking session. The core problem it solves is the context-length bottleneck: current LRMs can only sustain about 64K–128K tokens of continuous reasoning before hitting hardware limits, but IMO-level problems require roughly 8× that depth. The solution's shape is a hierarchical reasoning loop—a reasoner agent proposes partial solutions, a summarizer agent extracts proven intermediate results (lemmas) into a compact memory, and a verifier agent checks the logical validity of those lemmas before they're added to the repository, enabling each subsequent round to build on prior discoveries rather than starting from scratch.

3.2 Big-Picture Architecture (Diagram in Words)

The system has five major components that operate in a multi-round loop, as illustrated in Figure 2:

Reasoner Agent—an LRM (Intern-S1 variant) that takes the problem statement plus the accumulated lemma library as input and produces a reasoning trace containing partial or complete solutions. In each round, it tries to prove new lemmas or advance the proof toward the final answer.
Summarizer Agent—an LRM that takes the reasoner's verbose reasoning trace and compresses it into concisely stated, formally formatted lemmas, discarding dead ends, trial-and-error content, and redundant exploration.
Theorem Verifier—a lightweight verification module that, for each proposed lemma, performs multiple parallel verification passes (using a learned verifier) and computes a confidence score representing the proportion of passes that judge the lemma as logically sound.
Lemma Memory—a structured repository that stores all verified lemmas across rounds, serving as a persistent logical state that the reasoner can reference in subsequent rounds. This is the mechanism that decouples total reasoning depth from any single context window.
Process Verifier (OPV) and Revision Loop—in the final round, after a candidate solution is produced, the OPV examines it step by step, identifies logical gaps or errors, and the reasoner revises the solution iteratively (up to 8 rounds) until verification passes or a limit is reached.

Information flow at inference time: The problem enters → Reasoner produces a reasoning trace (Round 1, with only the problem as context) → Summarizer extracts lemmas from the trace → Theorem Verifier scores each lemma → High-confidence lemmas are added to the lemma library → Reasoner generates a new trace (Round 2, now with both the problem and the accumulated lemmas) → This loop repeats for up to 8 rounds → In the final round, the reasoner produces a complete solution → The Process Verifier examines it → Feedback triggers iterative revision → Final answer is output.

During training (OREAL-H): This same pipeline generates trajectories that are scored by the Process Verifier, and the RL framework uses these trajectories—plus rewards computed from the verifier's confidence scores—to update the policy model, improving both the reasoner's ability to generate useful lemmas and the overall solution quality.

3.3 Roadmap for the Deep Dive

First, the multi-round reasoning loop and lemma extraction mechanism (Section 3 of the paper), since this is the core architectural innovation that enables extended reasoning depth and all other components operate within or upon this loop.
Second, the theorem verifier for intermediate lemmas, because lemma quality control is critical for preventing error propagation across rounds—a single flawed lemma can derail all subsequent reasoning.
Third, the Process Verifier (OPV) and final solution revision loop, since this provides the quality guarantee for final outputs and also generates the training signal for RL.
Fourth, the OREAL-H reinforcement learning framework, including the Hierarchical MDP formulation, the lemma dependency graph for credit assignment, the conjugate reward model for noisy process verification, and the cold-start behavioral cloning procedure.
Fifth, the training pipeline and hyperparameters, connecting the algorithmic description to the concrete implementation that produced the reported results.

3.4 Detailed, Sentence-Based Technical Breakdown

This is primarily a systems paper that integrates multiple components—multi-agent reasoning, lemma-based memory, process verification, and hierarchical reinforcement learning—into a unified framework for Olympiad-level mathematical problem solving. The core technical insight is that by decomposing complex reasoning into rounds of partial progress and explicitly storing verified intermediate results, the system can achieve roughly 8× the effective reasoning depth of a single-pass model while avoiding the quadratic attention cost of extremely long sequences.

Multi-Round Hierarchical Reasoning and Lemma Extraction

The fundamental loop. The system operates in discrete reasoning rounds, with a maximum of 8 rounds per problem (Appendix B.1). In each round, the Reasoner Agent receives two inputs: (1) the original problem statement, and (2) the current lemma library—a structured collection of all lemmas that have been verified in previous rounds. The Reasoner's task is to produce a reasoning trace that either solves the problem completely or makes partial progress by proving new intermediate results.

Single-round output structure. The Reasoner's output is highly structured, enforced through a detailed system prompt (Appendix A.1) and reinforced through training. The output contains:

A Summary section with a verdict stating whether the solution is complete or partial, and a method sketch providing a high-level conceptual outline of the logical argument.
A Detailed Solution section containing the step-by-step mathematical proof.
Proven lemmas are explicitly boxed using \boxed{} environments, with each lemma formatted as **Lemma X:** followed by its statement and **Proof X:** with numbered steps. Multiple lemmas are separated by horizontal rules (---).

Partial progress as a design principle. A critical design choice is that the Reasoner is explicitly instructed to produce partial solutions rather than forcing a complete answer. The system prompt states:

"If you cannot provide a complete solution, you must provide any significant partial results that you can prove with full rigor. Do not guess or provide solutions with logical gaps."

This instruction directly addresses the "premature conclusion bias" the authors observed in single-pass models—when reasoning budgets are exhausted, models tend to fabricate incomplete answers rather than acknowledging what they have (and haven't) proven. By training the model to produce well-formed partial results, each round makes genuine logical progress even if the full problem remains unsolved, and that progress is captured for the next round.

Why structured output matters. The structured formatting (boxed lemmas with explicit numbering and step-by-step proofs) is not merely cosmetic—it enables the Summarizer Agent to reliably extract new lemmas from the reasoning trace. Without this formatting, distinguishing between exploratory reasoning, dead ends, and genuine proven results would require the summarizer to perform its own full logical analysis of the entire trace, which the authors note "is as complex as the exploration process itself."

From reasoning trace to lemma library. After each round, the Summarizer Agent (using the prompt in Appendix A.2) analyzes the Reasoner's output and extracts only the new lemmas—those that were proven in the current round and are not already present in the lemma library. The summarizer distinguishes between:

Proven lemmas: propositions with complete (or core) proofs provided in the current round's trace.
Reference lemmas: lemmas from the existing library that are merely cited, not reproved.

The summarizer outputs each extracted lemma in a pair of <lemma>...</lemma> tags with the lemma statement and proof in a standardized format. Importantly, the lemma numbering continues sequentially from the existing library, ensuring a unified namespace across all rounds.

Why a separate summarizer agent? The paper argues that summarizing exploration is inherently difficult—it requires independently assessing logical validity and relevance, not just copying text. The authors dedicate "a dedicated reasoning turn after each exploration step to update the lemma library," explicitly justifying this computational cost: "This computational cost is necessary to ensure the library remains useful for long-chain reasoning." In other words, the summarizer is not a lightweight post-processing step but a full LLM inference that re-reasons about what was actually proven.

Context management and the 8× extension. By storing only the compact lemma statements (not the full verbose reasoning traces) in the memory, each round's context window is dominated by the accumulated mathematical knowledge rather than redundant exploration. The paper states that Intern-S1-MO enables LRMs to use about 512K tokens to solve a single problem, effectively extending the 64K constraint by approximately 8×. This is achieved because the lemma library grows additively with each round (new verified results are appended) while the verbose traces from previous rounds are discarded—only their distilled essence persists.

Adaptive reasoning budget. The system does not blindly run all 8 rounds for every problem. The paper states that Intern-S1-MO "initiates multi-round exploration only for challenging tasks, ensuring efficient resource allocation." While the exact mechanism for deciding when to terminate early is not fully specified, the implication is that if the Reasoner produces a complete solution with high confidence (or if no new lemmas are being generated), the loop can terminate before the maximum round limit.

Theorem Verification for Intermediate Lemmas

The error propagation problem. A central challenge in multi-round reasoning is that a flawed intermediate lemma can "mislead subsequent deductive directions, leading to circular reasoning or invalid proofs." Unlike final answer verification (where a wrong answer is immediately detectable for solution-based problems), an incorrect lemma may appear plausible and get incorporated into the library, where it can poison all subsequent reasoning rounds. The paper frames this as a compounding risk: "if they rely on erroneous historical premises, they will expend significant resources trying to validate questionable results."

Why lemma verification is more tractable than full solution verification. The authors argue that "the verification of lemmas is comparatively more tractable than that of the complete problem" because lemmas are typically shorter, more self-contained logical units whose correctness depends on fewer premises and less context. This is a key design insight: by breaking the verification problem into smaller pieces (individual lemmas rather than the full proof), the system can achieve higher reliability in correctness judgments.

The verification mechanism. For each lemma extracted by the Summarizer, the Theorem Verifier performs n parallel verification passes (with n = 4 per the default budget in Appendix B.1). Each pass uses a learned verifier (the paper references OPV [34] and CompassVerifier [17] as the verifier models) that examines the lemma's proof and outputs a judgment. The verifier prompt (Appendix A.3) instructs the model to:

Execute a step-by-step check of the entire proof.
For each step, verify that logical inferences are sound and that any cited lemmas from the library are correctly applied (preconditions satisfied).
Identify the index of the first incorrect step, outputting \box{STEPk} where k is the step index, or \box{STEP-1} if all steps are correct.

Confidence scoring. The confidence score for a lemma is defined as the proportion of parallel verification runs that judge the lemma as fully correct:

$\text{confidence}(l) = \frac{\text{number of runs outputting STEP-1}}{n}$

where n is the number of parallel verification passes (typically 4). This is a simple but effective ensemble mechanism: by running multiple independent verifications (presumably with different random seeds or slight prompt variations), the system reduces the impact of false positives (a flawed lemma being marked correct by chance) and false negatives (a correct lemma being flagged due to verifier error).

What happens to low-confidence lemmas? The paper states that the theorem verifier's confidence scores are used to "assess and refine [lemmas'] correctness" (Section 5.4), but the exact threshold for accepting or rejecting a lemma is not explicitly defined in the main text. The implication from the overall architecture is that only lemmas with sufficiently high confidence are added to the lemma library for use in subsequent rounds, while low-confidence lemmas are either discarded or flagged for re-proving. The paper notes that this mechanism allows the agent to "recover historical exploration outcomes in subsequent steps" with reliability.

Design comparison to formal verification. The theorem verifier operates on natural language proofs, not formal logic. This is a deliberate tradeoff: formal verification would provide ironclad correctness guarantees but requires translating problems into formal logic (with associated costs and human-interpretability barriers) and involves extensive search overhead. The learned verifier approach provides probabilistic correctness assessments that are "good enough" to prevent most error propagation while maintaining flexibility and efficiency.

Process Verifier (OPV) and Final Solution Revision

Role of the process verifier. In the final stage of the pipeline, after the multi-round reasoning loop produces a candidate complete solution, the Process Verifier (OPV, from Wu et al., 2024 [34]) examines the solution and provides fine-grained feedback on logical correctness. The paper cites OPV's performance: "their verifier achieves an F1-score greater than 85% on ProcessBench, surpassing the performance of o1-mini."

How OPV evaluates a solution. The verifier prompt (Appendix A.4) instructs the model to:

Break the solution into steps (presented as separate paragraphs in the input).
Evaluate each step for logical soundness, checking every "logical inference at a small granularity carefully, either in natural language or in formulas."
Identify the index of the first incorrect step, outputting \box{STEPk} for step errors or \box{LEMMAk} if a specific lemma within the solution is flawed.
If all steps are correct, output \box{STEP-1}.

A notable design detail: the verifier is instructed to be lenient about minor issues that "do not affect the overall reasoning" or gaps that "can be recovered by [the verifier's] effort"—only genuine logical errors are flagged. This prevents the verifier from being overly pedantic about trivial omissions while still catching substantive mistakes.

Multi-verification for robustness. The OPV verification is run multiple times in parallel (the paper mentions 8-shot refinement in the CMO2025 configuration, Section 5.4). The results across runs are aggregated to improve reliability, analogous to the theorem verifier's confidence scoring.

The iterative revision loop. When the OPV identifies errors, the solution enters a modification loop (the rightmost part of Figure 2):

The OPV's feedback identifies the specific steps where logical gaps or errors exist (the "First Error" output and the detailed verification log).
The Reasoner Agent receives this feedback along with the problematic solution and produces an improved version, using the prompt in Appendix A.5. The prompt instructs the model to "fix all errors reasonably pointed out by comments, fill all gaps mentioned by comments and defend other issues that [are] defendable" while also compressing complexity.
The revised solution is re-verified by OPV.
This loop continues until verification passes or the maximum number of revision rounds (8, per Appendix B.1) is reached.

The revision prompt's design philosophy. The revision prompt (Appendix A.5) contains several subtle design choices:

Freedom to restructure: "You are free to decide the idea/approach of your improved solution. You can just fix specific issues, restructure certain parts of the previous answer, or even discard the original solution if considered as unfixable." This prevents the model from getting locked into a flawed approach and enables complete restarts when necessary.
High-school level preference: "You are advi[s]ed to use highschool level of math. If you choose to use university level, then you should treat the readers as smart highschool students with no backgrounds, then provide the specific introduction of certain knowledge needed." This biases the model toward accessible, self-contained proofs rather than relying on advanced theorems that may obscure logical gaps.
Comments are guidance, not authority: "Treat these as helpful guidance rather than authoritative. If they flag something, fix or defend." This prevents the model from blindly accepting verifier feedback that might itself be erroneous (since the verifier has ~85% F1, about 15% of its flags could be wrong).

Dual purpose in evaluation and training. The OPV serves two functions: (1) improving solution quality through test-time revision (evaluation), and (2) providing reward signals for reinforcement learning (training, discussed in the next section). The paper emphasizes that the verifier provides "high-quality feedback signals for iterative revision and reinforcement learning training to further optimize the agent's reasoning precision."

OREAL-H: Hierarchical Reinforcement Learning Framework

What OREAL-H is and why it's needed. OREAL-H extends the OREAL (Outcome Reward Reinforcement Learning) framework [18] to handle the hierarchical, multi-round structure of Intern-S1-MO. Standard RLVR (Reinforcement Learning with Verifiable Rewards) provides only a binary outcome signal (correct/incorrect final answer), which the paper argues is "insufficient for complex mathematical tasks requiring high process supervision." OREAL-H addresses two key challenges: (1) credit assignment across multiple reasoning rounds with delayed rewards, and (2) incorporating the Process Verifier's continuous, noisy assessments into a stable training signal.

Hierarchical MDP Formulation

State and action spaces. The paper formalizes the agentic reasoning process as a Hierarchical Markov Decision Process (MDP):

$\mathcal{M} = \langle \mathcal{S}, \mathcal{U}, \mathcal{V}, r, R, \gamma \rangle$

where $\mathcal{S}$ is the state space (problem context + reasoning trace + verification feedback), $\mathcal{U}$ is the high-level meta-action space (decisions like "extract lemmas", "invoke verification", "commit answer"), and $\mathcal{V}$ is the low-level token vocabulary.

What this formulation captures. The hierarchical structure reflects that the agent operates at two levels simultaneously: at the high level, it makes strategic decisions about what kind of reasoning to do in each round (propose lemmas, summarize, verify, revise); at the low level, it generates token sequences that implement those decisions. The state $s_t$ at round t includes not just the problem and lemmas discovered so far, but also the verification feedback from previous rounds—this is what enables the agent to learn from its history.

Policy decomposition. The agent's behavior is governed by two policies: a high-level policy $\pi_{\varphi}^H$ that selects meta-actions, and a low-level policy $\pi_{\theta}^L$ that generates token sequences conditioned on the current state and the chosen meta-action. The paper focuses primarily on optimizing $\pi_{\theta}^L$ (the reasoning policy), treating the high-level structure as largely fixed by the agent architecture.

Training objective. The optimization target is:

$J(\theta, \varphi) = \mathbb{E}_{\pi_{\varphi}^H, \pi_{\theta}^L} [R]$

where R is the final sparse reward indicating solution correctness. In words: maximize the expected final reward over trajectories generated by following the hierarchical policy.

Why hierarchical? A flat MDP over individual tokens would have an enormous action space and extremely delayed rewards (thousands of tokens between an action and any feedback). The hierarchical decomposition enables credit assignment at the round level—each round's contribution can be evaluated based on whether it produced useful lemmas that advanced the proof—which dramatically reduces the variance of advantage estimates.

Lemma Dependency Graph for Credit Assignment

The core problem: which rounds contributed? In a multi-round trajectory, some rounds produce valuable lemmas that eventually lead to a correct solution, while others may produce nothing useful or even introduce errors. Outcome-only rewards (correct/incorrect) cannot distinguish between these cases—all rounds in a correct trajectory get positive credit, and all rounds in an incorrect trajectory get negative credit, regardless of their individual merit.

Constructing the lemma graph. To solve this, the paper introduces a lemma dependency graph. For a given problem, the system generates K trajectories (multiple independent rollouts of the full multi-round process). All lemmas from all trajectories are collected, and a directed graph $\mathcal{G} = (\mathcal{V}, \mathcal{E})$ is constructed where:

Nodes $\mathcal{V}$ are individual lemmas.
Directed edges $\mathcal{E}$ indicate derivation relationships: if lemma l' was proved using lemma l as a premise, then l → l' is an edge (or equivalently, $l' \in \text{Succ}(l)$ where $\text{Succ}(l)$ is the set of valid lemmas derived directly from l).

Backpropagating value through the graph. The value of a lemma is defined recursively as the expected value of its successors:

$v(l) = \mathbb{E}_{l' \in \text{Succ}(l)} [v(l')]$

where $\text{Succ}(l)$ is the set of lemmas in the dependency graph that were derived directly from lemma l.

What this recursion computes: starting from terminal nodes (lemmas that directly contribute to a final correct solution, identified by having trajectories with non-zero final reward), the value propagates backward through the graph. A lemma that frequently leads to useful successor lemmas in trajectories that eventually succeed will accumulate high value; a lemma that never appears in successful trajectories will have low or zero value. This is explicitly analogized to "a computationally efficient surrogate to Monte Carlo Tree Search (MCTS), providing high-quality value estimation without the prohibitive overhead of extensive search."

Round-level advantage computation. For each reasoning round t that generates a set of candidate lemmas $\mathcal{L}_t$ , the state value of that round is defined optimistically:

$V(s_t) = \max_{l \in \mathcal{L}_t} v(l)$

In words: the value of a reasoning round is the maximum value among all lemmas it produced. This optimistic formulation captures the intuition that a round is valuable if it produces at least one lemma that proves useful downstream—even if it also produced many dead ends.

The round-level advantage is then computed as a temporal difference error:

$A_t = r_t + \gamma \max_{l' \in \mathcal{L}_{t+1}} v(l') - \max_{l \in \mathcal{L}_t} v(l)$

where $r_t$ is any immediate step reward (e.g., syntactic validity of the output) and $\gamma$ is the discount factor.

What this advantage represents: the improvement (or degradation) in the best available lemma quality between round t and round t+1. If round t+1 produces a lemma with substantially higher value than anything produced in round t, the advantage is positive—the agent made progress. If round t+1 fails to improve on round t's best lemma, the advantage is negative or zero.

Masking non-progress rounds. For intermediate rounds that produce no new lemmas ( $\mathcal{L}_t = \emptyset$ ), the advantage is set to zero: $A_t = 0$ . This "ensures that the gradient estimation is driven by the most promising reasoning path discovered at each step, decoupling optimization intensity from trajectory length and effectively filtering out noise from suboptimal branches."

Token-level policy gradient. Once round-level advantages are computed, the low-level policy gradient aggregates token-level log-likelihoods within each round, weighted by the round's advantage:

$\nabla_\theta J = \mathbb{E} \left[ \sum_{t=1}^{K} A_t \cdot \sum_{\tau=1}^{T_t} \nabla_\theta \log \pi_\theta^L(v_{t,\tau} | s_t, v_{t,<\tau}) \right]$

where $K$ is the total number of rounds, $T_t$ is the number of tokens in round t, and $v_{t,\tau}$ is the $\tau$ -th token generated in round t.

What this gradient does: for rounds with positive advantage, it increases the probability of the token sequences that led to that advantage; for rounds with negative advantage, it decreases those probabilities. Crucially, entire rounds are upweighted or downweighted together—the credit assignment occurs at the round level (via the advantage $A_t$ ), not at the individual token level. This is appropriate because the value of a reasoning trace comes from the lemmas it produces, not from individual word choices.

Why this form over alternatives: standard REINFORCE would assign credit uniformly across all tokens in a correct trajectory and penalize all tokens in an incorrect one. The lemma-graph-based credit assignment provides much finer-grained feedback: a round that produced a critical lemma gets positive advantage even if the overall trajectory eventually fails (because some later round made an error), and a round that contributed nothing gets zero advantage even in a correct trajectory (because its tokens are irrelevant to the success). This dramatically reduces variance and accelerates learning.

Conjugate Reward Modeling for Noisy Process Verification

The problem with using raw verification ratios as rewards. The Process Verifier provides a score for the final solution: out of n independent verification passes, k of them judge the solution as correct. A naive approach would use the empirical ratio k/n directly as a reward signal (or as a multiplier on the outcome reward). However, this is problematic because the verifier is imperfect—an F1-score of 85% means that in about 15% of cases, the verifier's judgment disagrees with ground truth. Using raw ratios risks "amplifying this noise, leading to unstable or misguided policy updates that overfit to verification artifacts rather than genuine mathematical rigor."

The Bayesian model. To address this, the paper adopts a principled probabilistic approach. The latent reasoning quality of a solution is modeled as an unknown probability $p \in [0, 1]$ (the probability that an ideal verifier would judge the solution as correct). A uniform prior is placed on p:

$p \sim \text{Beta}(1, 1)$

representing complete uncertainty before observing any verification results.

After observing k successes in n independent verification trials, the posterior distribution for p is the conjugate Beta-Bernoulli update:

$p \mid (k, n) \sim \text{Beta}(k + 1, n - k + 1)$

What this posterior represents: it's the updated belief about the solution's quality after seeing the verification evidence. The Beta distribution's mean is (k+1)/(n+2), which is a smoothed version of the empirical ratio—it pulls extreme estimates (0/n or n/n) toward 0.5, reflecting the uncertainty inherent in small sample sizes.

The conjugate reward definition. Rather than using a point estimate (like the posterior mean), the reward is defined as the probability that the current solution is strictly better than a baseline "completely invalid" solution—one that would fail all n verification checks:

$R(k, n) = \mathbb{P}(p_1 > p_0)$

where $p_1 \sim \text{Beta}(k + 1, n - k + 1)$ is the posterior quality of the current solution, and $p_0 \sim \text{Beta}(1, n + 1)$ is the posterior quality of a baseline solution that failed all n checks (k = 0).

The computation is:

$R(k, n) = \int_0^1 \int_0^1 \mathbf{1}(p_1 > p_0) \cdot f_{\text{Beta}(k+1, n-k+1)}(p_1) \cdot f_{\text{Beta}(1, n+1)}(p_0) \, dp_1 \, dp_0$

What this integral computes: the probability, under the posterior distributions, that a random draw from the current solution's quality distribution exceeds a random draw from the baseline's quality distribution. It's a direct measure of how much better (probabilistically) the current solution is than a known-bad one.

Practical instantiation. The paper fixes n = 4 verification passes, "balancing verification cost and signal fidelity." Under this setting, R(4, 4) ≈ 5.5, meaning that a solution passing all 4 checks has a 99.5% probability of being better than the baseline. Solutions with intermediate pass counts (k = 1, 2, 3) receive smoothly interpolated rewards between 0 and 5.5.

Why this form is better than alternatives:

It naturally suppresses spurious signals: A solution that passes 1 out of 4 checks (k = 1) might have an empirical ratio of 0.25, but the conjugate reward reflects the substantial uncertainty—the reward is low because the evidence for quality is weak, not because the point estimate is moderate.
It provides strong gradients for high-confidence solutions: A solution passing 4/4 checks gets a reward substantially higher than one passing 3/4, creating a clear incentive for producing solutions that are confidently correct.
It's grounded in relative comparison, not absolute scale: The reward is always defined relative to the k = 0 baseline, making it invariant to the overall calibration of the verifier. Even if the verifier has systematic biases (e.g., it's too lenient or too strict), the relative ordering of solutions is preserved.

Integration with the outcome reward. For problems amenable to outcome supervision (solution-based problems where the final answer can be checked), the final reward R is multiplied by (or conditioned on) outcome correctness: if the final answer is incorrect, R = 0 regardless of the process verifier's assessment. This prevents the system from rewarding solutions that pass process verification but produce wrong answers—process quality is valued only when it leads to correct outcomes.

Cold-Start Behavioral Cloning

Why cold-start training is necessary. Before online RL can be effective, the model must have a basic ability to follow the structured reasoning format and produce well-formed lemma summaries. Starting RL from a model that doesn't understand the agent protocol would result in nearly all trajectories being invalid, providing no useful learning signal. The paper's cold-start procedure ensures the model internalizes the "iterative agentic workflow" before optimization begins.

Data collection. The cold-start dataset $\mathcal{D}_{\text{init}}$ is constructed from two sources:

Filtered multi-round trajectories: The system generates candidate trajectories (using a variant of Intern-S1) on a collection of problems from Art of Problem Solving (AoPS) and in-house datasets spanning "middle school, university, and competition-level, including both solution-based and proof-based questions." Trajectories are filtered to retain only rounds where the output "admits a well-formed lemma summary (e.g., syntactically valid, non-empty, logically segmented)."
Outcome-filtered single-step data: The authors "continuously augment $\mathcal{D}_{\text{init}}$ with question-answer pairs that are filtered by outcome-based scoring, without previous thinking." These are simpler trajectories (single-round, correct final answers) that don't include the multi-round structure but help the model learn the basic problem → solution mapping.

Training objective. The cold-start phase uses standard supervised fine-tuning (referred to as Rejection Fine-Tuning, RFT) with a token-level log-likelihood objective:

$\mathcal{L}_{\text{RFT}}(\theta) = -\mathbb{E}_{(s_t, v_t) \sim \mathcal{D}_{\text{init}}} \left[ \sum_{\tau=1}^{T_t} \log \pi_\theta^L(v_{t,\tau} \mid s_t, v_{t,<\tau}) \right]$

where $(s_t, v_t)$ is a state–token-sequence pair from the filtered dataset, and $T_t$ is the sequence length.

What this loss computes: the standard cross-entropy between the model's predicted token distribution and the "correct" tokens from the supervised trajectories. Minimizing this loss increases the probability the model assigns to the demonstrated behavior.

Why this form: maximum likelihood estimation under the model's autoregressive factorization. This is the standard objective for behavioral cloning—it's simple, stable, and directly optimizes for reproducing the demonstrated behavior.

Emergent generalization. The paper reports an interesting empirical finding: "the model exhibits emergent generalization: patterns learned from these simplified trajectories boost agentic solving of the same problems, thereby improving the efficiency of positive trajectory discovery during online RL." In other words, training on single-round correct solutions (without the multi-agent structure) somehow transfers to better multi-round reasoning performance. The mechanism isn't fully explained, but it suggests that the base mathematical reasoning capability learned during cold-start provides a foundation that the RL phase can then shape into the specific multi-agent workflow.

Training Pipeline and Hyperparameters

Overall training loop. The complete OREAL-H training procedure is described in Algorithm 1 and proceeds as follows:

Sampling: For each batch of problems (64 questions per batch), generate K = 16 independent multi-round trajectories using the current policy $\pi_\theta$ .
Filtering: Calculate the pass rate for each problem (fraction of the 16 trajectories that are correct). Discard problems with pass rates of 0 or 1—these provide no useful learning signal because all trajectories are either uniformly wrong (no positive examples) or uniformly correct (no contrast).
Process verification: For each trajectory, evaluate the final solution using the Process Verifier, computing the conjugate reward $R(k, n)$ as described above.
Lemma graph construction: Collect all lemmas from all 16 trajectories for each remaining problem, construct the dependency graph, and backpropagate values using the recursive formula.
Advantage computation: For each round in each trajectory, compute $A_t$ using the round-level temporal difference formula with the lemma graph values.
Policy update: Apply the OREAL loss [18] to update the policy parameters $\theta$ . The OREAL loss is not fully specified in the paper but is referenced as the base optimization framework, augmented with the hierarchical advantage structure.
Repeat until convergence.

Key hyperparameters:

Batch size: 64 questions per batch.
Rollouts per question: 16 trajectories per question.
Maximum trajectory length: 65,536 tokens per rollout (matching the 64K context window).
Learning rate: $5 \times 10^{-7}$ for the policy model.
Learning rate schedule: Cosine annealing, decaying to 1/5 of the initial learning rate over the training duration.
Optimizer: AdamW.
KL penalty coefficient: $\beta = 0.01$ , used in the OREAL loss to prevent the policy from diverging too far from the reference (cold-start) model.
Verification passes (Theorem Verifier): n = 4 parallel verifications per lemma.
Verification passes (OPV conjugate reward): n = 4 (explicitly stated in Section 4.3.2: "we fix n = 4, balancing verification cost and signal fidelity").
Maximum reasoning rounds: 8 rounds per problem.
Maximum revision rounds: 8 rounds for the final iterative revision loop.
Maximum output length per agent: 64K tokens for Reasoner and Summarizer agents.

Verifier models. The paper uses two verifier models depending on the problem type:

CompassVerifier [17]: Used for solution-based problems where correctness is determined by final answer checking.
OPV [34]: Used for proof-based problems where correctness depends on logical reasoning quality rather than just final answer matching.

Both verifiers are employed during cold-start data generation to filter trajectories, and OPV is used during both RL training and inference-time revision.

Distillation for efficiency. The paper also creates Intern-S1-mini-MO, a "lite system based on Intern-S1-Mini" that is built by distilling the full Intern-S1-MO system. This variant achieves competitive results (e.g., 176.3 on CNMO2025, surpassing Gemini 2.5 Pro's 157.5) while being more parameter-efficient, demonstrating that the architectural innovations—not just model scale—drive the performance gains.

Summary of Design Choices and Their Justifications

Multi-round over single-pass: Single-pass models hit context-length ceilings and exhibit premature conclusion bias; multi-round with lemma memory extends effective depth 8× by decoupling total reasoning from any one context window.
Lemma extraction by separate summarizer agent: Summarizing exploration is as hard as exploration itself and requires dedicated reasoning; a separate agent ensures lemma quality without burdening the reasoner with meta-cognitive overhead.
Theorem verifier with parallel sampling: Multiple independent verification passes reduce false positives/negatives compared to single-pass verification; the confidence score provides a graded signal for lemma reliability.
Natural language over formal verification: Avoids translation costs, enables human-interpretable intermediate results, and maintains flexibility; the learned verifier provides "good enough" correctness assessments at lower computational cost.
Hierarchical MDP with lemma dependency graph: Flat MDPs over tokens have enormous action spaces and delayed rewards; round-level credit assignment using lemma value backpropagation provides dense, meaningful training signal.
Conjugate reward over raw verification ratios: Raw ratios amplify verifier noise; the Bayesian posterior comparison provides principled uncertainty-aware rewards that suppress spurious signals and provide strong gradients for high-confidence solutions.
Cold-start behavioral cloning before RL: RL from an untrained agent produces nearly all invalid trajectories; supervised fine-tuning on filtered data internalizes the structured reasoning format, providing a foundation for RL to build upon.
Outcome gating on process rewards: For solution-based problems, process quality is rewarded only when the final answer is correct, preventing the system from optimizing for verifier-pleasing but ultimately wrong solutions.

4. Key Insights and Innovations

Innovation 1: Lemma-Based Memory as a General Mechanism for Decoupling Reasoning Depth from Context Length

What's distinctive at the idea level. The field's dominant approach to handling harder reasoning problems has been to scale context length—either by engineering models that support longer sequences (pushing from 32K to 64K to 128K tokens) or by developing techniques that compress representations within a single context window. Intern-S1-MO introduces a fundamentally different mental model: instead of stretching the container to hold more reasoning, externalize intermediate results into a structured memory that persists across independent reasoning episodes. The key conceptual move is recognizing that mathematical reasoning has a natural hierarchical structure—proofs build on lemmas, which build on definitions and prior lemmas—and that this structure can be exploited to separate the discovery of intermediate results (which requires extensive exploration and trial-and-error) from their storage and reuse (which requires only compact, precise statements).

This is not simply "letting the model think longer." It is a reframing of reasoning as incremental knowledge accumulation rather than monolithic generation. The analogy is to how human mathematicians work: they don't hold an entire proof in working memory at once; they prove lemmas, write them down, and then reason about those lemmas as black-box building blocks. Intern-S1-MO's lemma library is the digital equivalent of a mathematician's notebook—a persistent, verified record of "what has been established so far" that frees subsequent reasoning rounds from rediscovering or re-deriving those results.

Comparison to prior work. The two dominant paradigms before this paper were (1) single-pass chain-of-thought with internal self-correction (o3, Gemini 2.5 Pro, DeepSeek-R1), which operates entirely within one context window and must either solve the problem or fail before hitting the token limit; and (2) formal proof search (Seed-Prover, DeepSeek-Prover-V2), which stores intermediate results in formal logic repositories but requires expensive translation between natural and formal language and exhaustive search over proof spaces. The first paradigm is bounded by hardware context limits; the second is bounded by computational overhead and the brittleness of formalization.

Intern-S1-MO occupies a previously unexplored middle ground: structured memory without formalization. The lemmas are expressed in natural mathematical language with LaTeX, making them human-interpretable and avoiding formalization costs, but they are still explicit, verified, and reusable objects in a growing knowledge base. This represents a conceptual advance over both prior paradigms because it demonstrates that structured accumulation, not just extended generation or formal verification, is a viable third axis for scaling reasoning capability.

Significance beyond raw performance. The lemma memory mechanism introduces a new diagnostic concept: effective reasoning depth as distinct from raw context length. A 64K-token model with lemma memory can sustain roughly 512K tokens of total reasoning across rounds, but more importantly, it can sustain cumulative logical depth that is qualitatively different from a single 512K-token generation. In a single long generation, the model must maintain coherence across all reasoning simultaneously—later steps can contradict earlier ones, and the model has no architectural support for distinguishing "established facts" from "speculative exploration." The lemma memory provides a truth maintenance system that separates proven results from ongoing reasoning, reducing the cognitive burden on each individual round.

Evidence. The ablation study (Table 2) shows that adding multi-round reasoning with lemma extraction ("+ Multi-round Reasoning") to a single-round baseline improves CNMO2025 from 178.0 to 201.7 and HMMT2025 from 70.8 to 85.4. This is before any verification or RL training—the mere ability to decompose reasoning across rounds with lemma accumulation provides substantial gains. The finding that the system can participate in CMO2025 under human time constraints and achieve 102/126 further demonstrates that this architecture enables sustained reasoning over hours (the competition spans two days with 4.5-hour sessions) without degradation.

Is this fundamental or incremental? The idea of maintaining structured memory for reasoning is not entirely new—it has roots in classical AI (production systems, blackboard architectures) and appears in simplified form in prior LLM-based systems (Tree-of-Thoughts, RAP). However, the paper's contribution is fundamental in two respects: (1) it demonstrates that learned models (not hand-crafted symbolic systems) can effectively create, verify, and reuse their own intermediate results in natural language, bridging the gap between neural generation and symbolic knowledge accumulation; and (2) it shows that this mechanism can be trained end-to-end through RL, meaning the model learns not just to solve problems but to manage its own knowledge state across extended reasoning sessions. The latter point—that meta-cognitive skills like lemma extraction and reuse can be optimized through learning—is what elevates this from an engineering trick to a conceptual innovation.

Innovation 2: Lemma Dependency Graphs as a Computationally Tractable Alternative to MCTS for Credit Assignment in Hierarchical Reasoning

What's distinctive at the idea level. Reinforcement learning for multi-step reasoning faces a fundamental credit assignment problem: when a long reasoning trajectory eventually succeeds, which intermediate steps contributed to that success, and which were irrelevant or even counterproductive? Prior approaches have tackled this through Monte Carlo Tree Search (MCTS), which explicitly explores the tree of possible reasoning paths and backpropagates value estimates. However, MCTS is computationally expensive—it requires generating and evaluating many alternative partial solutions at each decision point, making it impractical for the kind of deep, multi-round reasoning that IMO problems demand.

OREAL-H's key conceptual innovation is the lemma dependency graph: rather than searching over reasoning paths at inference time, the system aggregates lemmas from multiple complete trajectories (16 per problem during training), constructs a graph representing which lemmas were used to derive which other lemmas, and then backpropagates success probability through this graph. The insight is that lemma derivation relationships, not sequential order of generation, are what matter for credit assignment. A lemma produced in round 3 that proves essential for the final solution is valuable regardless of whether it came after or before less useful lemmas; a lemma that was never used downstream contributes nothing regardless of where it appeared.

This reframes credit assignment from a temporal problem (which round was helpful?) to a structural one (which lemma was useful?), making it possible to leverage information across multiple independent trajectories. The dependency graph aggregates evidence from 16 independent problem-solving attempts, providing a richer signal than any single trajectory could.

Comparison to prior work. MCTS-based approaches (rStar2-Agent, ReST-MCTS*) use explicit tree search to explore reasoning paths and estimate values, but they suffer from three limitations that the lemma graph addresses: (1) they are computationally expensive at inference time because search must be performed per problem; (2) they typically operate within single reasoning episodes rather than across rounds; (3) they provide no mechanism for transferring credit assignment insights across different attempts at the same problem. The lemma graph is a training-time construct—it's computed once during RL data processing and doesn't add inference-time overhead—and it naturally pools evidence across trajectories.

Process reward models (PRMs) provide per-step supervision but require either human labels (expensive) or automated rollout-based estimation (which is still per-trajectory and doesn't aggregate across attempts). The lemma graph provides a form of process-level supervision that is self-supervised and cross-trajectory: lemma values are estimated from the collective success patterns of many attempts at the same problem, not from explicit human judgments or per-step Monte Carlo rollouts.

Significance beyond raw performance. The lemma dependency graph introduces a new concept for the RL-for-reasoning community: structural credit assignment as an alternative to both temporal credit assignment (discounted returns, TD learning) and search-based value estimation. The key insight—that reasoning can be decomposed into reusable components whose value can be estimated from their downstream usage patterns—generalizes beyond mathematical proof to any domain where problems have decomposable structure. Code generation (functions depend on other functions), scientific reasoning (hypotheses build on established findings), and legal analysis (arguments cite precedents) all exhibit similar dependency structures.

Moreover, the paper demonstrates that this structural approach is not just theoretically elegant but practically tractable: the lemma graph is described as "a computationally efficient surrogate to MCTS, providing high-quality value estimation without the prohibitive overhead of extensive search." This efficiency claim is significant because it suggests that the approach could scale to problems requiring deeper reasoning than MCTS can feasibly explore.

Evidence. The incremental value of OREAL-H training over the full inference pipeline (Table 2, "+ OReal-H" row) shows gains of 5.9 points on HMMT2025, 2.6 points on AIME2025, and 17.2 points on CNMO2025 compared to the process-verifier-only baseline. These gains are achieved entirely through training—the inference architecture is identical between the "+ Process Verifier" and "+ OReal-H" rows; the only difference is that the policy model has been optimized using the lemma-graph-based credit assignment. The disproportionate improvement on CNMO2025 (the hardest benchmark) is particularly telling: it suggests that the credit assignment mechanism is most valuable on problems requiring extended multi-round reasoning, where temporal credit assignment from outcome rewards would be most noisy.

Is this fundamental or incremental? The idea of using dependency graphs for credit assignment is novel in the context of LLM reasoning agents, but it builds on concepts from program analysis (call graphs, dataflow analysis) and classical planning (causal link extraction). The contribution is fundamental in its application domain because it solves a practical bottleneck—how to provide dense, meaningful training signal for multi-round reasoning without expensive search—that had limited prior approaches. However, the dependency graph construction relies on the lemma extraction mechanism working reliably, and the paper doesn't fully explore failure modes (e.g., what happens when lemmas are incorrectly linked in the graph). This makes it a strong but incomplete innovation that opens a clear research direction rather than closing the book on the problem.

Innovation 3: Conjugate Reward Modeling as a Principled Solution to Noisy Process Verification

What's distinctive at the idea level. Using learned verifiers to provide training signal raises an immediate statistical problem: the verifier is imperfect, and naively treating its output as ground truth can lead to reward hacking—the policy learns to produce solutions that look correct to the verifier rather than solutions that are correct. This is the same over-optimization problem documented extensively in RLHF and in the prior paper analysis (PRM search over-optimization on easy problems). Existing approaches typically handle this by (1) using only outcome rewards (correct/incorrect final answer), which are clean but sparse, or (2) using process rewards from verifiers but with ad hoc discounting or thresholding.

OREAL-H's conjugate reward model introduces a Bayesian perspective on verifier uncertainty. Rather than treating the verifier's output as a point estimate of quality, it models the latent reasoning quality as a random variable with a Beta posterior distribution, and defines the reward as the probability that the current solution is better than a known-bad baseline. This is conceptually distinctive because it reframes the reward design problem from "how do we aggregate noisy verifier outputs?" to "how do we quantify the evidence for solution quality, accounting for verifier noise?"

The key mathematical insight is that by placing a conjugate prior on the latent quality parameter and computing the posterior after observing k successes in n verification trials, the reward naturally incorporates uncertainty: a solution passing 2/4 verification trials gets a much lower reward than one passing 4/4, even though both are "more than half," because the posterior distribution for 2/4 is much wider and has substantial mass below the baseline. This creates a built-in conservatism—the system is skeptical of solutions with weak evidence and only confidently rewards solutions with strong evidence.

Comparison to prior work. The dominant approach in RLVR is binary outcome rewards, which are noise-free but provide no intermediate guidance. Process reward models (PRMs) trained via Monte Carlo rollouts (as in the prior paper analysis) provide per-step scores but still treat those scores as point estimates, requiring careful calibration to avoid over-optimization. Some works use majority voting across verifier runs, which reduces variance but doesn't provide a principled way to convert vote counts into reward magnitudes.

The conjugate reward approach is more principled than ad hoc thresholding (e.g., "only reward solutions that pass ≥3/4 checks") because it provides a continuous, differentiable reward surface that reflects evidential strength. A solution passing 3/4 checks gets some positive reward (it's probably better than baseline), while a solution passing 4/4 gets substantially more (the evidence is much stronger), and a solution passing 0/4 gets zero. This smooth interpolation is important for stable RL training—it avoids the cliff effects that binary thresholds create.

Significance beyond raw performance. This innovation has implications beyond mathematical reasoning. Any RL system that relies on learned verifiers or reward models—including RLHF for language models, robotic policy learning with learned success detectors, and code generation with test-case-based rewards—faces the same noisy-verifier problem. The conjugate reward framework provides a general-purpose, statistically grounded method for converting noisy binary (or count-based) feedback into well-calibrated rewards. The key requirement is that the verification trials are approximately independent and that a Beta-Bernoulli model is a reasonable prior for the latent quality—conditions that hold in many settings.

Moreover, the paper's explicit choice of n = 4 verification passes as a practical balance between cost and fidelity provides a concrete reference point for practitioners. The computation of R(4, 4) ≈ 5.5 (99.5% probability of superiority) versus R(0, 4) = 0 establishes a clear reward scale grounded in statistical evidence rather than arbitrary scaling.

Evidence. The paper does not provide a direct ablation comparing conjugate rewards against raw verification ratios or binary thresholds. However, the overall performance of OREAL-H (Table 2) and the theoretical motivation in Section 4.3.2 provide supporting evidence. The authors explicitly justify the approach: "Directly using the empirical ratio k/n as a reward signal risks amplifying this noise, leading to unstable or misguided policy updates that overfit to verification artifacts rather than genuine mathematical rigor." The conjugate reward is presented as the solution to this identified problem. The fact that OREAL-H training improves performance without causing the reward hacking that plagues PRM search in the prior paper (where beam search over-optimizes the verifier on easy problems) is indirect evidence for the approach's effectiveness, though a head-to-head comparison would be stronger.

Is this fundamental or incremental? The Bayesian modeling itself is standard statistical methodology—Beta-Bernoulli conjugacy is textbook material. What makes this an innovation is the application of this framework to the specific problem of noisy process verification in RL for reasoning, combined with the insight that the reward should be defined as a relative comparison to a baseline rather than an absolute quality estimate. The relative-comparison formulation elegantly sidesteps the calibration problem (Is k/n = 0.75 "good enough"? It depends on the verifier's base rate) by always measuring against a within-distribution baseline. This is a small but clever conceptual move that makes standard Bayesian machinery directly applicable to a practical RL challenge.

The innovation is incremental in methodology but fundamental in practical impact: it provides a drop-in solution to a problem (noisy verifier rewards) that had been a recognized bottleneck, and it does so with minimal additional complexity (just replacing the reward computation, not the overall RL algorithm).

Innovation 4: Demonstrating That Architectural Innovation Can Substitute for Context-Length Scaling at Olympiad-Level Difficulty

What's distinctive at the idea level. The paper establishes an empirical result that challenges the implicit assumption driving much LLM development: that harder reasoning problems primarily require longer context windows. Figure 1(a) shows the exponential growth of token consumption with problem difficulty—a trend that, if sustained, would make IMO-level problems infeasible even with aggressive hardware scaling. The paper's counter-proposal is that architectural support for knowledge accumulation can substitute for raw context length, achieving equivalent or better reasoning depth with a fraction of the per-context-window token budget.

This is not just "test-time compute scaling works" (the finding of the prior paper analysis). That prior work showed that allocating more inference compute (more parallel samples, more search) can improve performance on problems within a model's capability range. Intern-S1-MO's finding is qualitatively different: it shows that structural decomposition—not just more compute, but better-organized compute—can push a model beyond the difficulty ceiling imposed by its context-length limit. The model's 64K-token-per-round constraint is fixed, but the system achieves roughly 512K tokens of effective reasoning by chaining multiple rounds together, with the lemma library serving as the bridge between rounds.

Comparison to prior work. The prior paper analysis established that test-time compute and pretraining compute are not 1-to-1 exchangeable, and that test-time compute helps most on easy-to-medium problems within a model's capability range. Intern-S1-MO extends this finding in a crucial direction: on Olympiad-level problems (which would fall into "bin 4-5" in the prior paper's difficulty taxonomy—problems largely outside the base model's single-pass capability), architectural innovation in how compute is organized can push the frontier substantially beyond what raw scaling would achieve.

Single-pass models like o3 and Gemini 2.5 Pro already achieve strong results on IMO problems (12.5–14 points in Table 1), but they do so through massive context windows and internal search. Intern-S1-MO achieves nearly double that score (26 points) with a 64K-token-per-round model by externalizing memory management. The comparison is not perfectly controlled (Intern-S1-MO uses multiple rounds totaling more tokens than a single 64K pass), but the key point is that the same total inference budget, when organized hierarchically, dramatically outperforms monolithic generation.

Significance beyond raw performance. This finding provides an empirical counterpoint to the "scale is all you need" narrative that dominates much LLM discourse. The exponential growth curve in Figure 1(a) implies that even a 10× increase in context length (from 128K to 1.28M) would be rapidly consumed by harder problems. The paper demonstrates that better architecture can provide the equivalent of an 8× context-length extension without requiring any hardware improvement. This is a practical roadmap for the near term: rather than waiting for the next generation of hardware to support 512K-context models, researchers can build agentic systems on current hardware that achieve comparable effective depth.

The CMO2025 result (102/126, gold medal) is particularly significant because it validates the approach under real-world competition conditions—time-limited, human-judged, with no special accommodations. This demonstrates that the system's benefits are not just benchmark artifacts but translate to genuine Olympiad-level reasoning capability.

Evidence. Table 1 shows Intern-S1-MO achieving 26/35 on IMO2025 non-geometry problems, compared to 14 for Gemini 2.5 Pro and 11 for GPT-OSS-120B. The gap is concentrated on the hardest benchmark (IMO), while performance on relatively easier benchmarks (AIME, HMMT) is strong but the gap is narrower—exactly the pattern one would expect if the architectural innovation primarily helps on problems that exceed single-pass context limits. The CMO2025 result (Table 3) shows full marks on 4 of 6 problems and partial credit on the remaining 2, demonstrating robust performance across diverse problem types under competition conditions.

A caveat on the claim. The paper does not provide a direct, FLOPs-matched comparison between Intern-S1-MO's multi-round architecture and a hypothetical single-pass model with equivalent total token budget. The 8× effective extension claim is based on the system using "about 512K tokens to solve a single problem" compared to a 64K single-pass limit, but those 512K tokens are spread across multiple independent context windows (each limited to 64K), and the lemma library occupies part of each window. A rigorous comparison would match total FLOPs between the multi-round system and a model with a proportionally longer context window, which the paper does not attempt. This makes the "architectural innovation substitutes for context length" claim more of a compelling empirical demonstration than a fully controlled experiment.

Is this fundamental or incremental? The demonstration that structured decomposition can overcome context-length limits is fundamentally significant because it provides existence proof that the "context scaling is necessary" narrative is false for at least one important domain. The paper doesn't fully dissect why structured decomposition works better than monolithic generation (Is it the verification step that catches errors? The forced summarization that reduces cognitive load? The ability to restart from clean context windows?), but it establishes the empirical fact compellingly enough to motivate substantial follow-up research. The finding is incremental in that it builds on established multi-agent and hierarchical reasoning ideas, but the scale of the demonstration (Olympiad gold medal) and the clarity of the architectural principle make it a significant contribution.

What's distinctive at the idea level. The paper's process verifier (OPV) serves two functions that are usually handled by separate systems: (1) at inference time, it provides feedback for iterative solution refinement, improving output quality through a revision loop; (2) at training time, the same verifier's outputs (after conjugate reward transformation) provide the reward signal for RL. This dual-use architecture is conceptually elegant because it creates a virtuous cycle: better verification improves both immediate solution quality (via revision) and long-term model capability (via RL training), and better model capability in turn produces solutions that are easier to verify.

This contrasts with the typical separation in prior work, where verifiers for inference-time selection (e.g., PRMs for best-of-N sampling) are distinct from reward models for RL training (e.g., outcome reward models trained on final answer correctness). By unifying these roles, OREAL-H ensures that the training signal and the evaluation criterion are aligned—the model is optimized to produce solutions that pass the same verification process that will be used to refine its outputs at test time. This alignment reduces the risk of training on a proxy metric that doesn't correlate with deployment performance.

Comparison to prior work. The prior paper analysis studied PRMs used purely for inference-time search (beam search, best-of-N weighted selection) and trained separate outcome reward models for the revision model's outputs. The PRM was not used for training the base model—only for selecting among its outputs. In contrast, OREAL-H uses OPV both for selection/revision at inference time and as the reward source for policy improvement during training. This creates a tighter feedback loop and ensures that improvements in the verifier translate directly into both better selection and better generation.

RLHF pipelines typically use a separate reward model trained on human preferences, which is then fixed during policy optimization. The policy can learn to exploit the reward model's blind spots (reward hacking), and the only defense is KL regularization to prevent the policy from straying too far from the base model. OREAL-H's approach—using a process verifier that evaluates logical step-by-step correctness rather than holistic preference—is potentially more robust to hacking because it's harder to "look logically correct without being logically correct" than it is to "look generally good to a preference model." However, the paper's OPV still has ~15% error rate (F1 > 85%), so some over-optimization risk remains.

Significance beyond raw performance. The dual-use design pattern is generalizable: any domain with a reliable (if imperfect) verifier can potentially adopt this architecture where the verifier serves both as an inference-time quality filter and a training-time reward signal. The conjugate reward modeling ensures that verifier noise doesn't destabilize training, while the iterative revision loop ensures that verifier feedback is immediately useful. This creates a self-improvement architecture that doesn't require external ground-truth labels during the online phase—the verifier provides all necessary feedback. For mathematical reasoning, this is particularly powerful because ground-truth solutions are often unavailable for novel problems, but logical verification is (in principle) possible without knowing the answer in advance.

Evidence. The ablation study (Table 2) shows that adding the process verifier ("+ Process Verifier") to the multi-round reasoning with theorem verification improves CNMO2025 from 203.0 to 215.2 (a 12.2-point gain) and HMMT2025 from 86.3 to 89.1 (a 2.8-point gain). The further addition of OREAL-H training—which uses the same OPV as reward signal—adds another 17.2 points on CNMO2025 and 5.9 points on HMMT2025. This progressive improvement demonstrates that OPV provides value at both inference time (through the revision loop) and training time (through RL), with the training-time benefit being substantially larger on the hardest benchmark.

Is this fundamental or incremental? The dual-use architecture is fundamentally significant as a design principle because it demonstrates that learned verifiers can close the loop between inference-time improvement and training-time optimization. This has been a recognized goal in the field (the "self-improving AI" vision) but prior implementations have struggled with verifier noise and over-optimization. OREAL-H's specific combination—conjugate reward modeling for noise robustness + lemma dependency graphs for credit assignment + iterative revision for immediate feedback—provides a concrete, working instantiation of this principle. The innovation is the integration rather than any individual component, and the Olympiad-level results validate that the integration works at scale.

5. Experimental Analysis

Evaluation Methodology

Dataset. The paper evaluates on five mathematical benchmarks spanning competition to Olympiad difficulty: AIME2025 (American Invitational Mathematics Examination), HMMT2025 Feb (Harvard–MIT Mathematics Tournament February edition), IMO2025 (International Mathematical Olympiad 2025, non-geometry problems only), CNMO2025 (Chinese National High School Mathematics Olympiad, non-geometry problems), and CMO2025 (Chinese Mathematics Olympiad 2025, the full competition). For CNMO2025 and IMO2025, only non-geometry problems are evaluated, since geometry problems involve visual reasoning that the system does not handle. The paper also uses a collection of problems from Art of Problem Solving (AoPS) and in-house datasets for cold-start training data, spanning middle school, university, and competition-level mathematics.
Base model(s). All experiments use variants of Intern-S1, an open-source large reasoning model developed by Shanghai AI Laboratory. The main system, Intern-S1-MO, is built on the full Intern-S1 model, while Intern-S1-mini-MO is a distilled "lite" version built on Intern-S1-Mini for efficiency comparisons. The choice is motivated by the model being open and reproducible, unlike proprietary alternatives (o3, Gemini 2.5 Pro), and by its strong but not saturated performance on competition mathematics—providing a foundation that test-time strategies can meaningfully improve upon rather than a model already near ceiling performance.
Metrics. For solution-based benchmarks (AIME2025, HMMT2025), the metric is exact final answer accuracy. For proof-based benchmarks (IMO2025, CNMO2025, CMO2025), the paper uses rubric-based scoring with fine-grained grading points (Appendix D). Each solution is evaluated in parallel across 8 independent runs using LLM-based judges, and the final score is the arithmetic mean of the eight scores. For benchmarks other than IMO2025, the paper reports pass@1 (unbiased estimator from 16 independent rollouts) as computed by Chen et al. (2021). For IMO2025 specifically, pass@4 is reported due to the extremely small test set (only 5 non-geometry problems), where pass@1 would be too noisy. For CMO2025—the official competition participation—solutions were scored by human experts using the same standards applied to human contestants, with the competition's official time limits (4.5 hours per day over two days, 3 problems per day).
Baselines. Six models serve as baselines: Gemini 2.5 Pro (Google DeepMind, 2025), o3-high (OpenAI, 2025), Grok4 (xAI, 2025), GPT-OSS-120B (OpenAI, 2025), DeepSeek-R1-0528 (Guo et al., 2025), and Qwen3-235B-A22B (Yang et al., 2025). For AIME2025 and HMMT2025, baseline scores are taken from their respective technical reports or Matharena (Balunović et al., 2025) results. For IMO2025 and CNMO2025, the paper evaluates the baselines using its own grading infrastructure to ensure fair comparison under identical scoring protocols. However, the paper does not specify how many samples or what decoding strategy were used for baseline evaluations—a notable omission since pass@1 estimates depend heavily on sampling temperature and the number of rollouts.
Generation budget / compute accounting. The inference budget is controlled through several hyperparameters (Appendix B.1): maximum 8 reasoning rounds for the Reasoner and Summarizer agents, 4 parallel verifications per lemma for the Theorem Verifier, and maximum 8 rounds for the final iterative revision loop based on the Process Verifier. Each agent's output is capped at 64K tokens per round. The paper states that Intern-S1-MO uses "about 512K tokens to solve a single problem" across all rounds—roughly 8× the 64K single-pass limit. The maximum inference budget is achieved by 16 independent rollouts per problem for pass@1 estimation, and up to 256-shot parallel search over 12 rounds for the CMO2025 competition configuration (Section 5.4). Crucially, the paper does not provide a FLOPs-matched comparison between Intern-S1-MO and the baseline models, nor does it account for the cost of multiple verification passes in the reported "budget." Compute is measured in tokens and rounds, not FLOPs, making direct efficiency comparisons with baselines difficult.
Cross-validation / statistical protocol. For benchmarks with larger test sets (AIME2025, HMMT2025, CNMO2025), pass@1 is computed as an unbiased estimator from 16 independent rollouts per problem, following Chen et al. (2021). For IMO2025, pass@4 is reported due to the tiny sample size (5 problems). The CMO2025 evaluation is not a statistical estimate but an official competition participation: the system was tested once under competition conditions and scored by human judges—there is no averaging or resampling. The paper does not report confidence intervals, standard errors, or any measure of statistical significance for the benchmark comparisons, which is a notable gap given that some claimed improvements (e.g., 95% vs. 82.5% on HMMT2025) are based on relatively small test sets. For the ablation study (Table 2), the paper does not specify whether results are averaged over multiple training runs or based on a single trained model, making it difficult to assess whether the incremental gains (e.g., 203.0 → 215.2 on CNMO2025 after adding process verifier) are reliable or within training variance.

Main Quantitative Results

Overall Benchmark Performance

The headline result is Intern-S1-MO's state-of-the-art performance across all evaluated benchmarks, as summarized in Table 1. On AIME2025, Intern-S1-MO achieves 96.6% pass@1, surpassing the previous best (GPT-OSS-120B at 92.5% and Grok4 at 91.7%) by a margin of approximately 4 percentage points. On HMMT2025, it achieves 95% pass@1, exceeding Grok4's 92.5% and substantially outperforming Gemini 2.5 Pro (82.5%) and o3-high (77.5%). On CNMO2025—the most challenging of the automated benchmarks with a maximum score of 260—Intern-S1-MO scores 232.4, compared to Gemini 2.5 Pro's 157.5, o3-high's 138.5, and GPT-OSS-120B's 130. This represents a gain of approximately 75 points over the best baseline, which is roughly a 47% relative improvement.

On IMO2025 (non-geometry problems, maximum 35 points), Intern-S1-MO achieves 26 points under pass@4, matching the silver medalist human performance threshold of 21 points and substantially exceeding Gemini 2.5 Pro (14 points), o3-high (12.5 points), and Qwen3-235B-A22B (14 points). The gap of 12 points over the best baseline on IMO2025 represents the largest relative advantage across all benchmarks, consistent with the paper's thesis that the multi-round architecture is most beneficial on the hardest problems.

Intern-S1-mini-MO efficiency. The distilled lite variant, Intern-S1-mini-MO, achieves 87.3% on AIME2025 and 79.2% on HMMT2025, placing it competitively among the full-scale baselines. On CNMO2025, it scores 176.3—already surpassing the best baseline (Gemini 2.5 Pro at 157.5) and nearly matching o3-high (138.5). On IMO2025, it achieves 17 points, exceeding all baselines. The paper presents this as evidence that "the performance gains are primarily attributable to our architectural innovations, and offers compelling evidence that complex mathematical reasoning can be achieved with favorable inference-time efficiency." However, the paper does not provide a parameter count for either Intern-S1 or Intern-S1-Mini, making it impossible to verify the efficiency claim quantitatively.

Performance patterns across difficulty. The paper observes a "qualitative divergence in problem-solving requirements" across benchmarks (Section 5.2). On relatively standard competition sets (AIME2025, HMMT2025), the gap between Intern-S1-MO and strong baselines is "present but narrower," which the authors hypothesize is because "performance in these regimes is partially saturated by models capable of pattern matching and heuristic retrieval from pre-training data." On CNMO2025 and IMO2025, where problems require "the construction of novel proof paths and the synthesis of auxiliary lemmas," Intern-S1-MO's advantage widens substantially. This pattern supports the architectural motivation: the multi-round lemma accumulation mechanism is most valuable when problems exceed the reasoning depth that single-pass models can sustain within their context windows.

IMO2025 contextualization. The paper notes that a score of 26 on IMO2025 "places Intern-S1-MO within the top percentile of global human competitors, outperforming the national team averages of most participating countries." An error analysis indicates that the remaining deficit "largely stems from problems requiring highly idiosyncratic transformations or 'spark-of-insight' constructions that elude systematic search." This is an important honesty about limitations: the architecture excels at systematic, decomposable reasoning but struggles with creative leaps that remain the hallmark of elite human mathematical intuition.

CMO2025 Official Competition Results

Table 3 reports the system's performance in officially participating in CMO2025, which consists of 6 problems each worth 21 points (total 126 points), conducted over two days with 4.5-hour time limits per day. Intern-S1-MO achieved a total score of 102 out of 126, exceeding the gold medal threshold of 78 points by a margin of 24 points. The per-problem breakdown shows full marks (21/21) on four problems (P1, P2, P4, P5) and partial credit on the remaining two (P3: 9/21, P6: 9/21).

For this competition configuration, the paper deployed an expanded search budget: "For each problem, we performed a 256-shot parallel search over up to 12 rounds. For intermediate lemmas, a lemma verifier provided multiple rounds of 8-shot feedback to help assess and refine their correctness. Upon obtaining candidate solutions, we applied an 8-shot refinement procedure comprising 24 rounds." This represents substantially more compute than the default evaluation configuration (8 rounds maximum, 16 rollouts), demonstrating that the system benefits from additional test-time scaling.

Significance of the CMO result. Unlike automated benchmarks where grading is algorithmic, CMO2025 solutions were "scored by human experts using the same standards as those used for human contestants." This eliminates concerns about LLM-judge bias or grading inconsistencies that might affect automated evaluations. The paper states that the system "not only matches the logical rigor and reasoning ability of top-tier high school math olympiad participants but also transcends the limitations of human problem-solving patterns by independently exploring to discover novel solution methods." However, the paper does not provide examples of these "novel solution methods" or compare the system's solutions with human contestants' solutions to substantiate the claim of transcending human patterns.

Ablation Studies and Robustness Checks

The paper presents a single incremental ablation in Table 2, building up from a minimal baseline to the full system. Each row adds one component, and results are reported on HMMT2025, AIME2025, and CNMO2025. IMO2025 is excluded from the ablation due to insufficient problems (only 5) for reliable comparison.

Single-round with Agents (baseline): This is the minimal configuration where "only one round of inference is performed in the agent system," corresponding to the left part of Figure 2. It achieves 70.8% on HMMT2025, 81.9% on AIME2025, and 178.0 on CNMO2025. This baseline already includes the structured prompting and agent architecture (reasoner producing boxed lemmas, etc.) but without multi-round accumulation, verification, or RL training.

+ Multi-round Reasoning: Adding multi-round reasoning with lemma search and summarization (but without theorem verification providing confidence scores for intermediate lemmas, and without the final process verifier revision loop) improves HMMT2025 to 85.4 (+14.6 points), AIME2025 to 91.0 (+9.1 points), and CNMO2025 to 201.7 (+23.7 points). This is the largest single-component gain across all three benchmarks, confirming that the multi-round decomposition itself—even without verification—provides substantial benefits. The CNMO2025 gain is proportionally largest, consistent with the paper's thesis that harder problems benefit most from extended reasoning depth.

+ Theorem Verifier: Adding confidence-scored lemma verification (the left and middle parts of Figure 2, now with intermediate lemma quality assessment) yields modest additional gains: HMMT2025 to 86.3 (+0.9), AIME2025 to 93.3 (+2.3), and CNMO2025 to 203.0 (+1.3). The relatively small improvement from theorem verification suggests that the raw lemma extraction (without verification) already achieves decent quality, or that error propagation from unverified lemmas is not catastrophic at this scale. An alternative interpretation is that the theorem verifier's 4-shot parallel verification (with unknown base verifier accuracy) may not be sufficiently discriminative to filter out many incorrect lemmas beyond what the summarizer already does implicitly.

+ Process Verifier: Adding the full inference workflow with OPV-based final solution verification and iterative revision improves HMMT2025 to 89.1 (+2.8), AIME2025 to 94.0 (+0.7), and CNMO2025 to 215.2 (+12.2). The CNMO2025 gain is dramatically larger than the gains on the other two benchmarks, suggesting that the process verifier's revision loop is particularly valuable for proof-based problems (CNMO2025) compared to solution-based problems (AIME2025, HMMT2025). This aligns with the paper's design rationale: OPV provides step-level feedback on logical rigor, which is more critical for proof problems than for final-answer problems where outcome checking may suffice.

+ OREAL-H: Adding the full RL training framework with lemma dependency graph credit assignment and conjugate reward modeling yields the final gains: HMMT2025 to 95.0 (+5.9), AIME2025 to 96.6 (+2.6), and CNMO2025 to 232.4 (+17.2). The pattern is consistent with the process verifier addition: the largest gains are on CNMO2025, the hardest benchmark. This suggests that RL training is most beneficial precisely where the base model's single-round performance is weakest—the RL signal provides meaningful learning on problems that the untrained agent struggles with, while problems that are already near-ceiling (AIME2025 at 94.0%) have less room for improvement.

Cumulative improvement. From the "Single-round with Agents" baseline to the full "+ OREAL-H" system, the total gains are: HMMT2025 +24.2 points (70.8 → 95.0), AIME2025 +14.7 points (81.9 → 96.6), CNMO2025 +54.4 points (178.0 → 232.4). The disproportionate improvement on CNMO2025 (both in absolute terms and relative to the score ceiling of 260) provides the strongest evidence for the paper's central claim that the multi-round architecture is specifically effective for "ultra-hard" problems requiring extended reasoning depth.

Missing ablations. Several ablations that would strengthen the paper's claims are absent:

Number of reasoning rounds: The paper fixes the maximum at 8 rounds but does not ablate this choice. How does performance scale with 2, 4, 6, or 12 rounds? Is there diminishing returns, and if so, where? This would clarify whether the 8× context extension claim is about achieved depth or merely theoretical capacity.
Number of parallel verification passes: The Theorem Verifier uses 4 parallel passes and the OPV conjugate reward uses 4 verification trials, but these numbers are not ablated. Would 2 or 8 passes significantly change performance?
Lemma confidence threshold: At what confidence score are lemmas accepted into the library? How does varying this threshold affect error propagation versus missed useful lemmas?
OREAL-H vs. simpler RL baselines: How would the system perform with standard outcome-only RLVR (no lemma graph, no conjugate reward) versus the full OREAL-H? This is the most critical missing ablation because it would directly test whether the paper's theoretical innovations (lemma dependency graph, conjugate reward) provide empirical benefits beyond simpler alternatives.
Per-component contribution of OREAL-H: OREAL-H combines lemma dependency graph credit assignment, conjugate reward modeling, and the cold-start cloning procedure. Which of these components contributes most to the final gains? An ablation within OREAL-H (e.g., removing the conjugate reward and using raw verification ratios, or removing the lemma graph and using temporal credit assignment) is not provided.

Critical Assessment

Central Claim 1: Multi-round hierarchical reasoning with lemma memory extends effective reasoning depth approximately 8× beyond the 64K token limit, enabling Olympiad-level performance.

The evidence broadly supports this claim but with important qualifications. The ablation study (Table 2) demonstrates that adding multi-round reasoning provides the single largest performance gain (e.g., CNMO2025 from 178.0 to 201.7), and the final system achieves gold-medal performance on CMO2025 (Table 3). However, the "8×" figure is an informal estimate (using about 512K tokens across all rounds versus a 64K single-pass limit), not a controlled measurement. The paper does not directly compare Intern-S1-MO's multi-round architecture against a single-round model with a proportionally longer context window (e.g., 512K tokens) using the same base model. Without this comparison, it's unclear whether the gains come from the structured decomposition (lemma memory, summarization, verification) or simply from having more total tokens to think with. The finding that the system achieves gold medal at CMO2025 under human time constraints is compelling, but the competition configuration used substantially more compute (256-shot parallel search with 12+24 rounds) than the standard evaluation, making it a demonstration of what the architecture can achieve at scale rather than what it typically achieves at the default budget.

Additionally, the paper explicitly acknowledges that the remaining IMO deficit "stems from problems requiring highly idiosyncratic transformations or 'spark-of-insight' constructions that elude systematic search." This is a genuine limitation: the architecture helps with problems that can be decomposed into incremental lemma-proving steps, but does not help with problems requiring non-decomposable creative leaps. The claim should be understood as: for decomposable Olympiad problems, multi-round lemma memory enables reasoning depth that exceeds single-pass context limits; for non-decomposable problems, the architecture provides no advantage.

Central Claim 2: OREAL-H, with lemma dependency graph credit assignment and conjugate reward modeling, effectively trains the multi-round agent using online RL, yielding significant performance improvements over the untrained system.

The evidence supports this claim but cannot disentangle which components of OREAL-H are responsible. Table 2 shows that "+ OREAL-H" adds substantial gains over the "+ Process Verifier" baseline (e.g., CNMO2025 +17.2 points). However, OREAL-H is a bundle of techniques (cold-start cloning, lemma graph credit assignment, conjugate reward, OREAL loss with KL regularization), and no ablation isolates their individual contributions. A critic could argue that the gains might come primarily from the cold-start data quality or from having any form of RL training (even simple outcome-only RLVR), rather than from the specific innovations of lemma dependency graphs and conjugate rewards. The paper's theoretical motivation for these components is strong (Section 4.3), but the empirical validation is incomplete without controlled ablations.

Moreover, the RL training process has several potential confounding factors. The paper filters out problems with pass rates of 0 or 1 (Section 4.2, Algorithm 1), which means RL training only occurs on problems of intermediate difficulty. This filtering could explain part of the gain: the model is not wasting capacity on trivially easy or impossibly hard problems. The paper's claim that OREAL-H specifically enables learning from process-level feedback would be strengthened by showing that the gains persist (or are larger) on the hardest problems—exactly where process feedback should matter most—compared to outcome-only RL. The CNMO2025 gain of 17.2 points is consistent with this pattern, but without a head-to-head comparison against outcome-only RL on the same filtered problem set, it's suggestive rather than definitive.

Central Claim 3: Intern-S1-MO achieves state-of-the-art performance on Olympiad-level benchmarks, surpassing all evaluated baselines including proprietary models like Gemini 2.5 Pro and o3-high.

This claim is the most straightforwardly supported by the evidence in Table 1, but several caveats apply. First, the baseline evaluations are not fully controlled. For AIME2025 and HMMT2025, baseline scores are taken from technical reports or Matharena, which may use different evaluation protocols (temperature, number of samples, pass@k estimator) than those used for Intern-S1-MO. The paper does not specify the sampling parameters for baseline evaluations, making it impossible to verify that the comparison is fair. For IMO2025 and CNMO2025, the paper states that baselines were evaluated "using its own grading infrastructure," which mitigates this concern, but the number of samples per baseline model is not reported.

Second, the baseline models (Gemini 2.5 Pro, o3-high, Grok4) are general-purpose reasoning models that were not specifically designed or optimized for multi-round Olympiad problem solving. They are evaluated with whatever default inference configuration their creators intended (likely single-pass with internal chain-of-thought). Intern-S1-MO, by contrast, uses a purpose-built multi-agent architecture with up to 512K tokens of inference compute. This is not a like-for-like comparison in terms of either architecture or compute budget. A more rigorous comparison would give the baseline models an equivalent total token budget (e.g., by running multiple sequential refinement passes with a simpler prompt, or by sampling multiple solutions with best-of-N selection), but this is not attempted.

Third, the paper does not report results on standard easier benchmarks (e.g., MATH, GSM8K) where the architectural overhead might be unnecessary or even harmful. This makes it difficult to assess whether Intern-S1-MO genuinely advances the state of the art across mathematical reasoning or specifically on the narrow slice of Olympiad-hard problems for which it was designed. The paper's own hypothesis—that single-pass models already perform well on easier problems through "pattern matching and heuristic retrieval"—implies that Intern-S1-MO might underperform simpler approaches on easier benchmarks due to unnecessary multi-round overhead or verification errors.

Central Claim 4: The system's architectural innovations, not model scale, are primarily responsible for performance gains.

This claim is supported by the Intern-S1-mini-MO results (Table 1), which show that a distilled lite variant achieves scores competitive with or exceeding the best full-scale baselines (e.g., 176.3 on CNMO2025 versus Gemini 2.5 Pro's 157.5). However, the paper does not disclose the parameter count of Intern-S1-mini-MO or Intern-S1-MO, nor does it provide a FLOPs comparison between the two. Without knowing the scale difference, it's impossible to assess how impressive the "lite" performance truly is—if Intern-S1-mini-MO is only 2× smaller than Intern-S1-MO, the result is less striking than if it is 10× smaller. The paper's statement that "performance gains are primarily attributable to our architectural innovations" is a plausible interpretation of the data but is not rigorously established without scale-controlled comparisons.

Additional weaknesses in experimental design:

Single base model family. All experiments use Intern-S1 variants. There is no demonstration that the multi-round architecture transfers to other base models (e.g., Qwen, DeepSeek, Llama). This leaves open the possibility that the gains depend on specific properties of Intern-S1's training or architecture.
Small IMO2025 test set. With only 5 non-geometry problems, pass@4 estimates are extremely noisy. A 2-point difference on IMO2025 (e.g., 26 vs. 24) could result from a single problem being solved in one configuration but not another, making it impossible to draw statistically reliable conclusions about relative performance on this benchmark. The paper acknowledges this implicitly by excluding IMO2025 from the ablation study.
No confidence intervals. None of the benchmark results in Table 1 or the ablation results in Table 2 report any measure of uncertainty. For pass@1 estimated from 16 rollouts, the sampling error is non-trivial—a 95% score could reasonably be 92% or 97% depending on the specific rollouts. Without error bars, small differences between configurations (e.g., 203.0 vs. 215.2 in the ablation) cannot be interpreted as reliable improvements.
Difficulty estimation cost not discussed. The prior paper analysis identified difficulty estimation cost as a major unaccounted factor in compute-optimal scaling. Intern-S1-MO faces an analogous issue: the system runs up to 8 reasoning rounds plus 8 revision rounds, with multiple parallel verifications per lemma. The paper reports total token usage (~512K tokens per problem) but does not compare this against the baseline models' token consumption. If Intern-S1-MO uses 10× more inference compute than Gemini 2.5 Pro to achieve a 12-point advantage on IMO2025, the efficiency picture changes substantially.
Grading protocol for baselines. The paper developed a fine-grained rubric-based grading scheme (Appendix D) and used 8-way ensemble LLM judging. It states that baselines were evaluated using this same infrastructure for IMO2025 and CNMO2025, which is good practice. However, it does not report inter-rater reliability of the 8 judges, calibration against human expert judgments (except for CMO2025, where human judging was used), or whether the grading scheme was validated against the official IMO/CNMO scoring guides. Without this, the absolute scores may not be comparable to officially reported IMO/CNMO results.

Experiments that would have strengthened the paper:

Head-to-head RL comparison: OREAL-H vs. standard outcome-only RLVR on the same problem distribution and base model, with matched compute budgets. This would isolate the contribution of the lemma dependency graph and conjugate reward.
Context-length scaling baseline: Intern-S1 evaluated with a single 512K-token context window (if feasible) versus the multi-round 8 × 64K architecture. This would test whether the gains come from structure or just from total thinking budget.
Round-count scaling analysis: Performance as a function of the number of reasoning rounds (1, 2, 4, 8, 12) to characterize the shape of the scaling curve and identify diminishing returns.
Baseline models with matched inference budget: Give Gemini 2.5 Pro or o3-high an equivalent ~512K token budget through repeated sampling, best-of-N, or sequential refinement, and compare against Intern-S1-MO.
Difficulty-stratified analysis: Break down performance by problem difficulty (following the prior paper's quintile binning approach) to test whether Intern-S1-MO's advantage is concentrated on the hardest problems as the paper claims.
Verifier quality ablation: Evaluate the system with different verifier qualities (e.g., by degrading the OPV through reduced ensemble size) to characterize sensitivity to verification accuracy—a critical practical consideration since OPV's 85% F1 leaves room for improvement.

6. Limitations and Trade-offs

1. The System Cannot Solve Problems Requiring Non-Decomposable Creative Insight

The assumption or constraint. Intern-S1-MO's architecture is built on the premise that Olympiad-level problems can be decomposed into a sequence of lemma-proving steps, each of which makes incremental progress toward a complete solution. The reasoner agent is explicitly prompted to embrace partial solutions and produce intermediate lemmas when a full solution is out of reach (Appendix A.1). This design assumes that problems have decomposable structure—that there exist useful intermediate results which, when accumulated across rounds, eventually unlock the final proof.

The paper acknowledges a failure mode of this assumption directly:

"Preliminary error analysis indicates that the remaining deficit largely stems from problems requiring highly idiosyncratic transformations or 'spark-of-insight' constructions that elude systematic search." (Section 5.2)

The consequence. On problems requiring a single creative leap that cannot be usefully decomposed into incremental lemmas, Intern-S1-MO provides no advantage over single-pass models. The multi-round architecture may even be counterproductive: the system expends substantial compute on lemma search and summarization that yields no useful intermediate results, and the accumulated (empty or irrelevant) lemma library provides no benefit to subsequent rounds. The consequence is not merely that the system fails on these problems—it fails expensively, using 8× or more compute than a single-pass attempt that would also fail, but faster and cheaper.

This limitation is structural, not parameter-dependent. The OREAL-H training procedure optimizes the model to produce useful lemmas and make partial progress, but it cannot teach the system to decompose problems that are fundamentally non-decomposable. A problem where the core difficulty is recognizing a non-obvious invariant, applying an obscure theorem in a novel way, or constructing an ad hoc combinatorial object may have no useful intermediate lemma that can be established independently—you either see the key insight or you don't. The paper's framework has no mechanism for generating such insights beyond random exploration across rounds, which the 8-round limit and 64K-token context windows constrain.

What evidence exists in the paper. The CMO2025 results (Table 3) provide indirect evidence: the system achieved full marks (21/21) on four problems but partial credit (9/21) on problems P3 and P6. The paper does not analyze what made P3 and P6 different from the fully solved problems, but the error analysis quote above suggests that problems requiring "spark-of-insight" constructions are the likely culprits. The IMO2025 results (Table 1) show a score of 26/35, with the remaining 9 points (across 5 problems, so roughly 1.8 points per problem on average) representing the gap that systematic decomposition cannot close. The pass@4 metric on IMO2025—where the system gets 4 attempts per problem—still leaves some problems unsolved, indicating that even multiple independent reasoning trajectories fail to bridge the insight gap.

The paper does not provide a difficulty-stratified analysis (e.g., classifying problems by decomposability and showing performance differentials), which would directly quantify the scope of this limitation. The ablation study (Table 2) does not distinguish between problem types.

Mitigation status. Not addressed, and the authors are transparent about this. The limitation is presented as a factual boundary condition rather than a solvable engineering problem within the current framework. The conclusion states that "the remaining deficit largely stems from problems requiring highly idiosyncratic transformations"—this is an acknowledgment, not a roadmap. The system provides no mechanism for generating creative insights, and the RL training (OREAL-H) optimizes for lemma production and verification, which reinforces the existing decomposition strategy rather than developing alternative problem-solving approaches.

A practitioner deploying this system should expect strong performance on problems with clear decomposable structure (proving inequalities through incremental bounds, combinatorial problems with case analysis, algebraic manipulations that can be broken into lemma chains) and weak performance on problems requiring a single non-obvious construction or transformation. The CMO2025 full-marks on 4/6 problems suggests the decomposable category may be the majority in competition mathematics, but the two partial-credit problems demonstrate that the boundary is real and practically significant.

2. Lemma Quality Control Relies Entirely on Learned Verifiers with No Formal Correctness Guarantees

The assumption or constraint. Intern-S1-MO operates entirely in natural mathematical language with LaTeX formatting, using learned verifiers (the Theorem Verifier for intermediate lemmas, OPV for final solutions) to assess logical correctness. Unlike formal proof assistants (Lean, Isabelle) that provide machine-checkable certificates of correctness, these learned verifiers produce probabilistic judgments with a non-trivial error rate. The paper cites OPV's performance: "their verifier achieves an F1-score greater than 85% on ProcessBench" (Section 3, Process Verification paragraph). An F1 > 85% means that in the best case, roughly 15% of verifier judgments are wrong—either false positives (flawed logic marked as correct) or false negatives (valid logic marked as incorrect).

The Theorem Verifier uses 4 parallel verifications per lemma and computes a confidence score as the proportion passing, but this ensemble approach reduces variance without eliminating bias—if the underlying verifier has systematic blind spots (e.g., consistently missing a particular class of logical error), four independent runs will all share that blindness. The paper does not provide an F1 score or calibration analysis specifically for the Theorem Verifier component.

The consequence. Error propagation is the central risk. Section 3 frames this explicitly:

"if [the system and model] rely on erroneous historical premises, they will expend significant resources trying to validate questionable results. Such a problem is compounded by error propagation, so that a flawed intermediate conclusion can mislead subsequent deductive directions, leading to circular reasoning or invalid proofs."

The probability of at least one flawed lemma entering the library grows with the number of rounds and the number of lemmas per round. If we assume optimistically that each lemma verification has a 5% false-positive rate (better than OPV's reported F1 suggests), and the system extracts an average of, say, 3 new lemmas per round over 8 rounds (24 total lemmas), the probability that at least one incorrect lemma passes verification is approximately 1 − (0.95)^24 ≈ 71%. This is a back-of-the-envelope estimate given the paper's lack of precise verifier calibration data, but it illustrates the structural vulnerability: the system is probabilistically almost certain to admit some errors over a full multi-round run, and a single error early in the dependency chain can invalidate all subsequent reasoning built upon it.

There is a second, subtler failure mode: the verifier may reject correct but non-obvious lemmas (false negatives), preventing useful intermediate results from entering the library. This would cause the system to waste subsequent rounds re-deriving results that were actually already proven, or to fail to build on progress that was genuinely made. The paper's Theorem Verifier confidence scoring partially mitigates this (low-confidence lemmas might be flagged for re-proving rather than discarded), but the mechanism is not fully specified.

For the final solution, the OPV-based revision loop can catch some errors that slipped through lemma verification, but OPV has the same ~15% error rate. A solution that builds on a subtly flawed lemma—where the flaw is non-obvious and the downstream reasoning appears logically consistent given the (incorrect) premise—may pass OPV verification with high confidence. The outcome gating (Section 4.3: "for problems amenable to outcome supervision, the final reward R is set to 0 if the final answer is incorrect") catches this for solution-based problems with verifiable answers, but proof-based problems (IMO, CMO) have no such safety net—an incorrect proof with an accidentally correct conclusion would receive full credit under verifier-based evaluation.

What evidence exists in the paper. The paper does not provide a direct measurement of lemma-level false positive/negative rates. The CMO2025 results (Table 3) show that human experts found issues in two of six solutions (P3 and P6 received 9/21 rather than full marks), which could reflect either genuine solution incompleteness or verifier-approved flaws that humans detected. However, the paper does not analyze whether the point deductions stemmed from verifier errors or from the system's inability to find complete solutions.

The ablation study (Table 2) shows that adding the Theorem Verifier ("+ Theorem Verifier") provides only modest gains over the unverified multi-round baseline: +0.9 on HMMT2025, +2.3 on AIME2025, +1.3 on CNMO2025. This small delta is ambiguous—it could mean that the baseline already extracts high-quality lemmas (making verification redundant), or that the verifier is too noisy to provide substantial filtering benefit, or that error propagation is not catastrophic at the tested scale. The paper does not investigate which interpretation is correct.

Mitigation status. Partially addressed through ensemble verification and the revision loop, but the fundamental gap—statistical rather than logical correctness guarantees—is not resolved. The paper does not compare its learned-verifier approach against a formal-verification baseline on problems where formalization is feasible, which would quantify the accuracy tradeoff. The authors do not propose a path toward formal correctness guarantees, nor do they discuss the possibility of hybrid systems that use learned verifiers for efficiency but fall back to formal verification for critical lemmas. The limitation is structural: the entire architecture assumes that "good enough" verification suffices for Olympiad-level reasoning, but the paper provides no evidence that the current verifier quality is actually "good enough"—the 85% F1 ceiling is stated as a fact without discussion of whether this level of reliability is adequate for proofs where a single error invalidates the entire solution.

3. Inference Compute Cost Is Not Controlled or Compared Against Baselines

The assumption or constraint. Intern-S1-MO's reported results are achieved with a substantially larger inference budget than the baseline models against which it is compared. The default configuration (Appendix B.1) uses up to 8 reasoning rounds with the Reasoner and Summarizer agents each capped at 64K output tokens, 4 parallel verifications per lemma for the Theorem Verifier, and up to 8 rounds of iterative revision with the Process Verifier. The paper states that this enables "about 512K tokens to solve a single problem" compared to the 64K single-pass limit of conventional LRMs. The pass@1 metric is computed from 16 independent rollouts per problem (Section 5.1), meaning the raw compute to produce a single reported accuracy number is 16 × 512K ≈ 8.2M tokens of generation—not counting the verifier inference costs, which add additional parallel passes.

The CMO2025 competition configuration (Section 5.4) used an even larger budget:

"For each problem, we performed a 256-shot parallel search over up to 12 rounds. For intermediate lemmas, a lemma verifier provided multiple rounds of 8-shot feedback... Upon obtaining candidate solutions, we applied an 8-shot refinement procedure comprising 24 rounds."

This is multiple orders of magnitude more compute than the default configuration, and the paper does not report the total token consumption or FLOPs for this setting.

The consequence. The headline comparisons in Table 1—where Intern-S1-MO achieves 95% on HMMT2025 versus Gemini 2.5 Pro's 82.5%, or 26 on IMO2025 versus Gemini's 14—are not compute-controlled. The baseline models are evaluated with whatever default inference configuration their creators intended, which likely involves single-pass generation with internal chain-of-thought (possibly with multiple samples for pass@k estimation). Intern-S1-MO's reported numbers use a purpose-built multi-agent architecture consuming roughly 8× more tokens per rollout than a single-pass 64K model, plus additional verifier inference.

Without a FLOPs-matched or token-matched comparison, the performance gap cannot be attributed to architectural sophistication versus simply spending more compute. A practitioner choosing between deploying Intern-S1-MO and using Gemini 2.5 Pro with best-of-N sampling or sequential refinement (to match the token budget) has no data to inform that decision. The paper's claim that "performance gains are primarily attributable to our architectural innovations" (Section 5.2) is plausible but unverified under controlled compute budgets.

The compute disparity is most extreme for the CMO2025 result (102/126). This used a 256-shot parallel search with additional verification and revision rounds, consuming vastly more compute than the default evaluation configuration. The paper presents this as evidence of the system's capability, which it is—but it does not acknowledge that a human contestant operating under a 4.5-hour time limit has a hard compute constraint (one brain, sequential reasoning) while the system benefits from massive parallelism (256 independent reasoning trajectories explored simultaneously). The gold medal comparison against human contestants is not compute-equivalent; the system had access to computational resources far exceeding what any human could deploy.

What evidence exists in the paper. The paper provides no direct comparison. Table 1 reports scores for both Intern-S1-MO and baselines, but there is no column for "inference tokens used," "FLOPs consumed," or "wall-clock time." The ablation study (Table 2) compares configurations within Intern-S1-MO but never against a baseline model given equivalent compute. The CMO2025 section (5.4) describes the expanded budget but does not quantify it in terms that would enable comparison with the default budget or with human problem-solving time.

Mitigation status. Not addressed. The paper does not acknowledge the compute disparity as a limitation, nor does it propose a compute-controlled experimental protocol. The prior paper analysis (from the context provided) established a framework for FLOPs-matched pretraining-vs-inference comparisons; Intern-S1-MO does not engage with this methodology. The closest the paper comes to a compute-efficiency argument is the Intern-S1-mini-MO results (Table 1), which show that a distilled model can achieve competitive scores. However, Intern-S1-mini-MO's parameter count is not disclosed, its inference budget is not compared to Intern-S1-MO's or to baselines', and its scores are lower than Intern-S1-MO's—so this does not constitute a controlled efficiency comparison.

A rigorous evaluation would compare Intern-S1-MO and baseline models at matched total token budgets: e.g., give Gemini 2.5 Pro the same ~512K token budget per problem (through repeated sampling, sequential refinement, or majority voting) and compare scores. Without this, the headline performance numbers are upper bounds on what the architecture can achieve with generous compute, not evidence of pareto-optimality in the accuracy-efficiency tradeoff space.

4. Evaluations Are Based on a Single Base Model Family with No Cross-Model Transfer Evidence

The assumption or constraint. All experiments—cold-start training, RL training, and evaluation—use variants of Intern-S1 as the base model. The paper states: "built on Intern-S1, we developed Intern-S1-MO" (Section 5.1), and the distilled variant uses Intern-S1-Mini. The multi-agent architecture, the lemma extraction prompts, the verifier models (CompassVerifier, OPV), and the OREAL-H training procedure are all tightly coupled to Intern-S1's output distribution, reasoning style, and failure modes.

The paper does not test whether the same architecture and training procedure would yield similar gains when applied to a different base model (e.g., DeepSeek-R1, Qwen3, Llama-4). It also does not test whether the verifiers (OPV, CompassVerifier) transfer to evaluating reasoning from other model families, or whether the cold-start data generated from Intern-S1 would be effective for fine-tuning other models.

The consequence. The claimed innovations—multi-round lemma memory, OREAL-H credit assignment, conjugate reward modeling—are validated only on Intern-S1. It is unknown whether these are general techniques that improve any sufficiently capable LRM, or whether they are specific optimizations that work well for Intern-S1's particular characteristics. Several components could be model-specific:

Lemma extraction quality: The structured output format (Appendix A.1) requires the base model to reliably produce boxed lemmas with step-by-step proofs. A model with different instruction-following behavior or different mathematical reasoning style might produce poorly formatted or semantically invalid lemma structures, breaking the summarizer's extraction pipeline.
Verifier calibration: OPV achieves >85% F1 on ProcessBench, but this metric was presumably computed on Intern-S1-like outputs. If a different base model produces reasoning traces with different error patterns (e.g., more subtle logical gaps, different mathematical conventions), OPV's accuracy could degrade substantially. The paper does not evaluate OPV on out-of-distribution reasoning traces.
OREAL-H training dynamics: The lemma dependency graph construction and round-level advantage computation assume that the model produces well-defined lemmas with clear derivation relationships. A model with different exploration behavior—e.g., one that tends to produce long, unstructured reasoning rather than discrete lemma blocks—might not generate usable dependency graphs, causing the credit assignment mechanism to fail.
Cold-start data distribution: The cold-start trajectories are generated by Intern-S1 variants on AoPS and in-house problem sets. These trajectories encode Intern-S1-specific reasoning patterns; fine-tuning another model on them might produce suboptimal results due to distribution mismatch.

The practical consequence is that a practitioner using a different base model cannot rely on the paper's reported performance numbers as predictive of what they would achieve. They would need to re-execute the entire pipeline—cold-start data generation, verifier training/calibration, behavioral cloning, RL training—and there is no guarantee that the gains would transfer.

What evidence exists in the paper. None. The paper does not include any experiments with non-Intern-S1 base models, nor does it discuss the transferability of the architecture. The related work section cites models from other families (DeepSeek-R1, Qwen3) as baselines for evaluation but never as base models for the Intern-S1-MO architecture. The verifier models (CompassVerifier, OPV) are described in terms of their own benchmark performance, not in terms of their robustness to distribution shift across model families.

Mitigation status. Not addressed. The paper does not acknowledge this as a limitation, nor does it propose cross-model experiments as future work. This is a significant gap for a systems paper that claims architectural innovation as its primary contribution: if the architecture is the key insight, it should in principle transfer across base models. The absence of any transfer experiment leaves open the possibility that Intern-S1-MO's gains are specific to Intern-S1 and would not replicate with other models. A minimal demonstration would be applying the multi-round lemma memory architecture (without OREAL-H training) to one other open-weights model and showing that the multi-round gains persist, establishing that the architecture rather than the base model drives the improvement.

5. The System Provides No Mechanism for Recognizing or Terminating Unproductive Reasoning Trajectories

The assumption or constraint. Intern-S1-MO allocates a fixed maximum budget of 8 reasoning rounds plus 8 revision rounds (Appendix B.1), with each round consuming up to 64K output tokens from the Reasoner, Summarizer, or both. The system does not have an explicit mechanism for detecting when further rounds are unlikely to produce progress and terminating early. The paper states that the system "initiates multi-round exploration only for challenging tasks, ensuring efficient resource allocation" (Section 3, Decomposing Sub-Problems), but the mechanism for deciding task difficulty and adapting the round budget is not described anywhere in the paper.

In practice, the system appears to run all or most rounds for every problem—the 8-round maximum is a fixed ceiling, not an adaptive limit. The counter-evidence is that the CMO2025 configuration used "up to 12 rounds" for the reasoner and 24 rounds for revision, suggesting the system always runs to its configured limit rather than self-terminating.

The consequence. The system wastes substantial compute on problems where early rounds have already converged or stalled. Several scenarios produce unproductive later rounds:

Early success: If the reasoner produces a correct complete solution in round 1 or 2, subsequent rounds serve no purpose—the process verifier and revision loop could directly process that solution without additional lemma search. The paper does not describe early stopping when a high-confidence solution is found.
Stalled progress: If rounds 3–8 produce no new verified lemmas (the existing library already contains everything the model can discover), the system still executes the full budget, with the reasoner generating reasoning traces that the summarizer finds contain no new lemmas, and the theorem verifier having nothing to verify. The round-level advantage masking in OREAL-H (Section 4.3.1: "For intermediate rounds yielding no new lemmas, the advantage is effectively masked") prevents these rounds from contributing to training, but at inference time they still consume compute.
Fundamentally unsolvable problems: For problems in the "spark-of-insight" category (Limitation 1) or difficulty bin 5 (from the prior paper's taxonomy—problems where the base model's pass@1 is near zero), all 8 rounds produce essentially no progress, but the system runs them anyway.

The waste is multiplicative: 16 independent rollouts × 8 rounds × 2 agents (reasoner + summarizer) × 64K tokens = up to ~16.4M tokens of generation per problem in the default evaluation configuration, plus verifier inference. A system that could detect futility after, say, 2 rounds and terminate would use 4× less compute on hard problems while losing nothing (since later rounds wouldn't produce useful results anyway).

What evidence exists in the paper. Indirect evidence comes from the ablation study (Table 2). The "Single-round with Agents" baseline achieves 70.8/81.9/178.0 on HMMT/AIME/CNMO. Adding multi-round reasoning ("+ Multi-round Reasoning") provides the largest gain: +14.6/+9.1/+23.7. But the diminishing returns from subsequent additions (Lemma Verifier adds ≤2.3 points, Process Verifier adds ≤12.2, OREAL-H adds ≤17.2) suggest that not all rounds are equally valuable—the majority of the gain comes from the first few rounds of decomposition, with later refinements providing smaller increments. However, the paper does not analyze performance as a function of round count, so this is speculative.

The IMO2025 results provide circumstantial evidence: the pass@4 score of 26/35 means that even with 4 independent 8-round trajectories per problem, some problems remain unsolved. On those problems, all 4 × 8 = 32 rounds across trajectories were unproductive, yet the system has no way to know this in advance and avoid the expenditure.

Mitigation status. Minimally addressed. The paper mentions adaptive resource allocation as a feature ("initiates multi-round exploration only for challenging tasks") but provides no mechanism, no experiments evaluating it, and no analysis of how much compute is wasted on problems that don't benefit from additional rounds. The OREAL-H training framework masks non-progress rounds during RL (setting advantage to zero), which prevents those rounds from distorting training, but this is a training-time mechanism that does not affect inference-time compute consumption.

This limitation is related to the difficulty estimation cost problem from the prior paper analysis: Intern-S1-MO has no way to estimate problem difficulty before committing to the full multi-round budget, and it has no mechanism for dynamically adjusting the budget based on intermediate progress signals (e.g., "lemma library hasn't grown in 2 rounds, terminating"). Such a mechanism would require a meta-cognitive assessment capability—judging whether current progress justifies continued exploration—which is not part of the current architecture. The paper does not propose this as future work.

6. The Paper Does Not Ablate or Justify Key Hyperparameters, Particularly the Number of Rounds and Verification Passes

The assumption or constraint. Intern-S1-MO's architecture involves numerous hyperparameter choices that are stated as defaults without empirical justification or sensitivity analysis. The most consequential include:

Maximum reasoning rounds: 8 (Appendix B.1). Why 8? The paper provides no scaling analysis showing how performance varies with round count, no evidence of diminishing returns, and no comparison against 4, 12, or 16 rounds. The CMO2025 configuration used 12 rounds, suggesting that more rounds are beneficial, but the relationship is uncharacterized.
Maximum revision rounds: 8 (Appendix B.1), with 24 used in the CMO2025 configuration. No ablation studies the effectiveness of revision as a function of round count.
Parallel verification passes: 4 for the Theorem Verifier, 4 for the OPV conjugate reward computation (Section 4.3.2: "we fix n = 4, balancing verification cost and signal fidelity"). The paper states this choice "balances verification cost and signal fidelity" but provides no data on how varying n affects either. Would 2 passes suffice? Would 8 passes substantially improve lemma quality? The conjugate reward formula R(k, n) depends strongly on n—a solution passing 2/2 checks receives R(2, 2) ≈ 2.0, while one passing 4/4 receives R(4, 4) ≈ 5.5, but the paper doesn't discuss whether the choice of n = 4 optimizes some tradeoff or was chosen arbitrarily.
Lemma confidence threshold: What confidence score is required for a lemma to be accepted into the library? The paper never states this threshold. If it's 1.0 (all 4 verification passes must succeed), then the effective false-negative rate could be high—a correct lemma that one verifier mistakenly flags (15% error rate, so ~48% chance of at least one rejection in 4 trials for a correct lemma, assuming independence) would be excluded. If the threshold is lower (e.g., 0.5), false positives increase. The threshold directly controls the precision-recall tradeoff for the lemma library, yet it is not specified or studied.
Number of RL rollouts per question: 16 (Section 4.2). The lemma dependency graph aggregates across these rollouts—why 16? More rollouts provide richer dependency graphs but cost proportionally more compute. No ablation studies this tradeoff.
KL penalty coefficient: β = 0.01 (Appendix B.2). This is a critical hyperparameter for RL training—too high and the policy can't improve; too low and it diverges or over-optimizes the verifier. The paper provides no sensitivity analysis.

The consequence. The reported results are tied to specific hyperparameter settings whose generalizability is unknown. A practitioner attempting to reproduce the system faces a large configuration space with no guidance on which parameters matter most, what values are reasonable, or how performance scales with resource allocation.

More importantly, the absence of hyperparameter analysis makes it impossible to evaluate whether the claimed architectural innovations are robust or brittle. If, for example, the system only works well at exactly 8 rounds and degrades at 6 or 10, that would suggest the architecture is fragile and the 8-round choice was tuned to the test benchmarks. Conversely, if performance improves monotonically with round count (as the CMO's use of 12 rounds hints), then the 8-round default is an arbitrary constraint and the reported scores understate the system's potential—but also overstate its efficiency relative to what a practitioner would need to deploy (since deploying 12+ rounds would be even more expensive).

The OREAL-H framework's complexity (hierarchical MDP, lemma dependency graphs, conjugate reward, cold-start cloning, outcome gating) creates many potential interaction effects between hyperparameters that are entirely unexplored. The RL training dynamics may depend sensitively on the balance between round count (which affects trajectory length and advantage variance), verification ensemble size (which affects reward noise), and KL penalty (which affects exploration).

What evidence exists in the paper. The ablation study (Table 2) varies components (multi-round, theorem verifier, process verifier, OREAL-H) but keeps all hyperparameters at their default values for each configuration. There is no experiment varying the round count, verification passes, confidence thresholds, RL rollouts per question, or KL coefficient. The CMO2025 section (5.4) uses different settings (12 reasoning rounds, 24 revision rounds, 256-shot parallel search) but reports only final scores without analyzing how these choices affected performance relative to the defaults.

The paper's statement that n = 4 verification passes was chosen for "balancing verification cost and signal fidelity" is the closest thing to a hyperparameter justification, but it is a qualitative assertion without supporting data. The conjugate reward derivation (Section 4.3.2) shows how R(k, n) varies with k/n, but does not explore how the choice of n affects downstream RL performance.

Mitigation status. Not addressed. The paper does not acknowledge the absence of hyperparameter analysis as a limitation, nor does it provide guidance for practitioners on configuring the system. This is a standard expectation for systems papers—particularly ones claiming practical applicability—and its absence weakens the reproducibility and deployability of the work. The hyperparameters are stated in appendices (B.1, B.2) as implementation details, but they are not studied as experimental variables. A thorough hyperparameter sensitivity analysis, or at minimum a discussion of which parameters are most critical and how they were chosen, would substantially strengthen confidence in the reported results.

7. Implications and Future Directions

How This Work Changes the Landscape

Intern-S1-MO introduces a reframing of reasoning depth as a memory management problem rather than a context-length scaling problem. This is not a paradigm shift that displaces existing approaches—single-pass chain-of-thought models remain dominant for most tasks, and formal verification systems remain the gold standard for correctness guarantees—but it is a substantial conceptual reframing that opens a third architectural axis between "scale the context window" and "formalize everything." The paper demonstrates convincingly that structured, natural-language memory (the lemma library) can provide roughly 8× the effective reasoning depth of a single-pass model without requiring either hardware advances (longer contexts) or formal logic translation (proof assistants).

The significance of this reframing extends beyond the raw Olympiad scores. It establishes that the unit of reasoning progress is the lemma, not the token. This is a diagnostic concept that changes how researchers should think about scaling inference: rather than measuring "how many tokens did the model generate?" the relevant question becomes "how many verified intermediate results did the model accumulate?" This shift in measurement suggests a different optimization target—not raw throughput, but lemma throughput per unit compute—and invites the development of systems that explicitly maximize verified knowledge accumulation rather than generation volume.

Reconciling prior contradictions. The paper helps resolve a tension that has existed in the mathematical reasoning literature between two camps: those who argue that "LLMs can self-correct reasoning" (citing prompt-based self-reflection and iterative refinement results) and those who argue that "LLMs cannot self-correct reasoning" (citing studies showing that naive self-correction degrades or fails on hard problems). Intern-S1-MO's architecture provides a reconciliation: self-correction works when it operates on verified, structured intermediate results (lemmas in the library) rather than on unstructured, unverified reasoning traces. The summarizer agent distills proven claims from exploratory reasoning, and the theorem verifier provides a quality filter before those claims enter the persistent memory. This structured approach avoids the garbage-in-garbage-out problem that plagues naive self-correction, where a model revising its own flawed reasoning may amplify rather than correct errors.

The paper also reconciles the gap between neural generation and symbolic knowledge accumulation that has historically separated the deep learning and formal methods communities. Intern-S1-MO is entirely neural (all components are LLMs) but achieves some of the benefits of symbolic systems (persistent, reusable knowledge with explicit dependency structure) through learned behaviors—lemma extraction, verification, and dependency tracking—rather than through hand-crafted formal rules. This suggests that the neural-symbolic boundary may be more permeable than assumed, and that learned models can develop proto-symbolic behaviors when trained with appropriate architectures and reinforcement signals.

Research directions that become more attractive:

Learned memory management for reasoning agents. The lemma library concept generalizes to any domain with decomposable structure: code generation (store verified functions), scientific reasoning (store established causal relationships), legal analysis (store precedents), and multi-step planning (store subgoals). The paper's demonstration that this can be trained end-to-end via RL makes this direction newly tractable.
Process verifier development as a first-class research investment. The paper's dual-use OPV—serving both inference-time refinement and RL training signal—demonstrates that verifier quality is a rate-limiting factor for self-improving reasoning systems. This mirrors the finding from the prior paper analysis that verifier over-optimization is the primary bottleneck for test-time compute scaling. The implication is clear: improving verifier F1 from 85% to, say, 95% would likely yield compound benefits through both better lemma filtering and stronger RL training signal.
Cross-trajectory credit assignment. The lemma dependency graph's ability to pool evidence across 16 independent trajectories and backpropagate value through structural (rather than temporal) relationships is a novel credit assignment mechanism that could be applied to any RL problem with decomposable state spaces, from program synthesis to scientific discovery.

Research directions that become less attractive (or at least require stronger justification):

Raw context-length scaling as the primary path to harder reasoning. Figure 1(a) shows exponential growth in required tokens with problem difficulty. If architectural innovations can provide 8× effective depth at fixed context length, the urgency of pushing context windows from 128K to 512K to 1M tokens is reduced—better architecture may provide equivalent gains at lower hardware cost.
Prompt-based self-correction without structural memory. The paper's evidence suggests that iterative refinement works when it operates on structured, verified knowledge, not when it's applied to unstructured reasoning traces. Prompt engineering alone is unlikely to bridge this gap; architectural support for memory management appears necessary.
Pure outcome-reward RL for complex reasoning. The OREAL-H results (Table 2) show substantial gains from process-aware training over the process-verifier-only baseline, and the theoretical motivation for lemma-graph credit assignment suggests that outcome-only RL would be substantially weaker. While the paper doesn't provide the head-to-head comparison (a notable gap), the conceptual argument raises the bar for outcome-only approaches on tasks requiring extended multi-step reasoning.

Follow-Up Research This Work Enables

1. Compute-controlled comparison between multi-round architecture and long-context single-pass generation. The paper's central claim is that structured decomposition achieves what raw context scaling cannot, but the evidence is confounded by unequal compute: Intern-S1-MO uses ~512K tokens across rounds while baseline models use unknown (likely much smaller) budgets. A direct experiment would take a single base model (Intern-S1 or another open model) and compare: (a) the multi-round architecture at 8 rounds × 64K tokens (512K total), versus (b) the same base model with a single 512K-token context window, solving the same problems. Token counts are normalized; the only difference is whether the 512K tokens are organized as one long generation or 8 structured rounds with lemma extraction and verification. This would isolate whether the gains come from structure (lemma memory, summarization, verification) or simply from total thinking budget. The experiment requires access to a model that supports 512K contexts or a technique for simulating long contexts (e.g., ring attention). A negative result—the single 512K-pass matching multi-round—would challenge the paper's architectural thesis; a positive result—multi-round substantially outperforming—would validate it.

2. Cross-model transfer of the Intern-S1-MO architecture. All results are on Intern-S1 variants, and the paper provides no evidence that the architecture transfers to other base models. A strong follow-up would replicate the multi-round reasoning loop (without OREAL-H training, initially) on 2–3 other open-weights models with strong mathematical reasoning—DeepSeek-R1, Qwen3-235B, or Llama-4—on a subset of CNMO2025 or IMO2025 problems. The key measurement is: does the multi-round gain over single-round (the "+ Multi-round Reasoning" delta in Table 2, which is +14.6 on HMMT2025 and +23.7 on CNMO2025 for Intern-S1) replicate at similar magnitude across model families? If yes, the architecture is general; if gains are Intern-S1-specific, then the paper's contributions are tied to that particular model's reasoning style, and the claimed architectural innovation is narrower than presented. This experiment also stress-tests the verifier models (OPV, CompassVerifier) on out-of-distribution reasoning traces, revealing whether the 85% F1 transfers or degrades.

3. Difficulty-stratified analysis following the prior paper's quintile methodology. Intern-S1-MO claims its gains are concentrated on the hardest problems (Section 5.2), but provides no difficulty-stratified breakdown. A direct follow-up would bin CNMO2025 and IMO2025 problems by Intern-S1's base-model pass@1 (following the prior paper's oracle difficulty estimation: 2048 samples per problem, bin into quintiles based on the fraction correct), then evaluate Intern-S1-MO's gain over single-pass Intern-S1 within each bin. The hypothesis: gains are largest in bins 3–4 (medium-hard problems where single-pass struggles but multi-round decomposition can make progress), moderate in bins 1–2 (easy problems where single-pass already succeeds), and near-zero in bin 5 (impossibly hard problems that even 8 rounds cannot crack). This would precisely characterize which Olympiad problems benefit from the architecture and would connect Intern-S1-MO's findings to the broader test-time scaling literature. The CMO2025 results (full marks on 4/6, partial on 2/6) hint at this pattern—the two partial-credit problems may correspond to bin 5 in the difficulty taxonomy.

4. Ablation of OREAL-H components: lemma dependency graph versus temporal credit assignment versus outcome-only RL. The paper bundles lemma dependency graph credit assignment, conjugate reward modeling, cold-start cloning, and the OREAL loss into a single "+ OREAL-H" ablation step. A critical follow-up would train three variants on the same problem distribution and base model: (a) full OREAL-H (lemma graph + conjugate reward), (b) OREAL-H with temporal credit assignment (standard discounted returns per round, no lemma graph construction), and (c) outcome-only RLVR (binary reward on final answer correctness, no process feedback). All three would use the same cold-start checkpoint and identical compute budgets for RL training. The comparison would measure: what fraction of the +17.2 CNMO2025 gain comes from having any RL training (c vs. no-RL baseline), what fraction comes from process-level feedback (b vs. c), and what fraction comes specifically from the lemma dependency graph's structural credit assignment (a vs. b). This experiment directly tests whether the paper's most theoretically distinctive contribution—the lemma graph—provides empirical benefits beyond simpler alternatives.

5. Verifier quality sensitivity analysis and threshold characterization. The paper's architecture depends critically on learned verifiers with unknown lemma-level error rates, yet provides no sensitivity analysis. A systematic follow-up would vary verifier quality and measure downstream system performance: (a) degrade OPV by reducing ensemble size (from 8 to 4 to 2 to 1 verification passes), (b) introduce controlled noise into the Theorem Verifier (flip a known fraction of verification decisions), and (c) measure how final solution accuracy varies with verifier F1. The goal is to characterize the verifier quality threshold below which the multi-round architecture breaks down—at what false-positive rate does error propagation overwhelm the benefits of lemma accumulation? The paper's 85% F1 ceiling is treated as a given; this experiment would determine whether improving verifiers to 90% or 95% is critical for further progress, or whether 85% is already in a plateau region where additional verifier gains yield diminishing returns. The conjugate reward formulation (Section 4.3.2) provides a theoretical framework for understanding verifier noise, but the empirical relationship between verifier quality and system performance is unexplored.

6. Dynamic budget allocation based on intermediate progress signals. Intern-S1-MO uses a fixed maximum of 8 reasoning rounds regardless of whether progress is being made. A natural extension—analogous to the prior paper's compute-optimal test-time scaling—would develop a dynamic round budget that terminates early when progress stalls. The mechanism would monitor the Lemma Library's growth rate: if no new verified lemmas are added in 2 consecutive rounds, or if the confidence scores of newly proposed lemmas are declining, the system terminates lemma search and proceeds to final solution generation. This requires training a lightweight "progress classifier" on features like: number of new lemmas per round, average lemma confidence score, and trend in lemma value estimates from the dependency graph. The experiment would compare fixed-8-round versus adaptive-round performance at matched average compute budgets, measuring whether dynamic allocation recovers the same accuracy with fewer rounds on easy problems while preserving accuracy on hard problems that genuinely need all 8 rounds. The prior paper demonstrated 4× efficiency gains from difficulty-adaptive allocation for single-pass reasoning; this experiment would test whether similar principles apply to multi-round architectures.

Practical Applications and Downstream Use Cases

1. Olympiad training and automated problem-solving for mathematics education. Intern-S1-MO achieves gold medal performance on CMO2025 (102/126, exceeding the 78-point threshold) and silver medal on IMO2025 (26/35). For mathematics competition training programs—national olympiad teams, specialized high schools, university preparation courses—the system could serve as an automated tutor that not only produces correct solutions but generates interpretable intermediate lemmas (the "lemma library") that students can study to understand proof structure. Unlike single-pass models that output monolithic solutions, Intern-S1-MO's multi-round trace shows how a solution was built incrementally—which lemmas were proved first, which cases were analyzed, and how partial results combined into the final proof. The system's natural-language lemmas (with LaTeX formatting) are directly human-readable, avoiding the accessibility barrier of formal proof assistants. The CMO2025 result under human-judged conditions (Section 5.4) validates that the outputs meet human expert standards for rigor and clarity.

2. Verification and refinement of human-generated proofs. The Process Verifier (OPV) achieves >85% F1 on ProcessBench and provides step-level error identification with natural-language feedback (Appendix A.4). This capability transfers directly to a proof-checking assistant for mathematicians: a researcher drafts a proof, submits it to OPV, and receives a detailed verification log identifying the first incorrect step (if any) along with explanations of logical gaps. The iterative revision loop (Section 3, "Verifying Process for Final Proof Completion") demonstrates that the system can not only detect errors but also suggest corrections—the revision prompt (Appendix A.5) instructs the model to "fix all errors reasonably pointed out by comments, fill all gaps mentioned by comments." For mathematical journals or conference program committees handling large volumes of submissions, an OPV-based pre-screening tool could flag proofs with likely errors for closer human review, prioritizing reviewer attention. The 8-way ensemble verification used in the paper's evaluation protocol would provide confidence scores that indicate which flagged errors are most likely to be genuine.

3. Self-improving data generation pipelines for mathematical reasoning models. The OREAL-H framework demonstrates that the same verifier used for inference-time refinement can also provide training signal for policy improvement. This enables a self-improvement loop for mathematical reasoning: (1) deploy Intern-S1-MO on a large corpus of novel problems (from AoPS, recent competitions, or synthetic problem generators), (2) use OPV with conjugate reward modeling to identify high-quality solutions, (3) add those solutions to the training data, (4) fine-tune the base model, (5) repeat. The cold-start procedure (Section 4.2) already implements a basic version of this for Intern-S1, but the full OREAL-H training with lemma dependency graphs could generate substantially higher-quality trajectories after each iteration. The paper's finding that filtering by outcome scoring (pass rate 0 or 1 problems discarded) improves RL efficiency suggests a natural curriculum: start with easy problems where the model already generates some correct solutions, use those to improve the policy, then tackle progressively harder problems. The Intern-S1-mini-MO results (176.3 on CNMO2025, exceeding Gemini 2.5 Pro's 157.5) demonstrate that distilled models can retain much of the capability at lower cost, making iterative self-improvement economically feasible.

4. Research platform for studying learned memory and knowledge accumulation in neural systems. Intern-S1-MO provides a concrete, reproducible testbed for studying how neural models represent, verify, and reuse structured knowledge over extended reasoning horizons. The lemma library is an explicit, inspectable artifact that researchers can analyze: which lemmas are extracted (and which are missed), how lemma values propagate through the dependency graph, when and why verification fails, and how the model's lemma-extraction behavior evolves during OREAL-H training. This is valuable for cognitive science and AI alignment research because it makes the model's "knowledge state" transparent—unlike the opaque activations of a single-pass model, the lemma library is a human-readable record of what the system believes it has proven at each point. The dependency graph (Appendix E, Figure 3) shows which intermediate results contributed to successful solutions and which were dead ends, enabling fine-grained analysis of reasoning strategies. For researchers studying reward hacking and verifier over-optimization (parallel to the prior paper's analysis of PRM search degradation), Intern-S1-MO provides multiple attack surfaces: the Theorem Verifier can be over-optimized (producing lemmas that look correct but aren't), and the OPV revision loop can be gamed (producing solutions that pass verification but are logically flawed). The system's modular design—separate reasoner, summarizer, and verifier components—allows targeted interventions to study each failure mode independently.

Dependency tree

Papers this one builds on, walking backwards through the same domain and shared topics.

Scaling Long-Horizon LLM Agent via Context-Folding2025· agents← LLM-judged similar
- Demystifying Reinforcement Learning in Agentic Reasoning2025· agents← in-domain predecessor
- A Subgoal-driven Framework for Improving Long-Horizon LLM Agents2026· agents← similar topic
- WildClawBench: A Benchmark for Real-World, Long-Horizon Agent Evaluation2026· agents← similar topic
- ReST meets ReAct: Self-Improvement for Multi-Step Reasoning LLM Agent2023· agents← similar topic
R-Horizon: How Far Can Your Large Reasoning Model Really Go in Breadth and Depth?2025· reasoning← LLM-judged similar
- Meta-Awareness Enhances Reasoning Models: Self-Alignment Reinforcement Learning2025· reasoning← in-domain predecessor
- Beyond Reasoning Gains: Mitigating General Capabilities Forgetting in Large Reasoning Models2025· alignment← topic thread
- Lost in the Noise: How Reasoning Models Fail with Contextual Distractors2026· reasoning← similar topic
- Beyond Length Scaling: Synergizing Breadth and Depth for Generative Reward Models2026· reasoning← similar topic
GR-RL: Going Dexterous and Precise for Long-Horizon Robotic Manipulation2025· rl-training← LLM-judged similar
- Stabilizing Reinforcement Learning with LLMs: Formulation and Practices2025· rl-training← in-domain predecessor
Towards a Science of Scaling Agent Systems2025· agents← in-domain predecessor
- Generative agent-based modeling with actions grounded in physical, social, or digital space using Concordia2023· agents← LLM-judged similar
- SIMA 2: A Generalist Embodied Agent for Virtual Worlds2025· agents← in-domain predecessor

What it influenced

Later papers in the same chain. Direction reversed.

ProAct: Agentic Lookahead in Interactive Environments2026· agents→ LLM-judged similar
- AgentCPM-Report: Interleaving Drafting and Deepening for Open-Ended Deep Research2026· agents→ in-domain predecessor
- Agent World Model: Infinity Synthetic Environments for Agentic Reinforcement Learning2026· agents→ similar topic
Memory in the Age of AI Agents2025· agents→ in-domain predecessor
- SAGE: Training Smart Any-Horizon Agents for Long Video Reasoning with Reinforcement Learning2025· agents→ in-domain predecessor
- A Survey of Self-Evolving Agents: What, When, How, and Where to Evolve on the Path to Artificial Super Intelligence2025· agents→ similar topic
- Memory Transfer Learning: How Memories are Transferred Across Domains in Coding Agents2026· agents→ similar topic
ReST meets ReAct: Self-Improvement for Multi-Step Reasoning LLM Agent2023· agents→ similar topic
- Search-R1: Training LLMs to Reason and Leverage Search Engines with Reinforcement Learning2025· training-methods→ LLM-judged similar
- AutoRT: Embodied Foundation Models for Large Scale Orchestration of Robotic Agents2024· agents→ in-domain predecessor
- Beyond Human Data: Scaling Self-Training for Problem-Solving with Language Models2023· training-methods→ topic thread
- ReAct: Synergizing Reasoning and Acting in Language Models2022· agents→ similar topic
- Scaling Long-Horizon LLM Agent via Context-Folding2025· agents→ similar topic
WildClawBench: A Benchmark for Real-World, Long-Horizon Agent Evaluation2026· agents→ similar topic
- ToolCUA: Towards Optimal GUI-Tool Path Orchestration for Computer Use Agents2026· agents→ in-domain predecessor
- TRIP-Bench: A Benchmark for Long-Horizon Interactive Agents in Real-World Scenarios2026· agents→ similar topic