AI热门论文

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

本文地址：http://syank.xrbh.cn/quote/6215.html    迅博思语资讯 http://syank.xrbh.cn/ , 查看更多