在人工智能大模型领域，数学推理一直是一个挑战。尽管 ChatGPT 等大型语言模型在多个方面表现出色，但在数学推理能力上仍有欠缺。为了解决这一问题，中山大学王海明团队提出了一种创新的即递归式证明（POETRY，PrOving thEorem Recursively）方法，有望为数学教育和AI推理带来突破。
背景介绍
自 ChatGPT 出现以来，大型语言模型得到了快速发展。然而，这些模型在数学推理方面的能力仍然有限。以往的研究多从数据入手，但由于自然语言数学数据的可自动验证性问题，这种方法存在一定的局限性。为了确保大模型的生成质量，需要找到一种新的方法来提高数学推理的准确性。
即递归式证明法的提出
王海明团队受到人类证明数学定理的思路启发，提出了一种新的证明方法。该方法通过递归填充证明的方式，来解决证明搜索空间的指数增长问题。
在传统的数学证明中，人们通常会假设一些中间引理，然后利用这些引理来证明当前的目标。这些中间引理的证明可以留到后面解决。王海明团队在形式化系统中使用 Sorry 关键字，跳过中间引理的证明，让大模型专注于当前目标。只有在成功证明当前目标后，才会深入探索中间引理的证明。
这种方法将一个长证明分解为多层，每一层只需要证明长度不到五的子证明，大大减少了搜索的困难程度。
实验结果
实验结果表明，递归式证明方法能够显著提升证明长度。在两个实验数据集上，该方法能够找到更长的证明，即解决更复杂的数学问题。特别是在 PISA 数据集上，GPT-f 方法需要 11 步才能找到最长的证明，而递归式证明方法则能提升到 26 步。
意义与展望
本次研究成果旨在解决 AI4Math 领域的研究问题，有望用于数学教育。该方法能够提供可验证的数学证明过程，显著提高数学教育 AI 产品的可靠程度，防止 AI 知识性欺骗。
此外，数学作为前沿性学科，AI 在解决一些数学难题方面的突破，将带动各个学科的蓬勃发展。来自英国爱丁堡大学和卡内基梅隆大学的同行评价称，这种层次化递归证明方法是大势所趋，并期待该方法能在 Lean 等其他形式化系统中得到扩展。
结语
王海明团队提出的即递归式证明方法，为 AI 数学推理能力提升带来了新的可能性。未来，随着该方法在其他形式化系统中的扩展，有望在数学教育和科研领域发挥更大的作用。人工智能在数学领域的突破，将为我们解锁更多未知世界的钥匙。
Views: 0