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.