摘  要

近期，随着大语言模型尤其是ChatGPT的发展，人们在自然语言处理领域取得了巨大的进步。尽管ChatGPT在回答大部分问题上表现出色，但它在定量推理方面仍有待提升，比如做简单的数学计算（例如计算11*32-223，或是求解一元二次方程），以及求解理工科题目（如给定质量和距离求引力，或是化学式的配平和计算）等。本文旨在介绍近期大语言模型在定量推理方面的进展，包括直接用大语言模型处理数学和科学问题，例如数据集的构建、大模型的训练和评估等，以及借助交互式定理工具来辅助大模型进行精确数学推理的方法。我们相信这些进展将更好地提升如ChatGPT、Bard等交互式AI问答的精准推理能力。

引  言

由于深度学习本身的特点，相关的应用往往集中在图像识别、情感分析、语音生成等无需精确推理的任务上。然而随着大型的语言模型（Large Language Models，LLM）的发展，基于自然语言处理的大语言模型如ChatGPT已经具备求解复杂问题的潜力。因此精准定量推理任务逐渐受到关注，例如编程语言的代码生成任务，数学问题的求解和证明任务，甚至是进行物理、化学问题等科学问题的定量计算任务。本文将聚焦于使用自然语言大模型来进行相关问题的定量推理问题。

 

首先需要明确什么是定量推理。定量推理是一种通过数学和统计方法来解决实际科学工程问题的方法。它可以将数据和科学理论模型联系起来，通过一些数学上的计算或者证明，做出一些精准的科学结论。简单的例子如，根据两地的距离和汽车的速度和加速度，估计出到达时间；或者是根据一些已知的行星运转轨道和周期，来求出太阳的质量。如果需要做出精准的定量推理，则需要掌握基础的算术能力、代数和几何能力，以及基础的物理化学等理工科的知识背景和相关的公式，通过多步的数学演算和证明，得到有效的科学推论。

 

那么为何可以用自然语言模型来处理数学问题？数学推理本身就可以转为一种用文本表示的形式语言，自然容易想到用大语言模型来处理。而使用语言模型来求数学题的基本思路是，用自然语言来描述数学问题，然后以字符形式输入到大模型中，当大模型读取这些数学文本，并结合大模型本身携带的预训练背景知识，以概率地方式逐个生成字符，从而模拟实际的数学推理过程，最终的解决方案则以文本的形式进行呈现。这里的关键在于训练模型时的数据样本，当语言模型经过足量的数学文本（通常为LaTeX等形式）的训练，则将使大模型具备理解数学符号和数学命题的能力，自动补全问题的背景和相关数学概念的细节，从而使得大模型具备数学推理的能力。同样，物理化学等科学问题的定量推理任务，也可以采用相同的形式进行处理。总之，大模型将扮演一个像是人类科学家的角色，根据给定的科学问题的文本描述，逐步生成基于题设要求的推理过程，从而生成包含最终解答的文本。

 

这种大语言模型的优势非常明显。当有了大语言模型，用户可以使用自然语言来向计算机提出数学问题，而不是重新学习一种特定的编程语言如Mathematica/Matlab、或者是Lean/Coq等。而语言模型又能够直接以自然语言的形式推理出所需的答案，从而节省用户大量的时间。另外大语言模型还可以结合搜索引擎检索特定的数学知识，可以解决用户自身没法求解的问题。当然，这也可以应用于教育环境中，学生可以向大语言模型询问有关他们不理解的概念或者公式，而无需自己查阅教科书或网站来寻找答案，尤其是那些改编过的，从未出现在网上的问题。

 

本文将从两个部分出发介绍相关方面的近期发展。第一部分是直接利用自然语言大模型求解数学问题；第二部分则是通过将大模型和定理证明工具（如Lean/Coq）相结合，以更严格的方式解决和证明数学问题。我们将探讨这两类方法并讨论相关的一些挑战，以及可能的解决方案。

 

直接用大语言模型进行定量推理

    用自然语言大模型求解理工科问题的一般步骤与常规的自然语言处理任务相似：

•  
• 收集数据：将理工科问题的描述与答案转换为文本数据集；
• 构建模型：构建能够处理数学符号能力的预训练语言模型；
• 训练模型：用含有理工科问题的数据集对预训练模型进一步训练；
• 评估结果：用训练好的模型生成推理文本，抽取结果与实际进行对比；

 

为了更加具体地展示相关内容，这里以近期谷歌的Minerva [1] 这篇文章来介绍这四方面的内容，这里先来看一下Minerva回答选择题时的示例（输出结果包含了推理步骤文本，而不是直接进行了四选一的输出）：

图1.Minerva回答问题的示例 [1]

图片来源：https://arxiv.org/abs/2206.14858

 

1. 数据集

数据集包含两部分内容，一部分是训练数据集，另外一部分是评估数据集。训练数据集决定了之后基于文本进行精准推理的能力，因此对数据集的清洗非常重要。Minerva的作者们在这部分的数据集做了很多的工作，他们从arXiv预印本服务器上以及相关的数学网站上收集了约38.5B个tokens的文本(B代表十亿)，其中包含有自然语言和具有LaTeX符号的文本数据，并且在尽可能保留数学文本标准化的同时，删去了文本中包含的HTML标签。而评估数据集则主要用来评估模型的效果，Minerva的作者们收集了三个类别的数据：

•  
• MATH: 高中数学竞赛问题，包含12500个高中的数学问题以及逐步推理解答；
• GSM8k: 小学级别的数学问题，高质量的基本算术运算（2-8步计算步骤）；
• MMLU-STEM: 高中大学理工科问题，涵盖高中和大学水平理工科数理化等问题。
• OCWCourses：大学本科理工科问题，为了更准的评估，作者们在麻省理工学院开放课程资源的基础上构建了200道题。

 

2. 模型与训练

    Minerva基于PaLM预训练模型（参数量分别为8B、62B和540B，B代表十亿），并在此基础上用训练数据集进一步地进行了训练。训练是在谷歌的v4 TPU上进行的，8B模型经过v4-128训练了14天，62B模型经过v4-512训练了17天，而540B模型经过v4-1024的训练了29 天。需要注意的是Minerva并没有使用评估数据集中的推理数据进行训练，而且在之后的结果中可以看到，即使如此，其在评估数据集上也得到了很好的效果。
 

图2.Minerva大模型训练参数 [1]

图片来源：https://arxiv.org/abs/2206.14858

 

3. 模型评估

对于相同的问题，大语言模型可以多次尝试给出结果，因此Minerva在评估模型时采用了多次回答，取多次回答中最普遍的答案作为最终结果输出。最后的评估结果如下：

 

图3.在评估数据集上的实验结果 [1]

图片来源：https://arxiv.org/abs/2206.14858

 

从评估结果来看，Minerva在进行精准地定量推理上得到了比较惊艳的结果，其在解决相关问题上取得了不错的表现，如下图：

 

图4.Minerva在评估数据集上的表现示例 [1]

图片来源：https://arxiv.org/abs/2206.14858
 

借助定理证明工具

使用大语言模型直接求解数学问题显得非常的直接。但这种方法也存在其局限性，例如不借助外部计算器的帮助，其计算结果未必可靠，而且在推理的过程中生成的文本并不是严格准确的，另外其对数据极度依赖，尤其是包含准确解答的大型数据集。而这些局限性其实可以通过借助一些外部的工具来克服，例如交互式的定理证明工具如Lean [2]、Coq [3] 等，当然也可以是其他功能的工具。

 

定理证明工具是一种可以帮助人们更加精准地推理的计算机程序。它能够将证明的步骤转换成有效的代码，并通过使用特定的算法和数据结构，对输入的数据进行有效地检查，从而实现更加有效地推理，以及避免错误。常见的定理证明工具有Lean、Idris、MetaMath、Isabelle、Coq等。以Lean [2]为例，它是一款开源的数学证明工具，使用一种名为归纳构造演算（Calculus of Inductive Constructions）的技术来构建数学概念，以及用一些特定的文本进行数学推理，使得用户可以像写代码一样，进行定理的证明，又可以像精准地数学推理一样对代码进行排错。其使用示例如下图：

图5.用Lean进行证明的示例

图片来源：https://leanprover-community.github.io/mathematics_in_lean/04_Sets_and_Functions.html#sets

但是从上图中也可以看出，这种定理证明工具的缺点是它的使用门槛较高，需要具备一定的数学知识和有关的编程技能才能使用。另外，它的推理能力有限，无法自动地推导复杂的数学定理，往往依赖使用者半自动地编写策略（tactic）来完成定理的证明。而恰好，大语言模型和定理证明工具可以相互弥补各自的不足，因此这也催生了一个新的领域——神经定理证明（Neural theorem proving）[4]。目前，定理证明工具与深度学习的结合正在发展。例如，GPT-f模型 [4]，它使用了GPT-3作为模型，其数据集取自定理证明工具Metamath [5]的set.mm数据库（与lean不同，其底层基础基于集合论）。

 

在这个新的领域中有两个值得关注的问题，一个是如何评估效果，另外一个是如何将大语言模型和定理证明工具的优势结合。由于在定理证明工具的选择上，会有很多种的选择，而不同的工具将导致不同语言编写的数据集，从而导致它们之间很难进行效果横向比较。为了应对这个问题，近期出现了一个可交叉评估的数据集MiniF2F [6]。它是一个面向奥林匹克竞赛难度的数学问题集，收录了来自IMO、AIME、AMC等的问题，并随机地将问题划分为验证集和测试集。它使用Metamath、Lean、Isabelle (部分)、HOL Light (部分)四种定理证明工具的形式化语言来描述数学问题和证明，从而使得不同的定理证明工具产生的数据集之间可以进行横向对比。

 

在基于miniF2F数据集上，近期发展了一种称为超树证明搜索（HyperTree Proof Search）[7] 的方法，该方法比之前的最好方法高出了20%的准确率，能够比现有方法解决五倍多的问题。它是一种基于Transformer的语言模型，并结合了一种类似蒙特卡罗树搜索的方法。由于结合了大语言模型，它还能够为其证明生成人类可读的解释。但是由于使用了特有的与定理证明相关的数据集，可以预见微调过后的模型在自然语言处理的能力上会被部分的削弱。而如何让大语言模型既能够很好地和人类自然流畅地地对话，又能够很好地进行数学推理，正在成为一个非常重要的研究方向。
 

小  结

本文主要关注了近期大语言模型在进行精准定量推理问题上的一些进展，围绕着直接用自然语言模型进行求解方法，介绍了Minerva模型，其通过加入对LaTeX数学公式更多的支持，以及包含更多的理工科知识相关的数据集，从而使得其在定量推理任务上有更好的表现。但是这种不借助外部工具的方法，使得其中的推理过程不够严格。因此本文的后半部分介绍了借助交互式定理证明工具来使得推理过程更加精准严格，并介绍了可交叉验证的数据集MiniF2F，以及一种称为超树证明搜索的方法。随着ChatGPT引发的热情，相信在这块研究领域上将会有更多的进展。
 

参考文献
1. Austin Derrow-Pinion, Jennifer She, David Wong, et al. ETA Predictionwith Graph Neural Networks in Google Maps. 20211. Lewkowycz, Aitor, et al. "Solving quantitative reasoning problems with language models." arXiv preprint arXiv:2206.14858 (2022).

2. https://leanprover.github.io/.

3. https://coq.inria.fr/.

4. Polu, Stanislas, and Ilya Sutskever. "Generative language modeling for automated theorem proving." arXiv preprint arXiv:2009.03393 (2020).

5. https://us.metamath.org/.

6. Zheng, Kunhao, Jesse Michael Han, and Stanislas Polu. "Minif2f: a cross-system benchmark for formal olympiad-level mathematics." arXiv preprint arXiv:2109.00110 (2021).

7. Lample, Guillaume, et al. "HyperTree proof search for neural theorem proving." arXiv preprint arXiv:2205.11491 (2022).

本文中所引用的图片和视频来源均已标明，若有侵权请联系我们予以删除。