ChopChop: A Programmable Framework for Semantically Constraining the Output of Language(…)
summary
ChopChop constructs constrained decoders that decide whether a token prefix has a completion satisfying a semantic spec by building prefix spaces and solving a realizability query with coinduction. It ships pruners for equivalence using egraphs and for a TypeScript subset enforcing type safety, evaluates on CodeLlama 13B, raises success rates versus grammar/unconstrained baselines, guarantees never emitting an invalid program by construction, and incurs a 2–3× decoding slowdown.
AI-written summary · about
chapters (12)
- 0:00Introduction to ChopChop
- 1:30Constraining language outputs
- 3:39Constraint decoding with examples
- 6:26Limitations of existing methods
- 9:15Core ideas of ChopChop
- 12:43Prefix spaces for ASTs
- 15:31Pruning functions with co-induction
- 18:01Equivalence constraints with egraphs
- 19:48Type safety in TypeScript
- 20:30Evaluation results and performance
- 21:54Summary and future work
- 22:15Q&A
related talks
01h 22mBeyond Decoding: Meta-Generation Algorithms for Large Language Models
26mDSPy: Compiling Declarative Language Model Calls into Self-Improving Pipelines
12mLanguage-Model Probabilistic Programming for Improving Autoformalization via Cycle(…)
21mChatGPT, LLMs, and LangChains - A Beginner's Guide
01h 50mChatGPT & LLMs: A Practical Starter's Guide to Language Chains
10mHomomorphic Reverse Differentiation of Iteration
41m"Do What I Mean": The History of AI and Program Synthesis
54mLost and Found in Translation