Combining Top-down Propagation and Bottom-up Enumeration for Inductive Synthesis

on YouTube ↗28m

" summary

Combines top-down propagation with bottom-up enumeration to generate small component expressions and compose them into full programs; implements this in Duet and evaluates on 1500 tasks from SyGuS and other benchmarks. Duet incrementally grows a component pool, uses inverse functions and alignment-based heuristics for string replace, and composes solutions that often use components of size ≤7 (average size 4). Empirically Duet solves 94% solved of problems, outperforming EUSolver and CVC4 and beating Euphony on harder cases.

AI-written summary · about

" chapters (20)

1. 0:00Start
2. 2:39Reconciling the Two Approaches
3. 3:00Our Contributions
4. 3:36Our Duet
5. 4:43Example
6. 6:43Existing Bottom-up Enumerative Strategy
7. 7:51Top-Down Propagation
8. 13:52Only for DSLs with Balanced Expressivity
9. 14:22Our Key Idea
10. 15:31Component Generation
11. 15:52Inverse Set Outputs of Components
12. 17:16We don't miss a solution
13. 19:28Component-guided Inverse Function
14. 23:07Our Inverse Functions for SyGus
15. 24:02Universal Inverse Function
16. 24:55Evaluation Setup
17. 25:23Benchmarks
18. 25:47Comparison to the Winners of SyGus Competitions
19. 26:47Comparison to Euphony
20. 27:31Analysis of Component Sizes