PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Huaiyuan Ying, Shuo Zhang, Linyang Li, Zhejian Zhou, Yunfan Shao, Zhaoye Fei, Yichuan Ma, Jiawei Hong, Kuikun Liu, Ziyi Wang, Yudong Wang, Zijian Wu, Shuaibin Li, Fengzhe Zhou, Hongwei Liu, Songyang Zhang, Wenwei Zhang, Hang Yan, Xipeng Qiu, Jiayu Wang, Kai Chen, Dahua Lin

arXiv:2402.06332v2cs.CL

TL;DR

InternLM-Math treats mathematical reasoning as an expression of LLMs’ abstract reasoning ability and builds on InternLM2-Base through continued pre-training and supervised fine-tuning. It combines problem solving with verification and other math-model development tasks, and reports open-source state-of-the-art performance across multiple settings and benchmarks.

  • Problem

    Math reasoning is presented as a measure of LLMs’ abstract reasoning, and building math-capable models requires pre-training on math corpora and supervised fine-tuning on math problems.

    Source: §1 · p. 1

  • Method

    InternLM-Math continues pre-training from InternLM2-Base and unifies chain-of-thought, reward modeling, formal reasoning, augmentation, and code interpretation in its training.

    Source: §1 · pp. 1–2

  • Results

    InternLM-Math reports open-source state-of-the-art performance under in-context learning, supervised fine-tuning, reward-model reranking, and Python-assisted reasoning across multiple benchmarks.

    Source: §1 · p. 2

  • Takeaways & Limitations

    The authors present InternLM-Math as a starting point for self-improvement through synthesizing problems and responses and verifying generated answers and processes.

    Source: §8 · p. 16

    Chain-of-thought equation rewriting is difficult to match comprehensively, repeated equals signs encourage repetition, and naive step-by-step calculations may annoy users.

    Source: Limitations · p. 16

Abstract

from arXiv · show

The math abilities of large language models can represent their abstract reasoning ability. In this paper, we introduce and open-source our math reasoning LLMs InternLM-Math which is continue pre-trained from InternLM2. 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. InternLM-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 including GSM8K, MATH, Hungary math exam, MathBench-ZH, and MiniF2F. Our pre-trained model achieves 30.3 on the MiniF2F test set without fine-tuning. We further explore how to use LEAN to solve math problems and study its performance under the setting of multi-task learning which shows the possibility of using LEAN as a unified platform for solving and proving in math. Our models, codes, and data are released at \url{https://github.com/InternLM/InternLM-Math}.

1 Introduction

InternLM-Math continues pre-training from InternLM2-Base and is presented as an open-source math reasoner with strong informal and formal benchmark performance. Its training and model design combine problem solving with verification and other math-LLM development abilities.

1 Introduction

  • The authors continue pre-training InternLM2-Base on collected math-related data to build InternLM-Math.The paper identifies math-corpus pre-training and math-problem supervised fine-tuning as requirements for building such models.Source: §1 · p. 1
  • InternLM-Math outperforms Minerva and Llemma on informal and formal math reasoning benchmarks.Figure 1 compares pre-trained base-model performance on 4-shot MATH with 256-vote majority sampling.Source: §1 · p. 2, Figure 1 · p. 2
  • Supervised fine-tuning covers chain-of-thought and code-interpreter problem solving alongside reward modeling and an augmentation helper.The authors describe these tasks as abilities for developing math LLMs.Source: §1 · p. 2
  • InternLM-Math unifies chain-of-thought reasoning, reward modeling, data augmentation, and formal reasoning in a seq2seq format.The model is supervised for problem solving and verification, and the authors also report reasoning interleaved with Python coding and exploration of LEAN.Source: §1 · p. 2

2 Related Work

Related work spans math pre-training, fine-tuning, verification, code interpretation, and formal proving. InternLM-Math combines several of these capabilities in one model and explores interleaved coding and LEAN-based reasoning.

Math Pre-training

  • Math pre-training draws on corpora, problem sets, and synthetic data; InternLM-Math collects math corpora and synthetic data for pre-training.Prior sources include arXiv, Common Crawl math pages, GSM8K and MATH problems, and rule- or script-generated problems.Source: §2 · pp. 2–3

Math Fine-tuning

  • Prior fine-tuning work augments problems or reasoning paths and uses reinforcement learning with reward models; InternLM-Math integrates verification, proof, code interpretation, and augmentation.The paper also describes building a stronger chain-of-thought SFT dataset.Source: §2 · p. 3

Math Verifier

  • InternLM-Math combines problem solving and verification in one seq2seq model, whereas prior approaches trained separate policy and reward networks.ORM verifies answers, while PRM verifies reasoning processes; the paper also explores translating reasoning paths into LEAN for verification.Source: §2 · p. 3

Math Code Interpreter

  • RICO interleaves reasoning and coding over multiple rounds until a problem is solved, unlike approaches based on one-time code execution.The authors describe this as a way to integrate code interpretation with reasoning.Source: §2 · p. 3

Math Prover

  • Formal theorem proving can assure process correctness, but sparse training data makes it difficult; InternLM-Math reports strong few-shot MiniF2F performance.The paper presents that performance as evidence of potential for building a strong math prover.Source: §2 · p. 3

3 Pre-training

InternLM-Math continues pre-training on collected math data, with data selection, deduplication, and decontamination steps. The paper also describes the training schedule and illustrates SFT formats and possible model uses.

3.1 Pretrain data composition

  • The pre-training collection includes 20B tokens of retrieved math-related data, 11B tokens of domain-specific data, and 0.2B tokens of synthetic numerical-operation data.The authors say they do not use LLM-generated data during pre-training.Source: §3.1 · p. 4

3.2 Data post-processing

  • Data post-processing uses a scoring model to identify high-quality datasets, Minhash-LSH deduplication above a 0.7 similarity threshold, and exact-formulation decontamination against MATH test items.For decontamination, formulations are extracted from paragraphs and matching paragraphs are removed.Source: §3.2 · p. 4

3.3 Training strategy

  • The authors collected 31.2 billion high-quality tokens and trained for 125 billion tokens overall, using four epochs for most datasets and early-stopping the 20B model at 80 billion tokens.Training uses a 4096-token context and a cosine learning-rate schedule after 2000 warm-up steps.Source: §3.3 · pp. 4–5
  • Figure 2 presents SFT query-response formats and two uses: synthesizing problems with augmentation, CoT, and reward modeling, and solving informal problems through formal languages.The latter pipeline uses CoT and formal-reasoning abilities.Source: Figure 2 · p. 5

4 Supervised Fine-tuning

Supervised fine-tuning trains InternLM-Math for problem solving and self-improvement tasks, including chain-of-thought reasoning, reward modeling, augmentation, and LEAN-based formal reasoning. The section describes calculation-focused reasoning changes and a stepwise rule for generating fundamental math abilities.

4 Supervised Fine-tuning

  • The SFT data combines human-written, rule-generated, and LLM-generated examples to train math solving and self-improvement abilities.The target abilities include problem augmentation, reward modeling, self-verification, formal reasoning, and code interpretation.Source: §4 · p. 5

Chain-of-thought

  • For chain-of-thought, the authors use MetaMath for English and in-house Chinese data, and filter augmented reasoning paths with final answers and a trained PRM.Reasoning-path augmentation is applied to selected datasets to address model weaknesses.Source: §4 · p. 5
  • To address calculation hallucination, the authors rewrite equations into intermediate steps within chain-of-thought reasoning.They report that this improves calculation ability during chain-of-thought reasoning.Source: §4 · pp. 5–6

Fundamental math abilities

  • Synthetic training examples cover prime checking, the game of 24, integer factoring, and triangle areas, with each next step determined only by generated tokens.For triangle areas, the model first checks whether the sides form a triangle and whether it is right-angled.Source: §4 · p. 6

Reward Modeling

  • The reward model unifies ORM and PRM in one seq2seq format and adds Chinese ORM data from self-sampled reasoning and corresponding answers.Reward modeling supports reranking generations and filtering synthesis data for self-improvement.Source: §4 · p. 6

Formal Math Reasoning

  • LEAN training assigns solver, verifier, and prover roles, including translating between chain-of-thought and LEAN to check calculations and generating tactics from LEAN states.The solver and verifier data are derived from 6,705 correct LEAN solutions to GSM8K training problems; MathLib-train supplies prover data.Source: §4 · p. 6

Augmentation helper

  • The augmentation helper rephrases or augments questions to increase question diversity and supports constructing synthesized data for self-improvement.The section also links natural-language statements to the use of formal math language for proving.Source: §4 · p. 6

5 Code Interpreter

RICO integrates code execution into ordinary chat-style reasoning through a general tool-calling protocol, supporting iterative reasoning and coding rather than one-shot code generation. The training data is updated iteratively with hard-example mining to reduce reliance on GPT-4.

5 Code Interpreter

  • Earlier program-of-thought approaches could not see execution results, while later one-shot code-execution approaches were less suited to multi-step reasoning and calculation.RICO is presented as addressing these limitations through repeated reasoning and execution rounds.Source: §5 · pp. 6–7
  • RICO lets the model alternate symbolic reasoning, program generation, and observation of execution results until it can answer the problem.It uses chat-response formatting and a general tool-calling protocol, avoiding ambiguity from embedding code in Markdown blocks.Source: §5 · p. 7
  • Training data uses iterative updates and hard-example mining: the previous model generates responses, and GPT-4-turbo fills remaining training examples.Correct responses from both sources train the next model; the initial data comes from ToRA-70B and is converted to the required format.Source: §5 · pp. 7–8

6 Experiments

Experiments assess InternLM-Math across informal and formal reasoning, reward-model reranking, code-assisted solving, and additional math abilities. Results include strong benchmark performance, alongside specific limitations in scaling and LEAN-based calculation.

6.1 Pre-train Performance

  • In-context learning results show continued pre-training improves both benchmarks over the initial checkpoints; InternLM2-Math-Base-7B scores 21.5 on MATH versus Llemma-7B's 18.0.The 20B base model scores 27.3 on MATH, outperforming Llemma-34B and performing similarly to Minerva-62B; after shared MetaMath fine-tuning, the 7B model retains an advantage over Mistral-7B and Llemma-7B on MATH.Source: Table 2 · p. 8, §6.1 · p. 8, Table 3 · p. 9

6.2.3 Formal Ability

  • On MiniF2F, InternLM2-Math-7B-Base solves 74 of 244 problems (30.3) and sets a new state of the art, while both base models find new proofs.The 7B and 20B models find 25 and 24 proofs, respectively, absent from the official repository; formal translation beats ProofGPT but trails CodeX and GPT-4, and LEAN solving reaches 70.4 on GSM8K for 7B and 73.9 for 20B, below chain-of-thought.Source: §6.1 · p. 8, Table 4 · p. 9, Table 7 · p. 11

6.2.1 COT Reasoning

  • 78.1 on GSM8K, 34.6 on MATH, 55 on the Hungary math exam, and 40 on MathBench-ZH for InternLM2-Math-7B in zero-shot chain-of-thought evaluation.The authors report stronger in-domain and out-of-domain performance at the same model size; InternLM2-Math-20B scores 37.7 on MATH and 66 on the Hungary exam, behind only GPT-4 and at smaller size than Qwen-72B and DeepSeek-67B.Source: §6.2.1 · pp. 9–10, Table 5 · p. 10

6.2.2 Reward Modeling

  • Reward reranking generally performs best with PRM, then ORM, then majority voting; LEAN reward modeling helps on GSM8K with 7B models, but its advantage diminishes at 20B.The 20B reward model reaches 50.0 accuracy on MATH(500), outperforming MetaMath-DeepSeek-67B reranking with fewer inference times, while remaining well behind GPT-4-MathMix; a gap remains to oracle performance.Source: §6.2.2 · p. 10, Table 6 · p. 10, Figure 4 · p. 11

6.2.3 Formal Ability

  • On GSM8K, LEAN-based solving scores 70.4 for 7B and 73.9 for 20B, below chain-of-thought; the authors identify natural-number subtraction and division conventions as calculation obstacles.They present this exploration as showing the possibility of using LEAN as a unified interface for solving and proving math problems.Source: Table 8 · p. 12, §6.2.3 · p. 12

6.2.4 Code Interpreter

  • With Python code interpreters, InternLM2-Math-7B surpasses previous open-source models on MATH except InternLM2-Chat-20B, and the 20B model achieves the best open-source result.The authors attribute the gains over InternLM2-Chat to improved math reasoning, since both use the same code-interpreter training data.Source: §6.2.4 · p. 12, Table 9 · p. 13

6.2.5 Other abilities

  • In Game of 24, single-sample accuracies are 26 for 7B and 35 for 20B, exceeding fine-tuned Llama2-7B and GPT-4; prime checking is nearly correct across tested digit lengths.The prime-checker test used 20 numbers per digit length from 2 to 10, split evenly between prime and composite numbers.Source: §6.2.5 · p. 12, Table 10 · p. 13

7 Discussion

The discussion finds diminishing returns from longer pretraining, a benefit from combining MetaMath with sparse LEAN data, and gains from the comprehensive SFT mixture. It also warns that outcome-only accuracy can count flawed reasoning as correct.

7.1 Compare Pretrain Performance with Pretraining Token Amount

  • After 80B tokens, performance did not improve significantly; training to 200B tokens (about seven epochs) began to degrade.Source: §7.1 · p. 13

7.2 LEAN Performance on GSM8K

  • LEAN on GSM8K performed worse with GSM8K-LEAN alone than with GSM8K-LEAN plus MetaMath; MetaMath also reduced sensitivity to SFT data amount.Source: §7.2 · p. 13

7.3 Data Ablation Study in SFT

  • The comprehensive SFT mixture outperformed MetaMath + CoT, while other compositions undermined results on almost all test datasets.Source: §7.3 · p. 14

7.4 False positive in MATH BenchMark

  • Outcome-only MATH accuracy can count flawed reasoning as correct, with such false positives appearing more often at higher difficulty.The authors manually checked 25 correct-answer samples, five from each difficulty level.Source: §7.4 · pp. 14–15

8 Conclusions

The authors present InternLM-Math as an initial step toward verifiable mathematical reasoning, combining generation and verification capabilities as a basis for self-improvement.

  • InternLM-Math is presented as a first step toward verifiable mathematical reasoning and as a starting point for self-improving models.Source: §8 · p. 16
  • Its chain-of-thought and augmentation abilities can synthesize new problems and responses.Source: §8 · p. 16
  • Its ORM, PRM, and LEAN abilities can verify generated answers and processes.Source: §8 · p. 16

Limitations

The authors identify limitations in scratchpad-style reasoning, self-critique and PRM training, language balance, LEAN version, possible data contamination, and prompt sensitivity.

Limitations

  • Scratchpad-style rewriting can require awkward equation matching, induce repeated equals signs, and produce user-annoying stepwise calculations.Source: Limitations · p. 16
  • The SFT data contains no self-critique examples because such data is difficult to generate and verify.Source: Limitations · p. 16
  • PRM performance is not significant; the authors suggest confusing PRM/SFT formats and an imbalance of positive and negative processes as possible reasons.Source: Limitations · p. 16
  • The English-heavy SFT data distribution can cause code-switching in some instructions or problem formats.Source: Limitations · p. 16
  • SFT uses LEAN 3 because GPT-4 generated LEAN 3 codes for GSM8K and MathLib translation data was also in LEAN 3; a later version is planned to use LEAN 4.Source: Limitations · p. 16
  • The authors did not check whether AlgebraicStack contains MiniF2F solutions, though they describe the comparison with Llemma as fair.Source: Limitations · p. 16
  • Performance can vary with prompt format and instruction wording.The authors give examples including “Question:” and “Please solve this question step by step.”Source: Limitations · p. 16

B SFT Experiment Configs

The SFT setup uses a 622.7-million-token dataset and differs in training resources by model size; detailed benchmark results are reported separately.

B SFT Experiment Configs

  • SFT used 622.7 million tokens for three epochs; 7B training took about seven hours on 32 GPUs, and 20B training about ten hours on 64 GPUs.Source: B SFT Experiment Configs · p. 22

C Detailed performance on MATH benchmark

D Case studies

The case studies present InternLM-Math-7B outputs across answer checking, answer comparison, proof translation, problem augmentation, and formal reasoning.

  • The Schur inequality prompt is rendered as a LEAN theorem with nonnegativity hypotheses and the inequality expression.Source: D Case studies · p. 22
  • For 5287, the model finds 17 as a divisor and concludes that the number is composite.Source: D Case studies · p. 22
  • A formal proof found by InternLM-Math using LEAN 4 is shown for amc12a 2013 p4.Source: D Case studies · p. 23
  • For THAT, the verifier labels the supplied answer of 24 arrangements wrong.Source: D Case studies · p. 23
  • In a worked-answer annotation, PRM marks the first two reasoning steps positive and steps 3–9 negative.Source: D Case studies · p. 23
  • In a two-answer comparison, the model selects Answer 2 as better.Source: D Case studies · p. 24
  • A question-answer pair becomes a proof statement asserting Grant’s score is 100 if and only if x = 45.Source: D Case studies · p. 24
  • An augmentation prompt for a harder remainder problem yields a squared polynomial divided by a squared divisor.Source: D Case studies · p. 24

E Results on InternLM-Math-Plus

InternLM-Math-Plus adds pre-training corpora and fine-tuning datasets across four model sizes. Its evaluation spans formal and informal math benchmarks, with an additional Python evaluation on MATH.

Loading 2402.06332v2…