パントグラフ：Lean 4における高度な定理証明、高レベルな推論、およびデータ抽出のための機械間インタラクションインタフェース

要旨

機械支援定理証明は、数学の定理の証明を自動的に生成するための構造化された推論を行うプロセスを指します。最近、機械学習モデルを証明支援ツールと組み合わせてこのタスクを実行するために興味が高まっています。本論文では、Lean 4証明支援ツールと効率的な証明探索を可能にするMonte Carlo Tree Searchなどの強力な探索アルゴリズムを介して、多目的インターフェースを提供するツール、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.

パントグラフ：Lean 4における高度な定理証明、高レベルな推論、およびデータ抽出のための機械間インタラクションインタフェース

Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4

要旨

Support