Pantograaf: Een machine-naar-machine-interactie-interface voor geavanceerd stellingbewijs, hoog-niveau redeneren en gegevensextractie 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

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

cs.AI

Samenvatting

Machine-ondersteund stellingbewijs verwijst naar het proces van het uitvoeren van gestructureerd redeneren om automatisch bewijzen te genereren voor wiskundige stellingen. Onlangs is er een toename van interesse geweest in het gebruik van machine learning modellen in combinatie met bewijsondersteunende systemen om deze taak uit te voeren. In dit artikel introduceren we Pantograph, een tool die een veelzijdige interface biedt naar de Lean 4 bewijsondersteunende systeem en efficiënte bewijszoekopdrachten mogelijk maakt via krachtige zoekalgoritmes zoals Monte Carlo Tree Search. Daarnaast maakt Pantograph hoog-niveau redeneren mogelijk door een robuustere behandeling van Lean 4's inferentiestappen mogelijk te maken. We geven een overzicht van de architectuur en functies van Pantograph. We rapporteren ook over een illustratieve gebruikssituatie: het gebruiken van machine learning modellen en bewijsconcepten om Lean 4 stellingen te bewijzen. De innovatieve functies van Pantograph banen de weg voor meer geavanceerde machine learning modellen om complexe bewijszoekopdrachten en hoog-niveau redeneren uit te voeren, waardoor toekomstige onderzoekers meer veelzijdige en krachtige stellingbewijzers kunnen ontwerpen.

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.