arXiv:2410.16429v2 通告类型: 替换-交叉 摘要: 机器辅助定理证明是指通过结构化推理自动为数学定理生成证明的过程。最近，人们越来越关注将机器学习模型与证明助手相结合，以执行这一任务。在本文中，我们介绍了Pantograph，这是一个提供了Lean 4证明助手多功能接口的工具，并通过强大的搜索算法（如蒙特卡洛树搜索）实现了高效证明搜索。此外，Pantograph 通过更稳健地处理 Lean 4 的推理步骤，支持高层次的推理。我们概述了Pantograph的架构和功能。我们还报告了一个示例应用场景：使用机器学习模型和证明草图来证明Lean 4定理。Pantograph的创新功能为更高级的机器学习模型执行复杂证明搜索和高层次推理铺平了道路，为未来的研究人员设计更灵活和强大的定理证明器提供了支持。