书生成数学“课代表”，上海AI实验室开源发布书生·浦语数学，计算推理能力刷新上限

1月23日，上海人工智能实验室（上海AI实验室）开源发布新一代数学模型书生·浦语数学（InternLM2-Math）。基于书生·浦语2.0（InternLM2）强大的基础能力，InternLM2-Math仅以中轻量级参数规模，即在多项数学评测中刷新开源模型数学能力上限；此外，InternLM2-Math不仅会“解题”，更会“判题”，突破了传统数学大模型应用局限，将为数学基础研究和教学提供优质应用基座。

InternLM2-Math为首个同时支持形式化数学语言及解题过程评价的开源模型，以强大内生计算和推理能力，为技术社区提供强大数学工具和模型范式。秉持“以高质量开源赋能创新”的理念，InternLM2-Math代码和模型完全开源，并支持免费商用。

数学能力是大语言模型推理水平的重要体现。近日，谷歌 DeepMind 运用AI数学模型AlphaGeometry解几何题，其水平已接近人类奥林匹克金牌得主，引发广泛关注。当前，全球数学大模型领域研究取得了突出进展，但与顶尖人类水平相比仍然存在差距。上海AI实验室将继续以开源开放理念，与全球研究人员合作，共同探索提升语言模型数学推理能力的提升路径。

InternLM2-Math对MATH评测集中Level-5难度题目的解题过程

开源链接

GitHub：

https://github.com/InternLM/InternLM-Math

Huggingface：

https://huggingface.co/internlm

ModelScope：

https://modelscope.cn/organization/Shanghai_AI_Laboratory

四两拨千斤，轻量级选手刷新能力上限

本次开源的InternLM2-Math同时包含轻量级（7B）及中量级（20B）两个版本。

为测试InternLM2-Math的能力水平，研究人员采用GSM8K、MATH、匈牙利数学竞赛等四项数学评测集作为验证“考题”。评测结果显示，InternLM2-Math-7B以轻量级参数规模达到了与GPT-3.5同等的数学水平；中量级的InternLM2-Math-20B 则在没有借助任何外部工具的条件下，取得了目前开源模型的最佳成绩，达到与GPT-4接近的数学能力，刷新当前开源模型数学能力上限。

GSM8K：OpenAI提出的英文小学算数习题集，共1000余题；

MATH：UC Berkeley提出的英文初高中竞赛习题集，共5000题；

匈牙利数学竞赛评测集：用来衡量模型在非常见分布上的数学性能的测试集，共30余小问，通过专家校阅进行打分。

多个同类模型在GSM8K评测集上评测成绩对比，InternLM2-Math综合领先通用模型和数学专用模型，接近GPT-4数学能力

从下图中可见，InternLM2-Math-7B在GSM8K和MATH上的测试评分分别达到78.1和34.6，超越其他7B量级的通用模型和数学专用模型，与ChatGPT（GPT-3.5）不分伯仲。InternLM2-Math-20B 则超越了更大规模参数的数学专用模型MetaMath-Llemma-34B以及数理能力较强的 70B 级别通用开源模型Qwen-72B和DeepSeek-67B，并且在各个数据集上都达到了GPT-4性能约九成的评测成绩。

为了考察InternLM2-Math通用的数学能力，研究人员引入了“匈牙利数学竞赛评测集”作为指标参考。该评测集用于衡量语言模型OOD（分布外泛化）的数学性能，共设置30余道问题，通过专家人工校阅打分。评测结果显示，InternLM2-Math的7B与20B版本分别获得55分和66分，远超同类开源模型并整体接近GPT-4。这表明，InternLM2的数学性能并非针对特定评测集“突击”优化而来，而是具备了增强通用的数学能力。

为了保证InternLM2-Math在参与考试前没有被“泄题”，研究人员采用了MinHash和严格的数字匹配对模型训练中可能遇到的测试集数据进行去重，避免产生“数据污染”，研究人员在两组对照数据集上进行了损失函数计算，若不存在数据污染，损失函数应接近或大于0。验证结果显示，在InternLM2-Math7B/20B两个版本的损失函数值分别为0.14及0.11，表明训练过程中不存在“数据污染”。InternLM2-Math的数学考试成绩来源于自身“硬实力”，没有“考前泄题”。

数学课代表是怎样炼成的

上海AI实验室近期开源的InternLM2模型基座语言建模能力获得质的提升，综合性能达到同量级开源模型的领先水平，得益于此，InternLM2获得了 “天赋”。

研究人员利用InternLM2基座版模型，精选数学相关语料进行继续预训练，包括中英文数学相关的代码、网页、书籍等。其中，InternLM2-Math-7B/20B分别经过了120B和80B token的继续预训练。

微调阶段使用的指令数据覆盖中英文双语，共计200余万条，包含CoT、工具调用、奖励模型、数据推广等多种形式。

研究人员同时对数据量较少、模型性能交叉的数学知识点进行了数据增广，运用奖励建模对增广数据进行了过滤，删除不可靠的回复。对于数据中的复杂计算过程，研究人员将其扩写为更详细的步骤，使模型减少跳步推理产生的计算幻觉。

通过以上多任务学习，“天赋选手”逐步获取了多种数学能力，成为“优等生”。

经过多任务学习的InternLM2-Math在不借助任何工具（计算器、Python、Wolfram）的情况下，已表现出了高性能的内生计算能力。为探索其由“优等生”进步为“尖子生”的可能性，研究人员在训练时引入了数学语言Lean。

Lean是一种形式化数学语言，通过机器可检查的数学证明来数字化数学定理的证明，目前，许多本科数学阶段以下的数学定理都已经被用Lean表述。权威数学家曾通过Lean语言将学术论文转为形式化表达，表明Lean已经具有对现代数学的描述能力。

经过训练，InternLM2-Math可使用Lean的代码进行解答题计算，可将自然语言的证明题与Lean语言的证明状态互相翻译，或者根据给定的Lean证明状态进行证明步骤的搜索。表明InternLM2-Math在内生计算能力上，衍生出了强大的数学推理能力，已由“天赋选手”进步为名副其实的“数学尖子生”。

下图为InternLM2-Math使用Lean 3解应用题的例子，模型在注释会描述自己的计算思路。

下图为InternLM2-Math进行交互式证明，模型会根据当前Lean的证明状态搜索下一个证明步骤。模型用形式化语言严格证明了给定命题。

会解题也会判题的“AI名师”

InternLM2-Math创新性地具备了对解题过程与结果的评价能力，不仅会“解题”，更会“判题”，这使得其超越了传统数学大模型，拥有更广阔的应用空间，为数学基础研究、教学提供优质应用基座。

研究人员在模型微调阶段同时引入Outcome Reward Model (ORM)、Process Reward Model (PRM)、Lean as Reward Model (LRM)训练数据。通过PRM能力的获取，使InternLM2-Math可以认识到“自身错误”并指出错误过程。而LRM可使模型将自己产生的CoT 过程转变为Lean的形式，再通过Lean的计算结果判断过程的正确性，达到形式化过程监督的目的。

下图展示了模型PRM的能力，模型指出了错误的过程。

作为首个同时支持形式化数学语言及解题过程评价的开源模型，InternLM2-Math能够判断模型思维链过程的正确与否，使得模型具备数学能力持续改进的潜力。