2022年开年不久,全球人工智能领域两大明星公司不约而同在今天宣布了重要进展:OpenAI称自己构建了一个神经定理证明器,该证明器学会了解决各种具有挑战性的高中数学问题,包括AMC12和AIME比赛的问题,以及改编自IMO的两个问题。DeepMind则表示,由其开发的名为AlphaCode的人工智能系统,该系统的“编程能力能与一般人类程序员相竞争”。
OpenAI的介绍,他们的证明器使用语言模型来寻找形式陈述的证明。每次找到一个新的证明时,OpenAI都会将其用作新的训练数据,用来改进神经网络,并使其能够通过迭代进而找到解决更难更复杂陈述的方案。OpenAI在miniF2F基准——一个具有挑战性的高中奥林匹克问题集合,测试中取得了目前的最先进的水平(41.2% vs 29.3%)。
DeepMind创建了一个名为AlphaCode的人工智能系统,该系统的“编程能力能与一般人类程序员相竞争”。开发团队针对人类竞赛中使用的编程挑战题目测试了该人工智能系统,发现其程序达到了“预期的排名”,使其在人类程序员中排名前54%。DeepMind说,该系统的结果是朝着自主编程迈出的重要一步,尽管现在为止AlphaCode的能力不一定能代替普通程序员完成日常编程任务。