机器之心 道
研究者预估，如果达到 100% 的正确率水平，
计算机被用来验证数学证明已经有一段时间了，但它们只有在使用专门设计的证明语言准备问题时才能做到这一点，而无法处理数学符 和数学家使用的书面文本的混合体。
如果把用自然语言编写的数学问题转换为正式代码，让计算机更容易解决它们，或许能够帮助构建能探索数学新发现的机器。
这个过程被称为形式化（formalisation），但仅仅一个证明就可能需要数年的工作，因此只有一小部分数学知识被形式化，然后由机器证明。
自动形式化（Autoformalization）指的是自动从自然语言数学翻译成正式语言的任务。一个成功的自动形式化工具在实践和哲学上的意义都是巨大的，它可以减少目前过度的形式化成本，并且从长远来看，它可以连接各种研究领域数学推理的自动化方面。
论文链接：https://arxiv.org/pdf/2205.12615.pdf
将 12500 个中学数学竞赛问题形式化
大型语言模型的一系列最新进展展示了模型理解形式化语言的潜力。然而，现有的成功仅限于在 络上存在大量语料库的形式化语言 (例如 Python)。相比之下，形式化的数学数据非常缺乏，最大的形式化数学语言库之一 Archive of Formal Proofs 只有 180mb 大小，这还不到大语言模型 Codex 训练数据的 0.18% 。
此外，与通用编程语言的情况不同，自然语言文档字符串是广泛可用的，自然语言和形式化数学语言之间几乎没有对齐的数据。因此，大型语言模型的成功是否能直接促进自动形式化的发展，仍是未知的。
鉴于证明语言与编程语言有相似之处，因此该团队决定看看 Codex 是否可以将包含 12500 个中学数学竞赛问题的库形式化。它能够将四分之一的问题转换为与形式证明求解程序 Isabelle 兼容的格式。
Wu 表示，许多不成功的转换是系统不理解某些数学概念的结果。
这项工作探讨了大语言模型的自动形式化的前景，研究者发现大型语言模型已经在一个交互式定理证明器中具备相当好的形式化自然语言数学的能力。
下图 1 是一个完美的自动形式化示例。该模型不仅转换成了语法上正确的 Isabelle 代码，而且还能够掌握自然语言中的重要推理点。
为了测试这种自动形式化程序的效力，团队随后又将 Codex 应用于一组已经有人类形式化版本的问题，Codex 也为这些问题生成了自己的形式化版本。团队使用了另一个名为 MiniF2F 的 AI 来解决这两个版本的问题。
自动形式化的问题将 MiniF2F 的成功率从 29% 提高到了 35%，这表明 Codex 在问题形式化方面取得了重要进展。
值得注意的是，许多数学竞赛的陈述往往是这样一种形式：一个人被要求找到某个问题的答案，而不是证明一个给定的命题。然而形式化的数学陈述是以命题的形式，而不是以问题的形式。
为了把一个问题转换成一个命题，研究者在问题后面附上了:
用来进行自动形式化的 prompt 格式是：
AI 将与人类数学家竞争？
这是一项有趣的进展，但 Wu 表示团队的工作只是一个概念证明。
剑桥大学团队成员 Albert Jiang 表示，如果进一步提高成功率，AI 将能够与人类数学家竞争。
团队近期的目标是改进自动形式化模型和自动化证明机器，但研究成果的未来影响将会更深远。Wu 表示，这些模型可以揭示人类目前未知的数学领域。
这种机器的推理能力也非常适合更广泛领域的验证任务。
利用机器探索数学是一个令人兴奋的发展，伦敦数学科学研究所的 Yang-Hui He 说，但真正的挑战是在大部分是用 LaTex 编写的数学研究中使用该模型。
He 说，因为用户可以在 LaTeX 中定义自己的函数和符 ，这些函数和符 可能只在一篇数学论文中使用，这对于仅在纯文本上训练过的神经 络来说可能很棘手。
参考链接: https://www.newscientist.com/article/2322999-ai-translates-maths-problems-into-code-to-make-them-easier-to-solve/#ixzz7VmyPBQM7
声明：本站部分文章及图片源自用户投稿，如本站任何资料有侵权请您尽早请联系jinwei@zod.com.cn进行处理,非常感谢！