用于交互式定理证明的策略库的自动化发现

《Proceedings of the ACM on Programming Languages》：Automated Discovery of Tactic Libraries for Interactive Theorem Proving

模块化证明与自动化战术发现方法研究。本文提出基于战术依赖图（TDGs）的自动战术发现方法，通过抽象战术应用间的逻辑依赖关系，实现证明策略的可重用性挖掘与重构。实验表明所开发的TacMineR工具相比Peano方法，战术学习量提升300%，平均证明规模缩减26%，并使现有自动化工具成功率达172%的增长。

　　

摘要

为了利用交互式定理证明器（ITPs）推进形式化推理，实现更简洁、更模块化的证明至关重要。由于许多ITPs（如Rocq和Lean）采用策略式证明方法，因此学习高级自定义策略对于证明的模块化和自动化至关重要。本文提出了一种新颖的策略发现方法，该方法利用策略依赖图（TDGs）来识别多个证明中可重用的证明策略。TDGs能够捕捉策略应用之间的逻辑依赖关系，同时忽略无关的句法细节，从而既有助于发现新的策略，也有助于将现有证明重构为更模块化的形式。我们已在名为TacMineR的工具中实现了这一技术，并将其与基于反统一的方法（Peano）进行了对比。评估结果表明，TacMineR能够学习的策略数量是Peano的3倍，并且在所有基准测试中都将证明的大小减少了26%。此外，评估还展示了学习自定义策略对证明自动化的好处，使得一款先进的证明自动化工具的成功率相对提高了172%。