Invited Talk: Finding Good Programs by Avoiding Bad Ones
summary
Shows that proving unrealizability — certifying that an entire grammar-derived search space contains no correct program — gives a practical pruning primitive for synthesis and LLM-guided code generation. Implements several approaches: nondeterministic program-with-assertions and reachability encoding, grammar flow analysis abstractions that yield decidability for linear integer fragments, and a generic semantics-to-solver pipeline via constraint Horn clauses (Sangus) with Spacer/Z3. Builds a decoding method that corrects sampling bias so constrained LLM output converges to the conditional distribution; the techniques are effective and faster on many benchmarks.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:06Program synthesis rise
- 14:08Unrealizability problem
- 21:17Proving unrealizability
- 25:09Imperative unrealizability
- 31:55Sangus framework
- 35:28Program invariants
- 41:09Bridging synthesis and large language models
- 47:12Pruning bad programs
- 51:51Future directions
- 55:42Q&A
related talks
53mSemantics-based program manipulation in the age of LLMs
41m"Do What I Mean": The History of AI and Program Synthesis
33mLeveraging LLM Reasoning with Dual Horn Programs
22mTowards Verified Code Reasoning by LLMs
11mWriting Programs! That Write Other Programs!!
30mToward Programming Languages for Reasoning -- Humans, Symbolic Systems, and AI ...
21mTowards Neural Synthesis for SMT-Assisted Proof-Oriented Programming
15mCurrent Practices for Building LLM-Powered Reasoning Tools Are Ad Hoc—and We Can Do Better