Inductive Program Synthesis via Iterative Forward-Backward Abstract Interpretation

on YouTube ↗17m

" summary

Implements a synthesis tool, Shimba, that uses iterative forward-backward abstract interpretation plus a reduced product domain and selective finite concretization (concretization size is a tunable parameter, default 8) to prune top-down SyGuS search more precisely. Evaluated on five benchmarks across branch-free, vector-manipulation and circuit-transformation tasks and compared to DUET/Pro, Shimba solves more problems and often runs faster, though a competitor outsolves Shimba on one branch-heavy suite by 27 cases; backward analysis provides the biggest speedup.

AI-written summary · about

" chapters (14)

1. 0:00Inductive program synthesis
2. 0:24Problem definition and approach
3. 1:47Forward-backward abstract interpretation
4. 3:11Limitations of forward-only
5. 4:15Synergy of forward and backward
6. 5:39Reduced product domain
7. 6:01Finite concretization for backward
8. 7:25Shimba tool architecture
9. 7:47Synthesis example
10. 9:54Component generation and pruning
11. 11:18Benchmark evaluation
12. 12:42Comparison with variants
13. 13:05Summary and future
14. 13:27Q&A