访问： 阿里云复工专属福利首购1元起 如果把用自然语言编写的数学问题转换为正式代码，让计算机更容易解决它们，或许能够帮助构建能探索数学新发现的机器。 这个过程被称为形式化（formalisation），但仅仅一个证明就可能需要数年的工作，因此只有一小部分数学知识被形式化，然后由机器证明。 自动形式化（Autoformalization）指的是 自动从自然语言数学翻译成正式语言的任务 。一个成功的自动形式化工具在实践和哲学上的意义都是巨大的，它可以减少目前过度的形式化成本，并且从长远来看，它可以连接各种研究领域数学推理的自动化方面。 在最近的一项研究中，Google的 Yuhuai Wu 与其合作者 使用 OpenAI Codex 的神经网络进行自动形式化工作 。Codex 已经接受了来自网络的大量文本和编程数据的训练，程序员可以使用它来生成可靠的代码。 论文链接：https://arxiv.org/pdf/2205.12615.pdf 将 12500 个中学数学竞赛问题形式化 大型语言模型的一系列最新进展展示了模型理解形式化语言的潜力。然而，现有的成功仅限于在网络上存在大量语料库的形式化语言 (例如 Python)。相比之下，形式化的数学数据非常缺乏，最大的形式化数学语言库之一 Archive of Formal Proofs 只有 180mb 大小，这还不到大语言模型 Codex 训练数据的 0.18% 。 此外，与通用编程语言的情况不同，自然语言文档字符串是广泛可用的，自然语言和形式化数学语言之间几乎没有对齐的数据。因此，大型语言模型的成功是否能直接促进自动形式化的发展，仍是未知的。 鉴于证明语言与编程语言有相似之处，因此该团队决定看看 Codex 是否可以将包含 12500 个中学数学竞赛问题的库形式化。它能够将四分之一的问题转换为与形式证明求解程序 Isabelle 兼容的格式。 Wu 表示，许多不成功的转换是系统不理解某些数学概念的结果。“如果你用一个解释这个概念的例子来展示模型，那么模型就可以快速掌握它。” 这项工作探讨了大语言模型的自动形式化的前景，研究者发现大型语言模型已经在一个交互式定理证明器中具备相当好的形式化自然语言数学的能力。 下图 1 是一个完 美的 自动形式化示例。该模型不仅转换成了语法上正确的 Isabelle 代码，而且还能够掌握自然语言中的重要推理点。 为了测试这种自动形式化程序的效力，团队随后又将 Codex…
阅读更多（Read More）