点击上方“用机器智能”，选择“明星”公众号

尽快获取有价值的内容

出自：机器之心

谷歌的托尼·吴（Tony Wu）等研究人员设计了一种名为“草稿、证明”（DSP）的新方法，将非正式的数学证明转换为正式的证明。 实验结果表明，自动验证机解决问题的比例从20.9%提高到38.9%。

自动证明数学定理是人工智能的初衷，也一直是一个难题。 到目前为止，人类数学家已经使用了两种不同的数学书写方式。

第一个是大家都熟悉的方法，就是用自然语言来描述数学证明。 大多数数学都是这样写的，包括数学课本、数学论文等。

第二种称为形式数学（ ）。 这是计算机科学家在过去半个世纪中创建的用于检查数学证明的工具。

如今，计算机似乎可以用来验证数学证明，但只有使用专门设计的证明语言才能做到这一点，并且无法处理数学符号和数学家使用的书面文本的混合。 将用自然语言编写的数学问题转换为正式代码，以便计算机可以更轻松地解决它们，可能有助于构建能够探索数学新发现的机器。 这个过程称为形式化（），自动形式化（）是指自动将数学从自然语言翻译为形式语言的任务。

形式证明的自动化是一项具有挑战性的任务，深度学习方法在这一领域尚未取得巨大成功，这主要是由于形式数据的稀缺。 事实上，形式化证明本身就非常困难，只有少数专家可以做到，这使得大规模的标注工作不现实。 用 Code（1994）编写的最大的形式证明语料库大小不到 0.6GB，比视觉或自然语言处理中常用的数据集小几个数量级。 为了解决形式证明的稀缺问题，之前的研究提出使用合成数据、自我监督或强化学习来合成额外的形式训练数据。 这些方法虽然在一定程度上缓解了数据的匮乏，但无法充分利用大量人工编写的数学证明。

我们以语言模型为例。 经过足够的数据训练后，我们发现它的数学能力非常强，在高中数学考试中可以取得高于平均分的成绩。 然而，这样的语言模型也有缺点。 它只能模仿，而不能独立训练来提高数学。 形式证明系统提供了训练环境，但形式数学的数据很少。

与正式数学不同，非正式数学数据丰富且广泛可用。 最近，基于非正式数学数据训练的大型语言模型表现出了令人印象深刻的定量推理能力。 然而，它们经常产生错误的证明，并且自动检测这些证明中的错误推理具有挑战性。

在最近的一项工作中，谷歌的 Tony Wu 等研究人员设计了一种称为 DSP（Draft、Prove）的新方法，将非正式的数学证明转换为正式的证明。 因此，它既具有正式系统提供的逻辑严密性，又具有大量的非正式数据。

论文链接：

今年早些时候，吴玉怀和几位合作者使用Codex的神经网络进行自动形式化工作，证明了使用大型语言模型自动将非正式语句翻译成正式语句的可行性。 DSP 更进一步，使用大型语言模型从非正式证明生成正式证明草图。 证明草图由高级推理步骤组成，可以由交互式定理证明器等形式系统进行解释。 它们与完整的形式证明不同，因为它们包含一系列不合理的中间猜想。 在DSP的最后一步，形式证明草图被详细阐述为完整的形式证明，使用自动验证器来证明所有中间猜想。

吴玉怀说：现在，我们已经证明LLM可以将其生成的非正式证明转换为经过验证的形式证明！

方法

方法部分描述了用于形式证明自动化的 DSP 方法，该方法利用非正式证明来指导自动化形式定理证明者的证明草图。 这里假设每个问题都有一个非正式命题和一个描述问题的正式命题。 整体包括三个阶段（如图1所示）。

图1。

起草非正式证明

DSP 方法的初始阶段包括根据自然数学语言（可能使用 LATEX）的描述找到问题的非正式证明。 由此产生的非正式证明被视为后续阶段的草稿。 数学教科书中一般都会提供定理的证明，但有时会缺失或不完整。 因此，研究人员考虑了与存在或不存在非正式证据相对应的两种情况。

在第一种情况下，研究者假设有一个“真实的”非正式证明（即由人类编写的证明），这是现有数学理论正式实践中的典型案例。 在第二种情况下，研究人员做出了一个更普遍的假设，即没有给出真正的非正式证明，并使用在非正式数学数据上训练的大型语言模型来起草候选证明。 语言模型消除了对人类证明的依赖，并且可以为每个问题生成多种替代解决方案。 虽然没有简单的方法来自动验证这些证明的正确性，但非正式证明只需要在下一阶段生成良好的正式证明草图时有用。

将非正式证明映射为正式草图

形式证明草图对解决方案的结构进行编码，并省略低级细节。 直观上，它是概述高级猜想陈述的部分证明。 图2是证明草图的具体示例。 尽管非正式证明通常会忽略低级细节，但这些细节不能在正式证明中排除，这使得非正式证明直接转换为正式证明变得困难。 相反，本文建议将非正式证明映射到共享相同高级结构的正式证明草图上。 校样草图中缺失的低级细节可以由自动校对器填充。 由于不存在大型非正式-正式并行语料库，因此标准机器翻译方法不适合此任务。 相反，这里使用了大型语言模型的小样本学习能力。 具体来说，该模型与一些包含非正式证明及其相应的正式草图的示例一起使用，然后将非正式证明进行转换，然后让模型生成后续令牌以获得所需的正式草图。 该模型称为“自动形式化器”。

图 2.

在草图中证明开放猜想

作为该过程的最后一部分，研究人员通过实施现成的自动证明器来填充证明草图中缺失的细节。 这里，“自动证明者”是指能够产生形式上可验证的证明的系统。 该框架与自动证明者的具体选择无关：它可以是符号证明者（例如启发式证明自动化工具）、基于神经网络的证明者或混合方法。 如果自动证明者成功填补了证明草图中的所有空白，它将返回最终的正式证明，可以根据问题的规范进行检查。 如果自动证明者失败（例如超过分配的时限），则认为评估不成功。

实验

研究人员进行了一系列实验，涉及从数据集中生成问题的形式证明，结果表明，很大一部分定理可以使用这种方法自动证明。 这里研究了两种环境，其中非正式证明由人类编写或由经过数学文本训练的大型语言模型起草。 这两种设置对应了现有理论形式化中经常出现的情况，即经常有非正式的证明，但有时会作为练习留给读者，或者由于页边的限制而缺失。

表 1 显示了在数据集中找到的成功形式证明的比例。 结果包括本文中的四个实验，以及具有人工编写证明和模型生成证明的 DSP 方法。

可以看出，附加11种启发式策略的自动证明器的性能大大提高，验证集上的成功率从9.9%提高到18.0%，测试集上的成功率从10.4%提高到20.9%。 使用语言模型和证明搜索的两种方法在测试集上分别取得了 29.9% 和 35.2% 的成功率。

基于人类编写的非正式证明，DSP 方法在验证集和测试集上取得了 42.6% 和 39.3% 的成功率。 488个问题中总共有200个问题可以用这种方法证明。 Codex 模型和 (8B) 模型在解决问题上给出了非常相似的结果：它们都引导自动验证器分别解决了验证集和测试集上 40.6% 和 35.3% 的问题。

当切换到(62B)模型时，成功率分别增加到43.9%和37.7%。 与人工编写的非正式证明相比，其在验证集上的成功率高出 1.3%，在测试集上的成功率低 1.6%。 总体而言，(62B) 模型能够解决上述问题中的 199 个，比人类编写的证明少一个。 (540B)模型分别解决了验证集和测试集中42.6%和38.9%的问题，还生成了199个成功的证明。

DSP 方法可以在两种情况下有效地指导自动证明者：使用人类的非正式证明或由语言模型生成的非正式证明。 DSP 使证明者的成功率几乎翻倍，并在 . 此外，更大的模型在指导自动化形式证明者方面几乎与人类一样有帮助。

如下图所示，DSP方法显着提高了+启发式证明者的性能（~20% ->~40%），实现了新的SOTA。

62B 和 540B 版本生成的证明与人类证明非常相似。

-END-
长按识别，即可关注
欢迎分享到朋友圈！好文章，我 在看