ImProver：基于智能体的自动化证明优化

BriefGPT - AI 论文速递 · 2024-10-07T00:00:00Z

LeanDojo是一个开源的交互式证明环境，提取Lean中的数据和注释来帮助选择前提。基于这些数据，我们开发了ReProver，这是首个带有检索功能的LLM证明程序，只需一台GPU训练一周。我们创建了一个包含96962个定理的新基准进行评估。实验表明，ReProver比非检索基线和GPT-4更有效。代码和数据集已发布以支持进一步研究。