Absynthe: Abstract Interpretation-Guided Synthesis

on YouTube ↗20m

" summary

Framework uses user-defined abstract domains to prune families of candidate programs during enumerative search, infers abstract values for intermediate holes, and checks candidates with concrete execution against test cases for soundness. Implementation in Ruby scales to SyGuS string benchmarks (competitive with enumerative solvers), uses Z3 for LIA-backed domains (e.g., 6,000 tests in ~100s) while cheap domains test many more faster (120k in ~47s), and synthesizes 18/26 AutoPandas tasks, demonstrating practical language-agnostic synthesis that combines domains to trade pruning for cost.

AI-written summary · about

" chapters (12)

1. 0:00Absynthe intro and abstract interpretation
2. 1:47Lightweight abstract domains
3. 3:16Example with pandas
4. 5:42Type checker for data frames
5. 6:48Column abstract interpreter
6. 8:54Synthesis process
7. 10:00Abstract values and evaluation
8. 11:49Handling abstract domains
9. 12:31Performance benchmarks
10. 14:17Solving autop pandas benchmarks
11. 15:18Conclusion and open-source
12. 15:40Q&A