InternLM-Math

新闻

• [2024.10.22] 我们发布了具有1.4万条Lean-Workbook中发现的证明的InternLM2.5-Step-Prover策略模型和批评家模型。🤗数据集 🤗策略模型 🤗批评家模型 📑 论文
• [2024.07.25] 我们发布了包含从100多个Lean 4仓库中整理出的2.9万条定理的Lean-Github以及在Lean-Github和Lean-Workbook上微调的7B模型——InternLM2-Step-Prover，其在MiniF2F测试（54.5%）、ProofNet（18.1%）和普特南竞赛（5道题）上的表现均达到当前最佳水平。🤗数据集 🤗模型 📑 论文 📖 README
• [2024.06.06] 我们发布了包含5.7万道用Lean 4形式化处理的数学问题的Lean-Workbook，其中5千道已搜索到证明，可用于自动形式化和自动定理证明。🤗数据集 📑 论文
• [2024.05.24] 我们发布了更新版本的InternLM2-Math-Plus，提供四种规模，性能均处于行业领先水平，包括1.8B、7B、20B以及8×22B版本。我们在非形式化数学推理（思维链和代码解释器）和形式化数学推理（LEAN 4翻译与LEAN 4定理证明）方面均有显著提升。
• [2024.02.10] 我们新增了技术报告和引用参考文献。
• [2024.01.31] 我们增加了MiniF2F测试结果及评估代码！
• [2024.01.29] 我们添加了来自ModelScope的检查点，并更新了多数投票和代码解释器的相关结果。技术报告正在撰写中！
• [2024.01.26] 我们增加了来自OpenXLab的检查点，方便中国用户下载！

InternLM2-Math-Plus

检查点

模型	模型类型	Hugging Face Transformers	ModelScope	发布日期
InternLM2-Math-Plus-1.8B	对话	🤗internlm/internlm2-math-plus-1_8b	Shanghai_AI_Laboratory/internlm2-math-plus-1_8b	2024-05-27
InternLM2-Math-Plus-7B	对话	🤗internlm/internlm2-math-plus-7b	Shanghai_AI_Laboratory/internlm2-math-plus-7b	2024-05-27
InternLM2-Math-Plus-20B	对话	🤗internlm/internlm2-math-plus-20b	Shanghai_AI_Laboratory/internlm2-math-plus-20b	2024-05-27
InternLM2-Math-Plus-Mixtral8x22B	对话	🤗internlm/internlm2-math-plus-mixtral8x22b	Shanghai_AI_Laboratory/internlm2-math-plus-mixtral8x22b	2024-05-27

形式化数学推理

我们对InternLM2-Math-Plus在形式化数学推理基准MiniF2F-test上的表现进行了评估。评估设置与Llemma相同，使用LEAN 4。

这是我们在MiniF2F上复现我们性能的方法。

模型	MiniF2F-test
ReProver	26.5
LLMStep	27.9
GPT-F	36.6
HTPS	41.0
Llemma-7B	26.2
Llemma-34B	25.8
InternLM2-Math-7B-Base	30.3
InternLM2-Math-20B-Base	29.5
InternLM2-Math-Plus-1.8B	38.9
InternLM2-Math-Plus-7B	43.4
InternLM2-Math-Plus-20B	42.6
InternLM2-Math-Plus-Mixtral8x22B	37.3

非正式数学推理

我们在非正式数学推理基准 MATH 和 GSM8K 上评估了 InternLM2-Math-Plus 的性能。在最小尺寸设置下，InternLM2-Math-Plus-1.8B 的表现优于 MiniCPM-2B。InternLM2-Math-Plus-7B 的表现则超过了当前最先进的开源数学推理模型 Deepseek-Math-7B-RL。InternLM2-Math-Plus-Mixtral8x22B 在 MATH（使用 Python）上取得了 68.5 分，在 GSM8K 上取得了 91.8 分。

关于工具调用推理和评估，请参阅代理部分。

模型	MATH	MATH-Python	GSM8K
MiniCPM-2B	10.2	-	53.8
InternLM2-Math-Plus-1.8B	37.0	41.5	58.8
InternLM2-Math-7B	34.6	50.9	78.1
Deepseek-Math-7B-RL	51.7	58.8	88.2
InternLM2-Math-Plus-7B	53.0	59.7	85.8
InternLM2-Math-20B	37.7	54.3	82.6
InternLM2-Math-Plus-20B	53.8	61.8	87.7
Mixtral8x22B-Instruct-v0.1	41.8	-	78.6
Eurux-8x22B-NCA	49.0	-	-
InternLM2-Math-Plus-Mixtral8x22B	58.1	68.5	91.8

我们还在 MathBench-A 上对模型进行了评估。InternLM2-Math-Plus-Mixtral8x22B 的表现与 Claude 3 Opus 相当。

模型	算术	小学	初中	高中	大学	平均
GPT-4o-0513	77.7	87.7	76.3	59.0	54.0	70.9
Claude 3 Opus	85.7	85.0	58.0	42.7	43.7	63.0
Qwen-Max-0428	72.3	86.3	65.0	45.0	27.3	59.2
Qwen-1.5-110B	70.3	82.3	64.0	47.3	28.0	58.4
Deepseek-V2	82.7	89.3	59.0	39.3	29.3	59.9
Llama-3-70B-Instruct	70.3	86.0	53.0	38.7	34.7	56.5
InternLM2-Math-Plus-Mixtral8x22B	77.5	82.0	63.6	50.3	36.8	62.0
InternLM2-Math-20B	58.7	70.0	43.7	24.7	12.7	42.0
InternLM2-Math-Plus-20B	65.8	79.7	59.5	47.6	24.8	55.5
Llama3-8B-Instruct	54.7	71.0	25.0	19.0	14.0	36.7
InternLM2-Math-7B	53.7	67.0	41.3	18.3	8.0	37.7
Deepseek-Math-7B-RL	68.0	83.3	44.3	33.0	23.0	50.3
InternLM2-Math-Plus-7B	61.4	78.3	52.5	40.5	21.7	50.9
MiniCPM-2B	49.3	51.7	18.0	8.7	3.7	26.3
InternLM2-Math-Plus-1.8B	43.0	43.3	25.4	18.9	4.7	27.1

简介（针对 InternLM2-Math）

• 7B 和 20B 中英双语数学语言模型，性能超越 ChatGPT。 InternLM2-Math 是在 InternLM2-Base 的基础上继续预训练得到的，使用了约 1000 亿高质量的数学相关 token，并结合约 200 万条双语数学监督数据进行 SFT 训练。我们采用了 minhash 和精确数字匹配方法来消除可能的测试集泄露问题。
• 新增 Lean 作为数学问题求解和数学定理证明的支持语言。 我们正在探索将 Lean 3 与 InternLM-Math 结合，以实现可验证的数学推理。InternLM-Math 可以为简单的数学推理任务（如 GSM8K）生成 Lean 代码，或根据 Lean 状态提供可能的证明策略。
• 也可被视为一种奖励模型，支持结果/过程/Lean 奖励模型。 我们使用多种类型的奖励建模数据对 InternLM2-Math 进行监督训练，使其能够验证思维链过程。此外，我们还增加了将思维链过程转换为 Lean 3 代码的功能。
• 数学推理增强助手 和 代码解释器。InternLM2-Math 可以帮助增强数学推理问题，并通过代码解释器解决问题，从而更快地生成合成数据！

模型

InternLM2-Math-Base-7B 和 InternLM2-Math-Base-20B 是预训练检查点。InternLM2-Math-7B 和 InternLM2-Math-20B 是 SFT 检查点。

模型	模型类型	Transformers(HF)	OpenXLab	ModelScope	发布日期
InternLM2-Math-Base-7B	基础	🤗internlm/internlm2-math-base-7b		internlm2-math-base-7b	2024-01-23
InternLM2-Math-Base-20B	基础	🤗internlm/internlm2-math-base-20b		internlm2-math-base-20b	2024-01-23
InternLM2-Math-7B	对话	🤗internlm/internlm2-math-7b		internlm2-math-7b	2024-01-23
InternLM2-Math-20B	对话	🤗internlm/internlm2-math-20b		internlm2-math-20b	2024-01-23

性能

预训练性能

我们基于贪婪解码和少样本 COT 评估预训练检查点。预训练的详细信息将在技术报告中介绍。

基准	GSM8K MAJ@1	GSM8K MAJ@100	MATH MAJ@1	MATH MAJ@256
Llama2-7B	14.6	-	2.5	-
Llemma-7B	36.4	54.0	18.0	33.5
InternLM2-Base-7B	36.5	-	8.6	-
InternLM2-Math-Base-7B	49.2	75.7	21.5	35.6
Minerva-8B	16.2	28.4	14.1	25.4
InternLM2-Base-20B	54.6	-	13.7	-
InternLM2-Math-Base-20B	63.7	84.8	27.3	46.2
Llemma-34B	51.5	69.3	25.0	43.1
Minerva-62B	52.4	68.5	27.6	43.4
Minerva-540B	58.8	78.5	33.6	50.3

我们使用 MiniF2F 上的少样本评估预训练检查点。请参阅 eval/pretrain/minif2f 进行评估。

基准	MiniF2F-test
ReProver	26.5
LLMStep	27.9
Code-Llama-7B	26.2
Code-Llama-34B	25.8
Llemma-7B	26.2
Llemma-34B	25.8
InternLM2-Math-7B-Base	30.3
InternLM2-Math-20B-Base	29.5

SFT 性能

所有性能均基于带有 COT 的贪婪解码。我们注意到，匈牙利任务的表现在我们的不同检查点之间存在较大差异，而其他任务的表现则非常稳定。这可能是由于匈牙利任务的数量问题所致。

模型	模型类型	GSM8K	MATH	匈牙利
Qwen-7B-Chat	通用	51.7	11.6	-
DeepSeek-7B-Chat	通用	63.0	15.8	28.5
InternLM2-Chat-7B	通用	70.7	23.0	-
ChatGLM3-6B	通用	53.8	20.4	32
MetaMath-Mistral-7B	数学	77.7	28.2	29
MetaMath-Llemma-7B	数学	69.2	30.0	-
InternLM2-Math-7B	数学	78.1	34.6	55
InternLM2-Chat-20B	通用	79.6	31.9	-
MetaMath-Llemma-34B	数学	75.8	34.8	-
InternLM2-Math-20B	数学	82.6	37.7	66
Qwen-72B	通用	78.9	35.2	52
DeepSeek-67B	通用	84.1	32.6	58
ChatGPT (GPT-3.5)	通用	80.8	34.1	41
GPT4（第一版）	通用	92.0	42.5	68

代码解释器性能

所有性能均基于与 Python 的交互测试。

模型	GSM8K	MATH
DeepSeek-Coder-Instruct-7B	62.8	28.6
DeepSeek-Coder-Instruct-1.5-7B	72.6	34.1
ToRA-7B	72.6	44.6
MathCODER-CL-7B	67.8	30.2
InternLM2-Chat-7B	77.9	45.1
InternLM2-Math-7B	79.4	50.9
ToRA-13B	75.8	48.1
MathCODER-CL-13B	74.1	35.9
InternLM2-Chat-20B	84.5	51.2
InternLM2-Math-20B	80.7	54.3
MathCODER-CL-34B	81.7	45.2
ToRA-70B	84.3	49.7
GPT-4 Code Interpreter *	97.0	69.7

评估

您可以使用 OpenCompass，只需一条命令，即可轻松评估 InternLM2-Math 在多种数学数据集上的表现，例如 Math 和 GSM8K。开始之前，请先安装 OpenCompass，然后在终端中执行以下命令：

python run.py --models hf_internlm2_chat_math_7b --datasets gsm8k_gen math_gen_736506

或者，为了更便捷的操作，您也可以使用预定义的配置文件。为此，请运行下面的命令，并根据您的需求调整参数：

python run.py config/eval_internlm_math_chat.py

推理

LMDeploy

我们建议使用 LMDeploy(>=0.2.1) 进行推理。

from lmdeploy import pipeline, TurbomindEngineConfig, ChatTemplateConfig

backend_config = TurbomindEngineConfig(model_name='internlm2-chat-7b', tp=1, cache_max_entry_count=0.3)
chat_template = ChatTemplateConfig(model_name='internlm2-chat-7b', system='', eosys='', meta_instruction='')
pipe = pipeline(model_path='internlm/internlm2-math-7b', chat_template_config=chat_template, backend_config=backend_config)

problem = '1+1='
result = pipe([problem], request_output_len=1024, top_k=1)

Huggingface

import torch
from transformers import AutoTokenizer, AutoModelForCausalLM
tokenizer = AutoTokenizer.from_pretrained("internlm/internlm2-math-7b", trust_remote_code=True)
# 设置 `torch_dtype=torch.float16` 可以以 float16 格式加载模型，否则会以 float32 加载，可能导致 OOM 错误。
model = AutoModelForCausalLM.from_pretrained("internlm/internlm2-math-7b", trust_remote_code=True，torch_dtype=torch.float16).cuda()
model = model.eval()
response, history = model.chat(tokenizer，"1+1="，history=[], meta_instruction="")
print(response)

特殊用法

我们列出了一些在我们的 SFT 训练中使用的指令，你可以参考这些来帮助你。当然，你也可以使用其他方式来引导模型，但以下方法是推荐的。InternLM2-Math 可能会结合以下能力，但并不保证一定能实现。

将证明问题翻译成 Lean：

使用 Lean 3 解决 GSM8K 问题：

根据 Lean 3 代码生成题目：

玩 24 点游戏：

增强一道更难的数学题：

描述	查询
通过思维链解题	{问题}
通过 Lean 3 解题	{问题}\n请用 Lean 3 来解决
结果奖励模型	给定一道题目和一个答案，判断其是否正确？\n题目：{问题}\n答案：{COT}
过程奖励模型	给定一道题目和一个答案，检查每一步的正确性。\n题目：{问题}\n答案：{COT}
奖励模型	给定一道题目和两个答案，哪个更好？ \n题目：{问题}\n答案 1：{COT}\n答案 2：{COT}
将思维链转换为 Lean 3	请将这个答案转换成 Lean3 格式。 题目：{问题}\n答案：{COT}
将 Lean 3 转换为思维链	请将这段 Lean 3 代码转换成一道带有答案的自然语言题目：\n{LEAN 代码}
将题目和思维链答案翻译成证明语句	请将这道题目和答案转换成证明格式。\n题目：{问题}\n答案：{COT}
将证明问题翻译成 Lean 3	请将这段自然语言表述转换成 Lean 3 定理形式：{定理}
将 Lean 3 翻译成证明问题	请将这段 Lean 3 定理表述转换成自然语言：{陈述}
根据 Lean 状态建议策略	给定 Lean 3 的策略状态，请建议下一步的策略：\n{LEAN 状态}
重新表述题目	请用另一种方式描述这道题目。 {问题}
增强题目	请基于：{问题} 增加一道新题
增加难度	提高题目的复杂度：{问题}
更改特定数字	更改特定数字：{问题}
引入分数或百分比	引入分数或百分比：{问题}
代码解释器	lagent
上下文学习	题目：{问题}\n答案：{COT}\n...题目：{问题}\n答案：{COT}

微调及其他

请参考 InternLM。

已知问题

我们的模型仍在开发中，并将持续升级。InternLM-Math 目前仍存在一些潜在问题。如果你发现某些能力的表现不够理想，欢迎提交问题。

• 跳过计算步骤。
• 由于 SFT 数据构成的原因，在中文填空题和英文选择题上表现不佳。
• 由于 SFT 数据构成的原因，面对中文问题时倾向于生成代码解释器。
• 奖励模型模式可以通过分配更合适的 token 概率来进一步优化。
• 由于 SFT 数据构成的原因，可能出现语言切换现象。
• Lean 的部分能力仅适用于类似 GSM8K 的问题（例如将思维链转换为 Lean 3），且与 Lean 相关的表现并不保证。

引用与技术报告

@misc{ying2024internlmmath,
      title={InternLM-Math: 开放数学大语言模型迈向可验证推理}, 
      author={Ying Huaiyuan, Zhang Shuo, Li Linyang, Zhou Zhejian, Shao Yunfan, Fei Zhaoye, Ma Yichuan, Hong Jiawei, Liu Kuikun, Wang Ziyi, Wang Yudong, Wu Zijian, Li Shuaibin, Zhou Fengzhe, Liu Hongwei, Zhang Songyang, Zhang Wenwei, Yan Hang, Qiu Xipeng, Wang Jiayu, Chen Kai, Lin Dahua},
      year={2024},
      eprint={2402.06332},
      archivePrefix={arXiv},
      primaryClass={cs.CL}
}
@misc{ying2024lean,
      title={Lean 练习册：大规模从自然语言数学问题形式化而来的 Lean 题库}, 
      author={Ying Huaiyuan, Wu Zijian, Geng Yihan, Wang Jiayu, Lin Dahua, Chen Kai},
      year={2024},
      eprint={2406.03847},
      archivePrefix={arXiv},
      primaryClass={cs.CL}
}
@misc{wu2024leangithubcompilinggithublean,
      title={LEAN-GitHub：编译 GitHub 上的 LEAN 仓库以构建多功能 LEAN 定理证明器}, 
      author={Wu Zijian, Wang Jiayu, Lin Dahua, Chen Kai},
      year={2024},
      eprint={2407.17227},
      archivePrefix={arXiv},
      primaryClass={cs.AI},
      url={https://arxiv.org/abs/2407.17227}, 
}
@misc{wu2024internlm25stepproveradvancingautomatedtheorem,
      title={InternLM2.5-StepProver：通过大规模 LEAN 问题上的专家迭代推进自动定理证明}, 
      author={Wu Zijian, Huang Suozhi, Zhou Zhejian, Ying Huaiyuan, Wang Jiayu, Lin Dahua, Chen Kai},
      year={2024},
      eprint={2410.15700},
      archivePrefix={arXiv},
      primaryClass={cs.AI},
      url={https://arxiv.org/abs/2410.15700}, 
}

InternLM-Math 快速上手指南

InternLM-Math 是上海人工智能实验室推出的开源双语数学推理大语言模型系列。它兼具求解器、证明器、验证器和数据增强器的功能，支持非形式化数学推理（如 GSM8K、MATH）和形式化数学推理（基于 Lean 4）。本指南将帮助您快速部署并使用 InternLM2-Math-Plus 系列模型。

环境准备

在开始之前，请确保您的开发环境满足以下要求：

• 操作系统: Linux (推荐 Ubuntu 20.04+) 或 macOS。
• Python: 3.8 或更高版本。
• GPU: 推荐使用 NVIDIA GPU。
  • InternLM2-Math-Plus-1.8B: 显存需求约 4GB+。
  • InternLM2-Math-Plus-7B: 显存需求约 16GB+ (FP16)。
  • 更大参数模型（20B, 8x22B）需要多卡或高显存环境，建议使用量化推理。
• 前置依赖:
  • torch (建议 2.0+)
  • transformers (建议 4.35+)
  • accelerate
  • sentencepiece

安装步骤

推荐使用 Python 虚拟环境进行安装。

1. 创建并激活虚拟环境：

   python -m venv internlm-math-env
   source internlm-math-env/bin/activate  # Windows 用户使用: internlm-math-env\Scripts\activate
   

2. 安装核心依赖： 为了加速下载，国内用户建议使用镜像源。

   pip install torch torchvision torchaudio --index-url https://download.pytorch.org/whl/cu118
   pip install transformers accelerate sentencepiece -i https://pypi.tuna.tsinghua.edu.cn/simple
   

3. 安装 InternLM 专用库（可选但推荐）： 如果需要完整功能（如特定的 Tokenizer 处理），可安装官方库：

   pip install git+https://github.com/InternLM/InternLM.git -i https://pypi.tuna.tsinghua.edu.cn/simple
   

基本使用

以下示例展示如何使用 transformers 加载 InternLM2-Math-Plus-7B 模型进行简单的数学问题推理。

1. 模型下载（国内加速）

国内开发者推荐使用 ModelScope (魔搭) 或 OpenXLab 下载模型，速度更快。

方式 A：使用 ModelScope 下载

pip install modelscope -i https://pypi.tuna.tsinghua.edu.cn/simple

在 Python 代码中直接加载（自动缓存到本地）：

from modelscope import snapshot_download
model_dir = snapshot_download('Shanghai_AI_Laboratory/internlm2-math-plus-7b')

方式 B：使用 Hugging Face (需网络条件)

from huggingface_hub import snapshot_download
model_dir = snapshot_download('internlm/internlm2-math-plus-7b')

2. 推理代码示例

创建一个名为 infer.py 的文件，填入以下代码。该示例展示了如何加载模型并进行对话式数学推理。

import torch
from transformers import AutoTokenizer, AutoModelForCausalLM

# 配置模型路径 (如果使用 ModelScope 下载，填写本地路径; 否则填写 HF repo ID)
# 例如: model_path = "./Shanghai_AI_Laboratory/internlm2-math-plus-7b"
model_path = "internlm/internlm2-math-plus-7b" 

# 加载分词器和模型
# trust_remote_code=True 是加载 InternLM 系列模型的必要参数
tokenizer = AutoTokenizer.from_pretrained(model_path, trust_remote_code=True)
model = AutoModelForCausalLM.from_pretrained(
    model_path, 
    torch_dtype=torch.float16, 
    device_map="auto", 
    trust_remote_code=True
)
model.eval()

# 构建输入提示 (Prompt)
# InternLM2-Math 通常遵循标准的对话格式
query = "Alice has 5 apples and Bob gives her 3 more. How many apples does Alice have now?"
history = [] # 历史对话列表，多轮对话时保留

# 生成回答
response, history = model.chat(tokenizer, query, history=history)

print(f"问题: {query}")
print(f"回答: {response}")

3. 运行测试

在终端执行脚本：

python infer.py

预期输出示例：

问题: Alice has 5 apples and Bob gives her 3 more. How many apples does Alice have now?
回答: Alice originally has 5 apples. Bob gives her 3 more apples. So, the total number of apples Alice has now is 5 + 3 = 8.

进阶提示：代码解释器模式

InternLM2-Math-Plus 支持调用 Python 代码解决复杂数学问题。在构造 Prompt 时，模型会自动识别是否需要生成代码块。若需强制开启代码解释器功能，请确保在推理参数中允许模型生成 <|action_start|><|interpreter|> 等特殊标记（具体取决于使用的推理框架版本，上述 model.chat 接口已内置基础支持）。