将数学题转化成代码，谷歌这项研究让机器证明的正确率大幅提高

机器之心报道
编辑：蛋酱
研究者预估，如果达到100%的正确率水平，「我们肯定会创造出赢得国际数学奥林匹克金牌的AI智能体。」
【将数学题转化成代码，谷歌这项研究让机器证明的正确率大幅提高】计算机被用来验证数学证明已经有一段时间了，但它们只有在使用专门设计的证明语言准备问题时才能做到这一点，而无法处理数学符号和数学家使用的书面文本的混合体。
如果把用自然语言编写的数学问题转换为正式代码，让计算机更容易解决它们，或许能够帮助构建能探索数学新发现的机器。
这个过程被称为形式化（formalisation），但仅仅一个证明就可能需要数年的工作，因此只有一小部分数学知识被形式化，然后由机器证明。
自动形式化（Autoformalization）指的是自动从自然语言数学翻译成正式语言的任务。一个成功的自动形式化工具在实践和哲学上的意义都是巨大的，它可以减少目前过度的形式化成本，并且从长远来看，它可以连接各种研究领域数学推理的自动化方面。
在最近的一项研究中，谷歌的YuhuaiWu与其合作者使用OpenAICodex的神经网络进行自动形式化工作。 Codex已经接受了来自网络的大量文本和编程数据的训练，程序员可以使用它来生成可靠的代码。

文章图片
论文链接：https://arxiv.org/pdf/2205.12615.pdf
将12500个中学数学竞赛问题形式化
大型语言模型的一系列最新进展展示了模型理解形式化语言的潜力。然而，现有的成功仅限于在网络上存在大量语料库的形式化语言(例如Python) 。相比之下，形式化的数学数据非常缺乏，最大的形式化数学语言库之一ArchiveofFormalProofs只有180mb大小，这还不到大语言模型Codex训练数据的0.18% 。
此外，与通用编程语言的情况不同，自然语言文档字符串是广泛可用的，自然语言和形式化数学语言之间几乎没有对齐的数据。因此，大型语言模型的成功是否能直接促进自动形式化的发展，仍是未知的。
鉴于证明语言与编程语言有相似之处，因此该团队决定看看Codex是否可以将包含12500个中学数学竞赛问题的库形式化。它能够将四分之一的问题转换为与形式证明求解程序Isabelle兼容的格式。
Wu表示，许多不成功的转换是系统不理解某些数学概念的结果。「如果你用一个解释这个概念的例子来展示模型，那么模型就可以快速掌握它。」
这项工作探讨了大语言模型的自动形式化的前景，研究者发现大型语言模型已经在一个交互式定理证明器中具备相当好的形式化自然语言数学的能力。
下图1是一个完美的自动形式化示例。该模型不仅转换成了语法上正确的Isabelle代码，而且还能够掌握自然语言中的重要推理点。

文章图片
为了测试这种自动形式化程序的效力，团队随后又将Codex应用于一组已经有人类形式化版本的问题， Codex也为这些问题生成了自己的形式化版本。团队使用了另一个名为MiniF2F的AI来解决这两个版本的问题。
自动形式化的问题将MiniF2F的成功率从29%提高到了35% ，这表明Codex在问题形式化方面可以比人类做得更好。

文章图片
值得注意的是，许多数学竞赛的陈述往往是这样一种形式：一个人被要求找到某个问题的答案，而不是证明一个给定的命题。然而形式化的数学陈述是以命题的形式，而不是以问题的形式。