Pantographe : Une interface d'interaction machine à machine pour la démonstration de théorèmes avancée, le raisonnement de haut niveau et l'extraction de données dans 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

Résumé

La preuve de théorèmes assistée par machine fait référence au processus de mener un raisonnement structuré pour générer automatiquement des preuves pour des théorèmes mathématiques. Récemment, il y a eu un regain d'intérêt pour l'utilisation de modèles d'apprentissage automatique en conjonction avec des assistants de preuve pour effectuer cette tâche. Dans cet article, nous présentons Pantograph, un outil qui fournit une interface polyvalente à l'assistant de preuve Lean 4 et permet une recherche de preuves efficace via des algorithmes de recherche puissants tels que la recherche arborescente Monte Carlo. De plus, Pantograph permet un raisonnement de haut niveau en permettant une gestion plus robuste des étapes d'inférence de Lean 4. Nous donnons un aperçu de l'architecture et des fonctionnalités de Pantograph. Nous rendons également compte d'un cas d'utilisation illustratif : utiliser des modèles d'apprentissage automatique et des croquis de preuve pour prouver des théorèmes Lean 4. Les fonctionnalités innovantes de Pantograph ouvrent la voie à des modèles d'apprentissage automatique plus avancés pour effectuer des recherches de preuves complexes et un raisonnement de haut niveau, permettant aux futurs chercheurs de concevoir des prouveurs de théorèmes plus polyvalents et puissants.

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.