一句话：提出战术依赖图（TDG）驱动的战术发现方法，自动学习可复用战术并将证明重构得更模块化。
交互式定理证明器（如 Rocq、Lean）多用 tactic 风格证明，学习高层自定义战术对证明模块化与自动化至关重要。本文提出基于战术依赖图（TDG）的战术发现方法：TDG 刻画 tactic 应用间的逻辑依赖，并抽象掉无关语法细节，从而既能在多个证明中识别可复用策略、发现新战术，也能把已有证明重构得更模块化。作者在工具 TacMiner 中实现该方法，并与基于 anti-unification 的 Peano 对比。实验显示，TacMiner 学到的战术数量为 Peano 的 3 倍，所有基准上证明规模减少 26%；学到的自定义战术还能提升证明自动化，使最先进自动化工具的成功率相对提高 172%。
Enabling more concise and modular proofs is essential for advancing formal reasoning using interactive theorem provers (ITPs). Since many ITPs, such as Rocq and Lean, use tactic-style proofs, learning higher-level custom tactics is crucial for proof modularity and automation. This paper presents a novel approach to tactic discovery, which leverages Tactic Dependence Graphs (TDGs) to identify reusable proof strategies across multiple proofs. TDGs capture logical dependencies between tactic applications while abstracting away irrelevant syntactic details, allowing for both the discovery of new tactics and the refactoring of existing proofs into more modular forms. We have implemented this technique in a tool called TacMiner and compare it against an anti-unification-based approach ( Peano ) to tactic discovery. Our evaluation demonstrates that TacMiner can learn 3× as many tactics as Peano and reduces the size of proofs by 26% across all benchmarks. Furthermore, our evaluation demonstrates the benefits of learning custom tactics for proof automation, allowing a state-of-the-art proof automation tool to achieve a relative increase of 172% in terms of success rate.
@article{paperbot2949,
title = {Automated Discovery of Tactic Libraries for Interactive Theorem Proving},
author = {Yutong Xin and Jimmy Xin and Gabriel Poesia and Noah D. Goodman and Qiaochu Chen and Işıl Dillig},
journal = {Proceedings of the ACM on Programming Languages},
volume = {9},
number = {OOPSLA2},
year = {2025},
doi = {10.1145/3763121}
}