LeanAgent: Lifelong Learning for Formal Theorem Proving

大型语言模型（LLM）在数学推理任务中表现出色，例如与Lean等交互证明助手集成时的形式定理证明。现有方法涉及在特定数据集上训练或微调LLM，以在特定领域（如本科数学）表现良好。这些方法在推广到高级数学方面方面面临困难。一个根本性的限制是这些方法在静态领域上操作，无法捕捉数学家通常如何同时或循环地跨越多个领域和项目工作。我们提出了LeanAgent，这是一个新颖的终身学习框架，用于定理证明，可以持续地推广和改进不断扩展的数学知识，而不会忘记先前学习的知识。LeanAgent引入了几个关键创新，包括一种课程学习策略，该策略优化数学难度的学习轨迹，一个动态数据库，用于有效管理不断发展的数学知识，以及渐进式训练，以平衡稳定性和可塑性。LeanAgent成功证明了23个不同的Lean存储库中的162个以前未被人类证明的定理，其中许多来自于高级数学。它的表现比静态LLM基线高出11倍，证明了抽象代数和代数拓扑等领域的具有挑战性的定理，同时展示了从基本概念到高级主题的明显学习进展。此外，我们分析了LeanAgent在关键终身学习指标上的出色表现。LeanAgent在稳定性和向后转移方面取得了异常的分数，其中学习新任务可以提高先前学习任务的表现。这强调了LeanAgent的持续推广和改进，解释了其卓越的定理证明性能。

解决问题：论文旨在解决数学推理中的通用性问题，提出了一个连续学习框架LeanAgent，以便在不断扩大的数学知识库中实现持续的泛化和改进。

关键思路：LeanAgent是一个基于生命周期的学习框架，通过优化学习轨迹、动态数据库和渐进式训练等关键创新，实现了持续的泛化和改进。

其他亮点：LeanAgent成功证明了23个不同的Lean存储库中的162个定理，包括高级数学领域的定理，性能比静态LLM基线高出多达11倍。实验设计了课程学习策略、动态数据库和渐进式训练，并在关键的生命周期学习指标上取得了优异的成绩。

相关研究：最近的相关研究包括使用LLM进行数学推理的工作，以及其他基于生命周期学习的学习框架，如ContinualAI和Lifelong-DNN。