Aesop: White-Box Best-First Proof Search for Lean
Aesop: White-Box Best-First Proof Search for Lean
复制标题
Aesop：精益的白盒最佳优先证明搜索
DOI：
10.1145/3573105.3575671
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Asta Halkjær From
中科院分区：
文献类型：
--
作者：
Jannis Limperg;Asta Halkjær From
我们提出了Aesop，一个用于Lean 4交互式定理证明器的证明搜索策略。Aesop对用户指定的一组证明规则执行基于树的搜索。它支持安全和不安全规则，并使用最佳优先搜索策略和可定制的优先级。Aesop还允许用户注册自定义规范化规则，并集成Lean的简化器以支持等式推理。Aesop搜索过程的许多细节都是为了使其成为白盒证明自动化策略而设计的，这意味着用户应该能够轻松预测他们的规则将如何应用，从而预测他们的Aesop调用将有多强大和快。由于我们使用最佳优先搜索策略，因此如何处理出现在多个目标中的元变量并不明显。处理元变量的最常见策略依赖于回溯，因此不适合最佳优先搜索。我们给出了一个算法，解决这个问题。该算法适用于任何搜索策略，独立于底层逻辑，并且对规则如何与元变量交互做出很少的假设。我们猜想，与公平的搜索策略，算法是完整的，因为给定的一组规则允许。
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.