팬토그래프: 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

초록

기계 지원 정리 증명은 수학 정리를 자동으로 증명하기 위해 구조화된 추론을 수행하는 과정을 가리킵니다. 최근에는 기계 학습 모델을 증명 보조 도구와 결합하여 이 작업을 수행하는 데 관심이 급증했습니다. 본 논문에서는 Lean 4 증명 보조 도구와 강력한 탐색 알고리즘인 몬테카를로 트리 탐색을 통해 효율적인 증명 탐색을 가능케 하는 다목적 인터페이스를 제공하는 Pantograph를 소개합니다. 또한 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.