Pantografo: un'interfaccia di interazione macchina-macchina per dimostrazioni teoriche avanzate, ragionamento di alto livello ed estrazione di dati 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

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

cs.AI

Abstract

La dimostrazione automatica assistita da macchina si riferisce al processo di condurre un ragionamento strutturato per generare automaticamente dimostrazioni per teoremi matematici. Recentemente, c'è stato un aumento di interesse nell'utilizzo di modelli di apprendimento automatico in combinazione con assistenti alla dimostrazione per svolgere questo compito. In questo articolo, presentiamo Pantograph, uno strumento che fornisce un'interfaccia versatile all'assistente alla dimostrazione Lean 4 e consente una ricerca efficiente delle dimostrazioni tramite potenti algoritmi di ricerca come la Ricerca ad Albero Monte Carlo. Inoltre, Pantograph permette un ragionamento di alto livello consentendo una gestione più robusta dei passaggi di inferenza di Lean 4. Forniamo una panoramica dell'architettura e delle funzionalità di Pantograph. Riportiamo anche un caso d'uso illustrativo: utilizzando modelli di apprendimento automatico e bozzetti di dimostrazione per dimostrare teoremi di Lean 4. Le caratteristiche innovative di Pantograph aprono la strada a modelli di apprendimento automatico più avanzati per eseguire ricerche di dimostrazioni complesse e ragionamenti di alto livello, dotando i futuri ricercatori di progettare dimostratori di teoremi più versatili e potenti.

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.