人工智能已经可以解决复杂的数学问题了，还有哪些工作是无法被取代的

2023-02-24 12:15:06来源：

大型语言模型（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 和强化学习的力量。

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