InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning

ArXiv: 2402.06332

🎯 Pitch

A unified math language model, fine-tuned to solve, verify, and formally prove problems, can boost its own reasoning via iterative self-improvement—improving both the accuracy and reliability of answer generation. Surprisingly, this model matches prior state-of-the-art reranking performance using only 100 samples instead of the typical 256, and on formal math proofs, its base version scores 30.3 on MiniF2F without any fine-tuning.

1. Executive Summary

This paper introduces and open-sources InternLM-Math, a family of math reasoning LLMs continued-pretrained from InternLM2-Base and fine-tuned to unify multiple capabilities—chain-of-thought reasoning, reward modeling, formal reasoning in LEAN, data augmentation, and code interpretation—under a single seq2seq format. The models achieve open-sourced state-of-the-art performance on both informal benchmarks (GSM8K, MATH, Hungary math exam, MathBench-ZH) and formal benchmarks (MiniF2F), with the 7B base model attaining 30.3 on the MiniF2F test set without fine-tuning and the 20B SFT model reaching 50.0 on MATH-500 using process reward model reranking with only 100 samples (matching prior work that required 256 samples with larger models). The paper further proposes reasoning interleaved with coding (RICO), a multi-turn code-interpreter integration that interleaves natural language reasoning with Python execution to achieve 54.3 on MATH—establishing that test-time tool use can substantially outperform chain-of-thought alone, though the gains are concentrated on problems where decomposed calculation and symbolic manipulation are the primary bottlenecks rather than problems requiring novel conceptual insight.

2. Context and Motivation

The Core Problem: Making Math Reasoning LLMs Truly Rigorous

The fundamental problem this paper tackles can be stated simply: how do we build an LLM that not only solves math problems correctly but does so in a way that can be independently verified? This is more than an incremental performance improvement — it represents a shift from models that produce answers (sometimes coincidentally correct, often with flawed reasoning) to models whose entire problem-solving pipeline is auditable.

This matters for several reasons that the paper makes explicit or strongly implies:

Correctness of reasoning is not guaranteed by correct answers. Section 7.4 documents a sobering finding: when the authors manually inspected 25 MATH test problems where InternLM2-Math-20B produced the correct answer, 5 of them (20%) contained incorrect reasoning. The model had gotten lucky — guessing an integer in a counting problem, making a logical error that happened to produce the right number, or listing numbers incorrectly while still arriving at the request count. As difficulty increases, this phenomenon worsens: at Level 5, only 3 of 5 "correct" answers actually had correct processes. This is particularly insidious because standard benchmarks reward these false positives, inflating our perception of model capabilities.

"Simply judging model abilities only by outcome accuracy may be unilateral. Therefore, one of our future works is to use reward models or LEAN to provide a better process checking."

This false-positive problem is not unique to InternLM-Math — it affects all LLMs evaluated on MATH — but the paper explicitly quantifies it and argues that the solution requires verifiable reasoning, not just better answer generation.

Self-improvement pipelines need reliable signals. A recurring theme is that the model should serve as a starting point for iterative self-improvement: use the model to generate new problems (augmentation), solve them (chain-of-thought), and verify the solutions (reward modeling or formal proof). If the verification step is unreliable — if the model cannot distinguish correct from incorrect reasoning — then self-improvement loops amplify errors rather than correcting them. By training the same model to both solve and verify, the paper creates a unified system that can generate, solve, and check its own work.

Formal reasoning remains disconnected from informal problem-solving. There is a fundamental disconnect in the current LLM math landscape. On one side, models like Minerva and Llemma achieve strong performance on informal benchmarks (GSM8K, MATH) using chain-of-thought, but their reasoning is opaque and unverified. On the other side, formal theorem provers like LEAN provide ironclad verification—a proof that compiles in LEAN is guaranteed correct—but formal proving datasets are sparse and the translation from natural language problems to formal statements is itself difficult. The paper asks: can we bridge these two worlds, using the same model for both informal problem-solving and formal verification?

Where Prior Approaches Fall Short

The paper identifies specific limitations in prior work across multiple axes:

Specialized models do one thing well. Prior math LLMs — MetaMath, MammoTH, ToRA, DeepSeek-Math — are trained primarily as solvers. They produce answers via chain-of-thought or code, but they do not verify, augment, or formalize. If you want a verifier, you typically train a separate reward model (as in Lightman et al., 2023). If you want formal reasoning, you train a separate prover (as in Llemma's formal-to-formal setting, or ReProver). Each capability lives in its own model, making composite pipelines — generate with one model, verify with another, augment with a third — complex, expensive, and vulnerable to distribution shift between the components.

Reward modeling requires expensive labeling or separate training. Lightman et al. (2023) demonstrated that process reward models (PRMs) significantly outperform outcome reward models (ORMs) for selecting the best among multiple candidate solutions. However, their PRM required human experts to label each intermediate step. Wang et al. (2023b, Math-Shepherd) addressed the labeling cost through automatic Monte Carlo rollouts, but their approach still treats the verifier and the solver as separate models — requiring double the parameter count for deployment. This paper asks: can we collapse solver and verifier into a single model, using the same architecture and weights for both?

Code interpreters are treated as black boxes. Prior work on code-augmented math reasoning falls into two categories. Program-of-thought approaches (Chen et al., 2023b; Gao et al., 2023) generate a single program that computes the answer, but the LLM never sees the execution output — it cannot revise its reasoning based on intermediate results. ToRA (Gou et al., 2023) allows the model to see execution results, but embeds code in markdown blocks within the text response, creating format ambiguities when deploying in chat systems. Crucially, neither approach is multi-turn in the way a human mathematician uses computation: solve part of the problem symbolically, realize you need more information, compute something numerically, reflect on the result, adjust your approach, and continue. The paper argues that "reasoning interleaved with coding" — where natural language reasoning and code execution alternate in multiple rounds — is both more natural and more powerful.

Formal reasoning is bottlenecked by data sparsity. Automated theorem proving with LLMs has shown promise (Han et al., 2021; Polu et al., 2022; Azerbayev et al., 2023a), but performance is limited by the scarcity of formal proof data. MiniF2F, the standard benchmark for formal math reasoning, has only 244 test problems — and prior SOTA models solve fewer than 30% of them. The paper identifies that one reason for this data sparsity is the difficulty of translating between natural language problems and formal LEAN statements. By training the model to do this translation as part of its SFT data, the paper aims to create a bridge that both improves formal proving and enables using LEAN as a verifier for informal reasoning.

Self-correction and verification are missing from existing math models. The paper explicitly notes in its limitations (Section 8) that it does "not contain any SFT data to let the model apply self-critique since such data can be hard to generate and verify by any means." This acknowledgment reveals a gap that the paper partially addresses (through reward modeling) but does not fully close — the model can verify others' solutions but cannot yet reliably critique its own.

How This Paper Positions Itself

The paper positions InternLM-Math not as a point-solution for achieving high benchmark scores, but as a platform for verifiable mathematical reasoning that integrates multiple capabilities into a single model. The key architectural decision is the unified seq2seq format (Section 4, Figure 2): every capability — chain-of-thought reasoning, reward modeling (ORM and PRM), formal reasoning (LEAN solving and proving), data augmentation, and code interpretation — is expressed as a query-response pair in the same textual format. This means a single model checkpoint can be prompted (or fine-tuned with different subsets of the SFT data) to serve any of these roles.

The positioning is encapsulated in the abstract:

"We unify chain-of-thought reasoning, reward modeling, formal reasoning, data augmentation, and code interpreter in a unified seq2seq format and supervise our model to be a versatile math reasoner, verifier, prover, and augmenter. These abilities can be used to develop the next math LLMs or self-iteration."

This is a departure from the prevailing paradigm of training separate specialist models. The paper argues that this unification is not merely convenient but potentially synergistic: the data ablation in Section 7.3 shows that adding formal reasoning, code interpreter, and reward modeling data to the SFT mix (beyond just MetaMath + COT data) leads to worse performance on individual benchmarks, but the full mixture recovers and improves upon the baseline — suggesting that the model learns shared representations that transfer across these superficially different tasks.

The paper also positions itself relative to the concurrent DeepSeek-Math (Shao et al., 2024) by noting in a footnote that the work is "concurrent with Deepseek-Math," establishing that these are parallel efforts pursuing similar goals (open-source math LLMs) but with different emphases: InternLM-Math emphasizes verifiability and multi-capability unification, while DeepSeek-Math emphasizes reinforcement learning from verifier feedback.

The Specific Gaps the Paper Claims to Fill

Reading across the abstract and introduction, the paper identifies these concrete contributions that address prior gaps:

1. Single-model solver + verifier: Prior work (Lightman et al., 2023; Wang et al., 2023b) required separate policy and reward models. InternLM-Math unifies them into one model that can be used for both generation and verification, reducing deployment complexity.

2. Formal reasoning accessible from a math LLM, not a code LLM: Prior SOTA on MiniF2F came from Llemma (a math-pretrained model) and DeepSeek-Coder (a code-pretrained model). InternLM-Math-Base-7B achieves 30.3 on MiniF2F-test — a new SOTA for 7B-scale models — demonstrating that math-focused pretraining can be as effective for formal reasoning as code-focused pretraining, and opening the door to using LEAN as a verifier for informal reasoning.

3. Multi-turn code integration: RICO is presented as a natural alternative to one-shot code generation (ToRA, PAL) that better mirrors how humans use computation in mathematical problem-solving.

4. LEAN as both solver and verifier for informal problems: The paper explores using LEAN not just for theorem proving but for solving grade-school math problems (GSM8K), demonstrating "the possibility of using LEAN as a unified interface for solving and proving math problems" (Section 6.2.3). This is an unusual direction — prior work typically keeps informal solving and formal proving separate — and the paper acknowledges it underperforms COT due to natural-number type limitations in LEAN 3, but frames it as a proof-of-concept for a unified formal interface.

The paper is thus positioned at the intersection of three research threads — math LLMs, automated theorem proving, and tool-augmented reasoning — with the ambition of unifying them into a single model capable of the full cycle: augment problems, solve them, and verify solutions, all within a framework that can support iterative self-improvement.

3. Technical Approach

3.1 Reader Orientation

The paper presents InternLM-Math not as a single-purpose math solver but as a multi-capability math reasoning platform built by continuing pre-training on InternLM2-Base models and then fine-tuning with a diverse SFT mixture that teaches the model to solve problems, verify solutions, translate between natural language and formal LEAN statements, augment problems, and use a code interpreter — all through a unified text-to-text format. The system solves the problem of building a math LLM whose reasoning can be verified (by itself or by external tools like LEAN), where "verified" means both informal verification (the model checks step-by-step correctness as a reward model) and formal verification (the model translates reasoning into LEAN code that a proof assistant can check). The solution's shape is a single model checkpoint that, depending on how it is prompted, can act as a solver, a verifier, an augmenter, or a formal reasoner — eliminating the need for separate specialist models and enabling self-improvement pipelines where the same model generates, checks, and augments its own training data.

3.2 Big-Picture Architecture (Diagram in Words)

The InternLM-Math system has four major stages, with the first two producing the base model and the last two producing the fine-tuned model:

Stage 1 — Data Collection for Continued Pre-training (Section 3.1): Three categories of math data are collected: (a) CC Retrieved Data from the Common Crawl using Query of CC to retrace InternLM2-Base's training corpus and select math-relevant pages (20B unique tokens), (b) Domain-Specific Data including web pages, arXiv papers, code repositories, forums, and books — partially sourced from the open-source AlgebraicStack dataset — totalling 11B unique tokens, and (c) Synthetic Data for numerical operations (0.2B unique tokens) covering arithmetic, exponentiation, logarithmic, trigonometric, and polynomial calculations. The collected data undergoes quality filtering via a trained scoring model, Minhash-LSH deduplication at similarity threshold 0.7, and exact formula decontamination against the MATH test set.

Stage 2 — Continued Pre-training (Section 3.3): Starting from InternLM2-Base checkpoints, the collected data is fed into continued pre-training using InternEvo, the same training framework and hyperparameters as the original InternLM2 training. For the 7B model, 125B tokens are consumed (most datasets at 4 epochs following Muennighoff et al., 2023); for the 20B model, training is early-stopped at 80B tokens based on ICL performance. The output is InternLM2-Math-Base.

Stage 3 — SFT Data Construction (Section 4, Appendix A): A 2.26M-sample supervised fine-tuning dataset is assembled covering seven capability categories: chain-of-thought reasoning (MetaMath, Goat, rule-generated arithmetic/prime/game-of-24/factoring/triangle data, MammoTH, Khan, in-house Chinese data, augmented MATH and Math23K), reward modeling (Math-Shepherd converted to ORM/PRM format, self-sampled Chinese ORM data), formal reasoning (GPT-4-distilled LEAN 3 solutions for GSM8K, COT-LEAN translation pairs, NL-LEAN translation from MathLib, LEAN state-tactic pairs), code interpreter (multi-turn reasoning-with-code solutions for GSM8K and MATH generated by GPT-4-Turbo or InternLM-70B), augmentation helper (question rephrasing and problem-to-theorem conversion data), and few-shot format templates. The data is deduplicated and decontaminated against test sets.

Stage 4 — Supervised Fine-tuning (Appendix B): InternLM2-Math-Base is fine-tuned on the mixed SFT data for 3 epochs using packed sequences with max length 32,768, peak learning rate 4e-5, and Adam optimizer. The output is InternLM2-Math (the SFT model), which can be prompted in multiple modes (solver, verifier, formal reasoner, augmenter, code interpreter user) by selecting the appropriate query format from the unified schema shown in Figure 2.

At inference time, the model can be deployed in several configurations:

• Solver mode: Generate chain-of-thought or RICO solutions, optionally with majority voting or verifier reranking.
• Verifier mode: Score candidate solutions as ORM or PRM, compare pairs of answers, or translate COT to LEAN and check equivalence.
• Formal mode: Translate problems to LEAN, prove statements, or solve problems directly in LEAN.
• Augmenter mode: Rephrase problems, generate harder variants, or convert Q&A pairs to proof statements.

3.3 Roadmap for the Deep Dive

• First, the continued pre-training pipeline — data composition, post-processing, and training strategy — because this establishes the base model's mathematical knowledge.
• Second, the unified SFT format and data construction, since this is the paper's central architectural innovation: how seven different capabilities are expressed in a single seq2seq schema.
• Third, the chain-of-thought data and the calculation hallucination problem, which motivates specific data construction choices.
• Fourth, the reward modeling integration (ORM and PRM in a single model), including how Math-Shepherd data is reformatted.
• Fifth, the formal reasoning data pipeline — using LEAN as solver, verifier, and prover — and how translation data bridges informal and formal reasoning.
• Sixth, the augmentation helper data and its role in self-improvement loops.
• Seventh, the RICO code interpreter design — the multi-turn interleaving protocol, data construction through iterative hard example mining, and how it differs from prior tool-augmented approaches.

3.4 Detailed, Sentence-Based Technical Breakdown

This is primarily a systems and data engineering paper whose core technical idea is that unification of multiple math-related capabilities into a single model's SFT data mixture — using a consistent seq2seq query-response format — enables a single checkpoint to serve as solver, verifier, augmenter, and formal reasoner, creating a platform for self-improvement that does not require separate specialist models.

Continued Pre-training: Data Composition and Processing

The continued pre-training of InternLM2-Base into InternLM2-Math-Base rests on the composition of three data categories, with post-processing to ensure quality and avoid test set contamination.

CC Retrieved Data (20B unique tokens). The authors used Query of CC (Fei et al., 2024) to retrace the original training corpus of InternLM2-Base — effectively asking "which web pages in Common Crawl did the base model already see?" — and then selected only the math-related subset. This is a continuation of the existing training distribution rather than an injection of entirely new data, which reduces the risk of catastrophic forgetting of non-math capabilities. The dataset "knowledge pile" (20B unique tokens × 4 epochs = 80B consumed tokens) and "open-web-math" (6B × 4 = 24B consumed tokens) together account for 104B of the 125B total training tokens — roughly 83% of the continued pre-training budget. The heavy emphasis on web-retrieved math data suggests the authors believe broad math exposure (not just formal mathematics) is important for downstream reasoning.

Domain-Specific Data (11B unique tokens). This category includes "algebraic-stack" (4B unique tokens × 4 epochs = 16B consumed), which the paper describes as sourced from the open-source dataset of Azerbayev et al. (2023b) — this is the same data used to train Llemma, making the comparison between InternLM-Math-Base and Llemma relatively fair at the pre-training data level. The "others" category (1B unique tokens × 4 epochs = 4B consumed) includes "web pages, codes, arXiv, forums, and books" — a curated in-house collection spanning multiple math subdomains. The inclusion of arXiv is standard for math LLMs (Minerva, Llemma both use it), while code repositories and forums provide exposure to applied mathematics and mathematical programming.

Synthetic Data (0.2B unique tokens). This small but targeted category addresses a specific weakness: numerical calculation. The paper states:

"We included five common operations including arithmetic, exponentiation, logarithmic, trigonometric, and polynomial calculations. For numerical operations, we traversed a set of commonly used values and randomly sampled a wider range of values within 10-digit numbers."

The synthetic data is consumed at 5 epochs (0.2B × 5 = 1B tokens), the highest repetition factor in the pre-training mix. This higher epoch count suggests the authors view numerical calculation as a skill that benefits from repeated exposure to varied instantiations of the same underlying patterns, rather than from seeing more unique text. To prevent overfitting to specific templates, the authors "diversely constructed templates to ensure the model's numerical computing capabilities generalize to some extent."

Data post-processing pipeline. Three sequential steps are applied:

1. Quality scoring: A trained scoring model (not further described in the paper) identifies and retains high-quality data. The nature of this scoring model — what it was trained on, what features it uses — is not specified, which is a detail gap.

2. MinHash-LSH deduplication: Near-duplicate documents are identified using MinHash with Locality-Sensitive Hashing, with "duplicate data with a similarity exceeding 0.7" being filtered out. The 0.7 threshold means that documents sharing more than 70% of their n-gram MinHash signatures are treated as duplicates.

3. Formula-level decontamination: For the MATH test set specifically, the authors "extract all formulations within a given paragraph" from the training data. If the concatenation of these extracted formulas matches any formula sequence in the MATH test set, that paragraph is removed. This is a more aggressive decontamination than typical n-gram overlap approaches (which might miss formula-only overlaps) but also more conservative than embedding-based approaches (which might flag conceptually similar but symbolically different problems). The paper does not apply this decontamination to GSM8K or the Hungary exam, and explicitly notes in the limitations that formal reasoning data from AlgebraicStack was not decontaminated against MiniF2F.

Training configuration. The continued pre-training uses:

• Context length: 4096 tokens (documents longer than this are truncated; shorter documents are concatenated to fill the context window)
• Mixed precision: bfloat16 with FlashAttention2 (Dao, 2023) for memory efficiency
• Optimizer: AdamW with $\beta_1 = 0.9$, $\beta_2 = 0.95$, $weight\_decay = 0.1$
• Learning rate: cosine schedule, warming up to $lr_{max} = 3 \times 10^{-5}$ over 2000 steps, then decaying to $lr_{min} = 3 \times 10^{-6}$
• Training framework: InternEvo

The 7B model trains on the full 125B tokens (approximately 4 epochs over the 31.2B unique tokens). For the 20B model, the authors "early stop at 80 billion tokens based on in-context learning performance" — a practical decision that the paper's pre-training ablation (Section 7.1, Table 12) supports: for the 7B model, ICL and SFT performance peaks around 80-120B tokens and begins to decline at 160-200B tokens, suggesting a sweet spot around 3-4 epochs of data recycling before overfitting or degradation sets in.

The Unified SFT Format: One Schema for Seven Capabilities

The central architectural innovation of InternLM-Math's fine-tuning stage is the unified seq2seq format illustrated in Figure 2. Rather than training separate heads, separate models, or separate fine-tuning runs for different capabilities, all SFT data is expressed as query-response pairs with consistent formatting tokens that indicate which capability is being exercised.

Query format structure. A query (the input to the model) consists of a sequence of blocks, each with a header indicating the type of content and a body containing the actual text. The blocks that can appear in queries include:

• [Problem]: A math problem statement in natural language.
• [COT]: A chain-of-thought solution (used when the task is to verify an existing solution or continue reasoning).
• [CI]: Code interpreter invocation (used in RICO data).
• [LEAN]: A LEAN code block, statement, or state.
• [NL Statement]: A natural language mathematical statement (for formal-informal translation tasks).
• [LEAN State]: A LEAN proof state (for theorem proving).
• [ORM]: An outcome reward modeling instruction (asking whether a solution is correct).
• [PRM]: A process reward modeling instruction (asking step-by-step correctness).
• [AUG]: An augmentation instruction (asking for problem rephrasing or harder variants).

Response format structure. The response (the target output) uses matching block types:

• [COT]: Step-by-step reasoning.
• [Code Interpreter]: Python code and execution results.
• [LEAN Calculation Code]: LEAN code that performs a calculation.
• [NL Statement]: A natural language statement (for formal→informal translation).
• [LEAN State]: A LEAN proof state.
• [LEAN Tactic]: A LEAN tactic (a proof step).
• [Correct / Incorrect]: Binary verdict for ORM.
• [Step K: Correct / Incorrect]: Per-step verdict for PRM.
• [AUG Problem]: An augmented or rephrased problem.

How the format enables multi-capability deployment. The same model checkpoint can serve different roles by changing which query template is used:

• As a solver: Query = [Problem] → Response = [COT]
• As a verifier (ORM): Query = [Problem] [COT] [ORM] → Response = [Correct / Incorrect]
• As a verifier (PRM): Query = [Problem] [COT] [PRM] → Response = [Step 1: Correct / Incorrect] [Step 2: ...]
• As a formal reasoner (solving): Query = [Problem] [LEAN] → Response = [LEAN Calculation Code]
• As a formal reasoner (proving): Query = [LEAN State] → Response = [LEAN Tactic]
• As a formal verifier: Query = [Problem] [COT] [LEAN] → Response = [LEAN Calculation Code] (the LEAN code is executed and checked against the COT answer)
• As an augmenter: Query = [AUG] [Problem] → Response = [AUG Problem]

This design means the SFT data mixture includes examples of all these query→response mappings, and the model learns to produce the appropriate output format based on the input block sequence.

Why unification matters for self-improvement. The paper's Figure 2 (right) shows two composite pipelines that use multiple capabilities from the same model:

1. Upper pipeline (data augmentation): Start with a [Problem] → use [AUG] mode to generate a variant → use [COT] mode on the variant → use [RM] mode to verify the solution. This produces verified training data without external models.

2. Lower pipeline (formal verification): Start with a [Problem] → use [COT] mode to get a solution → use [NL Statement] mode to extract the claim → use [LEAN] mode to translate to formal code → execute LEAN code to verify. This provides formal guarantees without human labeling.

Because a single model handles all steps, there is no distribution shift between the generator and the verifier — they share the same weights, the same training data, and the same output distribution. This is in contrast to systems where a GPT-4-based verifier checks a Llama-based generator's outputs, where the verifier's notion of "correct" may not align with the generator's typical outputs.

Chain-of-Thought Data and the Calculation Hallucination Problem

The COT component of the SFT data is the largest and most carefully engineered. The paper identifies a specific failure mode — calculation hallucination — and designs data augmentation strategies to address it.

Base COT data sources. The foundation is MetaMath (Yu et al., 2023b), which provides 395K English chain-of-thought solutions for GSM8K and MATH problems, augmented through question rephrasing and backward reasoning. This is supplemented with:

• Goat (Liu & Low, 2023): 100K synthetic arithmetic problems with step-by-step solutions
• MammoTH (Yue et al., 2023): 216K mixed COT and program-of-thought data
• Khan (Khan, 2021): 83K problems from Khan Academy
• In-house Chinese COT data: 293K human-written Chinese math problems
• Augmented MATH: 28K problems filtered by the authors' PRM
• Augmented Math23K: 195K Chinese problems generated by open-source LLMs and filtered by final-answer correctness
• Several small specialized datasets (prime checking, game-of-24, factoring, triangle area, math commonsense)

The calculation hallucination problem. After continued pre-training with synthetic calculation data (Section 3.1), the authors observed that the model still performed poorly on complex calculations during chain-of-thought. They diagnose the root cause:

"The reason comes from the format of SFT data which requires the model immediately to generate the equation answer like $(12 + 17)^3 = 24389$ inside the chain-of-thought process, and we denote it as calculation hallucination."

The problem is that standard COT data presents calculations as atomic facts — the model sees (12 + 17)^3 = 24389 and learns to emit such equalities directly, without showing intermediate work. When the calculation is complex (multiple brackets, decimals, fractions, powers), the model's next-token prediction is not reliable enough to produce correct compound calculations in a single step. The model either gets the arithmetic wrong (producing a wrong answer that propagates through the solution) or produces a plausible-looking but incorrect intermediate value.

Scratchpad-style rewriting as the solution. The authors apply a post-processing step to existing COT data:

"To alleviate calculation hallucination, we match and rewrite such equations ... inside the chain-of-thought processes as much as possible."

The example given in the paper shows the transformation. Before rewriting:

(12 + 17)^3 = 24389

After rewriting:

(12 + 17)^3 = 29^3 = 841 * 29 = (800 + 40 + 1) * 29 = 23200 + 1160 + 29 = 24389

The rewritten version decomposes the calculation into steps that each involve simpler operations: first evaluate the inner expression (12 + 17 = 29), then compute the cube (29^3 = 29 × 29 × 29, further decomposed as 841 × 29), then use distribution (800 + 40 + 1) × 29 = 23200 + 1160 + 29, and finally sum. Each step is a computation that the model can reliably perform because it involves only multiplication of small integers or addition of round numbers.

Limitations of scratchpad rewriting acknowledged. The paper notes three problems with this approach:

1. Incomplete coverage: "We cannot easily match all equations and calculations that need to be rewritten (e.g. We solve $x^3 - 3x^2 + 3x - 1 = 0$, and obtain $x = 1$)." — Equations involving symbolic manipulation (factoring polynomials) cannot be mechanically decomposed into arithmetic steps.

2. Repetition induction: "Multiple '=' induces models to repeat more." — The chain of equalities format can cause the model to continue producing repetitive calculations beyond what is needed.

3. Verbosity: "This sometimes generates naive step-by-step calculations which may annoy end users." — The decomposed calculations are longer and more tedious to read.

The paper suggests that implicit chain-of-thought reasoning (Deng et al., 2023), where intermediate calculations happen in latent space rather than in decoded text, could alleviate the verbosity issue in future work.

Algorithmic reasoning data (prime checking, game-of-24, etc.). Beyond calculation, the paper introduces SFT data for tasks that require following a specific algorithm:

"Our principle of synthesizing these data is The model generates chain-of-thought based on an algorithm flow chart. The next token prediction must be determined by generated tokens and not dependent on future tokens."

This principle is illustrated with the triangle area example in Section 4. The "good" response first checks whether three sides can form a triangle ($3 + 4 > 5$), then computes squares ($3^2 = 9, 4^2 = 16, 5^2 = 25$), then checks the right-triangle condition ($9 + 16 = 25$), concludes it is a right triangle, and finally computes the area. The "bad" response starts with "Since this triangle is a right triangle" — a claim that requires forward-looking knowledge of $3^2 + 4^2 = 5^2$ which has not yet been established in the reasoning sequence.

This principle enforces causal chain-of-thought: each step must be justified by previously generated tokens, not by information that appears later. Training on data that follows this principle teaches the model to reason forward from known facts rather than to state conclusions and then retroactively justify them — the latter being a common failure mode where the model "reasons" toward a pre-determined answer rather than deriving it.

PRM-based filtering of augmented reasoning paths. For the augmented MATH data (28K samples), the authors use their own trained PRM to filter out incorrect reasoning paths. This is a self-consistency check: the model generates candidate solutions, and the same model's PRM capability (learned from the reward modeling data) evaluates step-by-step correctness, keeping only solutions where every step is rated as correct. This is an early demonstration of the self-improvement loop the paper advocates: the model's generation and verification capabilities are used together to produce higher-quality training data than either could alone.

Reward Modeling: Unifying ORM and PRM in One Model

The reward modeling component enables the model to score candidate solutions — a capability used both at inference time (for reranking multiple samples) and in potential self-improvement loops (for filtering generated training data).

Data source and conversion. The primary data source is Math-Shepherd (Wang et al., 2023b), which provides process-level supervision automatically. Math-Shepherd works by: (1) sampling multiple completions from each intermediate step of a solution, (2) checking whether each completion reaches the correct final answer, and (3) labeling each step as positive or negative based on the fraction of correct completions. The authors "merge of Math Shepherd and self-sampled Math Shepherd-like data" — meaning they apply the same automatic labeling procedure to their own model's outputs, not just the original Math-Shepherd data. The total is 445K samples.

Format conversion for unified seq2seq. The original Math-Shepherd data is in a format specific to reward model training — typically input = (problem, partial solution up to step k), output = (binary label for step k). The paper converts this into the unified format:

ORM query:

[Problem] {problem text}
[COT] {complete solution text}
[ORM] {empty or "Check if this solution is correct"}

ORM response:

[Correct]  or  [Incorrect]

PRM query:

[Problem] {problem text}
[COT] {complete solution text with step markers}
[PRM] {empty or "Check each step"}

PRM response:

Step 1: {Correct/Incorrect}
Step 2: {Correct/Incorrect}
...

This means the model sees both complete-solution judgment (ORM) and step-by-step judgment (PRM) during training, and learns to produce either format depending on the query block sequence. The 445K samples include both ORM-format and PRM-format versions.

Chinese ORM data. The paper adds 104K self-sampled Chinese ORM samples:

"Self-sampled ORM data on Chinese problems."

The procedure is: generate candidate solutions for Chinese math problems using the model itself, check whether each solution's final answer matches the ground truth, and construct ORM training pairs where the label is "Correct" for matching answers and "Incorrect" for non-matching ones. This provides reward modeling capability in Chinese without requiring human-labeled Chinese verification data.

How reward modeling is used at inference time. Appendix D shows two reward modeling use cases:

1. Binary judgment: Given a problem and a candidate solution, the model outputs "This answer is wrong" or "This answer is correct" (shown in the ORM example).

2. Step-by-step marking: Given a problem and a candidate solution with numbered steps, the model annotates each step with <PRM +> or <PRM -> (shown in the PRM example, where a solution to a combinatorics problem has all steps marked negative because the reasoning is flawed).

The paper also shows a comparative judgment format:

[Reward model] Given a question and two answers, which one is better?
...
Response: Answer 2 is better.

This extends beyond binary correctness to relative quality assessment — useful for selecting the best among multiple candidate generations.

Reranking protocol. For benchmark evaluation (Section 6.2.2, Table 19), the reranking procedure is:

1. Sample K candidate solutions from the model (temperature = 0.7).
2. For each candidate, extract the final answer.
3. For ORM reranking: score each complete solution as Correct/Incorrect, select the highest-confidence correct solution.
4. For PRM reranking: score each step, compute an aggregate score (the paper does not specify the aggregation method — whether min, prod, or last — which is a detail gap), select the solution with the highest aggregate score.
5. For LRM (LEAN Reward Model) reranking: translate each COT solution to LEAN code, execute the LEAN code, and keep solutions where (a) the LEAN code compiles and (b) the LEAN output matches the COT's final answer.

Key performance characteristics from Table 19:

• For 7B/MATH: PRM@100 = 47.0 vs. ORM@100 = 46.0 vs. MAJ@100 = 44.8. PRM provides a 2.2-point advantage over majority voting, ORM provides 1.2 points.
• For 20B/MATH: PRM@100 = 50.0 vs. ORM@100 = 48.8 vs. MAJ@100 = 47.4. The gap narrows at larger scales (2.6 points for PRM over MAJ).
• Oracle@100 (upper bound if we could perfectly select the best among 100 candidates) is 80.8 for 7B and 81.8 for 20B — indicating that the reward models are leaving roughly 30+ points on the table compared to perfect selection, consistent with findings in Lightman et al. (2023) that current verifiers are far from oracle performance.

Formal Reasoning: LEAN as Solver, Verifier, and Prover

The formal reasoning component is the most ambitious part of the SFT data, attempting to use LEAN 3 for three distinct purposes: solving grade-school math problems, verifying natural language reasoning, and proving theorems.

Data sources for formal reasoning:

GSM8K-LEAN: Using LEAN as a solver. This is the most unusual component. The authors prompted GPT-4-1106 to generate LEAN 3 solutions for GSM8K training problems:

"We distill gpt-4-1106 to solve the GSM8K train set problems using LEAN 3. We select all codes that can generate correct answers. This part includes 6705 samples."

The generated LEAN code has a distinctive structure, as shown in the paper's example for "A robe takes 2 bolts of blue fiber and half that much white fiber. How many bolts in total does it take?":

def blue_fiber_per_robe : ℕ := 2
def white_fiber_per_robe : ℕ := blue_fiber_per_robe / 2
def total_fiber_per_robe : ℕ := blue_fiber_per_robe + white_fiber_per_robe
#eval total_fiber_per_robe

The model defines named constants, builds up the computation through successive definitions, and uses #eval to output the result. This is essentially a declarative programming approach to word problems — the LEAN code serves as an executable specification of the problem's arithmetic.

COT-LEAN: Translation for verification. The other half of the GSM8K-LEAN data is formatted differently:

"We split half into the format of generating LEAN based on the problem used for training a solver and another half into the format of translating between LEAN and COT used for training a verifier. The verifier translates COT to LEAN and can verify by checking every calculation of COT based on the LEAN calculation."

This creates a verification pipeline: given a natural language chain-of-thought solution, the model translates each calculation step into LEAN code. If the LEAN code executes and produces results matching the COT's intermediate values, the step is verified. This provides formal verification of informal reasoning without requiring the entire problem to be solved in LEAN — only the calculational steps need formal counterparts.

NL-LEAN: Statement translation. The 91K samples from MathLib-train provide training data for translating mathematical statements between natural language and LEAN. An example from Appendix D shows the model translating "Schur inequality" into LEAN 3:

theorem schur_inequality {a : Type*} [linear_ordered_field a] {x y z : a}
  (hnonneg : 0 ≤ x) (hnonneg1 : 0 ≤ y) (hnonneg2 : 0 ≤ z)
  x ^ 3 + y ^ 3 + z ^ 3 + 3 * x * y * z ≥ x * y * (x + y) + y * z * (y + z) +
  x * z * (x + z)

This bidirectional translation capability (formalization and informalization, evaluated in Table 7) is critical for bridging informal problem-solving and formal verification.

MathLib-Train: Theorem proving. The 169K state-tactic pairs from MathLib train the model on the core theorem-proving task: given a LEAN proof state (the current goals), generate the next tactic (proof step). This follows the standard approach of Han et al. (2021) and subsequent work, treating proof generation as a sequence-to-sequence problem where the input is the proof state and the output is the tactic.

LEAN 3 vs. LEAN 4. The paper explicitly notes that it uses LEAN 3, not the newer LEAN 4:

"We use LEAN 3 as our SFT data since GPT-4 can only generate LEAN 3 codes for GSM8K (even if you require it to apply LEAN 4). Furthermore, we find the data of translating between formal and informal from MathLib is preprocessed in LEAN 3."

This is a practical constraint — the data generation pipeline (GPT-4 distillation) and the existing dataset (MathLib preprocessing) are both locked to LEAN 3. The paper acknowledges this as a limitation and states the intention to migrate to LEAN 4 in future versions.

Performance gap between LEAN solving and COT solving. Table 8 shows that using LEAN to solve GSM8K underperforms COT:

• InternLM2-Math-7B: COT = 78.1, LEAN = 70.4 (gap of 7.7 points)
• InternLM2-Math-20B: COT = 82.6, LEAN = 73.9 (gap of 8.7 points)

The paper identifies the root cause as LEAN 3's type system:

"The reasons that using LEAN underperforms COT are: (1) $a - b = 0$ (when $a : \mathbb{N} < b : \mathbb{N}$) (2) division: $a/b = \lfloor a/b \rfloor$ (when $a : \mathbb{N}, b : \mathbb{N}$)."

In LEAN 3, natural numbers (ℕ) do not support negative results — subtraction of a larger number from a smaller number is defined as 0 (truncated subtraction). Similarly, division of natural numbers is floor division. These semantics, inherited from constructive type theory, are correct for many proof contexts but create problems when LEAN is used as a calculator for word problems that require exact rational arithmetic. The paper treats this as a known limitation rather than a fundamental obstacle, suggesting that using rational number types or LEAN 4 would resolve it.

Multi-task learning for LEAN with sparse data. Section 7.2 (Table 13) provides a revealing ablation: when the model is fine-tuned only on GSM8K-LEAN data (without MetaMath), LEAN solving performance drops dramatically and is highly sensitive to data quantity — reducing the data to 1/4 drops performance from 58.0 to 35.1. However, when MetaMath is included in the SFT mix, even with only 1/8 of the GSM8K-LEAN data, LEAN performance remains at 53.4. The interpretation:

"The model mainly needs to learn grammar from GSM8K-LEAN data and learn reasoning ability from MetaMath."

The LEAN-specific data primarily teaches syntax (how to write valid LEAN definitions and use #eval), while the mathematical reasoning capability transfers from the much larger MetaMath dataset. This is evidence for the paper's multi-task unification thesis: capabilities learned for one task (chain-of-thought reasoning) transfer to superficially different tasks (formal LEAN solving) when both are expressed in the same seq2seq format.

Augmentation Helper: Data for Self-Improvement

The augmentation helper data enables the model to generate new training examples from existing ones — a key capability for self-improvement loops.

Data composition (9K samples total):

• Augment-helper (7K): "ChatGPT-generated question augmentation (Luo et al., 2023; Li et al., 2023)" — examples of making problems harder by adding constraints, changing numbers, or modifying the scenario. The format is:

  [AUG] [Problem] {original problem}
  →
  [AUG Problem] {harder variant}
  

• QA-theorem (1K): "Rephrasing a question and an answer into a natural language proof statement." This connects the problem-solving and formal reasoning pipelines — given a solved problem, the model learns to extract the mathematical claim as a theorem statement that could be formally proved. Format:

  [Problem] {problem} [COT] {answer}
  →
  [NL Statement] {theorem statement}
  

• GSM8K-rephrased (2K): "Reformat rephrased questions from MetaMath for rephrasing." This teaches the model to produce semantically equivalent but textually different versions of problems — useful for data augmentation without changing difficulty.

The self-improvement vision (Figure 2, upper right pipeline). The augmentation helper is designed to work in a loop with the COT and RM capabilities:

1. Start with a seed problem.
2. Use [AUG] mode to generate a harder variant.
3. Use [COT] mode to solve the variant.
4. Use [RM] mode to verify the solution.
5. If verified correct, add (variant, solution) to the training data.
6. Fine-tune the model on the expanded dataset.
7. Repeat.

This loop requires no external models and no human labeling — the same model generates, verifies, and filters its own training data. The paper does not report results from running this loop (it is presented as a capability that the model is prepared for rather than one that has been demonstrated to improve performance), but the architecture is designed to support it.

Code Interpreter: Reasoning Interleaved with Coding (RICO)

The code interpreter capability is the most technically detailed component of the SFT system and introduces a novel interaction protocol.

Design principles. The RICO design is motivated by three desiderata that the paper argues prior approaches fail to satisfy:

1. Multi-turn interaction: The model should see code execution results and be able to write more code based on those results, mimicking how a human uses a calculator or programming environment — solve part of a problem, compute something, reflect, adjust, continue.

2. Format consistency with chat: The reasoning text should use the same format as a standard chat response (no special code-block delimiters that differ from the model's normal output format), allowing the code interpreter capability to be deployed in the same chat infrastructure as other capabilities.

3. Tool-calling protocol: The code generation should be invoked through a general tool-calling interface (similar to how GPT-4's function calling works) rather than being embedded in the text via markdown syntax. This separates the reasoning from the tool use cleanly.

The RICO interaction protocol (Figure 3). Each round of interaction follows a three-part structure:

1. <|Assistant|>: The model produces natural language reasoning, potentially setting up what needs to be computed next.

2. <|Interpreter|>: The model generates Python code (shown with "python prefix in the example) that will be executed.

3. <|Environment|>: The code execution results are inserted into the context, and the model can continue reasoning based on these results.

This cycle repeats until the model produces a final answer. Figure 3 shows an example with two rounds: the first round sets up variables and solves for x, getting the answer [2]; the second round substitutes x = 2 back into the expressions for y and z, getting (-1, 2), and then produces the final answer.

How RICO differs from prior approaches. The paper contrasts with:

• Program-of-thought (PAL, Chen et al., 2023b): Generates one program, executes it, and takes the output as the answer. The model never sees intermediate results and cannot adjust. RICO allows multi-turn adjustment.

• ToRA (Gou et al., 2023): Embeds code in markdown code blocks within the text. The model sees execution results but the format is inconsistent with chat — markdown code blocks have different semantics than tool calls. The paper argues this creates ambiguity when deploying in chat systems where markdown formatting is rendered for users.

• MathCoder (Wang et al., 2023a): Uses separate marks for text and code, which similarly creates format inconsistency with standard chat models.

RICO's format uses explicit boundary tokens (<|Assistant|>, <|Interpreter|>, <|Environment|>) that serve as unambiguous signals for the chat system: when <|Interpreter|> appears, extract the code and execute it; when <|Environment|> appears, the content is execution output, not model-generated text. This cleanly separates the model's reasoning from tool interactions.

Training data construction through iterative hard example mining. The RICO training data (76K samples) is constructed through a multi-iteration process designed to reduce reliance on GPT-4:

"At each iteration, we first use the model trained in the previous iteration to generate responses on the train set of GSM8K and MATH. Since the model cannot fully fit the train set, we use GPT-4-turbo to generate responses on the remaining train set once. The correct responses generated by the most recent model and GPT-4-turbo will be used to train a new model for the next iteration."

The procedure works as follows:

1. Initialization: Generate RICO-format solutions for GSM8K and MATH training problems using ToRA-70B (Gou et al., 2023). Since ToRA uses a different format (markdown code blocks), these are converted to the RICO format with explicit boundary tokens. This provides initial training data even though the quality may be suboptimal.

2. Iteration 1: Train InternLM2-Math on the initial RICO data. Use this trained model to generate solutions for all GSM8K and MATH training problems. Some problems will be solved correctly (by the model), others will not. For the unsolved problems, use GPT-4-Turbo to generate RICO solutions (one pass only — "once"). Collect all correct solutions (from both the model and GPT-4-Turbo) as the training data for the next iteration.

3. Iteration 2+: Repeat: train a new model on the expanded correct-solution dataset, generate on the training set, fill gaps with GPT-4-Turbo, and expand the dataset further.

This is an iterative distillation process: the model learns from a mix of its own (correct) outputs and GPT-4's outputs on problems it cannot yet solve. Over iterations, the model solves more problems correctly on its own, reducing the reliance on GPT-4. The final model, InternLM2-Math, is trained on the accumulated correct solutions from all iterations plus GPT-4's gap-filling contributions.

Why this matters for the benchmark results. The iterative mining strategy means that InternLM2-Math's RICO capability is not simply distilled from GPT-4 — it incorporates self-generated solutions that were verified correct (because they produced the right answer on the training set). This is a form of self-training, where the model's own successful reasoning becomes part of its training data for the next iteration. The paper does not report what fraction of the final 76K RICO samples came from the model vs. GPT-4 at each iteration, which would be informative about the degree of self-training vs. distillation.

InternLM2-Math vs. InternLM2-Chat on code interpreter. Table 9 shows that InternLM2-Math-7B (50.9 on MATH with Python) outperforms InternLM2-Chat-7B (45.1), despite both models using "the same training data for code interpreter." The paper attributes this gap to improved math reasoning ability from the math-specific continued pre-training and SFT:

"Since InternLM2-Math and InternLM2-Chat adopt the same training data for code interpreters, we believe the improvements of InternLM2-Math over InternLM2-Chat models result in the improvement of math reasoning ability."

This suggests that the code interpreter capability benefits from stronger underlying mathematical reasoning — knowing what to compute and how to structure the multi-turn interaction is as important as knowing the Python syntax for doing so.

SFT Training Configuration

The supervised fine-tuning configuration (Appendix B) uses:

• Initialization: From InternLM2-Math-Base checkpoints (7B or 20B).
• Learning rate: Peak $lr_{max} = 4 \times 10^{-5}$, minimum during warmup $lr_{min} = 6 \times 10^{-6}$. These are the same for both 7B and 20B models.
• Data volume: The SFT data is tokenized into 622.7M tokens.
• Batching: Batch size of 1 per GPU with packed dataset (multiple samples concatenated to fill the context window).
• Max sequence length: 32,768 tokens — substantially larger than the pre-training context length of 4,096, accommodating long multi-turn RICO interactions and LEAN code with comments.
• Optimizer: Adam (the paper says "Adam Optimizer" in Appendix B, though Section 3.3 specifies AdamW for pre-training — this may be a notation inconsistency or an intentional difference).
• Epochs: 3 epochs over the 622.7M tokens.
• Hardware: 32 GPUs for 7B (training takes ~7 hours), 64 GPUs for 20B (~10 hours).

The packed dataset with max sequence length 32,768 is noteworthy: it means that many short problems are concatenated into a single training sequence, separated by the model's end-of-sequence token, and the model learns to attend only within each problem's boundaries (via attention masking). This is more efficient than padding each sample to the max length individually, since it reduces wasted computation on padding tokens.

4. Key Insights and Innovations

Innovation 1: Difficulty-Conditioned Compute-Optimal Test-Time Scaling

The paper's most fundamental contribution is not any single method but rather the meta-strategy of adaptively allocating test-time compute based on prompt difficulty. Prior work treated test-time compute as a uniform knob: turn it up (more samples, more search) and performance improves. This paper demonstrates that the relationship between compute and performance is qualitatively different depending on problem difficulty, and that ignoring this heterogeneity leaves enormous efficiency on the table.

What makes this genuinely novel — rather than an obvious observation — is that the difficulty-dependent behavior is often counterintuitive. Beam search, the strongest optimizer, actually hurts performance on easy problems at high budgets due to verifier over-optimization (Figure 3, right), while it helps substantially on medium-difficulty problems. Similarly, sequential revisions dominate on easy problems but a balanced sequential-parallel ratio is optimal on hard ones (Figure 7, right). These are not monotonic relationships where "more powerful = better." The compute-optimal policy exploits these non-monotonicities to achieve 4× better efficiency than best-of-N (Figures 4 and 8), which is a significant practical gain.

This contribution is best understood as an inference-time analog of the Chinchilla scaling laws for pretraining. Just as Hoffmann et al. (2022) showed that the optimal allocation of pretraining compute between model size and data quantity varies with total budget, this paper shows that the optimal allocation of test-time compute between search strategies varies with problem difficulty. The conceptual parallel is direct, but the underlying mechanism is entirely different — pretraining scaling laws optimize over continuous variables (parameters, tokens), while this paper optimizes over a discrete, combinatorial space of strategy hyperparameters conditioned on a difficulty estimate.

A subtle but important point: the predicted (non-oracle) difficulty bins perform nearly as well as oracle bins (the curves largely overlap in Figures 4 and 8). This is what makes the contribution practical rather than merely analytical. If the gains required ground-truth labels to estimate difficulty, the approach would be circular. The fact that the PRM's own score distribution serves as a sufficient proxy means the system is deployable without access to answers.

Innovation 2: The Proposal Distribution and Verifier as Complementary, Independent Scaling Axes

The unifying framework in Section 2 — decomposing all test-time compute methods into modifications to the proposal distribution (what the model generates) versus the verifier (how outputs are selected) — is not itself technically novel. It echoes the proposer-scorer decomposition familiar from MCMC and reinforcement learning. What is novel is the paper's empirical demonstration that these two axes have complementary, difficulty-dependent strengths and that combining them yields gains neither achieves alone.

Concretely: revisions (proposal modification) are most effective on easy problems where the model's initial output is roughly correct and just needs refinement — a local search in answer space. Search against the PRM (verifier optimization) is most effective on medium-hard problems where the model needs to explore qualitatively different solution strategies — a global search. Prior work studied these mechanisms in isolation, often reaching pessimistic conclusions (e.g., "LLMs cannot self-correct reasoning" from Huang et al., 2023). This paper's framework reconciles those findings: self-correction does work, but only on the right difficulty tier. Search does help, but only with the right algorithm at the right budget. The conflicting prior results were an artifact of testing different methods on different (implicitly difficulty-biased) problem distributions.

This insight is more than taxonomic. It implies that future systems should not choose between revisions and search but should deploy both, switching between them per-prompt. The paper doesn't fully realize this vision (Section 8 acknowledges that PRM tree-search was not combined with revisions), but the framework provides the intellectual scaffolding for doing so.

Innovation 3: Empirical Evidence That Test-Time Compute Can Substitute for Pretraining — With Sharp Boundaries

The FLOPs-matched comparison in Section 7 is, to the authors' knowledge, the first to demonstrate in a realistic setting (no ground-truth access at inference) that a smaller model with additional test-time compute can outperform a ~14× larger model on problems within its capability range. This is significant not as a method but as an empirical finding with direct implications for how compute budgets should be allocated in production systems.

What distinguishes this from prior work on training-inference tradeoffs (Jones, 2021; Villalobos and Atkinson, 2023) is the specificity of the finding. The paper doesn't claim a universal substitution — it precisely characterizes where the substitution works (easy-to-medium problems, low R regimes) and where it fails (hard problems, high R regimes). The failure case is equally informative: on the hardest problems (bin 5), test-time compute provides essentially zero benefit regardless of budget, meaning that some capabilities can only be acquired through pretraining, not recovered at inference time. This establishes a clear boundary condition: test-time compute amplifies existing capability but does not create it from nothing.

The dependence on R = D_inference / D_pretrain adds practical nuance that prior analyses missed. For self-improvement pipelines where R ≪ 1, the case for test-time compute is strong. For high-throughput production deployments where R ≫ 1, the case weakens because the per-query inference cost of the larger model dominates the budget anyway. This is an incremental but practically important refinement of the training-inference tradeoff picture.

Innovation 4: Verifier Over-Optimization as a First-Class Phenomenon in Test-Time Scaling

While reward hacking / over-optimization is well-documented in the RLHF literature, this paper provides some of the first clear evidence that the same phenomenon governs test-time search scaling and is the primary bottleneck preventing unbounded improvements from additional compute. The evidence is concrete: beam search degrades easy-problem performance at high budgets (Figure 3, right); lookahead search — the most powerful optimizer — paradoxically performs worst overall (Figure 3, left); and qualitative examples in Appendix M show search producing degenerate outputs (repetitive low-information steps, overly short solutions) that score highly under the PRM.

This finding is significant because it shifts the narrative around test-time compute from "more is better" to "more is better only up to the verifier's reliability frontier." It explains why prior work found negative results for sophisticated search methods: those studies likely pushed past the over-optimization threshold. It also implies that improving verifier robustness is the key bottleneck for further scaling test-time compute, not improving search algorithms. The paper's compute-optimal policy can be understood partly as a way to stay below the over-optimization threshold per difficulty level — using weaker optimization (best-of-N) where the verifier is reliable (easy problems) and stronger optimization (beam search) only where the verifier signal has more room to provide genuine guidance (medium problems).

5. Experimental Analysis

Evaluation Methodology

Dataset. The paper evaluates on a diverse set of informal and formal math benchmarks. For informal reasoning, the primary datasets are GSM8K (Cobbe et al., 2021) and MATH (Hendrycks et al., 2021a). The authors use the specific MATH split from Lightman et al. (2022) with 12,000 training problems and 500 test problems. Additional informal benchmarks include the Hungary math exam (used to test out-of-domain generalization), MathBench-ZH (600 Chinese problems spanning primary through university levels), and TAL-SCQ5K (a Chinese multiple-choice dataset). For formal reasoning, the primary benchmark is MiniF2F (Zheng et al., 2021), consisting of 244 test problems in LEAN. The formal-informal translation evaluation uses the ProofNet dataset from Azerbayev et al. (2023a). The Game of 24 test set comes from Yao et al. (2023). For prime checking, the authors construct a custom test set of 20 numbers per digit length from 2 to 10, each with 10 prime and 10 composite numbers ending in 1, 3, 7, or 9.

Base model(s). All models are initialized from InternLM2-Base (7B and 20B parameter variants), described as a strong general-purpose LLM with demonstrated math, code, chat, instruction-following, and creative writing capabilities. The continued pre-training produces InternLM2-Math-Base, which is then fine-tuned to produce InternLM2-Math (the SFT model). For the FLOPs-matched scaling comparisons (Appendix E, InternLM2-Math-Plus), the paper also initializes from Mixtral-8x22B. The 7B scale is chosen as a standard open-source size for head-to-head comparison with Llemma-7B, Mistral-7B, and DeepSeek-Math-7B. The 20B scale provides a larger reference point between 7B and 34B+ models.

Metrics. For informal benchmarks, the primary metric is greedy accuracy (zero-shot or few-shot, single deterministic generation) or majority voting accuracy (MAJ@K: the most common answer among K sampled solutions is compared to the ground truth). For MATH specifically, the paper reports both greedy accuracy and MAJ@K where K = 256 for pre-trained models and K = 100 for SFT model reranking. For MiniF2F, the metric is proof success rate — the fraction of 244 test problems for which the model generates a LEAN proof that compiles and closes all goals, using a search budget of 1 × 32 (one attempt, generating up to 32 tokens per step). For formal-informal translation (Table 7), the metric is BLEU-4 score. For the Hungary exam and MathBench-ZH, accuracy is computed as the fraction of correct answers. For MathBench-ZH multiple-choice questions, the paper applies a strict criterion: "For each choice problem, we will shuffle the choice order 4 times. A model gives a correct answer 4 times can be considered as correct" — requiring consistent correctness across all choice permutations.

Baselines. The paper compares against a comprehensive set of open-source models: Llemma-7B and Llemma-34B (Azerbayev et al., 2023b) as the most direct math-pretrained competitors; Minerva-8B, Minerva-62B, and Minerva-540B (Lewkowycz et al., 2022b) as closed-source math-pretrained baselines; MetaMath fine-tuned on Llama-2-7B, Mistral-7B, and Llemma-7B (Yu et al., 2023b) as the primary SFT baseline; DeepSeek-Math-7B-RL (Shao et al., 2024) and DeepSeek-Coder-7B (Guo et al., 2024) as concurrent open-source math and code models; ToRA-7B, ToRA-13B, ToRA-70B (Gou et al., 2023) and MathCoder-CL variants (Wang et al., 2023a) as code-interpreter baselines; GPT-4 (original version and 0125-preview) and ChatGPT as closed-source upper bounds; ReProver (Yang et al., 2023a) and LLMStep (Welleck & Saha, 2023) as formal proving baselines. For the reward modeling comparison (Table 6), baselines include MetaMath-Llemma-34B and MetaMath-DeepSeek-67B (Wang et al., 2023b) and GPT-4-MathMix (Lightman et al., 2023).

Generation budget / compute accounting. The paper does not use a FLOPs-based compute accounting for the main experiments. Instead, the generation budget is measured in number of sampled solutions (K) for majority voting and reranking experiments, or single greedy generations for zero-shot accuracy. No cross-method compute equalization is applied — for example, RICO and COT are compared at the same number of problems solved, without accounting for RICO's additional cost of executing Python code or its multi-turn generation overhead. The search budget for MiniF2F is standardized at 1 × 32 across all compared models.

Cross-validation / statistical protocol. The paper does not report confidence intervals, standard deviations, or statistical significance tests for any results. There is no cross-validation in the main benchmark evaluations — test set performance is reported as a single number per benchmark. The only split-based protocol mentioned is the two-fold split of GSM8K-LEAN data (half for solver training, half for translation training). The Process Correctness study (Section 7.4, Table 15) uses manual human labeling of 25 problems, but this is too small a sample for statistical claims about false positive rates.

Main Quantitative Results

Pre-Training Performance on Informal Benchmarks (Table 2)

The continued pre-training from InternLM2-Base to InternLM2-Math-Base produces substantial improvements on both GSM8K and MATH under in-context learning. The headline numbers:

InternLM2-Math-Base-7B achieves 49.2 MAJ@1 and 75.7 MAJ@256 on GSM8K, and 21.5 MAJ@1 and 35.6 MAJ@256 on MATH. This represents large gains over the InternLM2-Base-7B starting point, which achieved only 36.5 MAJ@1 on GSM8K and 8.6 MAJ@1 on MATH — an improvement of 12.7 and 12.9 points respectively in greedy decoding. Against the closest open-source competitor, Llemma-7B (36.4 MAJ@1, 54.0 MAJ@100 on GSM8K; 18.0 MAJ@1, 33.5 MAJ@256 on MATH), InternLM2-Math-Base-7B outperforms by 12.8 points in GSM8K greedy accuracy and 3.5 points in MATH greedy accuracy.

InternLM2-Math-Base-20B achieves 63.7 MAJ@1 and 84.8 MAJ@256 on GSM8K, and 27.3 MAJ@1 and 46.2 MAJ@256 on MATH. This outperforms Minerva-62B (52.4 MAJ@1, 68.5 MAJ@100 on GSM8K; 27.6 MAJ@1, 43.4 MAJ@256 on MATH) on GSM8K by 11.3 points greedy despite being ~3× smaller, and essentially matches Minerva-62B on MATH (difference of 0.3 points greedy). Against Llemma-34B (51.5 MAJ@1, 69.3 MAJ@100 on GSM8K; 25.0 MAJ@1, 43.1 MAJ@256 on MATH), InternLM2-Math-Base-20B shows a 12.2 point greedy advantage on GSM8K and 2.3 points on MATH.

The majority-voting scaling curves (Figure 1) show that InternLM2-Math-Base-7B's performance trajectory on MATH (MAJ@256 = 35.6) lies between Llemma-7B (MAJ@256 = 33.5) and Llemma-34B (MAJ@256 ≈ 43), measured at 256 samples.

Fine-Tuning with MetaMath: Cross-Model Comparison (Table 3)

To validate that the continued pre-training benefits transfer to supervised fine-tuning, the paper fine-tunes multiple base models on the identical MetaMath dataset. Under this controlled SFT data comparison:

• InternLM2-Math-Base-7B achieves 76.4 on GSM8K and 33.8 on MATH, outperforming MetaMath-Mistral-7B (77.7 / 28.2) on MATH by 5.6 points while slightly underperforming on GSM8K (76.4 vs. 77.7). Against MetaMath-Llemma-7B (69.2 / 30.0), InternLM2-Math-Base-7B leads by 7.2 points on GSM8K and 3.8 on MATH.

• InternLM2-Math-Base-20B achieves 80.7 on GSM8K and 36.1 on MATH, outperforming MetaMath-Llemma-34B (75.8 / 34.8) on both benchmarks.

These results demonstrate that the continued pre-training provides a stronger foundation than Llemma's pre-training, even when both are fine-tuned on identical SFT data. The MATH improvement is particularly notable: the 7B model with MetaMath SFT (33.8) nearly matches the 20B model's performance after full InternLM-Math SFT (37.7, Table 5), suggesting the base model's pre-training quality is a major factor.

SFT Performance: Zero-Shot Chain-of-Thought (Table 5)

InternLM2-Math's full SFT data produces strong zero-shot chain-of-thought performance across four benchmarks:

InternLM2-Math-7B: 78.1 on GSM8K, 34.6 on MATH, 55 on the Hungary math exam, and 40.0 on MathBench-ZH. Compared to MetaMath-InternLM2-Math-Base-7B (which used only MetaMath for SFT, scoring 76.4 / 33.8 on GSM8K/MATH), the full SFT yields a 1.7-point GSM8K gain and 0.8-point MATH gain — modest, but the Hungary exam shows strong generalization (55 vs. 29 for MetaMath-Mistral-7B and 41 for ChatGPT). Against off-the-shelf chat models at similar scale, InternLM2-Math-7B substantially outperforms DeepSeek-7B-Chat (63.0 / 15.8) and Qwen-7B-Chat (51.7 / 11.6).

InternLM2-Math-20B: 82.6 on GSM8K, 37.7 on MATH, 66 on the Hungary exam, and 45.3 on MathBench-ZH. This places it second only to GPT-4 (original version: 92.0 / 42.5 / 68 / 47.2) among all evaluated models, outperforming Qwen-72B-Chat (78.9 / 35.2 / 52 / 47.8) and DeepSeek-67B-Chat (84.1 / 32.6 / 58 / 33.2) despite using ~4× fewer parameters. The Hungary exam score of 66 is particularly strong (GPT-4 scores 68), suggesting the in-house Chinese and English COT data mixture produces genuine cross-lingual and cross-domain generalization.

MATH by category and difficulty (Tables 17–18). The per-category breakdown shows InternLM2-Math-20B's strengths: 59.1 on Pre-Algebra, 55.9 on Algebra, 30.0 on Geometry, and 30.2 on Number Theory — with Geometry being the weakest category. By difficulty, performance predictably decreases: Level 1 (easiest) at 75.5, Level 5 (hardest) at 13.7 for the 20B model. The 7B model shows a steeper decline: 75.1 (Level 1) to 12.5 (Level 5). The difficulty trend is monotonic, with no anomalous reversals.

Code Interpreter: RICO Performance (Table 9)

Using reasoning interleaved with coding (RICO), InternLM2-Math achieves significant gains over chain-of-thought alone:

InternLM2-Math-7B: 79.4 on GSM8K with RICO (vs. 78.1 with COT, a 1.3-point gain) and 50.9 on MATH (vs. 34.6 with COT, a 16.3-point gain). The MATH improvement is dramatic — nearly 1.5× the COT accuracy — highlighting that complex calculations, symbolic manipulation, and multi-step computation are major bottlenecks for pure chain-of-thought reasoning. This surpasses ToRA-7B (44.6 on MATH) by 6.3 points and MathCoder-CL-7B (30.2) by 20.7 points.

InternLM2-Math-20B: 80.7 on GSM8K (actually lower than COT's 82.6 — RICO slightly underperforms COT on this benchmark) and 54.3 on MATH (vs. 37.7 with COT, a 16.6-point gain). This outperforms ToRA-70B (49.7) by 4.6 points on MATH despite using ~3.5× fewer parameters, and matches MathCoder-CL-34B (45.2) with a 9.1-point advantage. GPT-4 Code Interpreter scores 69.7 — still a substantial 15.4-point gap above InternLM2-Math-20B.

The GSM8K result (RICO underperforming COT on the 20B model) is noteworthy: GSM8K problems typically involve simple arithmetic that chain-of-thought handles well, and the overhead of generating and executing Python code may introduce more opportunities for format errors or unnecessary computation without accuracy benefits.

Reward Modeling: Reranking Performance (Table 6, Table 19, Figure 4)

Using the model as its own verifier for reranking, InternLM2-Math achieves:

InternLM2-Math-7B: On MATH@500, PRM reranking with K=100 samples achieves 47.0 accuracy — a 12.4-point improvement over greedy (34.6). ORM@100 achieves 46.0, majority voting@100 achieves 44.8. On GSM8K, PRM@100 achieves 84.0, compared to MAJ@100 at 83.5 — only a 0.5-point gain, indicating that the verifier provides more value on harder problems where the model's raw generation is less reliable.

InternLM2-Math-20B: On MATH@500, PRM@100 achieves 50.0 — a 12.3-point improvement over greedy (37.7). This outperforms MetaMath-Llemma-34B (PRM@256 = 47.3) and MetaMath-DeepSeek-67B (PRM@256 = 48.1), using 2.56× fewer samples and a ~3× smaller model.

The LRM (LEAN Reward Model) results are notable: on GSM8K with the 7B model, LRM@100 achieves 85.8, outperforming PRM@100 (84.0) and ORM@100 (84.2) by 1.6-1.8 points. However, on the 20B model, LRM@100 (89.0) is comparable to PRM@100 (89.3) — the advantage diminishes with scale. The paper does not report LRM performance on MATH, which is unfortunate given that MATH contains more complex reasoning where formal verification might provide greater benefit.

The oracle upper bound (optimal selection among K candidates) reveals substantial room for improvement: on MATH with the 20B model, oracle@100 is 81.8, while the best verifier (PRM@100) achieves only 50.0 — a 31.8-point gap. This gap is even larger than that reported in Lightman et al. (2023), where GPT-4 PRM@1860 achieved 78.2 vs. an oracle that would be nearly 100 for a model with high pass@1860. The large oracle gap suggests that either: (a) InternLM2-Math's PRM is significantly less reliable than GPT-4's, (b) the pass@100 rate is much higher than the PRM's selection accuracy indicates, or (c) both.

Formal Reasoning: MiniF2F Performance (Table 4)

In the few-shot (3-shot) in-context learning setting on MiniF2F-test, InternLM2-Math-Base achieves a new open-source state-of-the-art at the 7B scale:

InternLM2-Math-Base-7B solves 74 of 244 problems, achieving 30.3 accuracy. This outperforms Llemma-7B (26.2) and Llemma-34B (25.8), as well as DeepSeek-Coder-7B (28.7) and DeepSeek-Math-7B-Base (28.3). The paper notes that "InternLM2-Math-7B-Base and InternLM2-Math-20B-Base find 25 and 24 new proofs respectively which do not appear in the official MiniF2F repository" — suggesting that the model is not simply memorizing training set solutions but generalizing to novel proofs. Intriguingly, the 20B model (29.5) slightly underperforms the 7B model (30.3), consistent with the paper's observation that "we do not find the formal reasoning performances scale with model parameter sizes." This flat scaling curve for formal reasoning is consistent with findings from Llemma (Azerbayev et al., 2023b) and suggests that formal proof data sparsity, not model capacity, is the bottleneck.

The InternLM2-Math-Plus results (Table 20, Appendix E) show substantial improvements over the base version: Plus-7B achieves 43.4 on MiniF2F-test, Plus-1.8B achieves 38.9, and Plus-20B achieves 42.6. These results, using LEAN 4 and presumably improved training data, place InternLM2-Math-Plus-7B above all prior open-source models including HTTPS (41.0, Lample et al., 2022, which uses hyper-tree proof search).

Formal Translation Performance (Table 7)

On bidirectional translation between natural language and LEAN statements (evaluated on ProofNet's undergraduate math textbook excerpts):

InternLM2-Math-7B: BLEU-4 of 15.0 for formalization (NL → LEAN) and 9.4 for informalization (LEAN → NL). InternLM2-Math-20B: 15.7 and 10.2. These scores substantially outperform ProofGPT-1.3B (8.1/5.1) and ProofGPT-6.7B (4.7/6.0), but remain well below CodeX (25.1/13.2) and GPT-4 (27.1 for formalization). The 20B model shows only marginal improvement over the 7B (15.7 vs. 15.0), reinforcing the pattern that formal translation ability does not scale strongly with model size in this range.

LEAN as Solver: GSM8K Performance (Table 8)

Using LEAN 3 to directly solve GSM8K problems:

InternLM2-Math-7B: 70.4 with LEAN vs. 78.1 with COT (gap of 7.7 points). InternLM2-Math-20B: 73.9 with LEAN vs. 82.6 with COT (gap of 8.7 points). The underperformance is attributed to LEAN 3's natural number arithmetic semantics — truncated subtraction and floor division cause correctness issues on problems requiring negative numbers or exact rational results. Despite underperforming COT, the LEAN approach achieves non-trivial accuracy (70-74%), demonstrating feasibility of using formal languages for informal problem-solving, a novel direction.

Specialty Abilities: Game of 24 and Prime Checking (Tables 10-11)

The rule-generated SFT data for algorithmic reasoning tasks produces notable capabilities:

Game of 24 (Table 10): InternLM2-Math-7B achieves 26% accuracy with a single sample, compared to fine-tuned Llama2-7B at 11% and GPT-4 with COT at 4% — a substantial margin. The 20B model reaches 35%. These single-sample results already approach ToT's 45% (which uses 12 samples, b=1), suggesting the step-by-step search process SFT data teaches effective reasoning strategies. OVM (Yu et al., 2023a) reaches 79% with 20 samples, indicating further gains from test-time search are available.

Prime checking (Table 11): The 7B model correctly identifies 10/10 prime and 10/10 composite numbers at almost all digit lengths from 2 to 10, with minor errors on composites at 4-7 digits. The 20B model shows a similar pattern. In contrast, GPT-4-0125-preview performs well at 2-3 digits but degrades sharply: at 8 digits, it identifies 0/10 primes and 0/10 composites correctly — effectively random guessing. The paper does not explain this stark difference, though it likely reflects InternLM2-Math's explicit rule-generated training for prime factorization algorithms versus GPT-4's reliance on memorized facts.

Ablation Studies and Robustness Checks

Pre-training token amount (Section 7.1, Table 12): The 7B model is evaluated at 40B, 80B, 120B, 160B, and 200B continued pre-training tokens. ICL performance on GSM8K peaks at 120B (39.0) and declines at 200B (35.1), while MATH ICL peaks at 120B (21.5) and plateaus. SFT performance on MATH peaks at 120B (33.8 on MetaMath), with all checkpoints between 80B and 200B staying within 30.2-33.8. The finding is that performance does not substantially improve beyond 80B tokens (~3 epochs), and training to 200B (~7 epochs) begins to degrade ICL performance while SFT performance remains relatively robust — suggesting the model overfits to the pre-training distribution in ways that hurt few-shot generalization but are largely corrected by fine-tuning. This motivated the early stop at 80B for the 20B model.

LEAN data quantity and multi-task interaction (Section 7.2, Table 13): The amount of GSM8K-LEAN SFT data is varied from full (1/1) to 1/8, both with and without MetaMath in the SFT mix. Without MetaMath: LEAN solving performance drops from 58.0 (full data) to 38.4 (1/8 data) — highly sensitive to data quantity. With MetaMath: LEAN performance only drops from 66.0 (full data + MetaMath) to 53.4 (1/8 data + MetaMath) — far more robust. The COT performance with MetaMath remains stable (75.7 to 77.7 across LEAN data quantities), confirming that the LEAN data primarily teaches syntax while reasoning ability transfers from MetaMath. This is the paper's strongest evidence for multi-task synergy: sparse formal data is made effective by co-training with abundant informal reasoning data.

SFT data composition ablation (Section 7.3, Table 14): Starting from the full InternLM2-Math-7B SFT mixture, individual components are removed, keeping MetaMath as a baseline:

• Full SFT: 34.60 MATH / 78.09 GSM8K
• MetaMath only: 33.78 / 76.35
• MetaMath + COT: 34.02 / 77.63 (slightly better than MetaMath-only)
• MetaMath + CI (Code Interpreter): 33.56 / 77.63
• MetaMath + Formal: 32.12 / 76.12 (worse than MetaMath-only on MATH by 1.66 points)
• MetaMath + RM: 29.84 / 75.13 (worse on both benchmarks)
• MetaMath + Augmenter: 32.08 / 75.89

The key finding: adding any single non-COT component to MetaMath degrades performance (with the largest drop of 3.94 MATH points for RM). The paper interprets this as format interference — the reward modeling, formal reasoning, and augmentation formats introduce output patterns that conflict with pure chain-of-thought generation when mixed naively. Yet the full mixture outperforms all partial mixtures, recovering and exceeding the MetaMath+COT baseline. This is evidence for what the paper describes as "latent mutual helpfulness of comprehensive data beyond their original special usage" — the model learns shared representations when all formats are present together, but partial mixtures cause format confusion without providing enough diverse signal to overcome it.

False positive analysis (Section 7.4, Table 15): Manual inspection of 25 MATH problems where InternLM2-Math-20B produces the correct answer reveals: at difficulty Level 1, all 5 correct answers have correct reasoning (5/5). At Level 2, only 4/5 have correct reasoning. At Level 5, only 3/5 have correct reasoning. The overall false positive rate is 5/25 = 20%. The case study shows a counting problem where the model makes logical errors (listing odd numbers as even, misapplying GCD criteria) but coincidentally arrives at the correct integer count. This directly supports the paper's motivation for verification: outcome accuracy overstates reasoning quality, and the gap widens with difficulty.

MiniF2F decontamination (Section 8 limitations): The paper explicitly acknowledges that "we do not check the contamination of AlgebraicStack on MiniF2F. AlgebraicStack may or may not contain MiniF2F solutions. However, the comparison between Llemma and our model is fair." Since AlgebraicStack is sourced from the same open-source dataset used by Llemma, both models have equal exposure to any MiniF2F solutions in the pre-training data, making the comparison fair but the absolute scores potentially inflated for both.

Critical Assessment

On the Claim of Open-Sourced SOTA Performance

The paper claims that InternLM2-Math "obtains open-sourced state-of-the-art performance under the setting of in-context learning, supervised fine-tuning, and code-assisted reasoning in various informal and formal benchmarks." This claim is well-supported by the reported experiments, with important qualification:

The SOTA claim holds at the 7B scale across essentially all benchmarks: InternLM2-Math-Base-7B outperforms Llemma-7B on ICL (Table 2), InternLM2-Math-7B outperforms MetaMath-Mistral-7B, MetaMath-Llemma-7B, and all other 7B-class models on SFT (Table 5), and InternLM2-Math-Base-7B achieves the highest MiniF2F score of any 7B model (Table 4).

At the 20B scale, the claim is more nuanced. InternLM2-Math-20B outperforms Llemma-34B and Minerva-62B on GSM8K and MATH ICL (Table 2), and outperforms Qwen-72B-Chat and DeepSeek-67B-Chat on MATH and the Hungary exam despite being ~3-4× smaller (Table 5). However, the paper is concurrent with DeepSeek-Math (Shao et al., 2024), which is only partially compared against. Table 4 shows DeepSeek-Math-7B-Base achieving 28.3 on MiniF2F — close to InternLM2-Math-7B-Base's 30.3 — and the DeepSeek-Math SFT/RF model is not compared in the main tables. The InternLM2-Math-Plus results (Tables 20-22) show competitiveness with DeepSeek-Math-7B-RL (53.0 vs. 51.7 on MATH), but these were added in a post-hoc appendix without detailed comparisons. A direct head-to-head table against DeepSeek-Math across all benchmarks is notably absent.

On the Unification of Capabilities

The paper's central architectural claim is that unifying solver, verifier, augmenter, and formal reasoner into a single model is valuable. The evidence for this claim is mixed:

The data ablation (Table 14) provides the strongest evidence. The fact that individual non-COT components hurt performance when added to MetaMath, but the full mixture outperforms all partial mixtures, demonstrates that there is genuine multi-task synergy — not just the sum of independent capabilities. However, the mechanism of this synergy is not empirically isolated: is it that the PRM training improves the model's ability to self-evaluate during COT generation? That the formal reasoning data improves attention to logical structure? That the code interpreter data improves numerical precision in COT? None of these causal hypotheses are tested with appropriate ablations.

No demonstration of the self-improvement loop. The paper presents the model as "ready for self-improving" and shows the pipeline in Figure 2, but never demonstrates that using the model's augmentation + COT + RM capabilities in a loop actually produces a better model in the next iteration. This is a significant gap: the capabilities are individually demonstrated but their composition for self-improvement — which is arguably the paper's most ambitious claim — remains untested. The paper acknowledges this implicitly in the conclusion: "InternLM-Math integrates COT and augment helper abilities can be used for synthesizing new problems and new responses... We believe such verifiable data augmentation will improve the model's ability at high throughput." The word "believe" signals that this is a hypothesis, not a demonstrated result.

LEAN as verifier is underexplored. The LRM reranking results (Table 19) show promise on GSM8K (85.8 for 7B-LRM vs. 84.0 for 7B-PRM), but LRM performance on MATH is suspiciously absent from Table 19 — only rows for MAJ, ORM, and PRM are shown for MATH. Since the LEAN-to-COT translation verification should be most valuable on harder problems where reasoning errors are more subtle, the omission of MATH-LRM results weakens the case for LEAN as a practical verifier.

On the Code Interpreter Gains

The 16+ point improvement on MATH from adding code interpreter (34.6 → 50.9 for 7B, 37.7 → 54.3 for 20B) is the single largest empirical gain in the paper. However, the experimental setup does not isolate how much of this gain comes from RICO's multi-turn interaction vs. simply having access to a Python interpreter at all. A comparison against a single-turn "generate entire program, execute, output answer" baseline (like PAL) would reveal whether the interleaving specifically matters. The paper argues against this approach conceptually but does not provide a controlled comparison showing RICO outperforming single-turn code generation at the same model size.

Additionally, the iterative data construction process (using GPT-4-Turbo to fill gaps) means the RICO training data is partially GPT-4-distilled. This raises a contamination concern: if GPT-4-Turbo can solve certain MATH training problems with RICO, the model is learning from those solutions and may be reproducing GPT-4's reasoning patterns rather than developing independent RICO capability. The paper does not report what fraction of the final 76K RICO samples came from GPT-4-Turbo vs. the model itself, making it impossible to assess the degree of distillation vs. self-training.

On the Reward Modeling Results

The PRM reranking gains (12.3-12.4 points on MATH) are substantial but leave an enormous gap to oracle (31.8 points for 20B). The paper does not provide diagnostic analyses that would help understand this gap: what types of errors does the PRM make? Does it systematically over-score certain reasoning patterns or under-score others? Does the PRM's accuracy correlate with problem difficulty? Without such analysis, the paper provides a capability (reward modeling) but limited insight into its limitations or how to improve it.

The PRM format detail is also insufficiently specified: the paper states that PRM data is in the format of "Step K: Correct / Incorrect" but does not specify how step boundaries are determined or how the per-step scores are aggregated to select the best solution at inference time. This matters because aggregation method (min, prod, last) is known from prior work (Lightman et al., 2023; Wang et al., 2023b) to significantly affect reranking performance.

On the False Positive Analysis

The manual inspection study (Table 15) is an important and methodologically honest addition, but its small scale (25 problems total, 5 per difficulty level) limits its statistical reliability. With only 5 problems per bin, a single additional false positive at Level 3 would change the rate from 1/5 to 2/5 — the estimate is fragile. A larger-scale study (e.g., 100-200 problems) would be needed to reliably estimate false positive rates across difficulty levels.

That said, the existence of false positives at all — and their concentration at higher difficulty — qualitatively supports the paper's motivation for verification. The case study is particularly valuable because it shows that integer-answer counting problems are especially prone to false positives (the model guesses an integer, there are only so many plausible small integers, and sometimes it guesses right). This is a concrete, actionable insight for benchmark design: problems with small integer answers are more susceptible to outcome-based evaluation inflation.

Missing Baselines and Comparisons

Several comparisons would have strengthened the paper:

1. Single-turn code generation baseline for the RICO results, to isolate the value of multi-turn interleaving.

2. LRM reranking on MATH — its absence from Table 19 is conspicuous given that LRM shows the largest gains on GSM8K.

3. DeepSeek-Math-7B-RL across all benchmarks — as the most prominent concurrent work, a comprehensive head-to-head table would contextualize InternLM2-Math's SOTA claims.

4. PRM aggregation method comparison — no ablation of how per-step scores are combined (min vs. prod vs. last) is reported, despite this being a known design choice in prior work.

5. Pre-training data ablation by source — the paper reports that removing SFT components degrades performance, but never ablates the pre-training data sources (CC-Web vs. AlgebraicStack vs. synthetic data) to establish which contributes most to the base model's math ability.

6. Fine-tuning on only the unified format data vs. on capability-specific data — does the model need to see all formats during the same training run, or would separately fine-tuned LoRA adapters for each capability work equally well? This would test whether the claimed synergy requires shared training or merely shared pre-training.

Genuine Strengths

Despite these limitations, the paper has genuine empirical strengths:

The pre-training data recipe is effective. The jump from InternLM2-Base-7B (8.6 MATH MAJ@1) to InternLM2-Math-Base-7B (21.5) is a 2.5× improvement from continued pre-training alone, establishing that the data composition and processing pipeline (Query of CC retrieval + domain-specific data + synthetic numerical data, with formula-level decontamination) works.

The SFT data mixture is carefully engineered. The calculation hallucination analysis and scratchpad rewriting are concrete, problem-driven improvements rather than generic data scaling. The algorithmic reasoning data with the causal chain-of-thought principle (forward reasoning from established facts) is a thoughtful contribution to SFT data quality.

The multi-task synergy in Table 14 is a real finding. Even if the mechanism is opaque, the empirical fact that full-mixture SFT outperforms any partial mixture is evidence for beneficial interaction among the diverse training signals — a non-obvious result that challenges the assumption that specialization is always preferable.

RICO is more than a format change. The benchmark results (50.9 → 54.3 MATH across 7B to 20B) demonstrate that multi-turn code integration provides genuine capability improvements over chain-of-thought, even if the exact contribution of multi-turn vs. single-turn is not isolated. The gap over prior code-interpreter methods (ToRA, MathCoder) is substantial and goes beyond format preferences.

The false positive analysis is methodologically honest. In a paper that could have simply reported benchmark numbers, the willingness to manually inspect model outputs and report that 20% of "correct" answers have flawed reasoning is a rare and valuable contribution to the literature's understanding of benchmark validity.

6. Limitations and Trade-offs

The Headline SOTA Claims Rest on a Single Benchmark Family and Model Family

The paper's primary evaluation suite — GSM8K, MATH, Hungary math exam, MathBench-ZH — all test mathematical problem-solving with closed-form answers. The formal reasoning evaluation uses MiniF2F (244 test problems) and ProofNet for translation. Every result is produced with models derived from InternLM2-Base. The finding of multi-task synergy (Table 14), the 16-point MATH gain from RICO (Table 9), and the LEAN-as-solver feasibility (Table 8) are all demonstrated on this single model lineage applied to this single task domain.

The consequence is that practitioners cannot infer from this paper whether the core design decisions — continued pre-training from a strong general-purpose base model, unified seq2seq SFT across seven capabilities, iterative RICO data construction — would transfer to other model families (Llama, Mistral, Qwen) or to other reasoning domains (code generation, scientific reasoning, formal verification in Isabelle/Coq). The multi-task synergy observed in Table 14 is particularly vulnerable to this: format interference patterns are known to be sensitive to tokenizer, architecture, and pre-training data distribution. A practitioner fine-tuning Llama-3 on the same SFT mixture might observe entirely different ablation results, with no guidance from this paper about what would generalize and what would not. Similarly, the MiniF2F SOTA claim (30.3 for 7B-Base, Table 4) is evaluated on a benchmark with only 244 problems — a small absolute number where a few lucky proofs can shift the result by 1-2 percentage points, and where the paper's acknowledged lack of decontamination checking against AlgebraicStack adds further uncertainty.

The paper provides no cross-model-family evaluation, no cross-domain evaluation, and no guidance on which data mixture properties are likely to transfer. The authors do not list this as a limitation, which is itself a weakness — a paper making architectural claims about multi-capability unification should at minimum discuss the expected scope of those claims.

The Self-Improvement Loop Is Described but Never Demonstrated

The paper's most ambitious conceptual contribution — perhaps the primary motivation for unifying seven capabilities in a single model — is the vision of a self-improvement loop where the model augments problems, solves them, and verifies solutions without external models or human labeling. The architecture (Figure 2, right) shows two composite pipelines: an upper pipeline (AUG → COT → RM) for data generation, and a lower pipeline (COT → NL Statement → LEAN) for formal verification. Section 4 states that "these abilities can be used to develop the next math LLMs or self-iteration." The conclusion repeats: "InternLM-Math integrates COT and augment helper abilities can be used for synthesizing new problems and new responses. InternLM-Math obtains the abilities of ORM, PRM, and LEAN can be used for verifying the answers and processes of generated responses. We believe such verifiable data augmentation will improve the model's ability at high throughput."

Yet the paper never runs this loop. There is no experiment showing that InternLM-Math-7B, used to generate and verify additional training data, produces an InternLM-Math-7B-v2 that outperforms the original. There is no measurement of the augmentation quality (what fraction of AUG-generated problems are well-formed and solvable?), of the verification false-positive rate when applied to the model's own generated solutions (Section 7.4 measures false positives on MATH test set problems, not on self-generated training data), or of the compounding error risk (if verification is imperfect, does self-training degrade or improve over iterations?).

This is a substantial gap between the paper's stated vision and its empirical content. A practitioner reading the paper to decide whether to invest in building a self-improving math model pipeline gets a detailed description of the architecture but zero evidence that the loop works. The paper acknowledges a related limitation in Section 8: "We do not contain any SFT data to let the model apply self-critique since such data can be hard to generate and verify by any means." But the absence of self-critique data is a different issue from the absence of self-improvement loop results. The loop could in principle be demonstrated using the existing RM and AUG capabilities; the fact that it is not suggests either that preliminary results were not promising, or that the engineering effort to run the loop was beyond the paper's scope. Neither possibility is stated.

The paper does not attempt to mitigate this gap. It treats the self-improvement capability as a design goal that the model is "ready for" rather than a demonstrated result. This is a legitimate position for a model-release paper, but it means the central "platform for self-improvement" framing is aspirational, not empirical.

RICO's Gains Are Partially Unexplained and Potentially Contaminated by GPT-4 Distillation

The 16-point MATH improvement from RICO (34.6 → 50.9 for 7B, 37.7 → 54.3 for 20B; Table 9 vs. Table 5) is the single largest empirical gain reported in the paper. Understanding what produces this gain — and whether it is reproducible without access to GPT-4 — is directly relevant to any practitioner considering adopting RICO. The paper's experimental setup leaves two major questions unanswered.

First, the contribution of multi-turn interleaving vs. simply having access to Python is not isolated. The paper argues that prior approaches (PAL, ToRA, MathCoder) are limited because they either use single-turn code generation or embed code in markdown. But the paper provides no controlled experiment comparing RICO against a single-turn "generate entire program, execute, output answer" baseline using the same model, the same training data volume, and the same Python environment. Without this comparison, a practitioner cannot determine whether the 16-point gain comes from the interleaving protocol specifically (which would justify the engineering complexity of supporting multi-turn tool calling) or from simply training on code-augmented solutions at all (which could be achieved with a simpler single-turn setup). The paper attributes the improvement over InternLM2-Chat (which uses the same code interpreter training data) to "the improvement of math reasoning ability" — but this explains the 7B Math-vs-Chat gap (50.9 vs. 45.1), not the RICO-vs-COT gap.

Second, the iterative data construction process (Section 5) relies on GPT-4-Turbo to generate RICO solutions for training problems that the current model cannot solve. The paper states: "Since the model cannot fully fit the train set, we use GPT-4-turbo to generate responses on the remaining train set once." The fraction of the final 76K RICO samples that originated from GPT-4-Turbo (vs. from the model itself) is never reported. This matters because GPT-4-Turbo's RICO solutions constitute distillation from a substantially stronger, closed-source model. A practitioner who does not have access to GPT-4 (or an equivalently strong model) may not be able to replicate the RICO training pipeline. More importantly, if a large fraction of the MATH training set was solved by GPT-4-Turbo, the RICO model's strong MATH performance may partially reflect memorization or mimicry of GPT-4's reasoning patterns on problems that overlap in structure with the MATH test set, rather than genuine RICO reasoning capability.

The paper does not perform an ablation where only self-generated (not GPT-4-generated) RICO solutions are used after the first iteration. It also does not report whether performance degrades when the iterative process is run without GPT-4 gap-filling (e.g., using only the model's own correct solutions, which would naturally produce fewer training samples but avoid distillation). This leaves the RICO results in an ambiguous state: they demonstrate that multi-turn code integration can be powerful, but do not establish whether the demonstrated performance level is achievable without access to a stronger teacher model.

The 20% False Positive Rate on MATH Undermines Outcome-Based Evaluation, and the Proposed Fix (Verification) Is Not Yet Shown to Close the Gap

Section 7.4 documents that among 25 MATH test problems where InternLM2-Math-20B produces the correct final answer, 5 (20%) contain incorrect reasoning — the model got the right answer through flawed logic or coincidence. This rate increases with difficulty: at Level 5, only 3 of 5 "correct" answers have correct processes. The paper correctly identifies this as a fundamental threat to the validity of outcome-based benchmarks and frames LEAN-based verification as the path forward.

The problem is that the paper's own verification mechanisms are not shown to be sufficiently reliable to catch these errors. Table 19 shows that on MATH with the 20B model, the PRM@100 achieves 50.0 accuracy while the oracle@100 (perfect selection from the candidate pool) is 81.8 — a 31.8-point gap. This means that even the model's best verifier is selecting incorrect solutions as "best" a substantial fraction of the time. The PRM's false-positive rate on process verification — the rate at which it marks an incorrect step as correct — is never reported. Without this number, a practitioner cannot estimate whether using the PRM as a filter in a self-improvement loop would amplify errors (by incorrectly certifying wrong reasoning) or reduce them.

The paper acknowledges this gap implicitly, noting in the limitations that "we find that our model does not have a significant PRM performance which may be due to the confusing format among PRM and SFT," but does not quantify what "not significant" means in terms of false-positive/false-negative rates. The LEAN-based verification (LRM) offers a path toward formal guarantees — LEAN code that compiles and produces matching results provides ironclad verification of the calculational steps — but LRM results are reported only for GSM8K (Table 19), not for MATH. Since the false positive problem is most acute on harder problems (Level 5: 40% false positive rate), and MATH contains substantially harder problems than GSM8K, the absence of MATH LRM results leaves a critical gap: we do not know whether LEAN verification would catch the counting-problem false positive shown in the case study or would itself be limited by the translation step's accuracy.

The paper's position that outcome-based evaluation is "unilateral" and that verification is the solution is well-argued. But the empirical support for the solution is incomplete: the verifier is too weak to close the gap to oracle selection, and the formal verification path is too sparsely evaluated to be relied upon. A practitioner deploying this model for self-improvement could not be confident that the verification step would prevent error amplification.

Format Interference from Multi-Capability Training Is Demonstrated but Its Mechanism Remains Opaque, Leaving No Guidance for Practitioners

The SFT data composition ablation (Table 14) reveals a striking pattern: adding any single non-COT component (RM, Formal, CI, Augmenter) to MetaMath degrades MATH performance compared to MetaMath-only — sometimes substantially (RM causes a 3.94-point drop). Yet the full mixture containing all components outperforms MetaMath-only (34.60 vs. 33.78). The paper interprets this as evidence of multi-task synergy, but the interpretation does not come with diagnostic analysis that would help a practitioner design their own SFT mixture.

Several specific questions are unaddressed:

• Is the degradation from single-component addition caused by format confusion (the model occasionally producing RM-format outputs when prompted for COT) or by capacity dilution (the model's finite representational capacity being partially allocated to non-COT tasks)? The former could be addressed by stronger format prompting; the latter would require larger models or separate adapters. The paper provides no analysis of whether the degraded models produce more format errors or simply worse reasoning.

• What is the minimum viable mixture? The full SFT mixture uses 2.26M samples across seven categories. Could the synergy be achieved with a sparser combination — say, COT + RM + CI, omitting Formal and Augmenter — or does every component contribute to the final gain? The single-component removal (Table 14 bottom rows) shows that removing one component at a time hurts, but does not test whether removing multiple components simultaneously is equally harmful or more harmful. A practitioner with limited compute for SFT data construction needs to know which components are essential vs. nice-to-have.

• Does the synergy persist at different model scales? Table 14 is reported only for the 7B model. The 20B model might show less format interference (larger capacity reducing competition) or equal interference (the format confusion being a fundamental property of the training data, not a capacity issue). Without the 20B ablation, scaling expectations are pure speculation.

• Is the synergy a property of simultaneous training, or would sequential training (COT first, then RM, then CI, etc.) work equally well? The paper's self-improvement framing suggests that capabilities are built sequentially (the model generates, then verifies), but SFT trains on all capabilities simultaneously. The discrepancy between the training procedure and the intended usage pattern is unexamined.

The paper treats the SFT mixture as a fixed recipe and does not attempt to optimize it or explain its failure modes. For a paper whose central architectural claim is that multi-capability unification is valuable, this is a notable analytical gap. A practitioner who observes format interference in their own multi-capability training (which is a known challenge in instruction tuning) gets no diagnostic methodology or mitigation strategies from this work.

LEAN 3 as the Formal Backend Creates a Correctness Ceiling That the Paper Documents but Does Not Resolve

The formal reasoning component of InternLM2-Math is built on LEAN 3, a version of the proof assistant that is no longer the active development target (LEAN 4 has superseded it). The paper is transparent about this: "We use LEAN 3 as our SFT data since GPT-4 can only generate LEAN 3 codes for GSM8K (even if you require it to apply LEAN 4). Furthermore, we find the data of translating between formal and informal from MathLib is preprocessed in LEAN 3." The limitation section promises migration to LEAN 4 in future work.

The immediate consequence is a correctness ceiling on LEAN-as-solver: Table 8 shows that LEAN 3 solving of GSM8K underperforms COT by 7.7 points (7B) and 8.7 points (20B). The paper attributes this to LEAN 3's natural number arithmetic: subtraction of a larger ℕ from a smaller one yields 0 (truncated subtraction), and division of ℕ values yields floor division. These semantics are mathematically correct for ℕ in constructive type theory but semantically wrong for grade-school word problems that assume standard integer/rational arithmetic. A GSM8K problem like "John had 5 apples and gave away 7. How many does he have?" is ill-defined in ℕ arithmetic — the answer is not 0 (LEAN 3's truncation) but a negative number or "impossible."

This means that some fraction of the 70.4% accuracy achieved by LEAN solving is fundamentally unachievable in LEAN 3 — problems requiring negative intermediate values, exact rational arithmetic, or non-floor division will fail regardless of how well the model translates the problem into LEAN. The paper does not estimate what fraction of GSM8K problems fall into this category, so a practitioner cannot determine whether the 70.4% represents near-ceiling performance for LEAN 3 or leaves substantial room for improvement through better LEAN generation.

For the LRM (LEAN Reward Model) verification pipeline, the LEAN 3 limitations mean that translating COT reasoning into LEAN code for verification may produce false negatives: a COT solution that is mathematically correct but uses arithmetic that LEAN 3's ℕ semantics cannot faithfully represent will fail to verify. This could explain the paper's omission of MATH LRM results — MATH problems use a wider range of mathematical operations (rational numbers, real numbers, algebraic manipulation) than GSM8K, making LEAN 3 translation substantially harder. The promise of using LEAN as a "unified interface for solving and proving" is undermined when the interface's type system does not match the mathematical domain of the problems being solved.

The paper acknowledges the LEAN 3/4 issue as a practical constraint but does not treat it as a fundamental limitation of the formal verification approach. Migrating to LEAN 4 and using rational number types (ℚ) or real number types (ℝ) would resolve the arithmetic semantics issue, but the paper provides no estimate of how much performance improvement this migration would unlock, nor whether GPT-4 (or the model itself) can generate correct LEAN 4 code for math word problems at scale. A practitioner deciding whether to invest in LEAN-based verification for their math LLM pipeline needs to know whether the current LEAN 3 results represent a lower bound (with LEAN 4 being strictly better) or a fundamentally different capability profile (where LEAN 4's different libraries and syntax create new failure modes). The paper leaves this question entirely open.

7. Implications and Future Directions

How This Work Changes the Landscape

This paper shifts the conversation around math LLMs from point-solution engineering toward multi-capability platform design. Before InternLM-Math, the dominant approach was to train separate specialist models for each function: one model for chain-of-thought solving (MetaMath, MammoTH), another for verification (Math-Shepherd, separate PRMs), another for formal proving (Llemma, ReProver), and another for code-augmented reasoning (ToRA, MathCoder). Each capability lived in its own model checkpoint, with its own training recipe, its own SFT data, and its own inference pipeline. InternLM-Math demonstrates that these capabilities can coexist in a single model trained on a single SFT mixture, using a unified seq2seq format — and that the resulting model achieves competitive or SOTA performance across all of these tasks simultaneously.

The magnitude of this shift is more than incremental but not yet paradigm-changing. The multi-capability unification is a genuine methodological contribution: the data ablation (Table 14) showing that individual non-COT components hurt performance when added to MetaMath, while the full mixture recovers and improves upon the baseline, provides hard-to-ignore evidence that there is real multi-task synergy — not just the sum of independent capabilities. This challenges the assumption that specialization is always preferable and opens the door to research on which capabilities benefit from co-training and why. However, the shift is not yet paradigm-changing because the paper does not demonstrate the self-improvement loop that the platform is designed to enable. The capabilities are individually demonstrated, but their composition — the model generating problems, solving them, and verifying solutions in an iterative cycle that produces a measurably stronger model — remains aspirational. The paper provides the architecture and the justification, but not the empirical proof of the loop's efficacy.

The paper also resolves a latent tension in the verification literature. Prior work on process reward models (Lightman et al., 2023; Wang et al., 2023b) demonstrated that PRMs significantly improve answer selection over majority voting and ORMs, but required separate verifier models — effectively doubling the parameter count for deployment. This created a practical barrier: the improved accuracy came at the cost of hosting a second large model, which could instead be used to simply sample more solutions from the solver. InternLM2-Math shows that a single model can achieve PRM@100 = 50.0 on MATH (Table 6, 20B model) — competitive with MetaMath-DeepSeek-67B's PRM@256 = 48.1 — using the same weights for both generation and verification. This reframes the verifier question from "should we train a separate verifier?" to "how do we train a solver that also verifies?" — a more integrated and practically appealing framing.

The paper's documentation of the false positive problem (Section 7.4, Table 15) — that 20% of "correct" MATH answers have flawed reasoning, rising to 40% at the hardest difficulty level — provides concrete evidence for something the community has long suspected but rarely quantified. This shifts the evaluation conversation from outcome accuracy alone (which the paper shows is inflated) to process correctness, making the case that verifiers and formal proof checkers are not optional add-ons but necessary components of trustworthy math reasoning systems. The finding is specific (MATH, InternLM2-Math-20B, 5 samples per difficulty level) but its implications are general: any paper reporting MATH accuracy without a process-level audit is potentially overstating its model's reasoning ability.

Several research directions become more attractive in light of this work:

• Integrated solver-verifier training is now empirically demonstrated to work at the 7B-20B scale, making it a viable baseline for future math LLMs rather than an exotic design choice. Researchers building math models should now justify why they would keep the solver and verifier separate, rather than assuming separation is necessary.

• Formal reasoning as a verification backend gains credibility from the LRM results (GSM8K LRM@100 = 85.8 for 7B, Table 19), even though the results are limited to GSM8K and LEAN 3. The feasibility of translating COT reasoning to LEAN code for automatic verification is established, and the remaining challenge (migrating to LEAN 4 with richer types, scaling to harder problems) is more clearly scoped.

• Data mixture design for multi-capability models becomes a first-class research problem. The format interference documented in Table 14 (single non-COT components degrading performance) and the recovery with the full mixture suggest that mixture design is not simply additive — there are nonlinear interactions among training signals that need to be understood and optimized, analogous to how multi-task learning in computer vision requires careful task weighting and curriculum design.

Conversely, some directions become less attractive:

• Training ever-larger specialist math solvers (focusing exclusively on COT accuracy without verification capabilities) may face diminishing returns in credibility if the false positive problem documented in Section 7.4 generalizes. If 20-40% of correct answers have flawed reasoning, then pushing COT accuracy from 35% to 40% without improving process correctness may simply generate more convincing-looking wrong answers. The paper makes a strong implicit case that future math LLM development should be measured by both outcome accuracy and process correctness, and models that only optimize the former are incomplete.

• Human-labeled PRM data (as in Lightman et al., 2023) becomes harder to justify for open-source efforts, given that InternLM2-Math achieves competitive PRM performance using the Math-Shepherd automatic labeling approach (Table 6, 20B-PRM matching 67B-PRM with fewer samples). The cost-benefit tradeoff of human PRM labeling now needs to be compared against simply scaling up automatic labeling with your own model's outputs.

Follow-Up Research This Work Enables

Measuring and improving PRM false-positive rates on process verification. The paper documents that the PRM leaves a 31.8-point gap to oracle on MATH (Table 19, 20B model: PRM@100 = 50.0 vs. Oracle@100 = 81.8) but never reports the PRM's step-level false-positive rate — how often it marks an incorrect reasoning step as correct. A concrete follow-up would: (1) construct a diagnostic dataset of 200-500 MATH solutions with human-annotated step-level correctness labels (extending the 25-sample study in Section 7.4), (2) evaluate InternLM2-Math's PRM on this dataset to measure false-positive and false-negative rates by step type (arithmetic errors, logical leaps, incorrect assumptions), and (3) test whether targeted data augmentation — adding more negative PRM examples for the specific error types where the PRM is weakest — reduces the false-positive rate and narrows the oracle gap. This would directly address the paper's self-acknowledged limitation that "we do not have a significant PRM performance which may be due to the confusing format among PRM and SFT and the unbalanced distribution between positive processes and negative processes."

Demonstrating (or failing to demonstrate) the self-improvement loop. The paper's most ambitious unsubstantiated claim is that the unified model enables "verifiable data augmentation" for self-improvement. A direct follow-up would implement the Figure 2 upper-right pipeline end-to-end: (1) take InternLM2-Math-20B and use its AUG capability to generate 50K harder variants of MATH training problems, (2) use its COT capability to solve the variants, (3) use its PRM capability to filter solutions where all steps are marked correct, (4) add the verified (variant, solution) pairs to the SFT data, (5) fine-tune InternLM2-Math-20B on the expanded dataset to produce a v2 model, and (6) evaluate v2 on MATH, GSM8K, and Hungary exam. The key measurements would be: what fraction of AUG-generated variants are well-formed? What fraction of PRM-filtered solutions are actually correct (measured by ground-truth answer checking)? Does v2 outperform v1, and by how much? A negative result — v2 performing no better, or worse, than v1 — would be equally valuable, revealing whether the PRM's verification false-positive rate is too high for safe self-training. This experiment uses only the model's own capabilities with no external models, directly testing the paper's core vision.

Isolating the contribution of multi-turn interleaving in RICO. The 16-point MATH gain from RICO (Table 9: 34.6 COT → 50.9 RICO for 7B) is the paper's largest empirical effect, but it conflates two factors: access to a Python interpreter at all, and the multi-turn interleaving protocol. A clean ablation would train three variants of InternLM2-Math-7B using the same total volume of code-augmented SFT data (76K samples): (A) single-turn code generation (one program, execute, output answer, analogous to PAL), (B) two-turn RICO (reasoning, code, execution, reasoning, final answer), and (C) unrestricted multi-turn RICO (the paper's approach). If A achieves comparable MATH accuracy to C, then the interleaving design is unnecessary complexity — a single program-execute-answer pipeline would be simpler and likely more deployable. If A substantially underperforms C, the experiment would quantify the specific value of multi-turn interaction and provide design guidance for tool-augmented reasoning models. The paper's iterative data construction using GPT-4-Turbo gap-filling should also be ablated: train variants using only self-generated RICO solutions (no GPT-4 distillation) and measure the performance drop, quantifying how much of the RICO gain depends on teacher distillation.

Cross-model-family replication of multi-task synergy. The Table 14 ablation — where adding single non-COT components degrades performance but the full mixture recovers — is the paper's strongest evidence for multi-task synergy. This result was produced on InternLM2-Base-7B. A replication on Llama-3-8B and Mistral-7B-v0.3 using the same SFT data mixture would test whether the synergy is specific to InternLM2's architecture and pre-training distribution or is a general property of multi-capability training. The experiment would be: for each base model, fine-tune on MetaMath-only, MetaMath+RM, MetaMath+CI, MetaMath+Formal, and the full mixture, measuring MATH and GSM8K accuracy for each variant. If the same "U-shaped" pattern (individual additions hurt, full mixture helps) appears across model families, the finding becomes a general principle of math LLM training rather than a quirk of InternLM2. If the pattern disappears or reverses on other architectures, the paper's claims about multi-capability unification would need to be qualified as model-specific.

LEAN 4 migration and MATH verification. The paper's formal reasoning component is built on LEAN 3, which the authors acknowledge is a practical constraint that creates a correctness ceiling due to ℕ arithmetic semantics (Table 8: LEAN solving underperforms COT by 7.7-8.7 points). A natural follow-up would: (1) use GPT-4 or a stronger model to generate LEAN 4 solutions for the GSM8K and MATH training sets (targeting ℚ or ℝ types where appropriate to avoid the ℕ truncation problems), (2) fine-tune InternLM2-Math on these LEAN 4 solutions following the same multi-task SFT recipe, (3) measure LEAN-solving accuracy on GSM8K to determine how much of the 7.7-point COT-LEAN gap closes with better type semantics, and (4) measure LRM reranking performance on MATH (which the paper omits from Table 19) to evaluate whether LEAN 4 verification can improve answer selection on harder problems where reasoning errors are more consequential. This would directly address whether the LEAN-as-unified-interface vision is practically achievable or fundamentally limited by the difficulty of automated translation between informal reasoning and formal proofs.

Process-level evaluation benchmarks for math LLMs. Section 7.4 exposes a measurement problem: outcome accuracy on MATH overstates reasoning quality by 20-40% depending on difficulty. This finding, while based on a small sample (25 problems), suggests that the field needs benchmarks that evaluate reasoning correctness, not just answer correctness. A concrete follow-up would construct a process-evaluation dataset: take 500 MATH problems (the test set or an independent set), generate solutions from several open-source math LLMs (InternLM2-Math, DeepSeek-Math, Llemma, MetaMath variants), and have human experts annotate each step of each solution as correct/incorrect. This dataset would enable: (1) measuring the correlation between outcome accuracy and process accuracy across models (does a higher MATH score reliably mean better reasoning?), (2) benchmarking PRM performance across models on a standardized step-level evaluation, and (3) identifying which types of reasoning errors (arithmetic, algebraic, logical, misinterpretation) are most common and which are most likely to produce coincidentally correct answers. The paper's existing false positive case study provides a template and a justification; scaling it up to a community benchmark would make process evaluation a first-class metric alongside outcome accuracy.

Practical Applications and Downstream Use Cases

Cost-efficient answer reranking without a separate verifier model. The paper demonstrates that InternLM2-Math-20B's built-in PRM achieves 50.0 on MATH with only 100 samples (Table 6), matching MetaMath-DeepSeek-67B's PRM@256 = 48.1 while using a ~3× smaller model and 2.56× fewer samples. For a production math-solving service, this means: deploy a single InternLM2-Math-20B instance, sample 100 solutions per problem, use the same model in PRM mode to score and select the best solution, and achieve ~50% MATH accuracy — without the infrastructure complexity or GPU memory cost of hosting a separate verifier. The practical implication is that verifier-guided selection becomes more accessible: rather than requiring double the serving capacity (one model for generation, one for scoring), a single model serves both roles, roughly halving the deployment cost of verifier-augmented inference. The 12-13 point improvement over greedy decoding (37.7 → 50.0) is large enough to matter in applications where accuracy is worth the additional inference cost.

Automated training data quality control for math fine-tuning. The paper's PRM and ORM capabilities, combined with the AUG helper, provide a pipeline for generating high-quality math training data without human labeling. Concretely: a curriculum developer or math education platform can use InternLM2-Math to (1) generate variants of existing problems via the AUG capability, (2) solve the variants via COT or RICO, and (3) filter solutions using the PRM, keeping only those where every step is verified correct. This produces verified (problem, solution) pairs that can be used to fine-tune smaller or domain-specific models. The cost savings over human data creation are potentially large — generating and verifying 100K math problems using the model's own capabilities costs only inference compute, versus the hundreds of person-hours required for human problem authoring and solution checking. The key unknown (which follow-up research would need to establish) is the PRM's false-positive rate on self-generated data: if the PRM certifies incorrect solutions, the training data quality degrades. But the paper's PRM performance on MATH (50.0 vs. oracle 81.8) suggests that even imperfect verification can substantially enrich a training set compared to no filtering.

Formal verification of informal math competition solutions. The LEAN translation and LRM capabilities (Table 19: 7B-LRM achieves 85.8 on GSM8K) point toward a practical application in math competition settings: a student or contest organizer submits an informal solution to a problem, InternLM2-Math translates the solution's calculational steps to LEAN code, and the LEAN proof assistant verifies that each step's arithmetic is correct. This provides automated partial verification — it doesn't prove the logical reasoning is valid, but it catches arithmetic errors in multi-step calculations, which are a common source of incorrect answers in competition math. The 85.8% LRM accuracy on GSM8K suggests that for grade-school arithmetic problems, this pipeline is already reasonably reliable. The practical benefit is a scalable first-pass check that reduces the burden on human graders or catches errors before a solution is submitted. The limitation (LEAN 3 ℕ semantics, no MATH results) means the current version is restricted to problems using natural-number arithmetic, but the architecture and training recipe provide a template that can be extended to LEAN 4 and richer mathematical domains.

Integrated math assistant with self-verification for interactive learning. The multi-capability design means InternLM2-Math can serve as a complete math tutoring backend in a single deployment: (1) a student asks a question (the [Problem]), (2) the model generates a step-by-step solution ([COT]), (3) the model checks its own solution using PRM or ORM ([PRM]), and optionally (4) the model generates a harder follow-up problem for additional practice ([AUG]). The advantage over assembling this pipeline from separate models (e.g., Llama for generation, Math-Shepherd for verification, GPT-4 for augmentation) is consistency: the same model's internal representations of "correct reasoning" inform both its generation and its verification, reducing the risk that the verifier rejects solutions that are actually correct but in a style the verifier hasn't seen. The paper's results on specialty tasks (Game of 24: 35% single-sample accuracy; prime checking: near-perfect across 2-10 digits, Table 10-11) further suggest that the model can handle structured algorithmic reasoning beyond standard word problems, making it suitable for interactive math platforms that go beyond Q&A.