- 简介大型语言模型(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。
沙发等你来抢
去评论
评论
沙发等你来抢