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

📄 arXiv: 2402.06332v2 📥 PDF

作者: 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

分类: cs.CL

发布日期: 2024-02-09 (更新: 2024-05-24)

🔗 代码/项目: GITHUB

💡 一句话要点

提出InternLM-Math以解决数学推理能力不足的问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 数学推理 大型语言模型 推理能力 数据增强 代码解释器 多任务学习 开源模型

📋 核心要点

  1. 现有大型语言模型在数学推理能力上存在不足，难以进行复杂的数学问题解决和验证。
  2. 提出的InternLM-Math模型通过统一多种推理方法，增强了模型的数学推理、验证和证明能力。
  3. 在多个基准测试中，InternLM-Math在无微调情况下取得了30.3的高分，展示了其强大的数学推理能力。

📝 摘要（中文）

本文介绍了开源的数学推理大型语言模型InternLM-Math，该模型在InternLM2的基础上进行继续预训练。我们将链式思维推理、奖励建模、形式推理、数据增强和代码解释器统一为一个seq2seq格式，监督模型成为多功能的数学推理者、验证者、证明者和增强者。InternLM-Math在多项非正式和正式基准测试中表现出色，包括GSM8K、MATH、匈牙利数学考试、MathBench-ZH和MiniF2F，且在MiniF2F测试集上未进行微调时取得了30.3的成绩。此外，我们探索了如何使用LEAN解决数学问题，并研究了其在多任务学习下的表现，显示出LEAN作为数学解决和证明的统一平台的潜力。我们的模型、代码和数据已在GitHub上发布。

🔬 方法详解

问题定义：本文旨在解决现有大型语言模型在数学推理方面的不足，尤其是在复杂问题的解决和验证能力上存在的挑战。现有方法往往无法有效处理多样化的数学问题，导致推理结果不可靠。

核心思路：我们提出的InternLM-Math模型通过继续预训练和统一多种推理方法（如链式思维推理和奖励建模），使模型具备了多功能的数学推理能力。这样的设计旨在提升模型的灵活性和准确性，以应对不同类型的数学问题。

技术框架：InternLM-Math采用seq2seq架构，整合了链式思维推理、奖励建模、形式推理、数据增强和代码解释器等模块。模型的训练过程包括监督学习和无监督学习，确保其在多种任务下的适应性和性能。

关键创新：本研究的主要创新在于将多种推理方法整合为一个统一的框架，使得模型不仅能够进行数学推理，还能进行验证和证明。这种整合与现有方法的单一推理能力形成了鲜明对比。

关键设计：在模型设计中，我们采用了特定的损失函数来优化推理准确性，并通过数据增强技术提升模型的泛化能力。此外，模型的参数设置经过精心调整，以确保在不同基准测试中的最佳表现。

🖼️ 关键图片

img_0

📊 实验亮点

在多个基准测试中，InternLM-Math在无微调情况下在MiniF2F测试集上取得了30.3的成绩，显示出其在数学推理方面的卓越性能。与现有模型相比，InternLM-Math在多项任务中均表现出显著的提升，证明了其设计的有效性。

🎯 应用场景

InternLM-Math的研究成果在教育、科学计算和自动化证明等领域具有广泛的应用潜力。它可以用于开发更智能的数学教育工具，帮助学生理解复杂的数学概念，同时也能在科研中辅助数学问题的解决和验证，推动相关领域的发展。

📄 摘要（原文）

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}.