Holey: Staged Execution from Python to SMT (Talk Proposal)

on YouTube ↗22m

" summary

Holey is a Python library that stages satisfiability predicates to SMT by dynamic operator overloading and light AST rewriting, emits portable SMT‑LIB, swaps solvers, and re‑verifies candidate models back in Python for soundness. On the P3 benchmark the symbolic executor initially solves 64% of int puzzles, 34% of str, 27% overall and later reaches 42% overall after iteration, revealing a weakness in list encodings and synthesis queries. Results show solver differences (≈150 uniquely by Z3, 40 by CVC5) and a pragmatic hybrid where LLM heuristics help but do not fully replace solver guarantees.

AI-written summary · about

" chapters (16)

1. 0:00Holey and staged execution
2. 1:28Synthesis with Python and SMT
3. 7:26Solving synthesis puzzles
4. 8:11Holey pipeline core
5. 9:14Symbolic values dual representation
6. 10:39Conditionals and path exploration
7. 12:22Encoding lists in SMT
8. 13:27SMT-LIB vs solver bindings
9. 14:30Mutation and constraint explosion
10. 15:13Benchmark results
11. 16:16SMT solvers with LLM heuristics
12. 18:04Verification vs synthesis gap
13. 19:10Future with relational SMT
14. 19:51Lessons on functional encodings
15. 20:34Summary and acknowledgments
16. 20:55Q&A