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

• Existing constrained-decoding techniques are limited in either the expressivity of enforceable constraints or the programmability of specifying them.Source: §1 · p. 2
• ChopChop constrains abstract syntax trees, allowing users to express semantic properties over program structure rather than only token sequences.Source: §1 · p. 2
• Given a token prefix, ChopChop computes the space of ASTs obtainable from completions and checks whether any member satisfies the semantic constraint.Source: §1 · p. 2
• Users provide a concrete-syntax grammar with AST translations and semantic pruners, separating syntax from reusable semantic constraints.Source: §1 · p. 2
• Regular codata and corecursive pruners let ChopChop reason over potentially infinite program spaces through finite representations.Source: §1 · p. 2
• Across equivalence-guided and type-safe decoding, ChopChop more often produces semantically valid programs than unconstrained and syntax-constrained baselines, with small computational overhead.Source: §1 · p. 3

2 Overview of ChopChop

• ChopChop accepts a grammar with parse-tree-to-AST translations and semantic pruners that remove constraint-violating programs.Source: §2 · p. 3

2.1 Semantic Constrained Decoding as Realizability

• A prefix represents all ASTs obtainable from its string completions, so semantic decoding becomes a realizability question over that program space.Source: §2.1 · p. 4

2.2 Realizability as Analysis over Regular Codata

• Infinite program spaces are represented as regular coterms with finite cyclic descriptions, enabling solver operations without materializing infinitely many programs.Source: §2.2 · p. 5
• ChopChop lexes a prefix into possible lexical sequences, derives parsers for them, converts the results into AST spaces, and combines those spaces.Source: §2.2 · pp. 5–6
• Semantic pruners are corecursive transformations that can be composed, as with odds and even_sum, to retain sums of odd literals having an even total.Source: §2.2 · pp. 6–7
• A fixpoint-based nonemptiness check determines whether the pruned space contains a valid completion, operating over finite structure despite potentially infinite represented sets.Source: §2.2 · p. 7
• The complete pipeline combines lexing, parser derivatives, user-defined pruners, and nonemptiness checking to enforce semantic constraints during generation.Source: Figure 2 · p. 5, §2.2 · p. 7

3.2 Constrained Decoding

• Constrained decoding maintains a worklist of token prefixes, expanding only prefixes that a monitor deems completable and returning completed strings that satisfy the constraint.The worklist stores prefixes with generation probabilities and can be instantiated by different decoding strategies.Source: §3.2 · p. 8, Figure 4 · p. 9

3.2.1 Soundness and Relative Completeness of Constrained Decoding.

• Soundness guarantees that returned strings satisfy the constraint when the final predicate check is sound, even if the monitor itself is unsound.This follows because the algorithm checks the completed output before returning it.Source: §3.2.1 · p. 8
• If the monitor is complete, constrained decoding is complete up to top-p and top-k sampling, whereas greedy or deterministic strategies need not preserve this relative completeness.Discarding an incompletable prefix can alter which solution the language model explores under deterministic search.Source: §3.2.1 · p. 9

3.3 Semantic Constrained Decoding

• For semantic constraints, realizability checking can be implemented by composing a prefix-space construction with a sound or approximate checker over AST program spaces.The checker is sound when every accepted space contains a satisfying AST and complete when every realizable space is accepted.Source: §3.3 · p. 10, §3.3.1 · p. 10
• Semantic constrained decoding asks whether a prefix has a completion whose parsed AST satisfies a predicate, reducing completability to realizability over AST spaces.The reduction replaces string-level reasoning with checking whether the prefix space contains a satisfying AST.Source: §3.3 · p. 10

3.3.1 Soundness and Relative Completeness of Semantic Constrained Decoding.

• When the semantic checker is sound, semantic constrained decoding is sound; when it is complete, decoding is complete up to top-p and top-k sampling.The semantic guarantees follow from the corresponding general constrained-decoding theorems.Source: §3.3.1 · pp. 10–11

4 ChopChop: Semantic Constrained Decoding via Coinduction

• ChopChop represents program spaces as regular codata and implements semantic pruners through corecursion, enabling analysis of infinite sets of ASTs.This approach is based on the regular-codata framework of Jeannin et al..Source: §4 · p. 11

4.1 Programming with Regular Coinduction

• Regular codata captures infinite objects with finitely many distinct subterms, such as the cyclic representation ones = ICons 1 ones.Regularity permits finite representations of otherwise infinite streams.Source: §4.1 · p. 11, Figure 5 · p. 11
• Properties of regular codata can be computed in finite time using fixpoint procedures over their cyclic term graphs.This supports questions such as whether a represented program space is nonempty.Source: §4.1 · p. 11

Computations over Regular Codata.

• Regular corecursive functions compute over regular coterms by memoizing expansions and creating cycles when previously seen calls recur.This provides explicit computation over regular infinite structures.Source: Computations over Regular Codata · p. 12
• The framework does not enforce termination for user-defined functions, so nonregular outputs and nontermination remain outside its guarantees.Users are advised to recurse on input subterms and avoid certain fixpoint-annotated return types.Source: Computations over Regular Codata · p. 12

4.2 Program Spaces as Coterms

• ProgramSpace represents sets of ASTs using Empty, Union, Lit, and ASTNode constructors, with fixpoint analysis supporting emptiness checks for cyclic spaces.The representation lifts individual program datatypes into spaces that can be manipulated generically.Source: §4.2 · pp. 12–13

4.3 Parsers as Coterms

• The parser is represented as codata with states for failure, choice, lexical constants, completed lexemes, and sequential composition with AST-building actions.Actions specify how completed parse trees are converted into AST nodes.Source: §4.3 · p. 14, §4.3.2 · p. 15

4.3.1 Derivatives on Parsers.

• A corecursive derivative advances parser state by consuming lexemes, using nullability to move across completed sequence elements.The derivative handles parser states compositionally across empty, constant, choice, and sequence cases.Source: §4.3.1 · p. 14, §4.3.2 · p. 15

4.3.2 From Parsers to Program Spaces.

• The image function converts parser states into program spaces, producing unions, literal spaces, or AST-node spaces according to the parser structure.Together with lexing and derivatives, this tracks valid program completions during generation.Source: §4.3.2 · pp. 14–15

4.4 Implementation

• ChopChop is implemented as an embedded Python DSL for symbolic manipulation of coinductive structures.The implementation draws on regular-coinduction work such as CoCaml without using CoCaml directly.Source: §4.4 · pp. 15–16

5 Case Studies

• ChopChop demonstrates semantic constrained decoding for equivalence in a basic functional language and type safety in TypeScript.Source: §5 · p. 16

5.1 Equivalence-Guided Decoding

• Program equivalence is approximated with e-graphs that compactly represent rewrite-equivalent programs, whose regular tree language is converted into a semantic pruner.The pruner intersects the prefix space with the finite tree automaton induced by the e-graph.Source: §5.1 · pp. 16–17
• Let bindings are handled by adding a rewrite from a completed binding expression to its variable before pruning the final expression.Source: §5.1 · p. 17

5.2 Type-Safe Decoding for TypeScript

• Because well-typed terms are not generally a regular tree language, ChopChop uses an overapproximate pruner that conservatively discards many ill-typed programs while preserving all well-typed programs.The framework naturally supports this overapproximation through delayed checking with collapse.Source: §5.2 · pp. 17–19
• The TypeScript type pruner operates on program spaces, returning an overapproximation of programs well-typed under an environment and target type.It is designed as an analogue of deterministic bidirectional type-checking judgments.Source: §5.2 · p. 18
• Function applications require delaying argument pruning until the function space resolves to a single AST whose type can be inferred.Before resolution, the pruner excludes functions that cannot return the target type while leaving the argument space unmodified.Source: §5.2 · p. 18
• For left-to-right prefixes, function spaces resolve before arguments are written, enabling precise type pruning when argument generation begins.Source: §5.2 · p. 19

6 Evaluation

• The evaluation asks whether ChopChop improves semantic-constraint satisfaction and measures the computational cost of enforcing constraints.Source: §6 · p. 19

6.1 Experiment Setup

• The baselines are unconstrained decoding and grammar-constrained decoding, which enforces syntactic validity without semantic restrictions.Source: §6.1 · p. 19
• The equivalence benchmark contains 10 refactoring tasks, and correctness requires a complete equivalent program without post-processing.The study reports both undelimited and delimiter-prompted unconstrained variants to separate formatting failures from other failures.Source: Benchmarks: Equivalence-Guided Decoding · p. 19

• The benchmark extracts 72 of 809 TypeScript-translated MBPP tasks that can be solved in ChopChop’s language fragment.Prompts additionally instruct models to avoid constructs outside that fragment.Source: Benchmarks: Type-Safe Decoding · p. 19

• A TypeScript response is counted as correct when the generated program compiles, with comparison against Mündler et al.’s tool [32].Source: Benchmarks: Type-Safe Decoding · p. 20
• Experiments use DeepSeek-Coder-6.7b, CodeLlama-7B, and CodeLlama-13B at temperatures 0.01, 0.3, 0.5, 0.7, and 1.0.Source: Models, Parameters and Hardware · p. 20

• Runs stop when the END token is generated or a 150-second timeout is reached.The procedure applies this budget to each benchmark, model, decoder, and temperature.Source: Procedure · p. 20
• Rejected tokens are handled by removing the token and resampling after backtracking one token.Source: Procedure · p. 20
• Constrained runs can fail when unrealizable tokens exhaust the token or time budget, while unconstrained runs can fail without an END token.Source: Procedure · p. 20

6.2 RQ1: Effectiveness

• Semantic constrained decoding consistently and often dramatically improves successful generations over unconstrained and grammar-constrained decoding across benchmarks.Table 1 compares the three strategies across models and temperatures; success requires a complete program satisfying equivalence or type-safety constraints.Source: §6.2.1 · p. 20, Procedure · p. 20, Table 1 · p. 21

6.2.1 Quantitative Evaluation.

• Equivalence benchmarks expose poor unconstrained performance because small models, out-of-distribution toy languages, and natural-language outputs frequently prevent valid equivalent programs.Source: §6.2.1 · p. 20
• Semantic constrained decoding improves TypeScript success by 28.0%, 10.1%, and 23.2% for DeepSeek-Coder-6.7b, CodeLlama-7B, and CodeLlama-13B, respectively, averaged across temperatures.Grammar-constrained decoding performs worse than unconstrained generation in this setting, while Mündler et al. [32] performs better at medium and highest temperatures.Source: §6.2.1 · p. 21

6.2.2 Qualitative Evaluation.

• Grammar constraints can admit natural language as syntactically valid function calls, whereas semantic constraints reject undefined-variable programs and prevent premature termination of inequivalent programs.Source: §6.2.2 · pp. 21–22
• Type-safety constraints prevent variable-name and function-name hallucinations, eliminating many errors observed in grammar-constrained and unconstrained modes.Source: §6.2.2 · pp. 21–22

6.3 RQ2: Overhead

• Semantic constrained decoding adds tens to a couple hundred milliseconds per generated token, compared with 81 ms for unconstrained CodeLlama-13B generation.Table 2 reports the overhead in milliseconds per produced token.Source: §6.3 · p. 22, Table 2 · p. 23
• For CodeLlama-7B, Figure 12 shows how many unsuccessful tokens precede each realizable token during semantic constrained decoding.Source: §6.3 · p. 22, Figure 12 · p. 23
• Across all models, 96.4% of TypeScript tokens pass on the first semantic-constrained attempt, compared with 96.1% under grammar-constrained decoding.Source: §6.3 · pp. 22–23

• Unlike grammar-constrained decoding, ChopChop targets semantic properties that context-free grammars cannot express, such as type safety and program invariants.Source: §7 · p. 23
• String-based monitors and completion engines support expressive constraints but require users to write checkers over program strings rather than abstract syntax.ChopChop instead defines pruners over program spaces, enabling applications such as equivalence-guided decoding.Source: §7 · p. 23
• ChopChop builds on algebraic and derivative-based views of parsing, with zipper-based variants identified as possible efficiency improvements.Source: §7 · pp. 23–24
• Its implementation uses regular coinduction to represent cyclic program spaces and solvers analogous to those in CoCaml.Source: §7 · p. 24
• ChopChop’s corecursive backend requires productivity but also regularity or termination, so guarded corecursion alone is insufficient.Source: §7 · p. 24
• The framework adapts synthesis techniques for unrealizability and pruning, including type- and example-based infeasible-space removal, to language-model decoding.Source: §7 · p. 24
• Abstract finite tree automata can encode finite abstract domains as ChopChop pruners, while grammar-flow analysis addresses more complex infinite domains.Source: §7 · pp. 24–25
• Bidirectional typing maps naturally onto ChopChop: type checking constructs well-typed program spaces, while type inference analyzes spaces through fixpoints.Source: §7 · p. 25

• ChopChop imposes semantic constraints on abstract syntax trees rather than string syntax through recursive pruners over finite representations of infinite program spaces.Source: §8 · p. 25
• The framework enables equivalence-guided generation in which outputs are equivalent to an input program up to specified rewrite rules.Source: §8 · p. 25
• Users must define corecursive pruners that return regular spaces, while the current implementation incurs noticeable per-token overhead.The conclusion identifies better interfaces, faster backends, and automated reasoning about pruner approximation as future directions.Source: §8 · p. 25

A.1 Soundness and Completeness Proofs

• The appendix proves that constrained decoding returns only outputs satisfying the constraint and preserves nonzero-probability unconstrained solutions when realizability checking is complete.The completeness argument applies to top-p, top-k, and greedy decoding.Source: §A.1 · p. 29

A.2 Lexing

• Partial lexing incrementally tracks annotated regular-expression matches, discards non-maximal-munch candidates, removes ignorable tokens, and memoizes prefix computations.The resulting lexer state represents maximal-munch lexes of program completions under the stated whitespace and disjointness assumptions.Source: §A.2 · p. 30, Figure 13 · p. 31
• Under its stated assumptions, partial_lex exactly characterizes maximal-munch lexes of all continuations, with whitespace tokens removed.The proof relies on lexical-prefix coverage and uniqueness properties for every continuation.Source: §A.2 · p. 30

A.3.1 Details of Type Pruning.

• The TypeScript type-pruner uses an inference-only type system and recursively prunes program spaces, handling applications by first resolving the function before pruning its argument.Its implementation overapproximates type-checking program sets and combines pruning of subterms for cases such as addition and ternaries.Source: §A.3.1 · p. 32, Figure 14 · p. 34
• Bounding types to depth 3 prevents infinitely expanding function-application analyses and makes type_prune regular, but can accept ill-typed programs with deeply nested types.The authors report finding no such large types in generated programs; the overapproximation is the only relevant approximation for left-to-right constrained decoding.Source: §A.3.1 · p. 33

A.3.2 Benchmarks and Additional Data.

• The TypeScript evaluation uses instruct-mode prompts and 72 MBPP benchmarks from MultiPL-E, with task comments as prompts and function signatures as generation prefixes.The appendix also reports per-token guess counts for three generation modes and includes equivalence-guided benchmarks with rewrite rules added to prompts.Source: §A.3.2 · pp. 38, 40, Table 3 · p. 40

A.4 Equivalence-Guided Decoding

• The equivalence-guided benchmarks use a functional-language context restricting programs to identifiers, integers, arithmetic, application, and let expressions, with names drawn from the original program.A prompt variation adds rewrite rules to the language model, while NO-DELIMIT experiments remove the final context line.Source: §A.4.1 · pp. 40–41

A.4.1 Benchmarks and Additional Data.

• The refactoring prompt requires equivalent, readable programs using let bindings when helpful, without introducing new language features, comments, explanations, or variable redefinitions.It also requires outputting only code and stopping immediately.Source: §A.4.1 · p. 41
• The benchmark suite uses 10 benchmark programs; the cited passages explicitly list five: fetch_document, sqrt, pow, add_watermark, and start + (end - start) * scale.Source: §A.4.1 · p. 41
• The Egglog file defines arithmetic expressions and rewrites for constant folding, associativity, negation, distributivity, and reciprocal transformations.The encoded expression forms include addition, subtraction, negation, powers, square roots, multiplication, division, applications, numbers, strings, and variables.Source: §A.4.1 · pp. 42–43