Automated Discovery of Tactic Libraries for Interactive Theorem Proving
summary
A tool called TacMineR builds Tactic Dependence Graphs (TDGs) that encode formal input/output dependencies between tactic applications, finds isomorphic subgraphs via guided graph enumeration with pruning, and replaces them to refactor proofs into new higher-level tactics. Evaluation versus an anti-unification baseline (Peano) shows TacMineR learns 3× as many tactics, compresses corpora ~26% (baseline ~9%), and boosts a proof automation tool’s success rate by 172%.
AI-written summary · about
chapters (7)
- 0:00Tech Miner introduction
- 1:47Automate tactic discovery
- 3:34Proof refactoring with graphs
- 6:33Extracting tactics from proofs
- 8:18Pipeline: refactor and learn
- 9:01Evaluating Tech Miner
- 10:06Q&A
related talks
01h 03mImproved Assistance for Interactive Proof
19mAutomated Program Refinement: Guide and Verify Code Large Language Model with(…)
26mInteractive Theorem Provers for Proof Education
21mTowards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
01h 01mDiscussion
21mVerMCTS: Synthesizing Multi-Step Programs using a Verifier, a Large Language Model,(…)
45mUsing AI, statistics, and set theory to know what to test
47mExploring a complex codebase with AI