Aesop: White-Box Best-First Proof Search for Lean.
CPP(2023)
摘要
We present Aesop, a proof search tactic for the Lean 4 interactive
theorem prover. Aesop performs a tree-based search over a user-specified
set of proof rules. It supports safe and unsafe rules and uses a best-first
search strategy with customisable prioritisation. Aesop also allows users
to register custom normalisation rules and integrates Lean's simplifier to
support equational reasoning. Many details of Aesop's search procedure are
designed to make it a white-box proof automation tactic, meaning that users
should be able to easily predict how their rules will be applied, and thus how
powerful and fast their Aesop invocations will be. Since we use a best-first search strategy, it is not obvious how to handle
metavariables which appear in multiple goals. The most common strategy for
dealing with metavariables relies on backtracking and is therefore not
suitable for best-first search. We give an algorithm which addresses this
issue. The algorithm works with any search strategy, is independent of the
underlying logic and makes few assumptions about how rules interact with
metavariables. We conjecture that with a fair search strategy, the algorithm
is as complete as the given set of rules allows.
更多查看译文
关键词
lean,search,white-box,best-first
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要