LEGO-Prover：基于不断增长知识库的神经定理证明

尽管大型语言模型（LLMs）取得了显著进展，定理证明任务仍然是最具挑战性的推理任务之一，远未得到完全解决。此前基于语言模型的方法虽展现出一定的潜力，但在证明中学水平的定理方面仍存在明显困难。这些方法的一个共同局限在于：在整个定理证明过程中，假设定理库是固定不变的。然而众所周知，创造新的有用定理，甚至构建全新的理论体系，不仅对推动数学发展至关重要，更是实现更复杂、更深刻数学成果的必要前提。在本工作中，我们提出了 LEGO-Prover，该方法通过引入一个可动态扩展的“技能库”（skill library），其中包含经验证的引理作为可复用的“技能”，从而增强语言模型在定理证明中的能力。LEGO-Prover 采用模块化构建证明的策略，使语言模型能够在证明过程中检索并复用已有技能，同时在过程中自主生成新的技能。这些新生成的技能通过再次调用语言模型进行提示（prompting）以进一步演化，从而在更高层次上丰富技能库。随着模块化、可复用技能的持续积累，系统逐步具备应对日益复杂数学问题的能力。此外，所学习到的技能库还有效弥合了人类证明与形式化证明之间的鸿沟，使补全证明中缺失步骤变得更加可行。实验结果表明，LEGO-Prover 将 miniF2F-valid 数据集上的通过率从 48.0% 提升至 57.0%，在 miniF2F-test 数据集上则从 45.5% 提升至 47.1%，显著优于现有方法。在实际证明过程中，LEGO-Prover 共生成超过 20,000 项技能（包括定理与引理），并将其持续加入不断增长的技能库中。消融实验进一步验证了这些新增技能的有效性：当仅使用新生成的技能时，定理证明的成功率从 47.1% 提升至 50.4%。我们已公开发布该项目的全部代码及所生成的所有技能，以促进该领域的进一步研究与发展。