ACM通信
ACM TechNews
人工智能将数学问题转化为代码，使它们更容易解决
Codex神经网络被要求将12500个中学数学竞赛问题正式化，它能够将四分之一的问题转换成与伊莎贝尔正式证明求解程序兼容的格式。
来源:alengo /盖蒂图片社
谷歌的吴玉怀和同事使用人工智能(AI)研究公司OpenAI的Codex神经网络将数学问题从简单的英语转化为正式的代码。
Codex正确地将12500个中学数学竞赛问题中的25%翻译成一种与正式的证明求解程序Isabelle兼容的格式。
吴说，该系统无法理解某些数学概念是许多翻译失败的原因。
然后，该团队通过将Codex应用于人类预先确定的问题来测试这一过程。
该网络产生了自己的正式版本，研究人员使用MiniF2F AI解决了两个版本;自动正式化版本将MiniF2F的成功率从29%提高到35%，表明Codex的正式化优于人类。
从《新科学家》
查看全文
版权所有©2022SmithBucklin美国华盛顿特区
没有发现记录