将数学题转化成代码，谷歌这项研究让机器证明的正确率大幅提高( 二 ) 机器之心报道编辑：蛋酱研究

为了把一个问题转换成一个命题，研究者在问题后面附上了「TheFinalAnswer」:
用来进行自动形式化的prompt格式是：

文章图片
AI将与人类数学家竞争？
这是一项有趣的进展，但Wu表示团队的工作只是一个概念证明。「如果目标是训练一台媲美最顶级人类数学家的机器，那么自动形式化似乎是实现这个目标的关键道路。」
剑桥大学团队成员AlbertJiang表示，如果进一步提高成功率， AI将能够与人类数学家竞争。「如果我们达到了100%的水平，我们肯定会创造出赢得国际数学奥林匹克金牌的AI智能体。」
团队近期的目标是改进自动形式化模型和自动化证明机器，但研究成果的未来影响将会更深远。 Wu表示，这些模型可以揭示人类目前未知的数学领域。
这种机器的推理能力也非常适合更广泛领域的验证任务。「你可以验证一个软件是否完全按照你的要求做，或者可以验证硬件芯片，因此它在金融交易算法和硬件设计中都会有所应用。」
利用机器探索数学是一个令人兴奋的发展，伦敦数学科学研究所的Yang-HuiHe说，但真正的挑战是在大部分是用LaTex编写的数学研究中使用该模型。「我们只用LaTex是因为它打字顺畅，但它在某种意义上是一种自然语言，也有自己的规则。」
He说，因为用户可以在LaTeX中定义自己的函数和符号，这些函数和符号可能只在一篇数学论文中使用，这对于仅在纯文本上训练过的神经网络来说可能很棘手。
参考链接:https://www.newscientist.com/article/2322999-ai-translates-maths-problems-into-code-to-make-them-easier-to-solve/#ixzz7VmyPBQM7