太厉害了！在中国庆祝春节之际，两家知名人工智能研究机构DeepMind和OpenAI分别发布了重要研究成果：DeepMind发布了基于Transformer模型的AlphaCode，可以编写出与人类媲美的计算机程序；同时，OpenAI开发的神经定理证明器成功解决了两项国际奥林匹克难题。是不是觉得这两个被AI征服的领域似曾相识？没错，2021年，OpenAI发布了AI代码补全工具GitHubCopilot，并公布了其背后的技术CodeX。同样，在去年下半年，DeepMind也公布了他们在解决数学问题方面的AI研究成果，并登上了Nature。虽然两家研究机构的新成果为AI解决老问题提供了新思路，但网友们不得不感叹AI领域太复杂了！来源：网友微博截图AlphaCode击败46%的参与者在最近的一篇论文中，DeepMind研究人员介绍了AlphaCode。AlphaCode使用基于Transformer的语言模型来实现大规模代码生成并将其编写为程序。论文链接：https://storage.googleapis.com/deepmind-media/AlphaCode/competition_level_code_generation_with_alphacode.pdf研究人员在Codeforces挑战赛中测试了AlphaCode，这是一个类似于国际象棋中使用的Elo评分系统的竞争性编程平台，分享了编程挑战和问题每周排名。与程序员在构建业务应用程序时可能面临的任务不同，Codeforces的挑战更加独立，需要对计算机科学中的算法和理论概念有更广泛的理解，通常是逻辑、数学和编码专业知识的非常专业的组合问题.AlphaCode在Codeforces网站上针对5,000名用户解决的10项挑战进行了测试，总体排名前54.3%，这意味着它击败了46%的参赛者。DeepMind估计AlphaCode系统的CodeforcesElo为1238，在过去六个月内在该网站上竞争的用户中排名前28%。例如，在测试AlphaCode的挑战中，参赛者被要求找到一种方法，使用一组有限的输入将随机重复的s和t字母字符串转换为另一个相同字母的字符串。例如，参赛者不能只输入新字母，而必须使用“退格”命令从原始字符串中删除几个字母。对于AlphaCode，这些只是中等难度的挑战：其中十个以与人类完全相同的格式输入AlphaCode。然后，AlphaCode生成大量可能的答案，它通过运行代码和检查输出来筛选这些答案，就像人类竞争对手一样。“整个过程是自动的，无需手动选择最佳样本，”AlphaCode论文的联合负责人YujiaLi和DavidChoi说。在Codeforces挑战赛中脱颖而出并非易事。AlphaCode项目是两年多前启动的。随着大规模Transformer模型结合大规模采样和过滤技术的进步，DeepMind研究人员在AI可以解决的问题数量上取得了显着进步。受疫情影响，项目的大部分工作都是在家里完成的。研究人员在选定的公共GitHub代码上对模型进行了预训练，并在相对较小的竞赛编程数据集上对其进行了微调。在评估期间，研究人员为每个问题创建了大量的C++和Python程序，比之前的工作大了几个数量级。然后对这些解决方案进行筛选、聚类和重新排序，分配给一小组10个候选程序，并提交进行外部评估。这个自动化系统取代了竞争对手调试、编译、通过测试、最后提交的试错过程。总体而言，AlphaCode的排名大致相当于其竞争对手的中位数。虽然远未赢得比赛，但结果代表了人工智能解决问题能力的重大飞跃。这一进步展示了深度学习模型在需要批判性思维的任务中的潜力。DeepMind指出，AlphaCode目前的技能组合目前仅在竞争激烈的编程领域可用，但它的功能为创建未来工具打开了新的大门，这些工具可以使编程变得更容易，并有朝一日实现完全自动化。许多其他公司正在开发类似的应用程序。对于最终用户，这些系统的工作方式类似于Gmail的智能撰写功能，可为您撰写的内容提供建议。近年来，人工智能编程系统的发展取得了长足的进步，但这些系统还远未准备好接管人类程序员的工作。他们生成的代码经常有错误，而且由于系统经常在公共代码库上进行训练，因此有时会复制受版权保护的材料。在对GitHub的CopilotAI编程工具的研究中，研究人员发现其输出的代码中约有40%包含安全漏洞。安全分析师甚至建议，不良行为者可以故意编写代码并通过隐藏的后门在线共享，然后可以使用这些代码来训练AI程序，将这些错误插入到未来的程序中。像这样的挑战意味着人工智能编程系统可能会慢慢融入程序员的工作——换句话说，他们是学徒，从助手开始，然后才被信任自主执行工作，因为这些建议要被怀疑地看待.目前，DeepMind在GitHub上发布了竞赛级别的编程问题和解决方案数据集，其中还包括大量的测试数据，以确保通过这些测试的程序是正确的，这是当前数据集的关键不足。特征。DeepMind希望这个基准能够推动问题解决和代码生成方面的进一步创新。GitHub项目地址：https://github.com/deepmind/code_contests挑战奥林匹克题的神经定理证明器在学科竞赛领域，国际数学奥林匹克竞赛（I??MO）是一个非常著名的竞赛项目。东一）在本次比赛中取得了骄人的成绩。2021年，比赛迎来了细微的变化：微软研发多年的数学AILean也加入了比赛，与人类选手一较高下。据悉，Lean是微软研究院2013年推出的一款计算机定理证明器：数学家可以将数学公式转化为代码，然后输入Lean，让程序验证定理是否正确。自精益瞄准金牌以来，研究人员一直在对其进行打磨，包括被微软收购的OpenAI。刚刚，OpenAI发文称，他们已经为Lean创建了一个神经定理证明器，用于解决各种具有挑战性的高中奥林匹克问题，其中有两个改编自IMO，还有几个来自AMC12和AIME竞赛的问题。证明者使用语言模型来寻找形式陈述的证明。每次发现新的证据时，研究人员都会将其用作新的训练数据，从而改进神经网络，使其能够迭代地找到解决难度越来越大的命题的方法。证明者在miniF2F基准测试中达到了SOTA（41.2%对29.3%）的水平，该基准测试由一组具有挑战性的高中奥林匹克问题组成。研究人员将他们的方法称为课程学习，它由一组手动收集的不同难度级别的命题组成（无需证明），其中最难的命题与目标基准相似。最初，他们的神经证明器很弱，只能证明其中的几个。因此，他们反复搜索新的证据，并根据新发现的证据重新训练他们的神经网络。经过8次迭代，他们的证明者在miniF2F上取得了优异的成绩。形式数学（formalmathematics）是一个令人兴奋的研究领域，因为：1）它内容丰富，可以让你证明需要推理、创造力和洞察力的任意定理；自动确定证明是否成立（即由正式系统验证）的方法。如下图的例子所示，证明一个形式命题需要生成一系列的证明步骤，每个证明步骤都涉及对一个策略的调用。正式系统接受的工件是低级的（如汇编代码），人类很难生成。该策略是从更高级别的指令中生成此类工件的搜索过程，以帮助形式化。这些策略以数学术语作为参数，每次策略调用都会将当前要证明的命题转换为更容易证明的命题，直到没有任何东西需要证明。研究人员观察到，在训练过程中出现了生成策略参数所需的原始数学术语的能力，如果没有神经语言模型，这是不可能的。下面的证明就是它的一个例子：证明步骤“usen+1”（完全由模型生成）建议使用“n+1”作为解决方案，其余形式证明依赖于“ring_exp”验证它的策略它确实有效。研究人员还观察到，他们的模型和搜索过程能够产生连接多个重要推理步骤的证据。在下面的证明中，模型首先使用导致存在性陈述的对立(?(x:?),fx≠a*x+b)。然后它使用use(0:?)为它生成一个见证，并通过利用norm_num策略完成证明。该模型使用语句课程学习进行训练，以解决训练文本以及AMC12和AIME中的各种问题，以及从IMO改编的两个问题。以下是三个相关示例。形式数学涉及两大挑战，使得纯强化学习应用不太可能成功：1.无限行动空间：形式数学不仅具有非常大的搜索空间（如围棋），而且还有无限的行动空间。在寻找证明的每一步，模型不是从有限的行为良好的集合中选择的，而是从复杂和无限的策略集合中选择的，这些策略涉及必须生成的外生数学项（例如，生成数学命题用作证人）。2.缺乏自我博弈：与双人博弈相反，证明者不是与对手博弈，而是与一系列命题进行博弈来证明。当面对一个过于困难的命题时，没有明显的重构可以让证明者首先生成更易处理的中间语句。这种不对称性阻碍了在双人游戏中取得成功的自我博弈算法的简单应用。在这项工作中，研究人员通过从语言模型中采样动作来解决无限动作空间问题。语言模型能够生成策略调用和通常需要作为参数的原始数学术语。在没有自我博弈的情况下，他们观察到自我博弈在双人游戏中的关键作用是提供无监督的课程。因此，他们建议用一组不同难度的辅助问题命题（不需要证明）来代替这种无监督课程。他们的实验结果表明，当这些辅助问题的难度变化足够大时，他们的训练过程能够解决一系列难度越来越大的问题，最终泛化到他们关心的问题集。虽然这些结果非常令人兴奋，因为它们表明深度学习模型在与正式系统交互时能够进行重要的数学推理，但证明者远非竞赛中学生表现最好。研究人员表示，他们希望他们的工作能够推进这一领域的研究，特别是对于IMO，他们提出的语句课程学习方法将加速自动推理方面的研究进展。总结两家机构的最新研究成果相继出台，网上也出现了零星的评价：如果一个AI研究科学家发一系列长推文，AlphaCode要几年才能达到人类水平。排名有局限性，因为许多参与者是高中生或大学生；事实上，AlphaCode生成的绝大多数程序都是错误的，通过示例测试过滤AlphaCode实际上解决了一些问题。也有研究人员表示，这似乎是AlphaStar努力创造奇迹的结果。国内的AI从业者可以利用假期研究这两项研究，发表自己的看法。
