摘要
大语言模型生成的数学证明常不可靠。针对组合数学领域形式化知识匮乏的问题，本文首先构建了包含 93 个核心定义的 Lean 4 形式化库。其次，提出 LAMP 多智能体框架，利用本体论在推理时提供结构化领域知识，而非微调模型。该框架通过模型上下文协议协调规划者、构建者与验证者，在 90 个定理测试中实现了 96.7% 的验证通过率，显著优于现有基线。消融实验证实了其工具接地架构与规划模块分离设计的关键作用。
AI 推荐理由
论文提出多智能体框架 LAMP，核心在于 Planner 模块的任务分解与协调，显著提升证明合成率。
研究机构
Indian Institute of Information Technology, Design and Manufacturing, Kancheepuram
论文信息