Enhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipu...
summary
DryadSynth implements a concrete pipeline that combines term-graph-based enumeration, example-guided filtration, LLM-prioritized components, and a bottom-up deduction step to prune and prioritize bit-vector candidates. The solver evaluates on >700 SyGuS benchmarks plus Hacker’s Delight examples and outperforms state-of-the-art solvers in solved count, time, and solution size; it uniquely solves 31 synthesis problems for the first time, including 5 well-known Hacker’s Delight challenges.
AI-written summary · about
chapters (10)
- 0:00Syntax-guided synthesis intro
- 1:06Bit-vector challenges
- 3:10Existing synthesis approaches
- 6:01Why bit-vectors are hard
- 7:30Bottom-up deduction
- 10:01Term graph enumeration
- 11:07LLM-guided synthesis
- 12:56Implementation results
- 15:04Summary and future work
- 15:28Q&A
related talks
28mOriented Metrics for Bottom-Up Enumerative Synthesis
18mVerifying Solutions to Semantics-Guided Synthesis Problems
21mSynthesizing Formal Semantics from Executable Interpreters
31mLetting users do the undecidable: lessons from program synthesis
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
14mOne Down, 699 to Go: or, synthesising compositional desugarings
26mProgram Synthesis Using Example Propagation
32mHole Refinements for Polymorphic Type-and-Example Driven Synthesis