Optimal Program Synthesis via Abstract Interpretation
summary
The paper presents a synthesis framework that finds numerically parameterized programs optimally by enumerating generalized partial programs and running A guided by abstract-interval accuracy bounds*. It builds admissible heuristics from abstract interpretation (including custom abstract transformers for monotonic DSL semantics), implements the algorithm on two existing DSLs (Quiver and NEAR) and optimizes F1/accuracy on real labeled datasets, and empirically runs orders-of-magnitude faster than prior SMT-based optimal synthesizers while provably retaining optimality.
AI-written summary · about
chapters (6)
- 0:00Introduction to the problem
- 3:37Standard synthesis techniques
- 7:18Generalized partial programs
- 8:09Abstract search algorithm
- 12:54Implementation and evaluation
- 19:09Discussion and conclusion
related talks
28mSynthesizing Abstract Transformers
31mLetting users do the undecidable: lessons from program synthesis
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
13mProgram Analysis via Efficient Symbolic Abstraction
17mAlgebro-geometric Algorithms for Template-Based Synthesis of Polynomial Program...
37mA Tour of Program Optimization
25mNice to Meet You: Synthesizing Practical MLIR Abstract Transformers
30mAnalyzing Programs with SMT Solvers