作者刘媛媛，LZM
2022年初不久，全球人工智能领域的两家明星公司今天宣布了重要进展:OpenAI声称已经构建了一个神经定理证明器，它学会了解决各种具有挑战性的高中数学问题，包括AMC12和AIME竞赛的问题，以及改编自IMO的两个问题。
DeepMind表示，其开发的名为AlphaCode的人工智能系统“在编程能力上可以与普通人类程序员相媲美”。DeepMind表示，这个系统的结果是迈向独立编程的重要一步，尽管到目前为止，AlphaCode的能力可能无法取代普通程序员完成日常编程任务。
本文将分别介绍这两项成果。
1 OpenAI进军“数学的AI”[S2/]
根据OpenAI的说法，他们的证明者使用语言模型来寻找形式语句的证明。每次发现新的证明，OpenAI都会将其作为新的训练数据来改进神经网络，并使其能够通过迭代找到更困难、更复杂语句的解决方案。
OpenAI在高中奥数挑战集合miniF2F benchmark的测试中取得了最先进的水平(41.2% vs 29.3%)。
OpenAI的方法叫做语句课程学习，包括人工收集一组不同难度级别的语句(无需证据)，其中最难的语句与OpenAI的目标基准相似。起初，OpenAI的神经证明程序很弱，只有少数可以被证明。
OpenAI反复搜索新的证明，在新发现的证明上重新训练OpenAI的神经网络。经过八次迭代，最后，OpenAI的证明者在miniF2F上测试时表现非常好。
形式数学是一个令人兴奋的研究领域。首先，因为它的丰富性，你可以证明任何需要推理、创造力和洞察力的定理。其次，由于其与游戏的相似性——人工智能在游戏领域取得了惊人的成功——因为它使用了一种自动化的方式来确定证明是否成功(即通过形式系统验证)。
如下面的简单示例所示，正式的证明语句需要生成一系列证明步骤，每个步骤都包含对策略的调用。这些策略是基于数学术语的，每个策略调用都会把要证明的语句变成更容易证明的语句，直到什么都证明不了。
图1问题1
通过观察发现，在OpenAI的训练过程中，有一种能力，就是生成作为战术参数所需的原始数学项。没有神经语言模型，这是做不到的。下面的证明就是一个例子:证明步骤提出使用n+1作为解(完全由OpenAI的模型生成)，其余的形式证明依靠ring_exp策略验证确实有效。
图2问题2
OpenAI还观察到，OpenAI的模型和搜索程序可以生成链接多个非平凡推理步骤的证明。在下面的证明中，模型首先使用存在陈述的对立。然后使用为其生成一个见证，并通过使用norm_num策略完成证明。
图3问题3
OpenAI的模型可以解决培训教材和AMC12、AIME比赛中的各种问题，以及IMO通过演示课程学习和培训改编的两个问题。下面的OpenAI展示了这种生成的证明的三个例子。
图4问题4
图5问题5
图6问题6
形式数学涉及两个主要挑战，这使得强化学习的应用不太可能成功。
1)无限作用空区间:形式数学不仅有非常大的搜索空区间(如Go)，还有无限作用空区间。在证明搜索的每一步，模型不是从有限的行为良好的动作集合中进行选择，而是必须从复杂的、无限的策略集合中进行选择，这些策略集合涉及必须生成的外生数学术语(例如，生成用作见证的数学陈述，如“有一个xx st...步骤”中使用的对象，或切割、引入和链接证明的中间引理)。
2)缺乏自我博弈:与二人博弈相反，证明者不与对手竞争，而是与一组待证明的陈述竞争。当面对一个太难的语句时，没有明显的重构来使证明者生成一个更容易在中间首先解决的语句。这种不对称性阻碍了自博弈算法在双人博弈中的成功应用。
在OpenAI的工作中，无限动作空之间的问题是通过在搜索证明时从语言模型中采样动作来解决的。该语言可以生成策略调用和通常需要作为参数的原始数学术语。
其次，OpenAI观察到，双人游戏中自我游戏的关键作用是提供无监督的课程，作为解决自我游戏缺失的基础。OpenAI的方法建议用一组不同难度的辅助问题语句(无需证明)来代替这种无监督的课程。OpenAI的经验表明，当这些辅助问题足够困难时，OpenAI的训练程序可以解决越来越难的问题，最后扩展到OpenAI关心的问题集。
虽然这些结果非常令人兴奋，证明了深度学习模型在与形式系统交互时可以进行非凡的数学推理，但与这些竞赛中最优秀学生的表现相比，OpenAI的方法还远远不够完美。
在未来，OpenAI希望其工作可以刺激该领域的研究，特别是针对IMO的挑战。同时，OpenAI提出的语句课程学习方法可能有助于加速自动推理的整体进度。
2 DeepMind:用AI代替“程序员”[/s2/]
DeepMind创造了一个名为AlphaCode的人工智能系统，该系统“在编程能力上可以与普通人类程序员相媲美”。
开发团队针对人类使用的编程挑战对人工智能系统进行了测试，发现其程序达到了“预期排名”，使其跻身于人类程序员中的前54%。DeepMind表示，这个系统的结果是迈向独立编程的重要一步，尽管到目前为止，AlphaCode的能力可能无法取代普通程序员完成日常编程任务。
DeepMind的首席研究科学家OriolVinyals通过电子邮件告诉The Verge，这项研究仍处于早期阶段，但这一结果使该公司更接近于创造一种灵活和解决问题的人工智能——一种可以独立应对目前只属于人类领域的编码挑战的程序。Vinyals说:“从长远来看，我们对AlphaCode帮助程序员和非程序员编写代码、提高生产率或创造新的软件生产方法的潜力感到兴奋。”
根据竞争性编码平台Codeforces计划的挑战对代码进行测试，每周分享问题，并为编码员发布排名，类似于国际象棋中使用的Elo评级系统。这些挑战不同于编码器在制作时可能面临的任务类型(如商业应用)。他们比较自成体系，需要了解更多计算机科学的算法和理论概念。把它们想成是结合了逻辑、数学和编码专业知识的非常专业的谜题。
在AlphaCode测试的一个示例挑战中，参赛者需要找到一种方法，将一串随机重复的S和T字母转换为另一串输入集有限的相同字母。例如，参赛者不能只输入新字母，而必须使用“退格”命令从原字符串中删除几个字母。您可以阅读以下挑战的完整描述:
这些挑战中有10个以与人类完全相同的格式输入AlphaCode。然后，AlphaCode生成大量可能的答案，并像人类竞争对手一样，通过运行代码和检查输出来过滤它们。"整个过程是自动的，不需要手动选择最好的样品."AlphaCode论文的联合负责人鱼枷·李和大卫·崔通过电子邮件告诉The Verge。
Codeforces网站上的5，000名用户测试了10个挑战。平均而言，它排名前54.3%，DeepMind估计这使得系统的Codeforces Elo为1238，这使得它在过去6个月内在网站上竞争的用户中排名前28%。
“我可以肯定地说，AlphaCode的结果超出了我的预期，”Codeforces的创始人迈克·米尔扎亚诺夫(Mike Mirzayanov)在DeepMind发布的一份声明中表示。“我持怀疑态度，因为即使在简单的竞赛问题中，通常也不仅需要实现算法，还需要(这是最难的部分)发明算法。代码已经成功达到了一个有前途的新竞争者的水平。”
DeepMind指出，AlphaCode目前的技能只适用于竞技编程领域，但它的能力为创造未来的工具打开了一扇新的大门，这将使编程变得更容易，并有一天实现完全自动化。
许多其他公司正在开发类似的应用程序。例如，微软和人工智能实验室OpenAI将后者的语言生成器GPT-3改编为自动完成程序，输出代码字符串。(与GPT-3一样，AlphaCode基于名为transformer的人工智能架构，尤其擅长解析自然语言和代码等顺序文本)。对于最终用户来说，这些系统的工作方式就像Gmail的智能写作功能:为你正在写的任何东西提供建议。
近年来，人工智能编程系统的发展取得了很大进展，但这些系统还远远没有准备好接管人类程序员的工作。他们产生的代码通常会有一些问题，而且由于系统通常是在公共代码库中训练的，他们有时会“复制”有版权的材料。
在对代码库GitHub开发的名为Copilot的AI编程工具的研究中，研究人员发现其约40%的输出代码包含安全漏洞。安全分析师甚至建议，不良演员可以故意编写代码，并与隐藏的在线后门共享，然后这些代码可能被用来训练人工智能程序，并将这些错误插入未来的程序中。
像这样的挑战意味着人工智能编程系统可能会逐渐融入程序员的工作中——从助手开始，他们的建议会被怀疑，直到可以信任。换句话说，他们应该像学徒和师傅一样接受专业程序员的培训。到目前为止，这些人工智能编程系统正在快速学习。
