Pantógrafo: Una interfaz de interacción máquina a máquina para la demostración avanzada de teoremas, razonamiento de alto nivel y extracción de datos en 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
Autores: Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, Sanmi Koyejo
cs.AI
Resumen
La demostración de teoremas asistida por máquina se refiere al proceso de llevar a cabo un razonamiento estructurado para generar automáticamente demostraciones de teoremas matemáticos. Recientemente, ha habido un aumento de interés en utilizar modelos de aprendizaje automático en conjunto con asistentes de demostración para realizar esta tarea. En este documento, presentamos Pantograph, una herramienta que proporciona una interfaz versátil al asistente de demostración Lean 4 y permite una búsqueda de pruebas eficiente a través de algoritmos de búsqueda poderosos como la Búsqueda de Árbol de Monte Carlo. Además, Pantograph posibilita el razonamiento de alto nivel al permitir un manejo más sólido de los pasos de inferencia de Lean 4. Presentamos una visión general de la arquitectura y características de Pantograph. También informamos sobre un caso de uso ilustrativo: utilizando modelos de aprendizaje automático y bosquejos de pruebas para demostrar teoremas de Lean 4. Las características innovadoras de Pantograph allanan el camino para que modelos de aprendizaje automático más avanzados realicen búsquedas de pruebas complejas y razonamiento de alto nivel, capacitando a futuros investigadores para diseñar demostradores de teoremas más versátiles y potentes.
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.