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 3x 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.

翻译：提升证明的简洁性与模块化程度对于推动基于交互式定理证明器（ITP）的形式化推理至关重要。由于Rocq、Lean等多数ITP采用战术式证明范式，学习更高层次的定制战术对证明模块化与自动化具有关键意义。本文提出一种创新的战术发现方法，该方法通过战术依赖图（TDG）识别跨多证明的可复用证明策略。TDG在捕捉战术应用间逻辑依赖关系的同时，能够抽象无关的语法细节，从而既能发现新型战术，又能将现有证明重构为更具模块化的形式。我们将该技术实现为名为TacMiner的工具，并与基于反统一化的战术发现方法Peano进行对比评估。实验表明：TacMiner发现的战术数量是Peano的3倍，且在所有基准测试中平均将证明规模缩减26%。此外，评估结果验证了定制战术学习对证明自动化的增益效果——该方法使前沿证明自动化工具的成功率获得172%的相对提升。