Inductive Program Synthesis by Meta-Analysis-Guided Hole Filling
summary
Paper proposes a lightweight meta-analysis, feasibility square analysis, that predicts when forward/backward abstract interpretation will prune a partial program and ranks holes into three evidence tiers to choose the next hole to fill. Implementations add new forward/backward string operators (prefix/suffix+length), multihole simultaneous filling and incremental analysis for bitvectors and strings. The system proves soundness and an admissibility guarantee, measures a small overhead, and outperforms prior engines, uniquely solving 76 benchmarks and lowering cumulative solve time.
AI-written summary · about
chapters (19)
- 0:00Inductive program synthesis intro
- 0:45What inductive synthesis solves
- 1:50Role of holes in synthesis
- 3:17Why hole filling order matters
- 4:00Racer and booster analogy
- 5:26Feasibility square analysis intro
- 7:10Performance vs state-of-the-art
- 7:35Key results and solutions
- 7:55Main idea behind feasibility analysis
- 9:01Observations from analysis
- 10:26How feasibility analysis works
- 12:36Recommending hole order
- 14:06Admissibility guarantee
- 15:32Why feasibility analysis works
- 16:55Formal guarantees
- 17:19Adapting to synthesizers
- 17:42Ablation study and overhead
- 18:26Conclusion
- 18:47Q&A
related talks
25mRecursive Program Synthesis using Paramorphisms
32mHole Refinements for Polymorphic Type-and-Example Driven Synthesis
20mOptimal Program Synthesis via Abstract Interpretation
13mInductive Synthesis of Inductive Heap Predicates
40mSuperfusion: Eliminating Intermediate Data Structures via Inductive Synthesis
17mEfficient Bottom-Up Synthesis for Programs with Local Variables
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
19mPanel: Compilation Frameworks