大型语言模型（LLMs）是指采用机器学习技术，利用大量文本数据进行训练，以能够自然地理解和生成自然语言文本的人工智能模型。这些模型可以用于自然语言处理任务，如文本分类、文本生成、语言翻译、问题回答和摘要生成等。最近几年，由于深度学习技术的进步，大型语言模型已经取得了令人瞩目的成就，例如 OpenAI 的 GPT 系列模型和 Google 的 BERT 模型等。这些模型似乎具有人类的智力和创造力。他们对书面问题提供详细而清晰的回答。

几十年来，数学家一直试图将证明转化为计算机代码，这一过程被称为形式化。如果你把证明写成代码，计算机运行代码时没有错误，你就知道证明是正确的。但证明一个命题可能需要数百或数千个小时。

在过去的五年里，人工智能研究人员已经开始教LLMs自动将数学语句形式化。LLMs已经可以将一种自然语言翻译成另一种自然语言。但从数学到代码的转换是一个艰巨的挑战。

尽管LLMs在自然语言处理等领域取得了很大的成功，但是它们也存在一些问题：

数据偏差： LLMs 的性能取决于其训练数据。如果训练数据存在偏差，模型就会学到这些偏差，从而影响其性能。

偏见： LLMs 可能会从其训练数据中学习到偏见，并将这些偏见反映在其生成的文本中。这可能导致出现歧视性语言或错误的陈述。

知识表示： LLMs 没有真正的理解语言或世界的知识，它们只是学习出现在数据中的模式。这意味着它们可能会在处理新的情况时出现问题。

模型大小： LLMs 需要大量的计算资源和存储空间，以及大量的训练数据。这使得训练和部署成本非常高。

环境依赖性： LLMs 的性能取决于输入的上下文和环境。如果输入的数据与训练数据不同，它们可能会产生错误的输出。

基于上述问题，这些模型有时会做出不合逻辑的陈述，或者自信地把谎言说成事实。谷歌AI的吴宇怀表示：“我们不想创建一个像人类一样说话的语言模型，我们想让它明白自己在说什么。”

吴是最近两篇论文的合著者，这两篇论文提出了一种实现这一目标的方法。它们是关于一个非常具体的应用的：训练人工智能系统做数学。

第一篇论文描述了如何教LLM将普通的数学语句转换为计算机可以运行和检查的正式代码。第二篇训练LLM不仅要理解自然语言数学问题，而且要使用一个名为Minerva的系统实际解决这些问题。

Minerva指的是一个用于解决数学问题的系统，它是一个组合了自然语言处理和数学推理的系统。这个系统的作用是帮助计算机理解自然语言中的数学问题，从而能够通过推理和计算得出问题的答案。具体来说，这个系统包括多个子系统，包括自然语言处理、问题建模、数学知识库和推理引擎等。通过这些子系统的协作，Minerva能够有效地解决自然语言数学问题。

总之，这些论文提出了未来人工智能设计的蓝图，LLM可以通过数学思维学习推理。

研究人员主要使用名为Codex的LLM（基于GPT-3）。为了让Codex能够很好地理解数学，从而实现自动形式化，他们只提供了两个自然语言数学问题示例及其正式代码翻译。在简短的训练之后，Codex给出了来自高中比赛的近4000道数学题目的自然语言陈述。起初，Codex准确率略低于30%。当它失败时，它创造了一些术语来填补翻译词典的空白。

在此研究之前，Codex从未尝试在自然语言和形式数学代码之间进行翻译。但Codex通过在GitHub上的培训熟悉代码，也熟悉互联网上的自然语言数学。在此基础上，研究人员只需向它展示几个他们想要的例子，Codex就可以开始连接这些点了。

研究人员不仅试图教LLMs如何翻译数学问题，而且还试图教他们如何解决问题。

Minerva数学

第二篇论文虽然独立于早期的自动形式化工作，但也有类似的风格。谷歌的研究团队训练了一种LLM来详细回答高中竞赛级别的数学问题，例如“平行于y = 4x + 6的直线经过(5,10)，这条直线与y轴交点的y坐标是多少?”

作者从一个名为PaLM的LLM开始，它已经接受了一般自然语言内容的训练，类似于GPT-3。他们将这个增强模型命名为Minerva。

研究人员向Minerva展示了他们想要的四个例子。然后他们在一系列定量推理问题上测试了这个模型。Minerva的表现因科目而异：在某些科目如代数上，它的正确率略高于一半，而在其他科目如几何上则略低于一半。

作者们担心的一个问题是Minerva正确回答问题只是因为它已经在训练数据中看到了这些问题或类似的问题。这个问题被称为“污染（pollution）”，它使得人们很难知道一个模型是真正在解决问题，还是只是在复制别人的工作。

为了防止这种可能性，研究人员让Minerva参加了波兰的2022年国家数学考试，它答对了65%的问题。这表明训练有素的模型具有解决数学问题的能力。

桥

尽管Minerva的工作令人印象深刻，但它带有一个严重的问题，作者也指出了这一点：Minerva没有办法自动验证它是否正确地回答了问题。即使它确实正确地回答了一个问题，它也不能检查它所采取的步骤是否有效。

换句话说，Minerva它不能检查它的工作，这意味着它需要依靠人类的反馈来变得更好。因此，研究人员怀疑这种方法能否扩大到复杂问题上。

吴指出，一方面，如果你研究自然语言或Minerva类型的推理，有很多数据可以利用——整个数学互联网，但本质上你不能用它进行强化学习。另一方面，像Isabelle/HOL这样的证明助手提供了一个基础的环境，但几乎没有数据可供训练。我们需要某种桥梁把它们连接起来。

自动形式化就是那个桥。自动形式化的改进可以帮助数学家在编写证明和验证工作正确性方面实现自动化。

通过结合这两篇论文的进步，像Minerva这样的系统可以首先自动形式化自然语言数学问题，然后解决它们，并使用证明助手检查它们的工作。这种即时检查将为强化学习提供必要的反馈，使这些程序能够从错误中学习。最后，他们会得到一个可证明的正确答案，并附带一系列逻辑步骤——有效地结合了LLM和强化学习的力量。

人工智能研究人员还有更广泛的目标。他们认为数学是开发人工智能推理技能的完美证明，因为它可以说是所有推理任务中最难的。按照这种想法，如果一台机器能够有效地进行数学推理，那么它自然应该获得其他技能，比如编写计算机代码或提供医疗诊断的能力。

但是仍然有一些工作是目前的人工智能所无法替代的的，例如：

艺术创作：创造真正的、有创意的艺术作品需要人类的创造力和情感体验的。

心理治疗：面对严重的心理问题，人类专业心理医生提供的治疗和支持无法被取代。

体力劳动：虽然有机器人可以执行一些体力劳动工作，但是执行某些复杂的任务仍然需要人类的技能。

社交关系：建立和维护人际关系需要人类的情感和社交技能。

总之，在许多领域中，人类的情感、判断和创造力是无法被替代的。