自动形式化（Autoformalization）指的是自动从自然语言数学翻译成正式语言的任务。一个成功的自动形式化工具在实践和哲学上的意义都是巨大的，它可以减少目前过度的形式化成本，并且从长远来看，它可以连接各种研究领域数学推理的自动化方面。

在最近的一项研究中，谷歌的 Yuhuai Wu 与其合作者使用 OpenAI Codex 的神经网络进行自动形式化工作。Codex 已经接受了来自网络的大量文本和编程数据的训练，程序员可以使用它来生成可靠的代码。

论文链接：

https://arxiv.org/pdf/2205.12615.pdf

这项工作探讨了大语言模型的自动形式化的前景，研究者发现大型语言模型已经在一个交互式定理证明器中具备相当好的形式化自然语言数学的能力。

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

内容中包含的图片若涉及版权问题，请及时与我们联系删除