Пантограф: Интерфейс взаимодействия машин для продвинутого доказательства теорем, высокоуровневого рассуждения и извлечения данных в 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

Авторы: Leni Aniva, Chuyue Sun, Brando Miranda, Clark Barrett, Sanmi Koyejo

cs.AI

Аннотация

Машинное доказательство теорем относится к процессу структурированного рассуждения для автоматического генерирования доказательств математических теорем. Недавно возникло повышенное интересное к использованию моделей машинного обучения совместно с помощниками по доказательствам для выполнения этой задачи. В данной статье мы представляем Pantograph, инструмент, который предоставляет универсальный интерфейс к помощнику Lean 4 и обеспечивает эффективный поиск доказательств с помощью мощных алгоритмов поиска, таких как Монте-Карло поиск по дереву. Кроме того, Pantograph обеспечивает высокоуровневое рассуждение, позволяя более надежно обрабатывать шаги вывода Lean 4. Мы предоставляем обзор архитектуры и функций Pantograph. Мы также сообщаем об иллюстративном примере использования: использование моделей машинного обучения и эскизов доказательств для доказательства теорем Lean 4. Инновационные функции Pantograph прокладывают путь для более продвинутых моделей машинного обучения для выполнения сложных поисков доказательств и высокоуровневого рассуждения, что позволит будущим исследователям создавать более универсальные и мощные доказатели теорем.

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.