Pantógrafo: Uma Interface de Interação Máquina a Máquina para Prova de Teoremas Avançada, Raciocínio de Alto Nível e Extração de Dados no 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

Resumo

A prova de teoremas assistida por máquina refere-se ao processo de conduzir raciocínio estruturado para gerar automaticamente provas para teoremas matemáticos. Recentemente, houve um aumento de interesse em utilizar modelos de aprendizado de máquina em conjunto com assistentes de prova para realizar essa tarefa. Neste artigo, apresentamos o Pantograph, uma ferramenta que fornece uma interface versátil para o assistente de prova Lean 4 e permite uma busca eficiente de provas por meio de algoritmos de busca poderosos, como a Busca em Árvore de Monte Carlo. Além disso, o Pantograph possibilita o raciocínio em um nível mais alto ao permitir um tratamento mais robusto das etapas de inferência do Lean 4. Fornecemos uma visão geral da arquitetura e das funcionalidades do Pantograph. Também relatamos um caso ilustrativo: utilizando modelos de aprendizado de máquina e esboços de prova para provar teoremas do Lean 4. As funcionalidades inovadoras do Pantograph abrem caminho para modelos de aprendizado de máquina mais avançados realizarem buscas de provas complexas e raciocínio em um nível mais alto, capacitando futuros pesquisadores a projetar provadores de teoremas mais versáteis e poderosos.

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.