Automating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
summary
Claims that monotonicity of concrete semantics lets an SMT solver automatically generate sound and often tight interval abstractions for top‑down enumerative synthesis. An implemented tool Moito queries SMT for monotonicity proofs, runs grammarflow analysis to tighten hole intervals, and uses interval-based pruning to cut whole template spaces. Evaluation on SyGuS benchmarks and domains like regex, CSV schemas, and imperative programs shows clear speedups over naive enumeration and an ablation without grammarflow, with artifacts and results reproducible.
AI-written summary · about
chapters (10)
- 0:00Automated pruning in synthesis
- 1:27Top-down enumeration challenges
- 3:12Pruning in regex and programs
- 4:57Unifying pruning with intervals
- 6:46Monotonicity for interval transformers
- 9:13Refining intervals with grammar flow
- 11:21Synthesis framework overview
- 12:23Evaluating pruning techniques
- 13:48Conclusion and future work
- 15:53Q&A
related talks
14mDataflow-Based Pruning for Speeding up Superoptimization
28mOriented Metrics for Bottom-Up Enumerative Synthesis
20mOptimal Program Synthesis via Abstract Interpretation
31mLetting users do the undecidable: lessons from program synthesis
30mSemantics-Guided Synthesis
15mTowards Proof Stability in SMT-based Program Verification
19mEnhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipu...
19mPresynthesis: Towards Scaling Up Program Synthesis with Finer-Grained Abstract Semantics