Pith. sign in

REVIEW 4 major objections 5 minor 67 references

Intern-S1-MO claims to break the single-context ceiling by storing verified lemmas across reasoning rounds, reporting 26/35 on IMO 2025 non-geometry problems (silver-medal level) and 102/126 at CMO 2025 (above the 78-point gold threshold).

Reviewed by Pith at T0; open to challenge. T0 means a machine referee read the full paper against a public rubric. the ladder, T0–T4 →

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗

T0 review · deepseek-v4-flash

2026-08-04 06:30 UTC pith:WILE5ODX

load-bearing objection A real system with a genuinely external CMO validation; the IMO/CNMO numbers are self-graded and need independent human scoring before they are quoted as fact. the 4 major comments →

arxiv 2512.10739 v3 pith:WILE5ODX submitted 2025-12-11 cs.CL cs.AI

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

Yuzhe Gu , Songyang Gao , Zijian Wu , Lingkai Kong , Wenwei Zhang , Zhongrui Cai , Fan Zheng , Tianyou Ma
show 13 more authors
Junhao Shen Haiteng Zhao Duanyang Zhang Huilun Zhang Kuikun Liu Chengqi Lyu Yanhui Duan Chiyu Chen Ningsheng Ma Jianfei Gao Han Lyu Dahua Lin Kai Chen
This is my paper
classification cs.CL cs.AI
keywords mathematical reasoninglarge reasoning modelsmulti-agent systemslemma memoryprocess verificationreinforcement learningOlympiad problemslong-horizon reasoning
verification ladder T0 review T1 audit T2 compute T3 formal T4 reserved

The pith

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper tries to establish that the binding limit on Olympiad-level math reasoning is not the model's context window but its inability to keep verified intermediate results alive across attempts. It introduces Intern-S1-MO, in which a reasoner, summarizer, and verifier work in rounds: partial results become lemmas, the verifier certifies them, and the lemma library feeds the next round, effectively letting the model explore with hundreds of thousands of tokens on a single problem. On the five non-geometry problems of IMO 2025 the system scores 26/35, above the human silver-medal mark of 21; it reports 95, 96.6, and 232.4 pass@1 on HMMT2025, AIME2025, and CNMO2025; and in an official CMO2025 sitting graded by human judges it scores 102/126, beyond the 78 gold threshold. The paper also claims that the RL method OREAL-H, which trains on online trajectories with process-verifier rewards, is what lifts the agent from 215.2 to 232.4 on CNMO2025.

Core claim

The central discovery claim is that a large reasoning model can solve problems it cannot solve in one pass by externalizing its working memory as verified lemmas. Across rounds the reasoner proposes partial deductions, the summarizer compresses them, the theorem verifier scores them by parallel sampling, and only high-confidence lemmas are retained; the final solution then goes through a process-verifier-guided revision loop. This architecture reports 26/35 points (pass@4) on the five non-geometry IMO 2025 problems, matching silver-medal level; 102/126 points at CMO 2025 under official human grading, surpassing the gold threshold of 78; and pass@1 scores of 95 on HMMT2025, 96.6 on AIME2025,

What carries the argument

The lemma library is the load-bearing object. Each round's long chain-of-thought trace is distilled by a summarizer agent into concise candidate lemmas; a verifier runs parallel checks and assigns each lemma a confidence score; verified lemmas enter the library and are injected into the next round's prompt. This converts a single 64K-token episode into a multi-episode search whose compact state is a reusable set of facts. The RL side, OREAL-H, models the agent as a hierarchical MDP, backpropagates success values over a graph of lemma dependencies, masks rounds that produce no new lemmas, and maps verification pass counts k/n to a posterior probability that the solution is valid, using a conj

Load-bearing premise

Every headline score rests on the learned process verifier and lemma verifier correctly certifying mathematical validity — the same verifier family builds the lemma library, supplies the RL reward, and judges the final IMO/CNMO solutions in a rubric-based LLM evaluation, so a systematic false-positive bias would inflate all of them; Appendix F also shows retained lemmas with confidence 0.0, leaving the confidence-to-correctness relationship unstated.

What would settle it

Take the solutions behind the IMO2025 and CMO2025 scores, strip the agent's labels, and have a panel of human olympiad graders re-score them under the official contest rubric. If their totals fall clearly below 26/35 and 102/126, or if a sample of lemma-library lemmas is judged false at a high rate by humans despite high verifier confidence, the central claim fails.

Watch this falsifier. Get emailed when new claim-graph text bears on it.

If this is right

  • If these numbers hold, an open-weights LRM-based agent matches human silver-medal performance on IMO 2025 and exceeds the CMO 2025 gold threshold, not just on answer-extraction benchmarks but on human-graded proofs.
  • The ablation shows monotone gains from each module (CNMO2025: 178.0 single-round, 201.7 multi-round, 215.2 with process verifier, 232.4 with OREAL-H), supporting the claim that memory, verification, and RL each add independent value.
  • The roughly 512K-token per-problem budget reported for difficult problems implies context length is not the operative ceiling once memory is external; test-time compute can be spent across rounds rather than inside one window.
  • The agent's errors are concentrated, with full marks on four of six CMO problems and partial marks on two, suggesting the remaining gap is in isolated insight-heavy steps rather than in the overall proof architecture.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • If the verifier family is systematically lenient, the headline numbers could be self-consistent without being true; one cheap check is to compare lemma-verifier confidence against independent human scores on the same lemmas.
  • The rubric-scored IMO2025 and CNMO2025 results rest on an LLM judge over eight runs; a natural extension is to report score distributions and inter-judge agreement, since the paper's point estimates may carry large variance.
  • The lemma-memory design suggests applying the same round-based 'keep only verified sub-results' loop to formal theorem proving, where a proof assistant could replace the learned verifier and make the memory sound by construction.
  • The masking of rounds that generate no new lemmas implies only progress-yielding exploration is reinforced; one could test whether rewarding lemma diversity or novelty further improves the discovery rate of non-obvious intermediate facts.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. Intern-S1-MO is a multi-agent, multi-round hierarchical reasoning framework for olympiad-level mathematics. A reasoner agent explores solutions, a summarizer compresses reasoning into lemmas, and a theorem verifier scores each lemma before it enters a persistent lemma library; a final process-verifier loop refines the proposed solution. The paper additionally introduces OREAL-H, an RL algorithm that trains the reasoner with process-verifier feedback and lemma-dependency-graph advantages. On benchmarks, the system reports pass@1 96.6 on AIME2025, 95 on HMMT2025, 232.4/260 on CNMO2025, 26/35 on non-geometry IMO2025 problems (pass@4), and 102/126 on an official CMO2025 submission graded by human experts.

Significance. If the reported numbers hold, the paper is significant: it demonstrates that a structured agentic system with persistent lemma memory can substantially outperform single-pass LRMs on proof-heavy competition problems, and the official CMO2025 result, obtained under human grading and real contest conditions, is a strong independent existence proof for the system's olympiad-level competence. The AIME/HMMT results are objective and provide a useful lower-stakes confirmation of the framework's value. However, the headline IMO/CNMO scores rest on the authors' own LLM-based grading pipeline, and the CMO result, while credible, is not accompanied by released artifacts or an analysis of failure modes. The paper would be materially stronger if independent human grading or external verification were provided for at least a subset of the proof-based evaluations.

major comments (4)
  1. [§5.1–§5.2, Table 1 and Appendix D] The IMO2025 claim of 26/35 'matching silver medalists' is based on pass@4, whereas human contestants submit a single attempt under contest time limits. A system that is allowed four independent solution attempts is not directly comparable to a single human attempt. Moreover, the IMO and CNMO scores are produced by an LLM-based rubric judge (Appendix D) built on the same verifier family used for lemma verification and RL rewards; no independent human re-scoring, judge-agreement statistics, or released per-problem judge outputs are reported. The CMO2025 human-graded result mitigates this concern, but does not by itself validate the specific IMO/CNMO point scores. I request independent human grading (or a validated external judge) on at least the IMO and a random sample of CNMO problems, and reporting of per-problem scores and judge variance.
  2. [§5.1, Table 1] The AIME2025 and HMMT2025 baseline numbers are taken from external technical reports or MathArena, where protocols (number of samples, pass@1 estimation, answer extraction, judge) may differ from the authors' 16-rollout unbiased pass@1 protocol. This is particularly consequential for AIME2025, which has only 30 problems: 96.6 vs 92.5 is a difference of roughly two problems, and without confidence intervals or same-protocol reruns the 'surpassing SOTA LRMs' claim on these benchmarks is not statistically grounded. Please report bootstrap/confidence intervals and, if feasible, rerun the main baselines under the identical evaluation harness.
  3. [Appendix F] The case study is internally inconsistent with the verification mechanism described in §3. Lemmas 2, 10, 11, 12, and 13 are displayed with '(The confidence score is 0.0.)', meaning zero of n parallel verifications accepted them under the §3 procedure, yet these lemmas are stored in the library and are used in the final solution. Either the case study is not a faithful trace of the deployed system, or the confidence threshold is not enforced as described. Since lemma verification is a central claimed contribution, this discrepancy needs a precise explanation, and the reported confidence scores should be reconciled with the described filtering rule.
  4. [§4.3.2, Eqs. (7)–(8)] The conjugate reward R(k,n) is explicitly defined as a probability P(p1 > p0), which must lie in [0,1]. The text states 'R(4,4)≈5.5', which is impossible for a probability. If 5.5 is intended as a log-odds transform or an unscaled reward, this must be stated and the formula corrected accordingly. This is a load-bearing component of the OREAL-H training objective, and the current notation makes the method unreproducible as written.
minor comments (5)
  1. [Abstract and §5.2] The phrase 'non-geometry problems' is used without explaining why geometry is excluded from IMO2025 and CNMO2025. A brief justification (e.g., diagrammatic input, preprocessing difficulty) would help readers calibrate the claim.
  2. [§2.2, Ref. [14]] Reference [14] is cited as 'Prover-Verifier Games', but it is titled 'Prover-Verifier Games improve legibility of LLM outputs'. The citation is acceptable, but the claim about 'process-aware RL and verifier-guided training' would benefit from a more precise description of that work.
  3. [§4.3.1, Eq. (5)] The recursive definition v(l) = E[v(l')] over successors has no explicit base case for terminal lemmas (lemmas with no successors). The algorithm in Appendix C refers to terminal nodes with R≠0, but a formal base-case definition should be given to make Eq. (5) well-defined.
  4. [Figure 1(a) and §6] Figure 1(a) is presented as illustrating a scaling trend, but no source data or functional fit is given. Please label it as a conceptual illustration. Also, the conclusion says the system extends the 64K context by about 8 times; clarify whether this refers to total token budget across rounds (512K) rather than a single context window, since the architecture explicitly avoids a single long context.
  5. [Table 1] The table footnote should clarify that the IMO score is pass@4 and that the score is over the five non-geometry problems with a maximum of 35 points, not the full IMO2025 maximum of 42. The current notation is ambiguous.

Circularity Check

0 steps flagged

No by-construction circularity found; proof-based scoring overlap is a validity risk, not a definitional reduction.

full rationale

The paper's derivation chain is empirical rather than formal, and the key headline results have independent grounding. AIME2025 and HMMT2025 are scored by exact final-answer matching (Appendix D: 'A response is awarded full score if and only if the extracted final answer matches the ground truth exactly'), and the CMO2025 result is externally graded ('These solutions are scored by human experts using the same standards as those used for human contestants'). The IMO2025 and CNMO2025 scores do use an in-house rubric-based LLM judge (Appendix D), and the same verifier family (OPV/CompassVerifier) is used internally for data filtering and RL reward; if that verifier has systematic bias, those two proof-based numbers could be inflated. However, this is a validity/reproducibility limitation, not circularity: the paper nowhere defines the IMO/CNMO score as the OPV reward, and the grading rubrics are explicit and anchored to official problem requirements rather than fitted to model outputs. The self-citations to OPV/CompassVerifier are supported by external benchmark evidence (ProcessBench F1 > 85%), so they are not unverified self-support. No equation or fitted parameter is shown to reduce to its own input by construction.

Axiom & Free-Parameter Ledger

4 free parameters · 5 axioms · 0 invented entities

The central claims rest on hand-chosen inference and training budgets, on the reliability of the authors' own verifier and judge pipelines, and on self-reported contest participation. There are no new physical entities: the 'agents', 'lemma library', and 'lemma dependency graph' are software constructs, not postulated entities requiring external falsifiable evidence.

free parameters (4)
  • Verification trials n = 4
    Number of parallel lemma/verifier trials is fixed at n=4 (§4.3.2, Appendix B.1); the conjugate reward R(k,n) depends on it and it is a hand-chosen cost-accuracy tradeoff, not derived.
  • Inference round budget = 8 reasoner/summarizer rounds, 8 revision rounds, 64k max output
    Set to control evaluation cost; performance is measured under these budgets and the paper explicitly frames results as scaling with test-time budget, so they are free choices affecting all reported numbers.
  • RL hyperparameters = learning rate 5e-7, KL beta 0.01, batch 64 questions x 16 rollouts, trajectory max 65536 tokens
    Chosen without sensitivity analysis or grid search evidence; no demonstration that the reported results are robust to these choices.
  • CMO search budget = 256-shot parallel search, up to 12 rounds, 8-shot lemma feedback, 24 refinement rounds
    Used for the official CMO2025 run; this enormous best-of search makes the comparison to human contestants inequitable and is an ad hoc resource choice.
axioms (5)
  • domain assumption The OPV process verifier reliably certifies correctness of natural-language proofs (F1>85% on ProcessBench) and its confidence scores are trustworthy.
    Invoked in §3 and §4.3 as the source of lemma verification, process feedback, and RL reward; if the verifier has false positives, the lemma library accumulates errors and proof scores are inflated.
  • domain assumption The LLM-based rubric judge, averaged over 8 runs, approximates human Olympiad grading closely enough to score IMO/CNMO solutions.
    Appendix D describes the ensemble LLM judge with a custom refined grading scheme; no external human-grade validation of this judge is provided, yet IMO2025 and CNMO2025 scores come from it.
  • domain assumption Lemma summaries preserve logical validity, and the lemma library does not propagate errors across rounds.
    The entire multi-round design in §3 depends on this: if flawed lemmas pass verification, later deductions and the final proof inherit the errors.
  • domain assumption Baseline scores from external technical reports and Matharena are comparable under the same evaluation protocol.
    Used in Table 1 for AIME/HMMT comparisons; the paper does not re-run baselines under its own protocol, and IMO2025 is reported as pass@4 rather than pass@1.
  • domain assumption The stated CMO2025 official participation and human-expert scoring occurred as described.
    Section 5.4 reports that the system officially participated and was scored by human experts under contest conditions; this is self-reported and not independently verifiable from the paper.

pith-pipeline@v1.3.0-alltime-deepseek · 24883 in / 10693 out tokens · 95723 ms · 2026-08-04T06:30:02.278405+00:00 · methodology

0 comments
read the original abstract

Large Reasoning Models (LRMs) have expanded the mathematical reasoning frontier through Chain-of-Thought (CoT) techniques and Reinforcement Learning with Verifiable Rewards (RLVR), capable of solving AIME-level problems. However, the performance of LRMs is heavily dependent on the extended reasoning context length. For solving ultra-hard problems like those in the International Mathematical Olympiad (IMO), the required reasoning complexity surpasses the space that an LRM can explore in a single round. Previous works attempt to extend the reasoning context of LRMs but remain prompt-based and built upon proprietary models, lacking systematic structures and training pipelines. Therefore, this paper introduces Intern-S1-MO, a long-horizon math agent that conducts multi-round hierarchical reasoning, composed of an LRM-based multi-agent system including reasoning, summary, and verification. By maintaining a compact memory in the form of lemmas, Intern-S1-MO can more freely explore the lemma-rich reasoning spaces in multiple reasoning stages, thereby breaking through the context constraints for IMO-level math problems. Furthermore, we propose OREAL-H, an RL framework for training the LRM using the online explored trajectories to simultaneously bootstrap the reasoning ability of LRM and elevate the overall performance of Intern-S1-MO. Experiments show that Intern-S1-MO can obtain 26 out of 35 points on the non-geometry problems of IMO2025, matching the performance of silver medalists. It also surpasses the current advanced LRMs on inference benchmarks such as HMMT2025, AIME2025, and CNMO2025. In addition, our agent officially participates in CMO2025 and achieves a score of 102/126 under the judgment of human experts, reaching the gold medal level.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

67 extracted references · 31 linked inside Pith

  1. [1]

    L1: Controllinghowlongareasoningmodelthinkswithreinforcement learning.ArXiv, abs/2503.04697, 2025

    PranjalAggarwalandSeanWelleck. L1: Controllinghowlongareasoningmodelthinkswithreinforcement learning.ArXiv, abs/2503.04697, 2025. URL https://api.semanticscholar.org/CorpusID: 276813519. 1

    Pith/arXiv arXiv 2025

  2. [2]

    Intern-s1: A scientific multimodal foundation model.arXiv preprint arXiv:2508.15763, 2025

    Lei Bai, Zhongrui Cai, Yuhang Cao, Maosong Cao, Weihan Cao, Chiyu Chen, Haojiong Chen, Kai Chen, Pengcheng Chen, Ying Chen, et al. Intern-s1: A scientific multimodal foundation model.arXiv preprint arXiv:2508.15763, 2025. 1, 5.1

    arXiv 2025

  3. [3]

    Mislav Balunovi’c, Jasper Dekoninck, Ivo Petrov, Nikola Jovanovi’c, and Martin T. Vechev. Matharena: Evaluating llms on uncontaminated math competitions.ArXiv, abs/2505.23281, 2025. URLhttps: //api.semanticscholar.org/CorpusID:278996037. 2.1, 5.1, D

    Pith/arXiv arXiv 2025

  4. [4]

    Seed-prover: Deep and broad reasoning for automated theorem proving.arXiv preprint arXiv:2507.23726, 2025

    Luoxin Chen, Jinming Gu, Liankai Huang, Wenhao Huang, Zhicheng Jiang, Allan Jie, Xiaoran Jin, Xing Jin, Chenggang Li, Kaijing Ma, et al. Seed-prover: Deep and broad reasoning for automated theorem proving.arXiv preprint arXiv:2507.23726, 2025. 1

    Pith/arXiv arXiv 2025

  5. [5]

    Evaluating large language models trained on code.arXiv preprint arXiv:2107.03374, 2021

    Mark Chen. Evaluating large language models trained on code.arXiv preprint arXiv:2107.03374, 2021. 5.1

    Pith/arXiv arXiv 2021

  6. [6]

    Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities.ArXiv, abs/2507.06261, 2025

    Google DeepMind. Gemini 2.5: Pushing the frontier with advanced reasoning, multimodality, long context, and next generation agentic capabilities.ArXiv, abs/2507.06261, 2025. URLhttps://api. semanticscholar.org/CorpusID:280151524. 1, 5.1

    Pith/arXiv arXiv 2025

  7. [7]

    Advanced version of gemini with deep think officially achieves gold-medal standard at the international mathematical olympiad, 2025

    Google DeepMind. Advanced version of gemini with deep think officially achieves gold-medal standard at the international mathematical olympiad, 2025. URLhttps://deepmind.google/discover/blog/ advanced-version-of-gemini-with-deep-think-officially-achieves-gold-medal-standard-at-the-international-mathematical-olympiad/ . 1 10 Long-horizon Reasoning Agent fo...

    2025

  8. [8]

    Tora: A tool-integrated reasoning agent for mathematical problem solving.ArXiv, abs/2309.17452,

    Zhibin Gou, Zhihong Shao, Yeyun Gong, Yelong Shen, Yujiu Yang, Minlie Huang, Nan Duan, and Weizhu Chen. Tora: A tool-integrated reasoning agent for mathematical problem solving.ArXiv, abs/2309.17452,

    Pith/arXiv arXiv

  9. [9]

    Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning.arXiv preprint arXiv:2501.12948, 2025

    Daya Guo, Dejian Yang, Haowei Zhang, Junxiao Song, Ruoyu Zhang, Runxin Xu, Qihao Zhu, Shirong Ma, Peiyi Wang, Xiao Bi, et al. Deepseek-r1: Incentivizing reasoning capability in llms via reinforcement learning.arXiv preprint arXiv:2501.12948, 2025. 5.1

    Pith/arXiv arXiv 2025

  10. [10]

    Hmmt february problem archive.https://www.hmmt.org/ www/tournaments/testing

    Harvard–MIT Mathematics Tournament. Hmmt february problem archive.https://www.hmmt.org/ www/tournaments/testing. Accessed 9 May 2025. 5.1

    2025

  11. [11]

    Math-perturb: Benchmarking llms’ math reasoning abilities against hard perturbations.ArXiv, abs/2502.06453, 2025

    Kaixuan Huang, Jiacheng Guo, Zihao Li, Xiang Ji, Jiawei Ge, Wenzhe Li, Yingqing Guo, Tianle Cai, Hui Yuan, Runzhe Wang, Yue Wu, Ming Yin, Shange Tang, Yangsibo Huang, Chi Jin, Xinyun Chen, Chiyuan Zhang, and Mengdi Wang. Math-perturb: Benchmarking llms’ math reasoning abilities against hard perturbations.ArXiv, abs/2502.06453, 2025. URLhttps://api.semanti...

    Pith/arXiv arXiv 2025

  12. [12]

    Gemini 2.5 pro capable of winning gold at imo 2025.arXiv preprint arXiv:2507.15855, 2025

    Yichen Huang and Lin F Yang. Gemini 2.5 pro capable of winning gold at imo 2025.arXiv preprint arXiv:2507.15855, 2025. 1, 2.1

    arXiv 2025

  13. [13]

    A survey of frontiers in llm reasoning: Inference scaling, learning to reason, and agentic systems.Trans

    Zixuan Ke, Fangkai Jiao, Yifei Ming, Xuan-Phi Nguyen, Austin Xu, Do Xuan Long, Minzhi Li, Chengwei Qin, PeiFeng Wang, Silvio Savarese, Caiming Xiong, and Shafiq Joty. A survey of frontiers in llm reasoning: Inference scaling, learning to reason, and agentic systems.Trans. Mach. Learn. Res., 2025, 2025. URL https://api.semanticscholar.org/CorpusID:277781085. 1

    2025

  14. [14]

    Prover- verifier games improve legibility of llm outputs, 2024

    Jan Hendrik Kirchner, Yining Chen, Harri Edwards, Jan Leike, Nat McAleese, and Yuri Burda. Prover- verifier games improve legibility of llm outputs, 2024. URLhttps://arxiv.org/abs/2407.13692. 2.2

    Pith/arXiv arXiv 2024

  15. [15]

    Webthinker: Empowering large reasoning models with deep research capability.ArXiv, abs/2504.21776, 2025

    Xiaoxi Li, Jiajie Jin, Guanting Dong, Hongjin Qian, Yutao Zhu, Yongkang Wu, Ji-Rong Wen, and Zhicheng Dou. Webthinker: Empowering large reasoning models with deep research capability.ArXiv, abs/2504.21776, 2025. URLhttps://api.semanticscholar.org/CorpusID:278207550. 1

    Pith/arXiv arXiv 2025

  16. [16]

    Torl: Scaling tool-integrated rl.arXiv preprint arXiv:2503.23383, 2025

    Xuefeng Li, Haoyang Zou, and Pengfei Liu. Torl: Scaling tool-integrated rl.arXiv preprint arXiv:2503.23383, 2025. 2.2

    Pith/arXiv arXiv 2025

  17. [17]

    Compassverifier: A unified and robust verifier for llms evaluation and outcome reward

    Shudong Liu, Hongwei Liu, Junnan Liu, Linchen Xiao, Songyang Gao, Chengqi Lyu, Yuzhe Gu, Wenwei Zhang, Derek F Wong, Songyang Zhang, et al. Compassverifier: A unified and robust verifier for llms evaluation and outcome reward. InProceedings of the 2025 Conference on Empirical Methods in Natural Language Processing, pp. 33454–33482, 2025. 5.1

    2025

  18. [18]

    Exploring the limit of outcome reward for learning mathematical reasoning.arXiv preprint arXiv:2502.06781, 2025

    Chengqi Lyu, Songyang Gao, Yuzhe Gu, Wenwei Zhang, Jianfei Gao, Kuikun Liu, Ziyi Wang, Shuaibin Li, Qian Zhao, Haian Huang, et al. Exploring the limit of outcome reward for learning mathematical reasoning.arXiv preprint arXiv:2502.06781, 2025. 1, 27

    Pith/arXiv arXiv 2025

  19. [19]

    Agent rl scaling law: Agent rl with spontaneous code execution for mathematical problem solving,

    Xinji Mai, Haotian Xu, Zhong-Zhi Li, Xing W, Weinong Wang, Jian Hu, Yingying Zhang, and Wenqiang Zhang. Agent rl scaling law: Agent rl with spontaneous code execution for mathematical problem solving,

  20. [20]

    American invitational mathematics examination (aime) problems and solutions.https://maa.org/student-programs/amc/

    Mathematical Association of America. American invitational mathematics examination (aime) problems and solutions.https://maa.org/student-programs/amc/. Accessed 9 May 2025. 5.1

    2025

  21. [21]

    Malt: Improving reasoning with multi-agent llm training.ArXiv, abs/2412.01928, 2024

    Sumeet Ramesh Motwani, Chandler Smith, Rocktim Jyoti Das, Markian Rybchuk, Philip Torr, Ivan Laptev, Fabio Pizzati, Ronald Clark, and Christian Schröder de Witt. Malt: Improving reasoning with multi-agent llm training.ArXiv, abs/2412.01928, 2024. URLhttps://api.semanticscholar.org/CorpusID: 274446212. 1

    arXiv 2024

  22. [22]

    s1: Simple test-time scaling.arXiv preprint arXiv:2501.19393, 2025

    Niklas Muennighoff, Zitong Yang, Weijia Shi, Xiang Lisa Li, Li Fei-Fei, Hannaneh Hajishirzi, Luke Zettle- moyer, Percy Liang, Emmanuel Candès, and Tatsunori Hashimoto. s1: Simple test-time scaling.arXiv preprint arXiv:2501.19393, 2025. B.1 11 Long-horizon Reasoning Agent for Olympiad-Level Mathematical Problem Solving

    Pith/arXiv arXiv 2025

  23. [23]

    Introducing openai o3 and o4-mini, 2025

    OpenAI. Introducing openai o3 and o4-mini, 2025. URL https://openai.com/index/ introducing-o3-and-o4-mini/. 5.1

    2025

  24. [24]

    gpt-oss-120b & gpt-oss-20b model card, 2025

    OpenAI. gpt-oss-120b & gpt-oss-20b model card, 2025. URLhttps://arxiv.org/abs/2508.10925. 5.1

    Pith/arXiv arXiv 2025

  25. [25]

    Openai imo 2025 proofs, 2025

    OpenAI. Openai imo 2025 proofs, 2025. URL https://github.com/aw31/ openai-imo-2025-proofs. 1

    2025

  26. [26]

    Aske Plaat, Annie Wong, Suzan Verberne, Joost Broekens, Niki van Stein, and Thomas H.W. Back. Multi- step reasoning with large language models, a survey. 2024. URLhttps://api.semanticscholar. org/CorpusID:271218853. 2.1

    2024

  27. [27]

    Z. Z. Ren, Zhihong Shao, Jun-Mei Song, Huajian Xin, Haocheng Wang, Wanjia Zhao, Liyue Zhang, Zhe Fu, Qihao Zhu, Dejian Yang, Z. F. Wu, Zhibin Gou, Shirong Ma, Hongxuan Tang, Yuxuan Liu, Wenjun Gao, Daya Guo, and Chong Ruan. Deepseek-prover-v2: Advancing formal mathematical reasoning via reinforcement learning for subgoal decomposition.ArXiv, abs/2504.2180...

    Pith/arXiv arXiv 2025

  28. [28]

    rstar2-agent: Agentic reasoning technical report, 2025

    Ning Shang, Yifei Liu, Yi Zhu, Li Lyna Zhang, Weijiang Xu, Xinyu Guan, Buze Zhang, Bingcheng Dong, Xudong Zhou, Bowen Zhang, Ying Xin, Ziming Miao, Scarlett Li, Fan Yang, and Mao Yang. rstar2-agent: Agentic reasoning technical report, 2025. URLhttps://arxiv.org/abs/2508.20722. 2.2

    Pith/arXiv arXiv 2025

  29. [29]

    Zhihong Shao, Peiyi Wang, Qihao Zhu, Runxin Xu, Jun-Mei Song, Mingchuan Zhang, Y. K. Li, Yu Wu, and Daya Guo. Deepseekmath: Pushing the limits of mathematical reasoning in open language models.ArXiv, abs/2402.03300, 2024. URLhttps://api.semanticscholar.org/CorpusID:267412607. 1, 2.1

    Pith/arXiv arXiv 2024

  30. [30]

    Satori-r1: Incentivizing multimodal reasoning with spatial grounding and verifiable rewards.arXiv preprint arXiv:2505.19094, 2025

    Chuming Shen, Wei Wei, Xiaoye Qu, and Yu Cheng. Satori-r1: Incentivizing multimodal reasoning with spatial grounding and verifiable rewards.arXiv preprint arXiv:2505.19094, 2025. 2.2

    arXiv 2025

  31. [31]

    A survey of reasoning with foundation models: Concepts, methodologies, and outlook.ACM Computing Surveys, 57(11):1–43, 2025

    Jiankai Sun, Chuanyang Zheng, Enze Xie, Zhengying Liu, Ruihang Chu, Jianing Qiu, Jiaqi Xu, Mingyu Ding, Hongyang Li, Mengzhe Geng, et al. A survey of reasoning with foundation models: Concepts, methodologies, and outlook.ACM Computing Surveys, 57(11):1–43, 2025. 1, 2.1

    2025

  32. [32]

    Plan-and- solve prompting: Improving zero-shot chain-of-thought reasoning by large language models

    Lei Wang, Wanyu Xu, Yihuai Lan, Zhiqiang Hu, Yunshi Lan, Roy Ka-Wei Lee, and Ee-Peng Lim. Plan-and- solve prompting: Improving zero-shot chain-of-thought reasoning by large language models. InAnnual Meeting of the Association for Computational Linguistics, 2023. URL https://api.semanticscholar. org/CorpusID:258558102. 1

    2023

  33. [33]

    A survey on large language models for mathematical reasoning

    PengyuanWang, Tian-ShuoLiu, ChenyangWang, YidiWang, ShuYan, Cheng-XingJia, Xu-HuiLiu, Xin-Wei Chen, Jia-Cheng Xu, Ziniu Li, and Yang Yu. A survey on large language models for mathematical reasoning. ArXiv, abs/2506.08446, 2025. URLhttps://api.semanticscholar.org/CorpusID:279261286. 1

    Pith/arXiv arXiv 2025

  34. [34]

    OPV: Outcome-based process verifier for efficient long chain-of-thought verification

    Zijian Wu, Lingkai Kong, Wenwei Zhang, Songyang Gao, Yuzhe Gu, Zhongrui Cai, Tianyou Ma, Yuhong Liu, Wang Zhi, Runyuan Ma, Guangyu Wang, Wei Li, Conghui He, Dahua Lin, and Kai Chen. OPV: Outcome-based process verifier for efficient long chain-of-thought verification. 2025. 3, 5.1

    2025

  35. [35]

    Grok 4, 2025

    xAI. Grok 4, 2025. URLhttps://x.ai/news/grok-4. 5.1

    2025

  36. [36]

    Qwen3 technical report.arXiv preprint arXiv:2505.09388, 2025

    An Yang, Anfeng Li, Baosong Yang, Beichen Zhang, Binyuan Hui, Bo Zheng, Bowen Yu, Chang Gao, Chengen Huang, Chenxu Lv, et al. Qwen3 technical report.arXiv preprint arXiv:2505.09388, 2025. 1, 5.1

    Pith/arXiv arXiv 2025

  37. [37]

    Tree of thoughts: Deliberate problem solving with large language models.ArXiv, abs/2305.10601, 2023

    ShunyuYao, DianYu, JeffreyZhao, IzhakShafran, ThomasL.Griffiths, YuanCao, andKarthikNarasimhan. Tree of thoughts: Deliberate problem solving with large language models.ArXiv, abs/2305.10601, 2023. URLhttps://api.semanticscholar.org/CorpusID:258762525. 2.1

    Pith/arXiv arXiv 2023

  38. [38]

    Reinforce llm reasoning through multi-agent reflection.ArXiv, abs/2506.08379, 2025

    Yurun Yuan and Tengyang Xie. Reinforce llm reasoning through multi-agent reflection.ArXiv, abs/2506.08379, 2025. URLhttps://api.semanticscholar.org/CorpusID:279260670. 2.1 12 Long-horizon Reasoning Agent for Olympiad-Level Mathematical Problem Solving

    Pith/arXiv arXiv 2025

  39. [39]

    Does re- inforcement learning really incentivize reasoning capacity in llms beyond the base model?ArXiv, abs/2504.13837, 2025

    Yang Yue, Zhiqi Chen, Rui Lu, Andrew Zhao, Zhaokai Wang, Shiji Song, and Gao Huang. Does re- inforcement learning really incentivize reasoning capacity in llms beyond the base model?ArXiv, abs/2504.13837, 2025. URLhttps://api.semanticscholar.org/CorpusID:277940134. 1

    Pith/arXiv arXiv 2025

  40. [40]

    Simplerl- zoo: Investigating and taming zero reinforcement learning for open base models in the wild.ArXiv, abs/2503.18892, 2025

    Weihao Zeng, Yuzhen Huang, Qian Liu, Wei Liu, Keqing He, Zejun Ma, and Junxian He. Simplerl- zoo: Investigating and taming zero reinforcement learning for open base models in the wild.ArXiv, abs/2503.18892, 2025. URLhttps://api.semanticscholar.org/CorpusID:277940848. 1

    Pith/arXiv arXiv 2025

  41. [41]

    Rest-mcts*: Llmself-trainingviapro- cess reward guided tree search.ArXiv, abs/2406.03816, 2024

    DanZhang, SiningZhoubian, YisongYue, YuxiaoDong, andJieTang. Rest-mcts*: Llmself-trainingviapro- cess reward guided tree search.ArXiv, abs/2406.03816, 2024. URLhttps://api.semanticscholar. org/CorpusID:270285630. 1, 2.1

    Pith/arXiv arXiv 2024

  42. [42]

    Artist: Improving the generation of text-rich images with disentangled diffusion models and large language models, 2024

    Jianyi Zhang, Yufan Zhou, Jiuxiang Gu, Curtis Wigington, Tong Yu, Yiran Chen, Tong Sun, and Ruiyi Zhang. Artist: Improving the generation of text-rich images with disentangled diffusion models and large language models, 2024. URLhttps://arxiv.org/abs/2406.12044. 2.2

    Pith/arXiv arXiv 2024

  43. [43]

    Zhuosheng Zhang, Aston Zhang, Mu Li, and Alexander J. Smola. Automatic chain of thought prompting in large language models.ArXiv, abs/2210.03493, 2022. URLhttps://api.semanticscholar.org/ CorpusID:252762275. 1

    Pith/arXiv arXiv 2022

  44. [44]

    ProcessBench: Identifying Process Errors in Mathematical Reasoning.arXiv e-prints, art

    Chujie Zheng, Zhenru Zhang, Beichen Zhang, Runji Lin, Keming Lu, Bowen Yu, Dayiheng Liu, Jingren Zhou, and Junyang Lin. ProcessBench: Identifying Process Errors in Mathematical Reasoning.arXiv e-prints, art. arXiv:2412.06559, December 2024. doi: 10.48550/arXiv.2412.06559. 3

    Pith/arXiv arXiv doi:10.48550/arxiv.2412.06559 2024

  45. [45]

    Denny Zhou, Nathanael Scharli, Le Hou, Jason Wei, Nathan Scales, Xuezhi Wang, Dale Schuurmans, Olivier Bousquet, Quoc Le, and Ed H. Chi. Least-to-most prompting enables complex reasoning in large language models.ArXiv, abs/2205.10625, 2022. URLhttps://api.semanticscholar.org/ CorpusID:248986239. 1

    Pith/arXiv arXiv 2022

  46. [46]

    Solving formal math problems by decomposition and iterative reflection

    Yichi Zhou, Jianqiu Zhao, Yongxin Zhang, Bohan Wang, Siran Wang, Luoxin Chen, Jiahui Wang, Haowei Chen, Allan Jie, Xinbo Zhang, Haocheng Wang, Luong Ngoc Trung, Rong Ye, Phan Nhat Hoang, Huishuai Zhang, Peng Sun, and Hang Li. Solving formal math problems by decomposition and iterative reflection. ArXiv, abs/2507.15225, 2025. URLhttps://api.semanticscholar...

    Pith/arXiv arXiv 2025

  47. [47]

    Ttrl: Test-time reinforcement learning.arXiv preprint arXiv:2504.16084,

    Yuxin Zuo, Kaiyan Zhang, Li Sheng, Shang Qu, Ganqu Cui, Xuekai Zhu, Haozhan Li, Yuchen Zhang, Xinwei Long, Ermo Hua, et al. Ttrl: Test-time reinforcement learning.arXiv preprint arXiv:2504.16084,

    Pith/arXiv arXiv

  48. [50]

    The scientific ideas, methodology, analyses, and conclusions were entirely developed by the authors, while the LLMs assisted only in improving clarity and readability of the text

    2.2 13 Long-horizon Reasoning Agent for Olympiad-Level Mathematical Problem Solving The Use of Large Language Models (LLMs) We used LLMs solely for language polishing. The scientific ideas, methodology, analyses, and conclusions were entirely developed by the authors, while the LLMs assisted only in improving clarity and readability of the text. A. System...

  49. [51]

    * The final answer is secondary to the correctness of the derivation

    **Rigor is Paramount:** * Every step in your proof must be logically sound and clearly justified. * The final answer is secondary to the correctness of the derivation. A correct ˓→answer resulting from a flawed or incomplete proof will be considered a failure

  50. [52]

    * If you cannot provide a complete solution, you must provide any significant ˓→partial results that you can prove with full rigor

    **Embrace Partial Solutions:** * It is understood that a complete solution may not be found in a single attempt. * 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.** Instead, focus on what ˓→you *can* prove. * Examples ...

  51. [53]

    I have found a complete ˓→solution. The answer is

    **Mathematical Formatting:** * All mathematical variables, expressions, equations, and relations must be ˓→formatted using TeX. For example: ‘Let $G$ be a group and let $H$ be a subgroup of ˓→$G$.‘ **Output Format:** Your response MUST be structured into the following sections, in this exact order. --- **1. Summary** **a. Verdict:** * Begin by stating cle...

  52. [54]

    ‘### Problem ###‘: The mathematical problem requiring resolution

  53. [55]

    ‘### Provided Lemmas ###‘: A set of known, proven lemmas for reference during problem- ˓→solving

  54. [56]

    **Your output must adhere to the following principles and format:** #### **A

    ‘### Model’s Thinking Process ###‘: The reasoning process generated by the large ˓→language model to solve the problem. **Your output must adhere to the following principles and format:** #### **A. Extraction Principles**

  55. [57]

    Do not include lemmas from the ‘Provided Lemmas‘ if the model ˓→utilises them

    **Novelty**: Extract only lemmas first introduced or proven within the ‘Model’s ˓→Thinking Process‘. Do not include lemmas from the ‘Provided Lemmas‘ if the model ˓→utilises them

  56. [58]

    #### **B

    **Classification**: Extract only new lemmas satisfying the following conditions: * **Proven Lemmas**: Propositions explicitly stated or implicitly utilised within ˓→the ‘model’s problem-solving approach‘, accompanied by a complete or core proof. #### **B. Strict Formatting Requirements** Your output must strictly adhere to the following Markdown and LaTeX...

  57. [59]

    The number of ‘<lemma>...</lemma>‘ environments must match the ˓→number of lemmas extracted in this round

    **Format for Proven Lemmas:** * Each **proven lemma** and its proof must be placed within a separate, non-nested ˓→‘<lemma>...</lemma>‘ environment, with the opening and closing tags each occupying a ˓→distinct line. The number of ‘<lemma>...</lemma>‘ environments must match the ˓→number of lemmas extracted in this round. Note that input lemmas may not be...

  58. [60]

    The Main Question: The overarching problem providing context

  59. [61]

    Provided Lemmas: A library of existing statements assumed to be correct

  60. [62]

    - A key part of your evaluation is to verify that any use of a lemma from the Provided ˓→Lemmas library is correctly applied and that its preconditions are satisfied

    The New Lemma and Its Proof: The student’s work to be evaluated, with the proof ˓→skeleton broken down into steps. - A key part of your evaluation is to verify that any use of a lemma from the Provided ˓→Lemmas library is correctly applied and that its preconditions are satisfied. The ˓→logical inferences within the proof must be sound and either self-evi...

  61. [63]

    The Main Question: The overall problem providing context

  62. [64]

    Provided Solution: The student’s work to be evaluated, with a verdict and the ˓→complete solution divided into steps

  63. [65]

    I have not found a complete solution

    Previous Comments: Prior attempts to detect specific types of errors. Treat these as ˓→helpful guidance rather than authoritative. If they flag something, fix or defend. - You must present a improved solution with SAME FORMAT. Typically a solution comes with a ˓→summary section and a detailed solution section. - You are free to decide the idea/approach of...

  64. [66]

    Isosceles-Free Sets Three points form an isosceles triangle if and only if one of them is equidistant from the other two

    between points ofℒ. Isosceles-Free Sets Three points form an isosceles triangle if and only if one of them is equidistant from the other two. Therefore, a set 𝒮⊆ℒ contains **no** isosceles triangle precisely when, for every𝑃∈𝒮 , the distances{|𝑃 𝑄|:𝑄∈𝒮∖{𝑃}} are all different. Since (6) lists only eight possible distances, a point can be the apex of at mos...

  65. [67]

    Hence,(0,1)/∈𝒯

    Thus,(0,1) is equidistant from (0,0)and(1,0), forming an isosceles triangle. Hence,(0,1)/∈𝒯. 29 Long-horizon Reasoning Agent for Olympiad-Level Mathematical Problem Solving • Admissible Set:The only points of𝐴𝐶 that can coexist with all five points of𝐴𝐵 without creating a duplicate distance are(0,2),(0,3), and (0,4). Therefore,𝒯 must be a subset of the ei...

  66. [2023]

    URLhttps://api.semanticscholar.org/CorpusID:263310365. 2.1

  67. [2025]

    URLhttps://arxiv.org/abs/2505.07773. 2.2

    Pith/arXiv arXiv