作者 | 刘媛媛、LZM

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

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

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

1 OpenAI进军「AI for 数学」

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

图1 问题1

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

图3 问题3

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

图4 问题4

其中 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 编程系统正在飞快地学习。

花粉社群VIP加油站