Pantograph: Eine Maschine-zu-Maschine-Interaktions-Schnittstelle für fortgeschrittene Theorembeweise, hochrangiges Argumentieren und Datengewinnung in 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

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

cs.AI

Zusammenfassung

Die maschinengestützte Beweisführung bezieht sich auf den Prozess des strukturierten Argumentierens zur automatischen Generierung von Beweisen für mathematische Theoreme. In letzter Zeit hat das Interesse zugenommen, maschinelle Lernmodelle in Verbindung mit Beweisassistenten zu verwenden, um diese Aufgabe zu erfüllen. In diesem Artikel stellen wir Pantograph vor, ein Tool, das eine vielseitige Schnittstelle zum Beweisassistenten Lean 4 bietet und eine effiziente Beweissuche über leistungsstarke Suchalgorithmen wie Monte-Carlo-Baumsuche ermöglicht. Darüber hinaus ermöglicht Pantograph ein hochrangiges Argumentieren durch eine robustere Behandlung der Inferenzschritte von Lean 4. Wir geben einen Überblick über die Architektur und Funktionen von Pantograph. Wir berichten auch über einen veranschaulichenden Anwendungsfall: die Verwendung von maschinellen Lernmodellen und Beweisskizzen zur Beweisführung von Lean 4-Theoremen. Die innovativen Funktionen von Pantograph ebnen den Weg für fortschrittlichere maschinelle Lernmodelle, um komplexe Beweissuchen und hochrangiges Argumentieren durchzuführen und zukünftigen Forschern die Möglichkeit zu geben, vielseitigere und leistungsstärkere Theorembeweiser zu entwerfen.

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.