2402.06332.md

背景

• 背景
  论文介绍了大型语言模型在数学能力方面的抽象推理能力的表现。针对数学问题的预训练和监督式微调是构建此类模型的两个重要步骤。

• 已有的工作为什么解决不了 前人工作未能结合链式推理、奖励建模、形式化推理、数据增强和代码解释器在统一的序列到序列(seq2seq)格式下，以此来监督模型，并使其成为多功能的数学推理机。之前的研究通常需要独立的验证模型来鉴定不同的推理过程和答案，这既低效也耗费人力。

核心贡献

• 提出了InternLM-Math模型

  • 挑战1：怎样使模型具备多方面的能力 InternLM-Math统一了多种能力使其成为完备的数学推理、验证、证明和对下一代数学LLMs的迭代开发工具。

  • 挑战2：数学问题的解决与证明过程 提出了利用LEAN作为解决和证明数学问题的统一平台的可能性，并且检查了多任务学习环境下的性能。

实现与部署

该模型在多个非正式和正式的数学推理基准测试中，通过上下文内学习、监督式微调和代码辅助推理，获得了开源的最先进性能。例如在GSM8K, MATH，匈牙利数学考试，MathBench-ZH和MiniF2F上的测试。未经微调的预训练模型在MiniF2F测试集上达到30.3的分数。值得一提的是，该模型的预训练表现在多任务学习环境中表现出了使用LEAN解决数学问题并在数学上进行证明的潜力。

总结

InternLM-Math模型是一种基于LLMs的数学推理工具，它整合了多种能力并提供了监督学习以帮助模型在各种数学推理任务中实现最先进的性能，并开源其代码和数据。论文还探讨了利用程序语言LEAN在多任务学习设置中解决数学问题的新方法，彰显了LLMs在形式化和代码辅助推理中的潜能。