计算机被用来验证数学证明已有一段时间了，但只有在使用专门设计的程序准备问题时才能这样做证明语言到这一点，无法处理数学符号和数学家使用的书面文本的混合。通过将自然语言编写的数学问题转换为形式代码，使计算机更容易解决这些问题，这可能有助于构建能够探索数学新发现的机器。这个过程称为形式化，但仅仅一个证明可能需要多年的工作，因此只有一小部分数学知识被形式化然后由机器证明。自动形式化是指将数学从自然语言自动翻译成形式语言的任务。成功的自动化形式化工具的实际和哲学意义是巨大的，它可以降低当前过度形式化的成本，并且从长远来看，可以将数学推理的自动化方面与各个研究领域联系起来。在最近的一项研究中，谷歌的吴宇怀和他的合作者使用OpenAICodex的神经网络进行自动化形式化工作。Codex已接受来自网络的大量文本和编程数据的培训，程序员可以使用这些数据生成可靠的代码。论文链接：https://arxiv.org/pdf/2205.12615.pdf最近将12,500个中学数学竞赛问题形式化为大型语言模型的一系列进展展示了模型理解形式语言的潜力。然而，现有的成功仅限于网络上存在大量语料库的正式语言（如Python）。相比之下，形式化的数学数据非常稀缺。ArchiveofFormalProofs是最大的形式化数学语言库之一，大小只有180mb，不到大型语言模型Codex训练数据的0.18%。此外，与自然语言文档字符串广泛可用的通用编程语言不同，自然语言和形式数学语言之间几乎没有对齐数据。因此，大规模语言模型的成功能否直接推动自动形式化的发展，还是一个未知数。鉴于证明语言和编程语言之间的相似性，该团队决定看看Codex是否可以形式化一个包含12,500个中学数学竞赛问题的库。它能够将四分之一的问题转换成与形式证明求解器Isabelle兼容的格式。吴说，许多不成功的转换是系统不理解某些数学概念的结果。“如果你用一个例子来解释这个概念，模型可以很快地掌握它。这项工作探索了大型语言模型自动形式化的前景，研究人员发现该模型已经具有相当好的能力，可以在交互式定理证明器中形式化自然语言数学。下面的图1是自动形式化的一个完美示例。该模型不仅可以翻译成句法正确的Isabelle代码，还可以掌握自然语言中的重要推理点。为了测试这种自动形式化器的功效，该团队随后将Codex应用于一组已经具有人类形式化版本的问题，Codex还为此生成了自己的形式化版本。该团队使用了另一种名为MiniF2F的AI来解决这两个版本的问题。自动形式化问题将MiniF2F的成功率从29%提高到35%，表明Codex在问题形式化方面取得了重要进展。值得注意的是，许多数学竞赛演示往往是这样的形式：要求一个人找到某个问题的答案，而不是证明一个给定的命题。然而，正式的数学陈述是命题的形式，而不是问题。为了将问题转化为命题，研究人员在问题后面附上了“TheFinalAnswer”：用于自动形式化的提示格式为：AI将与人类数学家竞争？这是一个有趣的发展，但吴说团队的工作只是概念证明。“如果目标是训练出可与人类顶尖数学家媲美的机器，那么自动形式化似乎是实现这一目标的关键途径。”剑桥大学团队成员AlbertJiang表示，如果成功率进一步提高，AI将能够与人类数学主场竞争。“如果我们达到100%，我们肯定会创造出在国际数学奥林匹克竞赛中赢得金牌的AI代理。”该团队的近期目标是改进自动化形式模型和自动化证明机，但研究成果的未来影响会更大。深刻的。吴说，这些模型可以揭示人类目前未知的数学领域。此类机器的推理能力也非常适合更广泛领域的验证任务。“你可以验证一个软件是否完全按照你想要的方式运行，或者你可以验证一个硬件芯片，因此它在金融交易算法和硬件设计中都有应用。”用机器探索数学是一个令人兴奋的发展，伦敦数学但真正的挑战，科学研究所的Yang-HuiHe说，是在主要用LaTex编写的数学研究中使用模型。“我们只使用LaTex，因为它是一种流畅的类型，但从某种意义上说，它是一种自然语言，它有自己的规则。He说，因为用户可以在LaTeX中定义他们自己的函数和符号，而这些函数和符号可能只用在数学论文中，这对于仅在纯文本上训练的神经网络来说可能很棘手。
