科学家提出即递归式证明，有望用于数学教育

在 ChatGPT 出现之后，大模型迎来了蓬勃发展。在众多大模型中，ChatGPT 依然是“扛把子”般的存在。

尽管它在诸多方面都表现十分出色，但是数学推理能力依旧有些欠缺。

此前很多针对大模型数学推理的研究，主要是以数据为入手。但是，在自然语言数学的领域，数学数据存在可自动验证性的问题。

要想确保大模型的生成质量，数据就必须得正确。然而，对于自然语言的数据来说，它的正确性无法得到自动验证，必须通过大量的人力来判断。

并且因为是数学相关的数据，有时甚至还需要专家的参与才可以判断其正确性。对于形式化系统来说，它旨在解决数学的可自动验证性问题。

目前，主流的形式化系统有 Metamath、Lean 和 Isabelle 等。

在使用时，只需把数学定理写在形式化系统的语言下，就可以让形式化系统来自动验证某个数学定理是否是正确的证明。

形式化系统的发展，驱动了基于形式化系统和大模型结合的神经-符号方法的发展，包括 OpenAI 的开山之作 GPT-f、基于 Isabelle 语言的 Thor、以及基于 Lean 语言的 Leandojo。

GPT-f 等方法主要采用形式化系统和大模型交互协作的方式来证明定理。

其中，形式化系统会给到大模型需要证明定理的前提和目标。而大模型会根据当前的前提和目标，给出相应的证明策略。

根据大模型给出的证明策略，形式化系统会更新当前的证明状态，从而得到新的证明状态。

直到证明状态更新到特定的证明成功状态，或达到失败条件从而处于证明失败状态，否则大模型和形式化状态之间会不断交替进行上述步骤。

而为了找到更加复杂的证明，GPT-f 等方法通常还使用搜索算法，来充分地探索不同的证明路径。常用的搜索算法包括最优优先搜索和蒙特卡洛树搜索。

然而，由于证明步骤可以是任意的代码，这意味着每一次搜索时的 action 都有可能是无限的，这会导致整个搜索空间变得无穷大。

相关问题的搜索空间甚至远超围棋等游戏的棋盘空间，故会给上述方法带来严峻挑战。

举例来说，当使用 Leandojo 方法的时候，要想在 MiniF2F 数据集上找到最长的步骤只需要 3 步。

然而，人类写的证明步骤通常有十几步甚至几十步之多。为了尽快达到人类水平，解决搜索空间的指数增长问题迫在眉睫。

基于此，中山大学王海明非常希望能够解决证明搜索空间的问题。于是，他们提出了即递归式证明（POETRY，PrOving thEorem RecursivelY）。

受到人类证明数学定理的思路启发，他们发现可以通过递归去填充证明的方式，来在一定程度上解决上述问题。

研究人员指出，人类在做复杂数学题的时候，通常会尝试假设一些中间的引理，然后利用这些引理来证明当前的目标，而这些引理的具体证明则会留到后面去解决。

基于此，王海明和同事使用形式化系统中的 Sorry 关键字，跳过了中间引理的证明，以便让大模型专注于实现当前目标。

这时，只有在使用中间引理成功证明当前目标之后，研究人员才会选择深入地探索中间引理的证明。

这样的好处在于：能够把一个长度为十几的证明分解为多层，而在每一层只需要证明长度不到五的一个子证明。

并能把一些中间引理的证明留到之后去做，借此能够大大减少搜索的困难程度。

从实验结果来看，递归式证明能够显著提升证明长度。在本次研究中的两个实验数据集上，递归式证明方法能够找到更长的证明，也就是找到更难题目的证明。

特别需要指出的是，在 PISA 数据集上，要想找到最长的证明，GPT-f 方法需要 11 步，而本次方法则能提升到 26 步。

总的来说，本次成果旨在解决 AI4Math 的研究问题。在 AI4Math 领域，本次成果有望用于数学教育，即能够提供可验证的数学证明过程，从而可以显著提高数学教育 AI 产品的可靠程度，进而防止 AI 知识性欺骗。

此外，数学属于前沿性学科，如能通过 AI 解决一些数学难题，必将带领各个学科的蓬勃发展。

来自英国爱丁堡大学的一位同行评价称，本次研究中的层次化递归证明方法是大势所趋。而另一位来自美国卡内基梅隆大学的教授则表示非常期待本次方法能在 Lean 等其他形式化系统中得到扩展。

但是，本次提出的证明方法与具体的形式系统无关。只不过出于方法实现上的方便性，他们才选择在 Isabelle 这个方法上加以实现。

而在后续，他们希望把本次方法扩展到其他形式化系统上，比如拓展到 Lean 或 Hol 等形式化系统之中。

参考资料：

1.https://arxiv.org/pdf/2405.14414