卷起来了！AI版程序员上线，当天奥数“题霸”解决方案也来了( 二 ) 机器之心报道编辑：张倩、蛋

文章图片
总体来说， AlphaCode的排名在竞争对手中大致相当于中位数。虽然远远没能赢得比赛，但这个结果代表了人工智能解决问题能力的实质性飞跃。这一进步证明了深度学习模型在需要批判性思维的任务中的潜力。 DeepMind指出， AlphaCode目前的技能组合目前仅适用于竞赛性质的编程领域，但它的能力为创建未来工具打开了新的大门，这些工具使编程变得更加容易，并且有朝一日完全自动化。
许多其他公司正在开发类似的应用程序。对于终端的用户来说，这些系统就像Gmail的SmartCompose功能一样工作，提供一些关于你正在编写的任何内容的建议。
近年来， AI编程系统的开发取得了很大进展，但这些系统还远未准备好接管人类程序员的工作。他们生成的代码通常有问题，而且由于系统通常是在公共代码库上进行训练的，所以有时会复制受版权保护的材料。
在一项关于GitHubCopilotAI编程工具的研究中，研究人员发现其输出的代码约有40%包含安全漏洞。安全分析师甚至建议，不良行为者可以故意编写代码并与隐藏的后门（backdoor）在线共享代码，然后这些代码可能被用来训练AI程序，将这些错误插入到未来的程序中。
像这样的挑战意味着AI编程系统可能会慢慢融入程序员的工作中——换句话说，他们要进行学徒训练，从助理开始做起，在被信任能够自主执行工作之前， AI给出的建议都要受到怀疑。

文章图片
目前， DeepMind已在GitHub上发布了竞赛级编程问题和解决方案的数据集，其中也包括广泛的测试的数据，以确保通过这些测试的程序是正确的，这是目前数据集所缺乏的一个关键特性。 DeepMind希望这个基准能够推动在解决问题和代码生成方面的进一步创新。
GitHub项目地址：https://github.com/deepmind/code_contests
挑战奥数题的神经定理证明器
在学科竞赛领域，国际数学奥林匹克竞赛（IMO）是非常有名的一个，我们熟悉的很多数学大神（如韦东奕）都在这一竞赛中取得了骄人的成绩。
2021年，这项比赛迎来了一个微小的变化：微软研发多年的数学AI——Lean也加入了竞争，和人类选手一决高下。据悉， Lean是微软研究院在2013年推出的计算机定理证明器：数学家可以把数学公式转换成代码，再输入到Lean中，让程序来验证定理是否正确。
由于Lean剑指金牌，研究人员一直在对其进行不停的打磨，其中也包括被微软收购了的OpenAI 。刚刚， OpenAI发文表示，他们已经为Lean创建了一个神经定理证明器，用于解决各种具有挑战性的高中奥林匹克问题，包括两个改编自IMO的问题和来自AMC12、AIME竞赛的若干问题。
该证明器使用一个语言模型来寻找形式化命题（formalstatement）的证明。每次发现一个新的证明，研究者就把它作为新的训练数据，这改善了神经网络，使它能够在迭代中找到越来越难的命题的解决方案。
该证明器在miniF2F基准测试中实现了SOTA（41.2%vs29.3%）水平， miniF2F包含一组具有挑战性的高中奥林匹克问题。
研究者将他们的方法称为statementcurriculumlearning ，该方法包括手动收集的一组不同难度级别的命题（无需证明），其中最难的命题类似于目标基准。最初，他们的神经证明器很弱，只能证明其中的几个。因此，他们迭代地搜索新的证明，并在新发现的证明上重新训练他们的神经网络。经过8次迭代，他们的证明器在miniF2F上取得了出色的成绩。