Tactic Script Optimisation for Aesop
summary
Generates an optimized Lean tactic script from Aesop output using a three-stage pipeline (local dynamic optimization, structuring with static and dynamic reordering, global static passes), checks optimized single-tactic replacements by re-running them against the recorded pre/post states using goal equality up to renaming, avoids unsafe reorders when shared metavariables appear, and evaluates on 6,000 Aesop calls from Mathlib showing dynamic reordering is slower but practically usable and artifacts are available.
AI-written summary · about
chapters (11)
- 0:00ASOP and tactic optimization
- 1:06Tactic script generation
- 3:55Motivation for optimizing scripts
- 7:05Script optimization pipeline
- 9:57Local dynamic optimization
- 11:01Comparing goals with unpredictable names
- 13:51Structuring tactic scripts
- 16:42Reordering tactics with meta variables
- 19:55Dynamic reordering approach
- 20:39Conclusion and future work
- 21:43Q&A
related talks
26mTowards Efficient Model Comparison Using Automated Program Rewriting
36mStatic Analysis of APL for Tooling and Compliance
25mEGSTRA: E-Graph-Based Strategy for Test Suite Reduction and Abstraction
15mHeuristic Analysis from Source Code via Symbolic-Guided Optimization
15mStrategic Tree Rewriting in Attribute Grammars
14mA Sound Static Analysis Approach to I/O API Migration
45mAI agents in practice - beyond the prototype
21mProgram Synthesis From Partial Traces