Letting users do the undecidable: lessons from program synthesis
summary
Argues that undecidable program synthesis becomes usable by shifting work into an interaction model and adapting the synthesizer: examples go through a live UI with projection boxes that collect trace-complete examples, the backend uses grammar-based generate-and-test plus an SMT solver, and the synthesizer is extended to check variable-orderings for loop traces. Demonstrations show solver answers in ~2–3s for examples, timeouts around 7s, and symbolic results are correct by construction versus flaky LLM completions.
AI-written summary · about
chapters (12)
- 0:00Program synthesis intro
- 1:57What is program synthesis
- 3:27Correctness in synthesis
- 7:47Programming by example
- 13:38Synthesis search challenges
- 14:42Why synthesizers are hard
- 16:49Interaction models role
- 19:20Live programming boxes
- 21:50Loops in synthesis
- 26:48Generalizing interaction
- 27:49Future of synthesis research
- 28:13Q&A
related talks
26mProgram Synthesis Using Example Propagation
20mOptimal Program Synthesis via Abstract Interpretation
14mOne Down, 699 to Go: or, synthesising compositional desugarings
53mSemantics-based program manipulation in the age of LLMs
20mAutomating Pruning in Top-Down Enumeration for Program Synthesis Problems with(…)
19mEnhanced Enumeration Techniques for Syntax-Guided Synthesis of Bit-Vector Manipu...
21mSynthesizing Formal Semantics from Executable Interpreters
22mCounterexample-Guided Inference of Modular Specifications