Intern-S1-MO: Long-horizon Reasoning Agent for Olympiad?Level Mathematical Problem Solving

1 Introduction

• State-of-the-art reasoning models typically support 64k or 128k tokens, which the paper says is insufficient for ultra-challenging problems such as IMO problems.The paper identifies hardware and data limitations as barriers to unlimited context-length scaling.Source: §1 · p. 2
• Earlier multi-round and self-reflective approaches do not cumulatively build on prior trajectories, while formal-language search incurs verification and traversal overhead and requires translating informal problems into formal logic.The paper presents Intern-S1-MO as a response to these limitations and the lack of access to proprietary LRM methodologies and models.Source: §1 · p. 2
• Intern-S1-MO extends reasoning beyond one context window by compressing each round’s reasoning into sub-lemmas stored in memory for later rounds.The framework also uses process verification and revision, and permits additional reasoning rounds for challenging tasks.Source: §1 · pp. 2–3
• OREAL-H trains the LRM with online reinforcement learning, using continuous outcome-process-verifier rewards in a hierarchical MDP for the multi-agent setting.The framework is intended to bootstrap the LRM’s reasoning ability and improve Intern-S1-MO on complex problems.Source: §1 · p. 3
• 26 out of 35 points on IMO2025 non-geometry problems, 232.4 out of 260 on CNMO2025, and 102 out of 126 at CMO2025, with the CMO2025 score exceeding the 78-point gold threshold.The introduction also reports 96.6% and 95% pass@1 on AIME2025 and HMMT2025, respectively, surpassing current advanced LRMs.Source: §1 · p. 3

2 Building Hierarchical Reasoning Agents

• The agent is refined to produce partial deductive progress, such as intermediate sub-lemmas, rather than rushing to an incomplete final answer when its reasoning budget runs out.The paper frames decomposition into manageable sub-lemmas as a way to break long-chain reasoning into incremental steps.Source: §2 · p. 3
• A dedicated reasoning turn distills each exploration into validated intermediate lemmas, reducing redundant trial-and-error content in the structured library used by later rounds.The paper notes that summarization and independent validity checking add computational cost, which it considers necessary to keep the library useful.Source: §2 · pp. 3–4
• The reasoner explores a problem, the summarizer compresses the history into lemmas, and the verifier checks them before they enter memory for later rounds.In the final round, verifier feedback guides solution revision until verification passes or the loop limit is reached.Source: Figure 2 · p. 4
• A theorem verifier uses parallel checks for each lemma, with the proportion correctly identified serving as its confidence score.The paper says this is intended to improve verification reliability and avoid some false positives or false negatives.Source: §2 · p. 4
• The process verifier aggregates checks across runs for test-time robustness and supplies feedback for iterative revision and reinforcement-learning training.The cited verifier is reported to achieve a higher F1-score on ProcessBench than o1-mini.Source: §2 · p. 4

3.1 Preliminaries

• The Hierarchical MDP separates high-level reasoning actions from low-level token generation, with verifier feedback providing intermediate proxy rewards and correctness providing a sparse final reward.The objective is to maximize expected final reward.Source: §3.1 · p. 5

3.2 Cloning Success Trajectory for Cold Start

• Filtered rounds with well-formed lemma summaries initialize the policy by behavioral cloning, and outcome-scored question-answer pairs are added to the training data.The paper reports that simplified trajectories boost agentic solving of the same problems and improve the efficiency of finding positive trajectories during online RL.Source: §3.2 · p. 5

3.3 OREAL with Conjugate Reward under Process Judgement

• OREAL-H adapts OREAL to hierarchical reasoning, addressing delayed credit across high-level actions and continuous, noisy process-verifier feedback.The agent is modeled as a Hierarchical MDP: high-level actions select operations such as extracting lemmas or invoking verification, while low-level generation produces reasoning tokens; intermediate feedback and final correctness provide rewards.Source: §3.3 · p. 5, §3.1 · p. 5

3.3.1 Progress-Conditioned Advantage via Lemma Dependency Graphs

• A lemma dependency graph links supporting lemmas to dependent ones, then propagates positive final-proof reward backward from terminal success nodes to earlier lemmas and reasoning rounds.For each round, the state value is the maximum value among its generated candidate lemmas; rounds producing no new lemmas have their advantage masked.Source: §3.3.1 · p. 6

3.3.2 Conjugate Reward Modeling for Noisy Process Verification

• Process-verifier pass counts are noisy, so the reward estimates the probability that a solution is better than a baseline that fails every verification check.With n = 4 checks, the all-pass reward is approximately 0.996; intermediate cases are smoothly interpolated, and the calibration is intended to suppress weak-pass signals while preserving strong ones.Source: §3.3.2 · pp. 6–7

4.1 Experiment Setup

• The evaluation used Intern-S1 trained on AoPS and in-house data, and compared the system against six named advanced models across five competition benchmarks.The listed benchmarks are AIME2025, HMMT2025, IMO2025, CNMO2025, and CMO2025 non-geometry problems.Source: §4.1 · p. 7

4.2 Overall Results

• Intern-S1-MO significantly outperforms current state-of-the-art baselines, with prominent advantages on CNMO2025 and IMO2025 and narrower gaps on HMMT2025 and AIME2025.Preliminary error analysis says remaining gaps mainly involve highly customized transformations or impromptu key constructions, which are difficult for systematic search strategies.Source: §4.2 · p. 8

4.3 Real-world Evaluation: CMO2025

• 102 out of 126 points exceeded CMO2025’s 78-point gold medal threshold under human-expert judgment.The evaluation comprised six questions completed over two days under the same standards used for human contestants.Source: §4.3 · p. 8, Table 2 · p. 8

4.4 Analysis of the Impact of Lemmas

• Approximately 70% of explored lemmas contributed to final solutions on high-difficulty CNMO2025 and IMO2025 problems.The average length ratio before and after lemma compression was approximately 64:1; the qualitative cases show cross-round lemma reuse and an incorrect pre-RL bound motivating verifier-guided refinement.Source: Table 3 · p. 8, §4.4 · p. 9

4.5 Ablation Study

• Each agent component brought consistent gains across benchmarks; the full system raised CNMO2025 from 178.0 to 232.4 versus the initial baseline.The ablation study evaluates HMMT2025, AIME2025, and CNMO2025 because IMO2025 has only five problems and volatile results.Source: §4.5 · p. 9, Table 4 · p. 9

• Tree search and tool-augmented methods broaden inference search spaces but often lack enough depth to decompose highly complex problems.Source: §5 · p. 10
• Structured frameworks combine planning, exploration, and reflection, yet often rely on carefully designed prompts or human hints and remain within one reasoning episode.Source: §5 · p. 10
• Outcome-reward RL can yield self-correction and adaptive tool use, but cited agents lack cross-episode memory, while existing process-aware methods rely on predefined rules rather than flexible natural-language-proof feedback.Source: §5 · p. 10

6 Conclusion

• 26/35 on IMO2025’s five non-geometry problems was comparable to many silver medalists on that subset, while 102/126 at CMO2025 reached gold-medal level under human judgment.The paper notes that the IMO2025 result does not constitute an official IMO medal result.Source: §6 · p. 10
• Intern-S1-MO conducts reasoning, summary, and verification over multiple rounds, using lemmas as compact memory to extend the LRM’s 64K context constraint by about 8 times.OREAL-H is an RL framework that trains the LRM to bootstrap its reasoning ability and improve the overall agent.Source: §6 · p. 10
• The conclusion identifies extending the lemma-and-proof context mechanism to long-horizon tasks beyond mathematical reasoning, such as scientific reasoning, as future work.The authors note that mathematical reasoning naturally represents intermediate progress as lemmas and proofs.Source: §6 · p. 10

A.5 Self-improve with Verify Feedback

• The prompt asks for an improved solution that fixes or defends flagged issues, fills gaps, and compresses the reasoning, preferably at a high-school level.University-level methods are allowed if the necessary knowledge is introduced for readers without that background.Source: §A.5 · p. 21
• Previous comments are guidance rather than authority, and the solver may fix issues, restructure the response, or discard an unfixable solution.The prompt supplies the main question, the student's solution and verdict, and prior comments; the improved solution should retain the same format, typically a summary and detailed solution.Source: §A.5 · p. 21
• If an attempted improvement contains no useful information, the prompt directs the solver to return “I have not found a complete solution.”Source: §A.5 · p. 21

B.1 Experiment Setup Details

• The approximately 5K training problems come from 95 sources, predate 2025, and are deduplicated by normalized problem statement.These temporal and statement-level filters mitigate, but cannot categorically rule out, potential benchmark contamination.Source: §B.1 · p. 22
• Evaluation covers AIME2025, HMMT2025 Feb, IMO2025, CNMO2025, and CMO2025, with only non-geometric problems used for IMO2025 and CNMO2025.Each sample uses 16 independent rollouts and unbiased pass@1, except IMO2025, which uses pass@4; CMO2025 uses the official contest window and grading protocol but parallel search, so the paper does not claim compute equivalence with human contestants.Source: §B.1 · p. 22
• Comparisons include Gemini2.5-pro, o3-high, Grok4, GPT-OSS-120B, DeepSeek-R1-0528, and Qwen3-235B-A22B.AIME2025 and HMMT2025 baseline scores come from technical reports or MathArena.Source: §B.1 · p. 22
• The default inference budget allows up to 8 reasoner–summarizer rounds, 4 parallel theorem-verifier checks per lemma, and 8 final revision rounds.The reasoner and summarizer each have a 64K-token output limit; across the reported benchmarks, the system averages 4.48 reasoning rounds per problem. CMO2025 uses a larger contest-time budget.Source: §B.1 · p. 22

B.2 Hyperparameters Details

• RL training uses 64-question batches, 16 rollouts per question, and a maximum rollout length of 65536 tokens; questions with pass rates of 0 or 1 are discarded.The policy learning rate is 5e−7, with cosine annealing to one-fifth of its initial value, AdamW optimization, and KL coefficient β = 0.01.Source: §B.2 · p. 23

B.3 Token-Budget-Matched Parallel Sampling

• The comparison uses the same grading protocol on the five non-geometry IMO2025 problems, with seven-way parallel sampling for GPT-OSS-120B.The paper cautions that this is not a strict compute-matched comparison because hardware utilization, wall-clock cost, and implementation details differ.Source: Table 5 · p. 23, §B.3 · p. 23
• 11 to 18: parallel sampling improves GPT-OSS-120B, but it remains below Intern-S1-MO under a comparable generated-token budget.Intern-S1-MO uses 391.7K generated tokens per problem on average, versus 55.9K per GPT-OSS-120B rollout; seven GPT-OSS-120B rollouts were sampled for a nearly matched aggregate token budget.Source: §B.3 · p. 23, Table 5 · p. 23

B.4 Lemma Verifier Reliability

• The manual reliability analysis samples 50 generated lemmas and compares verifier decisions with judgments of mathematical validity in context.Each lemma receives four parallel theorem-verifier checks; a score greater than 0.25 counts as verifier-accepted, and lower scores count as rejected.Source: §B.4 · p. 23, Table 6 · p. 23
• 93.1% precision, 81.8% recall, 87.1% F1, and 84.0% accuracy: the verifier’s results support using its scores as soft reliability annotations.Low-confidence lemmas are retained as uncertain because false negatives may still suggest useful search directions that later reasoning can reprove or correct.Source: §B.4 · p. 23

B.5 OREAL-H Component Ablation

• Both OREAL-H components improve performance across all three benchmarks, and removing the lemma dependency graph causes the larger degradation, particularly on CNMO2025.Replacing the conjugate reward with raw verifier pass ratios also consistently reduces performance; full OREAL-H performs best, indicating complementary contributions.Source: §B.5 · p. 24, Table 7 · p. 24

C Grading Details

• The revised proof-grading scheme couples sub-propositions with their conclusion requirements to address false positives from ambiguous grading rubrics.The evaluation protocol also uses eight independent grading runs and averages their total scores; partial credit is given for valid partial proofs on items worth more than one point.Source: C Grading Details · pp. 24–25

D OREAL-H Algorithm

• OREAL-H’s training procedure samples multi-round trajectories, verifies them, builds a lemma dependency graph, propagates values, computes progress-conditioned advantages, and optimizes with the OREAL loss.Rounds without progress are masked in the advantage calculation.Source: D OREAL-H Algorithm · p. 26

E Lemma Graph

• The lemma graph marks lemmas used in a final conclusion in red, with labels indicating the rollout in which each lemma appeared.For positive-reward trajectories, reward is injected into terminal success lemmas and propagated backward to earlier lemmas and their producing reasoning rounds.Source: Figure 3 · p. 27

F Case Example

• The paper presents a detailed reasoning trace for AMO-Bench Problem 1, illustrating reasoning-process and lemma accumulation.The trace’s problem asks for the smallest number of selected lattice points that guarantees an isosceles triangle.Source: F Case Example · p. 28, Case Study: AMO-Bench P1 · p. 28

Case Study: AMO-Bench P1

• For the AMO-Bench triangle-lattice problem, the largest isosceles-free set has 5 points, and only the five points on one side attain that maximum.Therefore, selecting 6 points guarantees an isosceles triangle.Source: Case Study: AMO-Bench P1 · pp. 28–29

Round 2

• Any two points on different sides have a unique third lattice point equidistant from them, on the third side or in the interior.The text gives the equidistance condition 2i + j = a + b for points on sides AB and AC.Source: Round 2 · p. 29
• For six boundary points, avoiding a side with three or more selected points leaves two points per side, and an equidistant third point completes an isosceles triangle.The (2, 2, 2) case is resolved by the equidistant-point property across sides.Source: Round 2 · pp. 29–30, A Useful Fact: Equidistant Third Point · p. 32
• An interior point has exactly four distinct squared distances to the other fourteen lattice points, so five additional selected points force an equal-distance pair.The two points at equal distance, together with the interior point, form an isosceles triangle.Source: Round 2 · p. 31

A Useful Fact: Equidistant Third Point

• Any two points on one side determine a single lattice point on a different side that is equidistant from them.The property holds symmetrically for the other two sides.Source: A Useful Fact: Equidistant Third Point · p. 31
• The boundary-case analysis concludes that every set of six boundary points contains an isosceles triangle.It checks the possible side-count distributions and uses equidistant third points to rule each one out.Source: A Useful Fact: Equidistant Third Point · pp. 31–32
• Five points on one side avoid an isosceles triangle, but every set of six of the fifteen lattice points contains one.The five points are collinear; the six-point claim combines the interior-point and boundary cases.Source: A Useful Fact: Equidistant Third Point · p. 32

A Failure Case before RL Training

• 8 distinct distances yield only a preliminary upper bound of 10 on the size of an isosceles-free set.The argument then sharpens this bound by showing that size nine is impossible.Source: A Failure Case before RL Training · p. 33
• The five points on AB together with AC points (0, 2), (0, 3), and (0, 4) form an isosceles-free set of size eight.The text verifies that no point in this set is equidistant from two others.Source: A Failure Case before RL Training · p. 33
• Any ninth point added to the admissible eight-point set creates an isosceles triangle.The remaining candidates are the interior points and the excluded boundary point (0, 1).Source: A Failure Case before RL Training · p. 34
• 8 is the largest possible size of an isosceles-free subset of the fifteen lattice points.A nine-point set cannot avoid an isosceles triangle.Source: A Failure Case before RL Training · pp. 33–34