ImProver：基于智能体的自动化证明优化
原文中文，约300字，阅读约需1分钟。发表于：。本文针对现有形式证明在可读性、简洁性等方面的优化问题提出了新的解决方案。通过引入ImProver这一基于大型语言模型的智能体，本文实现了对形式证明的自动化优化，使得优化后的证明在长度、模块化程度及可读性等指标上显著提升。研究结果表明，该方法在多种数学定理的优化中表现出色，具有广泛的应用潜力。
LeanDojo是一个开源的交互式证明环境，提取Lean中的数据和注释来帮助选择前提。基于这些数据，我们开发了ReProver，这是首个带有检索功能的LLM证明程序，只需一台GPU训练一周。我们创建了一个包含96962个定理的新基准进行评估。实验表明，ReProver比非检索基线和GPT-4更有效。代码和数据集已发布以支持进一步研究。
