InternLM-Math

InternLM-Math ^热门

最先进的双语开源数学推理大语言模型。 一个解题器，证明器，验证器，增强器。

📑 论文 💻 Github 🤗 演示 🤗 检查点 ModelScope

新闻

• [2024.07.25] 我们发布了Lean-Github和InternLM2-Step-Prover，包含从100多个Lean 4仓库编译的29K个定理，以及在Lean-Github和Lean-Workbook上微调的7B模型，在MiniF2F-test (54.5%)、ProofNet (18.1%)和Putnam (5个问题)上取得了最先进的性能。🤗数据集 🤗模型 📑 论文 📖 README
• [2024.06.06] 我们发布了Lean-Workbook，包含57K个用Lean 4形式化的数学问题，其中5K个带有搜索证明，用于自动形式化和自动定理证明。🤗数据集 📑 论文
• [2024.05.24] 我们发布了更新版本InternLM2-Math-Plus，有4种规模，包括1.8B、7B、20B和8x22B，在非形式化数学推理性能（思维链和代码解释器）和形式化数学推理性能（LEAN 4翻译和LEAN 4定理证明）方面都取得了显著提升。
• [2024.02.10] 我们添加了技术报告和引用参考。
• [2024.01.31] 我们添加了MiniF2F结果和评估代码！
• [2024.01.29] 我们添加了来自ModelScope的检查点。更新了关于多数投票和代码解释器的结果。技术报告即将发布！
• [2024.01.26] 我们添加了来自OpenXLab的检查点，方便中国用户下载！

InternLM2-Math-Plus

检查点

形式化数学推理

我们在形式化数学推理基准MiniF2F-test上评估了InternLM2-Math-Plus的性能。评估设置与Llemma在LEAN 4上相同。

如何复现我们在MiniF2F上的性能。

非形式化数学推理

我们在非形式化数学推理基准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分。

关于工具调用推理和评估，请参见agent部分。 | 模型 | 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相当。

简介 (InternLM2-Math)

• 性能优于ChatGPT的7B和20B中英文数学语言模型。 InternLM2-Math是在InternLM2-Base的基础上，通过约1000亿高质量数学相关token的持续预训练和约200万双语数学监督数据的SFT而得到的。我们应用了最小哈希和精确数字匹配来消除可能的测试集泄露。
• 添加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评估预训练检查点。预训练的详细信息将在技术报告中介绍。

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

SFT 性能

所有性能基于贪婪解码和思维链。我们注意到匈牙利问题的性能在不同检查点之间差异较大,而其他性能则非常稳定。这可能是由于匈牙利问题的数量问题。

代码解释器性能

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

评估

你可以使用OpenCompass轻松地在各种数学数据集（如Math和GSM8K）上评估InternLM2-Math，只需一条命令即可。安装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格式加载，可能导致内存溢出错误。
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点游戏：

增强更难的数学问题：

微调和其他

请参考 InternLM。

已知问题

我们的模型仍在开发中，将会升级。InternLM-Math 存在一些可能的问题。如果您发现某些能力的表现不佳，欢迎提出问题。

• 跳过计算步骤。
• 由于 SFT 数据组成，在中文填空问题和英文选择题上表现不佳。
• 由于 SFT 数据组成，在面对中文问题时倾向于生成代码解释器。
• 奖励模型模式可以通过分配的令牌概率更好地利用。
• 由于 SFT 数据组成导致的代码切换。
• 一些 Lean 的能力只能适应类似 GSM8K 的问题（例如将思维链转换为 Lean 3），与 Lean 相关的性能不能保证。

引用和技术报告

@misc{ying2024internlmmath,
      title={InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoning}, 
      author={Huaiyuan Ying and Shuo Zhang and Linyang Li and Zhejian Zhou and Yunfan Shao and Zhaoye Fei and Yichuan Ma and Jiawei Hong and Kuikun Liu and Ziyi Wang and Yudong Wang and Zijian Wu and Shuaibin Li and Fengzhe Zhou and Hongwei Liu and Songyang Zhang and Wenwei Zhang and Hang Yan and Xipeng Qiu and Jiayu Wang and Kai Chen and Dahua Lin},
      year={2024},
      eprint={2402.06332},
      archivePrefix={arXiv},
      primaryClass={cs.CL}
}
@misc{ying2024lean,
      title={Lean Workbook: A large-scale Lean problem set formalized from natural language math problems}, 
      author={Huaiyuan Ying and Zijian Wu and Yihan Geng and Jiayu Wang and Dahua Lin and Kai Chen},
      year={2024},
      eprint={2406.03847},
      archivePrefix={arXiv},
      primaryClass={cs.CL}
}
@misc{wu2024leangithubcompilinggithublean,
      title={LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN prover}, 
      author={Zijian Wu and Jiayu Wang and Dahua Lin and Kai Chen},
      year={2024},
      eprint={2407.17227},
      archivePrefix={arXiv},
      primaryClass={cs.AI},
      url={https://arxiv.org/abs/2407.17227}, 
}