自动证明数学定理是人工智能的一个初衷，也是一个由来已久的难题。迄今为止，人类数学家使用了两种不同的方式来编写数学。第一种是大家熟悉的方式，就是用自然语言来描述数学证明。很多数学都是这样写的，包括数学教科书、数学论文等等。第二种叫做形式数学。它是近半个世纪以来计算机科学家创造的一种工具，用于测试数学证明。今天看来，计算机可以用来验证数学证明，但它们只能使用专门设计的证明语言来验证，这种语言无法处理数学家使用的数学符号和书面文本的混合。通过将自然语言编写的数学问题转换为形式代码，使计算机更容易解决这些问题，这可能有助于构建能够探索数学新发现的机器。这个过程称为形式化，自动形式化是指将自然语言数学自动翻译成形式语言的任务。形式化证明的自动化是一项具有挑战性的任务，深度学习方法在这方面尚未取得巨大成功，主要是因为形式化数据的稀缺。事实上，形式化证明本身就非常困难，只有少数专家可以做到，这使得大规模标注工作变得不切实际。用Isabelle代码（Paulson，1994年）编写的最大形式证明语料库的大小不到0.6GB，比视觉或自然语言处理中常用的数据集小几个数量级。为了解决正式证明的稀缺性，之前的研究提出使用合成数据、自我监督或强化学习来合成额外的正式训练数据。这些方法虽然在一定程度上缓解了数据的不足，但无法充分利用大量手工编写的数学证明。我们以语言模型Minerva为例。经过足够多的数据训练后，我们发现它的数学能力非常强，在高中数学考试中都能拿到中等以上的分数。但是，这样的语言模型也有缺点。只能模仿，不能自主训练提高数学水平。形式证明系统提供了训练环境，但形式数学的数据非常少。与正式数学不同，非正式数学数据丰富且广泛可用。最近，在非正式数学数据上训练的大型语言模型展示了令人印象深刻的定量推理能力。然而，它们经常产生错误的证明，并且自动检测这些证明中的错误推理具有挑战性。在最近的一项工作中，Google的宇怀TonyWu和其他研究人员设计了一种称为DSP（Draft、Sketch和Prove）的新方法，将非正式的数学证明转换为正式的Proof，使其既具有正式系统提供的逻辑严密性，又具有大量的非正式数据。论文链接：https://arxiv.org/pdf/2210.12283.pdf今年早些时候，吴宇怀和几位合作者使用OpenAICodex的神经网络进行自动形式化工作，证明使用大型语言模型转换非正式形式化句子自动翻译成形式化句子的可行性。DSP更进一步，利用大型语言模型从非正式证明生成正式证明草图。证明草图由高级推理步骤组成，可以由交互式定理证明器等正式系统解释。它们不同于完整的形式证明，因为它们包含一系列不合理的中间猜想。在DSP的最后一步，形式证明草图被制定为一个完整的形式证明，使用一个自动验证器来证明所有中间猜想。吴玉怀说：现在，我们证明LLM可以将它生成的非正式证明转化为经过验证的正式证明！方法方法部分描述了一种用于形式证明自动化的DSP方法，该方法利用非正式证明来指导自动形式定理证明器的证明草图。这里假设每个问题都有一个非正式命题和一个描述问题的正式命题。整个流水线由三个阶段组成（如图1所示）。图1.非正式证明的起草。DSP方法的初始阶段包括根据自然数学语言（可能是LATEX）的描述寻找问题的非正式证明。由此产生的非正式证明被认为是后续阶段的草案。在数学教科书中，通常会提供定理证明，但有时会缺失或不完整。因此，研究人员考虑了与存在或不存在非正式证据相对应的两种情况。在第一种情况下，研究人员假设存在一个“真实的”非正式证明（即由人类编写的证明），这在形式化现有数学理论的实践中很典型。在第二种情况下，研究人员做出更普遍的假设，即没有给出真正的非正式证明，并使用在非正式数学数据上训练的大型语言模型来起草证明候选者。语言模型消除了对人工证明的依赖，可以为每个问题生成多个替代解决方案。虽然没有简单的方法可以自动验证这些证明的正确性，但非正式证明只需要在下一阶段有用即可生成良好的正式证明草图。将非正式证明映射到正式草图正式证明草图对解决方案的结构进行编码并省略低级细节。直觉上，它是勾勒出一个高级猜想命题的部分证明。图2是一个验证草图的具体示例。虽然非正式证明经常遗漏低级细节，但这些细节在正式证明中无法穷尽，使得非正式证明直接转换为正式证明很困难。相反，本文建议将非正式证明映射到共享相同高级结构的正式证明草图上。证明草图中缺少的低级细节可以由自动证明器填充。由于缺乏大量的非正式-正式平行语料库，标准的机器翻译方法不适合这项任务。相反，这里使用了大型语言模型的小样本学习能力。具体来说，模型被提示一些包含非正式证明及其对应的形式化草图的示例对，然后是要转换的非正式证明，然后要求模型生成后续标记以获得所需的形式化草图。该模型称为“自动形式化器”。图2.证明草图中的公共猜想。作为该过程的最后一部分，研究人员执行现成的自动验证器以填充验证草图中缺失的细节。在这里，“自动证明者”是指能够产生形式上可验证的证明的能力。系统。该框架与自动证明器的具体选择无关：它可以是符号证明器（例如启发式证明自动化工具）、基于神经网络的证明器或混合方法。如果自动证明器成功地填补了证明草图中的所有空白，它会返回最终的正式证明，可以根据问题的规范进行检查。如果自动证明者失败（例如，它超过了分配的时间限制），则认为评估不成功。实验研究人员进行了一系列实验，涉及miniF2F数据集生成问题的形式证明，并表明大部分定理可以通过这种方式自动证明。这里研究了两种环境，其中非正式证明由人类编写或由在数学文本上训练的大型语言模型起草。这两个设置对应于现有理论形式化中经常出现的情况，其中非正式证明通常可用，但有时留给读者作为练习，或者由于空白限制而缺失。表1显示了在miniF2F数据集上找到的成功形式证明的比例。结果包括本文中试验的四个基线，以及具有人工编写证明和模型生成证明的DSP方法。可以看出，附加了11种启发式策略的自动证明器大大提高了Sledgehammer的性能，其在miniF2F验证集上的成功率从9.9%提高到18.0%，在测试集上从10.4%提高到20.9%。使用语言模型和证明搜索的两个基线在miniF2F测试集上分别取得了29.9%和35.2%的成功率。基于非正式的人工证明，DSP方法在miniF2F的验证和测试集上取得了42.6%和39.3%的成功率。488个问题中总共有200个可以这样证明。Codex模型和Minerva(8B)模型在解决miniF2F问题时给出了非常相似的结果：它们都引导自动验证器分别解决了验证集和测试集上40.6%和35.3%的问题。当切换到Minerva(62B)模型时，成功率分别上升到43.9%和37.7%。与非正式的人工证明相比，它在验证集上的成功率高1.3%，在测试集上的成功率低1.6%。总体而言，Minerva(62B)模型能够在miniF2F上解决199个问题，比人工编写的证明少一个。Minerva(540B)模型分别在miniF2F的验证集和测试集上解决了42.6%和38.9%的问题，并且还生成了199个成功的证明。DSP方法在两种情况下有效地指导自动证明：使用人类的非正式证明或由语言模型生成的非正式证明。DSP几乎将证明者的成功率提高了一倍，并在Isabelle的miniF2F上产生了SOTA性能。此外，更大的Minerva模型在指导自动化形式证明者方面几乎与人类一样有用。如下图所示，DSP方法显着提高了Sledgehammer+heuristicprover的性能（~20%->~40%），在miniF2F上实现了新的SOTA。Minerva的62B和540B版本生成的证明与人类证明非常相似。有关更多详细信息，请参阅原始论文。
