• 大模型数学推理
• • Why Math?
  • • 数学作为验证大模型能力的学科
    • 数学作为大模型可以发挥作用的学科
  • 算术推理
  • 数学应用题（Math word problem)
  • 定理证明
  • 相关数据集
  • 相关开源项目
  • • 联系我们
• 参与单位

大模型数学推理

基于自然语言处理的生成式大模型已经在很多领域，包括知识、写作、理解上达到甚至超过了人类水平。但与大模型在许多领域上超越人类的表现不同,在需要复杂推理的数学领域上，大模型与人类、甚至大模型与大模型之间的差异依然显著,GPT-4的数学能力只相当于一个成绩中等的数学系学生(Frieder et al. 2023),而在普遍被用于衡量数学能力的GSM8K（小学水平的数学应用题）,MATH数据集（数学竞赛及本科水平）上,GPT-4要优于目前最先进的开源大模型2-4倍,因此模型的数学能力也可以被间接用于评估模型的性能。 另一方面,随着大语言模型的能力增长，对其在特定领域，如数学的应用也引发了广泛关注。不仅仅是解决基础数学应用题，更高级的自动定理证明也逐渐被看作是大模型的潜在应用领域。这使得如何提高模型的推理和数学能力，利用大模型解决更复杂的数学问题,成为日益受到关注的问题。

数学作为一个极度依赖多步逻辑的学科，解决数学问题的能力客观地反映了模型的逻辑水平和对上下文之间隐含知识的充分理解，因此增强大模型的数学能力是真正意义上提高大模型智能水平的重要标志。
对于数学相关的题目和任务，我们按照解决问题所需要的模型能力层级，将其分为三级,并维护相应的排行榜。

Why Math?

数学作为验证大模型能力的学科

1. 极度依赖多步逻辑推理能力
2. 极度依赖步骤间一致正确性
3. 较高难度的数学缺乏足够的训练语料

数学作为大模型可以发挥作用的学科

1. 数学作为自然科学的根基，对数学的理解会提高模型对自然科学的认知
2. 数学学科本身难度跨度较大，人类很难掌握多个分支，对一个有广泛且高水平认知的模型有需求
3. 数学作为人类智慧的结晶，是人工智能达到甚至超过人类水平的重要标志

算术推理

这类题目的问题和答案都主要基于自然语言描述，答案附带含有四则运算的算术式对题目中出现的数量关系进行转换和理解，并借由步骤来分隔解题逻辑，最终通过一步一步地推理和运算，得到最终答案，其难度主要是小学数学题，小学奥数题和部分初中题目，代表性的任务数据集是GSM8k。解决这类问题需要模型具备逐步推理能力和简单的计算能力。

数学应用题（Math word problem)

这类题目同样含有自然语言描述，但题目包含代数式和方程，往往没有充足的自然语言描述的实体对象，是相较于应用题更加抽象的数学题目。模型需要经过代数符号与代数式的推导和方程求解得到最终答案，其难度类似于中学数学竞赛以及本科数学的题目，代表性的数据集是MATH。解决这类问题需要模型具备较为完整的数学知识体系，理解抽象概念和符号的能力同时根据这些概念进行创造性推理的能力。

定理证明

这类问题包括复杂的数学证明和所有我们真正关心的数学问题，由于其严谨的逻辑性和抽象性，其难度远远超过了前两类问题。由于其自然语言数据的相对匮乏和命题的多样性，我们无法通过简单分析模型的输出评判模型回答的对错，对于这类问题，我们需要将问题转化为机器证明语言，通过训练和提示让模型输出合法的计算机语句来完成命题的证明。代表性的数据集和评价指标包括miniF2F、ProofNet和IMO Grand Challenge。解决这类问题需要模型的数学能力与代码能力的深度对齐，甚至需要外挂知识库和评估模式来指导和优化模型产生正确的输出。

相关数据集

• GSM8K: GSM8K是一个数据集，包含8.5K个由人类问题编写者创建的高质量、语言多样的小学数学文字题目。该数据集分为7.5K个训练问题和1K个测试问题。这些问题需要2到8个步骤来解决，解决方案主要涉及执行一系列基本算术运算（+ − ×÷）的基础计算，以得出最终答案。一个聪明的中学生应该能够解决每一个问题。它可以用于多步骤的数学推理。

• MATH: MATH是一个全新的数据集，包含12,500个具有挑战性的竞赛数学问题。MATH中的每个问题都有一个完整的分步解决方案，可用于教导模型生成答案的推导和解释。

• miniF2F: MiniF2F是一个正式的奥林匹克级数学问题陈述的数据集，旨在为神经定理证明提供一个统一的跨系统基准。目前的miniF2F基准测试针对Metamath、Lean和Isabelle，包括488个问题陈述，这些问题来自AIME、AMC和国际数学奥林匹克竞赛（IMO），以及高中和本科数学课程的材料。

相关开源项目

• Optimus-LM: 一个高效地并行训练框架，与HuggingFace接口对齐，可以作为Pretraining, SFT, RLHF的后端实现。
• CoT-Hub:一个基于CoT的多步推理模型的训练和评测平台，可以用于算术推理和数学应用题的训练和评测。

Frieder, Simon, Luca Pinchetti, Ryan-Rhys Griffiths, Tommaso Salvatori,
Thomas Lukasiewicz, Philipp Christian Petersen, Alexis Chevalier, and
Julius Berner. 2023. “Mathematical Capabilities of ChatGPT.” arXiv.
http://arxiv.org/abs/2301.13867.

联系我们

如果你对本项目的使用和代码有任何问题，可以提交issue。同时你也可以通过邮箱 xuchx@pcl.ac.cn 直接联系我们

参与单位

鹏城实验室，南方科技大学，哈尔滨工业大学。