Pantograph：用于Lean 4中高级定理证明、高级推理和数据提取的机器对机器交互界面。

Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4

October 21, 2024

作者: Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, Sanmi Koyejo

cs.AI

摘要

机器辅助定理证明是指通过进行结构化推理来自动生成数学定理证明的过程。最近，人们对将机器学习模型与证明助手结合使用以执行此任务表现出了极大的兴趣。在本文中，我们介绍了 Pantograph，这是一个工具，提供了与 Lean 4 证明助手的多功能接口，并通过强大的搜索算法（如蒙特卡洛树搜索）实现高效的证明搜索。此外，Pantograph 通过更强大地处理 Lean 4 推理步骤，实现了高层次推理。我们概述了 Pantograph 的架构和特性。我们还报告了一个示例用例：使用机器学习模型和证明草图来证明 Lean 4 的定理。Pantograph 的创新特性为更先进的机器学习模型执行复杂的证明搜索和高层次推理铺平了道路，为未来的研究人员设计更多功能强大的定理证明器提供了支持。

English

Machine-assisted theorem proving refers to the process of conducting structured reasoning to automatically generate proofs for mathematical theorems. Recently, there has been a surge of interest in using machine learning models in conjunction with proof assistants to perform this task. In this paper, we introduce Pantograph, a tool that provides a versatile interface to the Lean 4 proof assistant and enables efficient proof search via powerful search algorithms such as Monte Carlo Tree Search. In addition, Pantograph enables high-level reasoning by enabling a more robust handling of Lean 4's inference steps. We provide an overview of Pantograph's architecture and features. We also report on an illustrative use case: using machine learning models and proof sketches to prove Lean 4 theorems. Pantograph's innovative features pave the way for more advanced machine learning models to perform complex proof searches and high-level reasoning, equipping future researchers to design more versatile and powerful theorem provers.