AI“双子星”同日联动：DeepMind加速编程自动化，OpenAI新方法解开2道国际奥数题

大数据文摘

大数据文摘授权转载自学术头条

作者：刘媛媛、LZM

2022 年开年不久，全球人工智能领域两大明星公司不约而同在今天宣布了重要进展：OpenAI 称自己构建了一个神经定理证明器，该证明器学会了解决各种具有挑战性的高中数学问题，包括 AMC12 和 AIME 比赛的问题，以及改编自 IMO 的两个问题。

DeepMind 则表示，由其开发的名为 AlphaCode 的人工智能系统，该系统的“编程能力能与一般人类程序员相竞争”。DeepMind 说，该系统的结果是朝着自主编程迈出的重要一步，尽管现在为止 AlphaCode 的能力不一定能代替普通程序员完成日常编程任务。

本文将分别介绍这两项成果。

OpenAI：AI 进军数学

根据 OpenAI 的介绍，他们的证明器使用语言模型来寻找形式陈述的证明。每次找到一个新的证明时，OpenAI 都会将其用作新的训练数据，用来改进神经网络，并使其能够通过迭代进而找到解决更难更复杂陈述的方案。

OpenAI 在 miniF2F 基准——一个具有挑战性的高中奥林匹克问题集合，测试中取得了目前的最先进的水平（41.2% vs 29.3%）。

OpenAI 的方法称之为陈述课程学习（statement curriculum learning），包括手动收集一组不同难度级别的陈述（没有证据），其中最难的陈述与OpenAI的目标基准相似。最初，OpenAI 的神经证明器能力很弱，只能证明其中的几个。

OpenAI 反复搜索新的证明，并在新发现的证明上重新训练 OpenAI 的神经网络，经过 8 次迭代，最终 OpenAI 的证明器在 miniF2F 上测试时表现的非常出色。

形式数学是一个令人兴奋的研究领域，首先因为它具有丰富性，让你可以证明需要推理、创造力和洞察力的任意定理；其次因为它与游戏的相似性——人工智能在游戏领域取得了惊人的成功——因为它用一种自动化的方式来确定证明是否成功（即，由形式系统验证）。

如下面的简单示例所示，证明形式陈述需要生成一系列证明步骤，每个证明步骤都包含对策略的调用。这些策略以数学术语作为论据，每个策略调用都会将当前要证明的陈述转换为更容易证明的陈述，直到没有任何东西可以证明。

图1 问题1

通过观察发现，在 OpenAI 的训练过程中出现了一种能力，即生成作为战术参数所需的原始数学术语。如果没有神经语言模型，这是无法完成的。下面的证明就是一个例子：证明步骤提出使用 n+1 作为解决方案（这完全由 OpenAI 的模型生成），其余的正式证明依靠 ring_exp 策略来验证它确实是有效的。

图2 问题2

OpenAI 还观察到，OpenAI 的模型和搜索程序能够生成链接多个非平凡推理步骤的证明。在下面的证明中，模型首先使用存在性陈述的对立。然后使用为它生成一个见证，并通过利用 norm_num 策略完成证明。

图3 问题3

OpenAI 的模型经过陈述课程学习训练，能够解决培训教科书和 AMC12 和 AIME 比赛中的各种问题，以及改编自 IMO 的 2 个问题。下面 OpenAI 展示此类生成证明的三个示例。

图4 问题4

图5 问题5

图6 问题6

形式数学涉及两个主要挑战，这使得强化学习的应用不太可能成功。

1）无限的动作空间：形式数学不仅有一个非常大的搜索空间（例如围棋），它还有一个无限的动作空间。在证明搜索的每一步，模型不是从行为良好的有限动作集中进行选择，而是必须从一组复杂且无限的策略中进行选择，其中涉及必须生成的外生数学术语（例如，生成用作见证的数学语句，诸如“存在一个 xx st ...”之类的步骤中使用的对象“，或作为剪切，证明中间引理引入和链接）。

2）缺乏自我博弈：与二人博弈相反，证明器不是与对手比赛，而是与一组要证明的陈述进行比赛。当面对一个太难的陈述时，没有明显的重构可以让证明器生成中间更容易首先解决的陈述。这种不对称性阻止了在二人博弈中成功的自我博弈算法的应用。

在 OpenAI 的工作中，通过在搜索证明时，从语言模型中采样动作来解决无限动作空间问题。语言模型能够生成策略调用以及通常需要作为参数的原始数学术语。

其次，OpenAI 观察到自我博弈在二人博弈中的关键作用是提供无监督的课程，以此作为解决缺乏自我博弈的基础，OpenAI 的方法建议用一组不同难度的辅助问题陈述（不需要证明）来代替这种无监督的课程。OpenAI 的经验表明，当这些辅助问题的难度足够多时，OpenAI 的训练程序能够解决越来越难的问题的课程，最终推广到 OpenAI 关心的问题集。

虽然这些结果非常令人兴奋，它们证明了深度学习模型在与正式系统交互时能够进行非凡的数学推理，但与这些比赛中最好的学生的表现相比，OpenAI 的方法还差的很远。

未来，OpenAI 希望，自己的工作能够激发该领域的研究，特别是针对 IMO 大挑战，与此同时，OpenAI 提出的陈述式课程学习方法，或将有助于加速自动化推理的总体进展。

DeepMind：写代码自动化更进一步

DeepMind 创建了一个名为 AlphaCode 的人工智能系统，该系统的“编程能力能与一般人类程序员相竞争”。

开发团队针对人类竞赛中使用的编程挑战题目测试了该人工智能系统，发现其程序达到了“预期的排名”，使其在人类程序员中排名前 54%。DeepMind 说，该系统的结果是朝着自主编程迈出的重要一步，尽管现在为止 AlphaCode 的能力不一定能代替普通程序员完成日常编程任务。

DeepMind 的首席研究科学家 OriolVinyals 通过电子邮件告诉 The Verge，研究仍处于早期阶段，但结果使公司更接近于创建一个灵活的、解决问题的人工智能——一个可以自主应对目前仅属于人类领域的编码挑战的程序。Vinyals 说：“从长远来看，我们对【AlphaCode】帮助程序员和非程序员编写代码、提高生产力或创建新的软件制作方法的潜力感到兴奋。”

AlphaCode 根据 Codeforces 策划的挑战进行了测试，Codeforces 是一个竞争性的编码平台，每周共享问题，并为编码人员发布类似于国际象棋中使用的 Elo 评级系统的排名。这些挑战不同于编码器在制作（例如商业应用程序）时可能面临的任务类型。它们更自成一体，需要更广泛地了解计算机科学的算法和理论概念。把它们想象成结合了逻辑、数学和编码专业知识的非常专业的谜题。

在 AlphaCode 测试的一个示例挑战中，要求竞争对手找到一种方法，使用有限的输入集将一串随机、重复的s和t字母转换为另一串相同的字母。例如，竞争对手不能只键入新字母，而是必须使用删除原始字符串中几个字母的“退格”命令。您可以阅读以下挑战的完整描述：

其中 10 个挑战以与人类完全相同的格式输入 AlphaCode。然后，AlphaCode 生成大量可能的答案，并像人类竞争对手一样通过运行代码和检查输出来筛选这些答案。“整个过程是自动的，无需人工选择最佳样本，”AlphaCode 论文的联合负责人 Yujia Li 和 David Choi 通过电子邮件告诉 The Verge。

AlphaCode 针对 Codeforces 网站上 5,000 名用户解决的 10 项挑战进行了测试。平均而言，它的排名在前 54.3%，DeepMind 估计这使该系统的 Codeforces Elo 为 1238，这使其在过去六个月中在该网站上竞争的用户中排名前 28%。

“我可以肯定地说 AlphaCode 的结果超出了我的预期，”Codeforces 创始人 Mike Mirzayanov 在 DeepMind 发布的一份声明中这样说。“我持怀疑态度，因为即使在简单的竞争问题中，通常不仅需要实现算法，更需要（这是最困难的部分）发明它。AlphaCode 成功地达到了一个有前途的、新竞争对手的水平。”

DeepMind 指出，AlphaCode 目前的技能仅适用于竞争性编程领域，但它的能力为创建未来工具打开了新大门，这些工具使编程更易于进行，并且有朝一日完全自动化。

许多其他公司正在开发类似的应用程序。例如，微软和 AI 实验室 OpenAI 已将后者的语言生成程序 GPT-3 改编为输出代码字符串的自动完成程序。（与 GPT-3 一样，AlphaCode 也基于称为 transformer 的 AI 架构，它特别擅长解析自然语言和代码这类顺序文本）。对于终端用户来说，这些系统就像 Gmail 的 Smart Compose 功能一样工作：为完成您正在编写的任何内容出谋划策。

近年来，人工智能编程系统的开发取得了很大进展，但这些系统还远未准备好接管人类程序员的工作。他们产出的代码通常有些问题，而且由于系统通常是在公共代码库上进行训练的，因此他们有时会“复制”受版权保护的材料。

在一项由代码存储库 GitHub 开发的名为 Copilot 的 AI 编程工具的研究中，研究人员发现其输出代码的大约 40% 包含安全漏洞。安全分析师甚至建议，不良行为者可以故意编写代码并与隐藏的在线后门共享代码，然后这些代码可能被用来训练人工智能程序，将这些错误插入到未来的程序中。

像这样的挑战意味着人工智能编程系统可能会慢慢融入程序员的工作中——从助手开始，他们的建议在能够被信任之前都将受到怀疑。换句话说：他们要向徒弟跟师傅一样接受专业程序员的训练。目前为止，这些 AI 编程系统正在飞快地学习。

点「在看」的人都变好看了哦！