# ChopChop: a Programmable Framework for Semantically Constraining the Output of Language Models

arXiv: https://arxiv.org/abs/2509.00360 · HTML: https://mlsanity.com/paper/2509.00360/

## Key facts

- Cited by 15 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 30 Aug 2025.

## Built on by (most cited first, 15 of 15)

- [SEVerA: Verified Synthesis of Self-Evolving Agents](https://mlsanity.com/paper/2603.25111/) (2026)
- [Neuro-Symbolic Synergy for World Modeling](https://mlsanity.com/paper/2602.10480/) (2026)
- [The Alignment Problem in Constrained Code Generation](https://mlsanity.com/paper/2606.21619/) (2026)
- [Generative Compilation: On-the-Fly Compiler Feedback as AI Generates Code](https://mlsanity.com/paper/2607.13921/) (2026)
- [LLMs + Security = Trouble](https://mlsanity.com/paper/2602.08422/) (2026)
- [Hydra: Efficient, Correct Code Generation via Checkpoint-and-Rollback Support](https://mlsanity.com/paper/2605.15238/) (2026)
- [Learning the Error Patterns of Language Models](https://mlsanity.com/paper/2605.28328/) (2026)
- [Projectional Decoding: Towards Semantic-Aware LLM Generation](https://mlsanity.com/paper/2605.30054/) (2026)
- [Decode-Time Grammars: Constrained LLM Generation over a Refinement Order of Grammar Fragments](https://mlsanity.com/paper/2607.18357/) (2026)
- [Specification-Guided Synthesis of Deadlock-Free Communication Protocol Refinements with Large Language Models](https://mlsanity.com/paper/2607.27964/) (2026)
- [SafeQL: Search-based Refinement for Safe and Efficient LLM-based Text-to-SQL](https://mlsanity.com/paper/2608.09260/) (2026)
- [Semantic Prefix Oracles for LLM Decoding: Contracts and Differential Validation](https://mlsanity.com/paper/2609.35425/) (2026)
- [Constraint-Aware Training](https://mlsanity.com/paper/2610.02909/) (2026)
- [Structural Automata for Neural Semantic Parsing](https://mlsanity.com/paper/2610.13896/) (2026)
- [Nudge the Judge: Uncovering Program Decision Hijacking in Real-World Jev Applications](https://mlsanity.com/paper/2610.18612/) (2026)

## Abstract (arXiv)

Language models (LMs) can generate code but cannot guarantee its correctnessunicodex2014often producing outputs that violate type safety, program invariants, or other semantic properties. Constrained decoding offers a solution by restricting generation to only produce programs that satisfy user-defined properties. However, existing methods are either limited to syntactic constraints or rely on brittle, ad hoc encodings of semantic properties over token sequences rather than program structure. We present ChopChop, the first programmable framework for constraining the output of LMs with respect to semantic properties. ChopChop introduces a principled way to construct constrained decoders based on analyzing the space of programs a prefix represents. It formulates this analysis as a realizability problem which is solved via coinduction, connecting token-level generation with structural reasoning over programs. We demonstrate ChopChop's generality by using it to enforce (1) equivalence to a reference program and (2) type safety. Across a range of models and tasks, ChopChop improves success rates while maintaining practical decoding latency.