泛图：一种用于先进定理证明、高级推理和数据提取的机器间交互界面
原文中文，约300字，阅读约需1分钟。发表于：。本文解决了机器辅助定理证明中的高效证明搜索和推理能力不足的问题。通过引入Pantograph工具，结合蒙特卡罗树搜索等算法，本文展示了其在Lean 4证明助手中的应用，提高了推理的鲁棒性和复杂证明搜索的能力。Pantograph的创新特性为设计更强大的定理证明工具铺平了道路，为未来研究者提供了便利。
LeanDojo是一个开源的交互式证明环境，提取Lean中的数据和注释。我们开发了ReProver，一个基于LLM的低成本证明程序，能够有效选择定理前提。构建了包含96962个定理的新基准，实验结果显示ReProver优于非检索基线和GPT-4。相关代码和数据集已发布以促进研究。
