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

TL;DR

ChopChop is a novel programmable framework that constrains language model outputs to satisfy semantic properties like type safety and program equivalence, improving correctness without sacrificing efficiency.

Contribution

It introduces a principled, structure-aware decoding method based on program analysis and coinduction, enabling semantic constraints beyond syntactic restrictions.

Findings

Improves success rates in constrained program generation

Maintains practical decoding latency

Enforces semantic properties like type safety and equivalence

Abstract

Language models (LMs) can generate code but cannot guarantee its correctness$\unicode{x2014}$often 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.

Figures

Tables

Table 1. Table 1 . Successful generations for different decoding strategies across models and temperatures (higher is better). For equivalence-guided decoding we report the number of benchmarks for which an equivalent program was produced. For TypeScript we report the number of benchmarks on which compilable code was produced. Best results per column are bolded .

		DeepSeek-Coder-6.7b						CodeLlama-7B						CodeLlama-13B
		Temperature					Tot.	Temperature					Tot.	Temperature					Tot.
		0.01	0.3	0.5	0.7	1.0		0.01	0.3	0.5	0.7	1.0		0.01	0.3	0.5	0.7	1.0
Equivalence No Delimit (10 programs)	Unconstrained	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
	Grammar	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
	Semantic	7	7	8	8	3	33	8	9	9	9	8	43	10	8	8	10	6	42
Equivalence Delimit (10 programs)	Unconstrained	0	0	0	0	0	0	3	4	2	3	1	13	4	2	2	3	2	13
	Grammar	0	0	0	0	1	1	5	6	7	4	1	23	6	5	2	2	0	15
	Semantic	10	10	8	9	8	45	9	10	10	6	6	41	9	8	7	8	6	38
TypeScript (72 programs)	Unconstrained	57	55	48	45	9	214	69	71	71	66	31	308	68	67	60	47	17	259
	Grammar	38	31	28	19	10	126	67	65	62	59	36	289	68	67	57	36	8	236
	Semantic	65	62	61	58	28	274	72	71	72	66	58	339	72	69	69	66	43	319
	typespaper	62	69	71	68	67	337	67	72	70	71	71	351	70	72	70	68	67	347

Table 2. Table 2 . Overhead of checking realizability in semantic constrained decoding (milliseconds/produced token).

Overhead in ms/token	DeepSeek-Coder-6.7b					CodeLlama-7B					CodeLlama-13B
	Temperature					Temperature					Temperature
	0.01	0.3	0.5	0.7	1.0	0.01	0.3	0.5	0.7	1.0	0.01	0.3	0.5	0.7	1.0
Equiv No Delimit	225	221	199	233	216	159	77	74	77	161	58	68	67	61	142
Equiv Delimit	82	73	564	198	162	50	55	65	121	156	63	74	79	49	128
TypeScript	202	204	185	161	167	85	64	101	107	165	116	107	129	135	173

Table 3. Table 3 . Equivalence-guided decoding benchmarks with rewrite rules added to prompts.

		DeepSeek-Coder-6.7b						CodeLlama-7B						CodeLlama-13B
		Temperature					Tot.	Temperature					Tot.	Temperature					Tot.
		0.01	0.3	0.5	0.7	1.0		0.01	0.3	0.5	0.7	1.0		0.01	0.3	0.5	0.7	1.0
Equivalence Rules + No Delimit (10 programs)	Unconstrained	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
	Grammar	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0
	Semantic	4	3	4	6	3	20	8	6	10	6	4	34	9	10	10	7	6	42
Equivalence Rules + Delimit (10 programs)	Unconstrained	0	0	0	0	0	0	3	3	5	0	1	12	2	2	4	2	0	10
	Grammar	0	0	0	0	0	0	3	3	5	4	1	16	2	6	1	2	3	14
	Semantic	8	8	7	8	6	37	8	7	5	8	8	36	8	8	7	9	7	39

Equations

$$\begin{array}[]{rcl@{\hspace{1em}}l}\text{{int}}&::=&{[0\text{-}9]+}\hfil\hskip 9.24994pt&\\[2.0pt] E&::=&\textsc{int}\hfil\hskip 9.24994pt&\{\text{Lit \textdollar 1}\}\\[2.0pt] &\mid&E~\texttt{"+"}~\textsc{int}\hfil\hskip 9.24994pt&\{\text{Sum \textdollar 1 \textdollar 3}\}\end{array}$$

$$\mathsf{completable}(\omega ,\Phi )=\exists {\omega }^{\prime }\in {\Sigma }^{\ast }.\Phi (\omega {\omega }^{\prime })$$

$$\mathsf{completable}(\omega ,\Phi )\equiv \exists {\omega }^{\prime }.\varphi (\text{parse}(\omega {\omega }^{\prime }))$$

$$\mathsf{PrefixSpace}(\omega )\triangleq \{\text{parse}(\omega {\omega }^{\prime })\mid {\omega }^{\prime }\in {\Sigma }^{\ast }\}$$

$$\mathsf{completable}(\omega ,\Phi )\equiv \exists t\in \mathsf{PrefixSpace}(\omega ).\varphi (t)$$

$$\mathsf{realizable}(T,\varphi )\triangleq \exists t\in T.\varphi (t)$$

$$\mathsf{completable}(\omega ,\Phi )\equiv \mathsf{realizable}(\mathsf{PrefixSpace}(\omega ),\varphi )$$

$$L=\{\text{[1, +, 3]},\text{[1, +, 3[0-9]+]}\}$$

$$L=\{\text{[print]}\}$$

$$D_i(\text{pr @ int})=\text{pri @ nt}$$

$$\tilde{L}=\{(\text{pri @ nt})\}$$

$$\omega ={\alpha }_1{\alpha }_2{\alpha }_3{\alpha }_4\dots {\alpha }_{m-1}a$$

$${\omega }^{\prime }=\omega b{\alpha }_{m+1}{\alpha }_{m+2}$$

$$\begin{array}[]{ll}\text{Statements}\to&\\ &\text{\hskip-70.0001ptStatement}\\ &\text{\hskip-70.0001pt| Statement Statements}\\ \\ \text{Statement}\to&\\ &\text{\hskip-70.0001ptAssignment ;}\\ &\text{\hskip-70.0001pt| Exp ;}\\ &\text{\hskip-70.0001pt| return Exp ;}\\ &\text{\hskip-70.0001pt| Block}\\ &\text{\hskip-70.0001pt| function Var () : Type Block}\\ &\text{\hskip-70.0001pt| function Var ( Params ) : Type Block}\\ &\text{\hskip-70.0001pt| for ( Assignment ; Exp ; Reassignment ) Block}\\ &\text{\hskip-70.0001pt| while ( Exp ) Block}\\ &\text{\hskip-70.0001pt| if ( Exp ) Statement else Statement}\\ &\text{\hskip-70.0001pt| if ( Exp ) Statement}\\ \\ \text{Assignment}\to&\\ &\text{\hskip-70.0001ptlet Var : Type = Exp}\\ &\text{\hskip-70.0001pt| const Var : Type = Exp}\\ &\text{\hskip-70.0001pt| let Var = Exp}\\ &\text{\hskip-70.0001pt| const Var = Exp}\\ &\text{\hskip-70.0001pt| Reassignment}\\ \\ \text{Reassignment}\to&\\ &\text{\hskip-70.0001ptVar = Exp}\\ &\text{\hskip-70.0001pt| Var ++}\\ &\text{\hskip-70.0001pt| ++ Var}\\ &\text{\hskip-70.0001pt| Var += Exp}\\ \\ \text{Type}\to&\\ &\text{\hskip-70.0001ptnumber}\\ &\text{\hskip-70.0001pt| boolean}\\ &\text{\hskip-70.0001pt| () => Type}\\ &\text{\hskip-70.0001pt| ( Params ) => Type}\\ \\ \text{Block}\to&\\ &\text{\hskip-70.0001pt\{\}}\\ &\text{\hskip-70.0001pt| \{ Statements \}}\\ \end{array}$$

$$\begin{array}[]{ll}\text{Exp}\to&\\ &\text{\hskip-160.00024ptP3\_Exp}\\ &\text{\hskip-160.00024pt| P3\_Exp ? Exp : Exp}\\ \\ \text{P3\_Exp}\to&\\ &\text{\hskip-160.00024ptP2\_Exp}\\ &\text{\hskip-160.00024pt| P2\_Exp \&\& P3\_Exp}\\ &\text{\hskip-160.00024pt| P2\_Exp || P3\_Exp}\\ \\ \text{P2\_Exp}\to&\\ &\text{\hskip-160.00024ptP1\_Exp}\\ &\text{\hskip-160.00024pt| P1\_Exp < P1\_Exp}\\ &\text{\hskip-160.00024pt| P1\_Exp == P1\_Exp}\\ &\text{\hskip-160.00024pt...}\\ \\ \text{P1\_Exp}\to&\\ &\text{\hskip-160.00024ptBase\_Exp}\\ &\text{\hskip-160.00024pt| Base\_Exp + P1\_Exp}\\ &\text{\hskip-160.00024pt| Base\_Exp - P1\_Exp}\\ &\text{\hskip-160.00024pt...}\\ \\ \text{Base\_Exp}\to&\\ &\text{\hskip-160.00024ptLiteral}\\ &\text{\hskip-160.00024pt| Var}\\ &\text{\hskip-160.00024pt| ( Exp )}\\ &\text{\hskip-160.00024pt| Base\_Exp ( )}\\ &\text{\hskip-160.00024pt| Base\_Exp ( Args )}\\ &\text{\hskip-160.00024pt| - Base\_Exp}\\ \\ \text{Literal}\to\text{INT | "true" | "false"}\\ \\ \text{Var}\to\text{ID}\\ \\ \text{Args}\to\text{Exp | Exp , Args}\\ \\ \text{Typed\_Id}\to\text{Var : Type}\\ \\ \text{Params}\to\text{Typed\_Id | Typed\_Id , Params}\\ \end{array}$$

$$\frac{\text{vbox}\text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢\text{0}⟹\text{int}}$$

$$\frac{\text{vbox}\text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢\text{True}⟹\text{bool}}$$

$$\frac{\text{vbox}(x,\tau ,\_)\in \Gamma \text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢x⟹\tau }$$

$$\frac{\text{vbox}\Gamma ⊢e1⟹\text{int}\Gamma ⊢e2⟹\text{int}\text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢e1+e2⟹\text{int}}$$

$$\frac{\text{vbox}\Gamma ⊢e_1⟹\text{bool}\Gamma ⊢e_2⟹\tau \Gamma ⊢e_3⟹\tau \text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢(e_1?e_2:e_3)⟹\tau }$$

$$\frac{\text{vbox}\Gamma ⊢f⟹{\tau }_1,\dots ,{\tau }_n\to \tau \forall j<n.\Gamma ⊢x_j⟹{\tau }_j\text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢f(x_1,\dots ,x_n)⟹\tau }$$

$$\frac{\text{vbox}\Gamma ⊢e⟹{\tau }^{\prime }\Gamma ⊢\bar{s}⟹\tau \text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢e;\bar{s}⟹\tau }$$

$$\frac{\text{vbox}\Gamma ⊢e⟹\top \Gamma +(x,\tau ,\text{mutable})⊢\bar{s}⟹{\tau }^{\prime }\text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢\text{let}x:\tau =e;\bar{s}⟹{\tau }^{\prime }}$$

$$\frac{\text{vbox}\Gamma ⊢e⟹\tau \Gamma +(x,\tau ,\text{immutable})⊢\bar{s}:{\tau }^{\prime }\text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢\text{const}x:\tau =e;\bar{s}:{\tau }^{\prime }}$$

$$\frac{\text{vbox}\Gamma ⊢e⟹\text{bool}\Gamma ⊢s_1⟹\tau \Gamma ⊢s_2⟹\tau \Gamma ⊢\bar{s}⟹\tau \text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢\text{if}e\text{then}{s}_1\text{else}{s}_2;\bar{s}⟹\tau }$$

$$\frac{\text{vbox}\Gamma ⊢e⟹\text{bool}\Gamma ⊢s_1⟹\tau -()\Gamma ⊢s_2⟹\tau -()\Gamma ⊢\bar{s}⟹\top \text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢\text{if}e\text{then}{s}_1\text{else}{s}_2;\bar{s}⟹\tau }$$

$$\frac{\text{vbox}\Gamma ⊢e⟹\text{bool}\Gamma ⊢s⟹\tau \Gamma ⊢\bar{s}⟹\tau \text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢\text{while}(e)s;\bar{s}⟹\tau }$$

$$\frac{\text{vbox}\text{vbox}}{\text{vbox}\text{vbox}\Gamma ⊢\cdot ⟹()}$$

Full text

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.

LLM, Semantic Constrained Decoding, Coinduction

††copyright: cc††doi: 10.1145/3776708††journalyear: 2026††journal: PACMPL††journalvolume: 10††journalnumber: POPL††article: 66††publicationmonth: 1††ccs: Software and its engineering General programming languages††ccs: Computing methodologies Machine learning††ccs: Theory of computation Semantics and reasoning

1. Introduction

Language models (LMs) have fundamentally transformed how we interact with code—generating functions, completing boilerplate, and even suggesting entire programs. Yet despite their success, LMs offer no guarantees of correctness: they often produce code that looks plausible but violates critical syntactic or semantic properties. This limitation arises because LMs generate text in a purely probabilistic fashion—at each step, they sample the next token from a distribution conditioned on the sequence they have produced so far.

Constrained decoding addresses this problem by enforcing constraints on the sequence an LM generates (wang2023grammar; willard2023efficient; geng2023grammarconstrained; monitors; typespaper): a constrained decoder modifies the sampling process to forbid selecting next tokens that would violate the constraint. Concretely, a constrained decoder performs a completability analysis at each step to determine whether the partially generated sequence can still be extended into a completion that satisfies the constraints. If not, the LM backtracks and tries another token. By construction, any output a constrained decoding algorithm returns satisfies the user-provided constraints.

Existing constrained-decoding techniques are limited in either expressivity (the complexity of the constraints they can enforce) or programmability (the ease with which users can specify constraints).

Programmable but not Expressive. Most of the constrained-decoding literature is interested in the problem of forcing the LM to only produce sequences that are accepted by a user-given context-free grammar (CFG) (greatgramma; gad; syncode; llguidance). While CFGs provide a programmable interface for specifying syntactic constraints, many desirable semantic properties—such as type safety or adherence to invariants—cannot be expressed as context-free languages.

Expressive but not Programmable. monitors proposed an automaton-based framework (which they call monitors) to connect string-based static analyses (e.g., those offered by a Language Server Protocol) to a constrained decoder. typespaper implement a monitor to enforce well-typedness of TypeScript code. Although monitors are expressive, they operate on the string representation of a program. Because semantic constraints are usually defined over abstract syntax trees, it is nontrivial (and often unnatural) to translate semantic constraints into a corresponding completability analysis over strings. For example, while an expression like 1 + myString would likely be considered ill-typed as a complete program, as an incomplete program it may still admit a valid continuation (e.g., 1 + myString.length). Furthermore, because monitors are not defined over abstract syntax, they must manually handle syntax-level concerns—lexing, precedence, left recursion, and so on—failing to separate syntactic and semantic constraints. By operating over concrete syntax, monitors sacrifice programmability and offer no clear path for enforcing program equivalence or other complex semantic invariants.

In this paper, we ask:

Can we design a framework for constrained decoding that is both expressive and programmable?

Our approach.

We present ChopChop, a framework that enables programmable constrained decoding. The key novelty of ChopChop is that it allows one to constrain the abstract syntax trees corresponding to the output sequences produced by an LM.

Conceptually, given a semantic constraint over abstract syntax trees, ChopChop has to decide whether a sequence of tokens in the concrete syntax (i.e., the output of an LM) can be completed so that parsing it will produce an abstract syntax tree that satisfies the given constraint. Given a sequence of tokens, ChopChop solves the above problem in two steps: (i) it computes a representation of the set of ASTs (a program space) producible by completing the token sequence with some suffix string—and (ii) it checks whether any AST in this space satisfies the semantic constraint.

More concretely, to use ChopChop, users provide two inputs: (i) a grammar defining the concrete syntax of the language and how abstract syntax trees can be extracted from sequences in the concrete syntax, and (ii) a set of semantic pruners which describe how to prune constraint-violating ASTs from a program space. Decoupling the semantic constraint from concrete program syntax separates concerns, allowing for an interface that is easy to program.

The key programming-language insight that enables ChopChop’s pipeline to work despite having to deal with infinite sets of ASTs is the following: program spaces can be represented as regular codata and semantic pruners can be implemented via corecursion in the style of (cocaml).

Applications.

We demonstrate the generality of ChopChop through two diverse applications:

• •

Program equivalence-guided decoding: We constrain a language model to generate programs equivalent, modulo term rewriting, to a reference program. Here, the semantic pruner uses e-graphs (egg) as program spaces to efficiently represent all programs that are equivalent to the reference program.

• •

Type-safe decoding: We constrain a language model to emit only well-typed programs in a subset of TypeScript. Here, the semantic pruner lifts type checking to operate over co-inductively defined sets of abstract syntax trees—i.e., the pruner constrains away possible program completions that will not typecheck.

For these domains, ChopChop produces programs that satisfy given semantic constraints more often than both unconstrained language models and approaches that only constrain the program syntax.

Contributions.

• •

The first programmable framework for semantic constrained decoding (Section 2).

• •

A formal connection between semantic constrained decoding and realizability in program synthesis, showing that enforcing semantic properties during generation reduces to checking whether the set of possible completions contains a valid program (Section 3).

• •

A novel constrained decoding algorithm based on corecursion; the algorithm incrementally builds and analyzes a coinductive representation of the space of programs obtainable from a prefix (Section 4).

• •

An implementation of our framework in a tool, ChopChop, which we instantiate in two challenging domains—equivalence-guided decoding and type-safe generation—demonstrating the generality of our approach (Section 5).

• •

An evaluation of ChopChop on the two domains—ChopChop produces programs that satisfy given semantic constraints more often than both unconstrained and purely syntax-constrained baselines while incurring a small computational overhead (Section 6).

Section 7 discusses related work, and Section 8 concludes.

2. Overview of ChopChop

We illustrate our approach with the following simple prompt one might task an LM with:

[TABLE]

For example, the expression 5+7 is a valid solution, since 12 is even and both 5 and 7 are odd. In general, there is no guarantee that an LM will produce a valid response—it could generate a sum with even numbers (e.g., 2+2), an odd total (e.g., 1+1+1), or totally nonsensical output (e.g., banana).

A user of ChopChop can enforce the constraints mentioned in the prompt by providing two inputs:

1. (1)

A grammar (Figure 1) defining the syntax of the language, annotated with rules for translating parse trees to ASTs. 2. (2)

A set of semantic pruners (Figures 3(a) and 3(b)) each representing a constraint on ASTs. At a high-level, a pruner is a function that takes in a representation of a space of programs and returns (an approximation of) the subspace of constraint-satisfying programs.

Given these inputs, ChopChop guarantees that any generated program is syntactically valid and satisfies the provided semantic constraints—in our case, the output being a sum of odd integers with an even total.111While the constraints being enforced in this example are task-specific, in practice users would write pruners for general constraints that apply across all tasks in an application domain (as in Section 5). Crucially, ChopChop enforces constraints during generation, rather than waiting for the LM to produce a complete program and then retrying from scratch upon failure.

2.1. Semantic Constrained Decoding as Realizability

Returning to our example, suppose the LM has already generated the prefix 1+2, and the LM’s top two choices for the next token are + and 2. ChopChop disallows + since any program starting with 1+2+ will contain an even integer. However, it allows the next token 2 as it can still lead to a valid completion (for example, 1+221).

To rule out the token +, ChopChop must determine that no completion of the sequence 1+2+ parses to an AST satisfying our example constraints. We say that ChopChop solves semantic constrained decoding because it prunes the LM’s choices based on semantic constraints over ASTs (as opposed to syntactic constrained decoding which enforces shallow syntactic properties of the token stream). It is challenging to prune the LM’s choices directly because constraints are expressed at the AST level, while 1+2+ is an incomplete string prefix.

Our first key insight is that a prefix represents the space of programs corresponding to its completions. Instead of attempting to reason about AST-level properties on string completions of 1+2, ChopChop reasons about the space of ASTs that this prefix represents. In the synthesis literature, checking satisfiability of constraints over spaces of ASTs is studied under the name realizability (unrealizability2019). The next section outlines our realizability-based approach to semantic constrained decoding in more detail.

2.2. Realizability as Analysis over Regular Codata

Next, we show how to formulate and solve the realizability problem to which completability of the prefix 1+2 reduces. We split this problem into three goals:

1. (1)

Representation: How can we finitely describe infinite program spaces? 2. (2)

Completion: Given a string $\omega$, how can we construct the space of all ASTs corresponding to completions of $\omega$? 3. (3)

Analysis: Does there exist a program in the constructed space satisfying the constraint?

Our next key insight is that regular codata provides a structured abstraction for reasoning about spaces of programs. Our solutions to (1)-(3) are built around this idea. In the rest of the section, we describe our approach following the overview given in Figure 2.

Goal 1: Representing Infinite Program Spaces

In our example, programs consist solely of integer literals and sums. To represent an AST for a single program, we can use the following datatype:

⬇

data Expr = Lit String -- a numeric literal, e.g., Lit "5"

| Sum Expr Expr -- a sum of two expressions

We would like to lift this definition to represent (possibly infinite) spaces of ASTs. The first step is to extend the signature of Expr as follows:

⬇

data ExprSpace = Empty

| Union [ExprSpace]

| Lit Regex

| Sum ExprSpace ExprSpace

An ExprSpace can be empty, a union of spaces, a regular expression that represents a set of concrete literals, or an application of the Sum constructor lifted to the product of two program spaces. Readers familiar with version space algebras (VSA2003; FlashMeta2015) will recognize this representation as a version space, where Union is the union node and Sum is a join node.

For spaces to represent infinite sets, we must generalize the shape of terms and allow corecursion. We represent program spaces as regular coterms, i.e., infinite, cyclic terms with a finite description. For example, the space consisting of all sums of integers can be represented using the following corecursive definition:

⬇

all =

let int = Lit "[0-9]+" in

Union [int, Sum all int]

Note that even though all is self-recursive, it has a finite representation in memory as a cyclic term in which the definition of all contains a back-reference to itself. Coterms that admit a finite representation (but are potentially infinite) are called regular.

In ChopChop, all program spaces are regular and represented using this finite, cyclic form (Section 4). We implement and manipulate coterms via a solver inspired by CoCaml (cocaml), an extension to OCaml that supports equational reasoning for regular coterms. This solver can perform computations over program spaces—e.g., applying transformations such as odds and even_sum (Figure 3)—without materializing infinite sets.

Goal 2: Computing Prefix Spaces

Given a string prefix $\omega$, we need to compute the space of all ASTs that can be produced by parsing any completion of $\omega$. This construction is done with reference to a user-supplied parser definition that defines a grammar for the language as well as how to convert parse trees to ASTs (Figure 1).

As a first step, we lex $\omega$ into a finite set of lexical prefixes that encode how $\omega$ can be lexed once its last lexeme has been completed. For example, the prefix $\omega=\text{1+2}$ has two valid lexical prefixes, representing the different ways $\omega$ could be lexed depending on the next character:

• •

["1","+","2"]: where the next character is non-numeric (as in 1+2+).

• •

["1","+","2[0-9]+"]: where the next character continues the numeric literal (as in 1+21).

Next, for each lexical prefix we construct a corresponding program space representing its completions. This construction can be done naturally following the parsing with derivatives methodology (parsingWithDerivatives). In our framework, parsers are regular coterms representing the set of possible parse trees producible from their current state222We use the term lexeme for programming-language tokens to avoid confusion with LM tokens.. Cycles in parsers directly mirror cycles in the underlying context-free grammar. Critically, parsers support a derivative operation that advances the state of a parser as if it read one additional lexeme.333This approach mirrors the definition of the Brzozowski derivative  (Brzozowski) of a language $L$ with respect to characer $u$, which is $u^{-1}L=\{w\mid uw\in L\}$.

For each lexical prefix—e.g., ["1","+","2"]—we start from the user-provided parser and apply successive derivatives for each lexeme in the prefix; this results in a parser that accepts exactly those programs that begin with the given lexical prefix. Finally, we convert each derived parser into a corresponding program space (essentially by discarding the information about concrete syntax) and combine the program spaces from different lexical prefixes using the Union constructor. For our example, the prefixes ["1","+","2"] and ["1","+","2[0-9]+"] together would induce the following program space:

⬇

S = Union [ Sum (Lit "1") (Lit "2"),

Sum (Lit "1") (Lit "2[0-9]+"),

Sum S (Lit "[0-9]+") ]

Goal 3: Analyzing Program Spaces

The final step towards evaluating realizability is to determine whether there exists a constraint-satisfying program in the prefix space computed in the previous step. Unfortunately, this problem is undecidable in general, even when the constraint is decidable for individual ASTs (popl23unrealizabilitylogic; kim2025). To make the analysis tractable, we therefore turn to the canonical strategy in program synthesis: pruning. Specifically, users encode their constraints by defining semantic pruners, functions that take as input a space of programs and return (an approximation of) the subspace of constraint-satisfying ones. In ChopChop, just as program spaces are modeled as codata, pruners are modeled as corecursive functions.

Pruners can be composed to enforce conjunctions of constraints, allowing users to modularly define and reuse semantic constraints across tasks. For our running example, we supply two pruners (shown in Figure 3): odds, which removes programs with even literals, and even_sum, which removes programs whose total is odd. When we apply the two pruners in sequence, we obtain a new regular coterm S’ that represents the subspace of even sums of odd literals:

⬇

S’ = even_sum (odds S)

Since S is cyclic, evaluating S’ = even_sum (odds S) eventually leads back to even_sum (odds S). To avoid infinite recursion, our solver tracks previously expanded terms and creates a cycle in S’ when we re-visit a subterm. For example, the inner term odds S expands until we reach the state:

⬇

odds S = Union [ Sum (Lit "1") Empty,

Sum (Lit "1") (Lit "2[0-9]*[13579]"),

Sum (odds S) (Lit "[0-9]*[13579]") ]

Finally, we must check if there exists a program in the pruned space. Note that checking emptiness is not the same as checking if the space is exactly the term Empty, since the presence of cyclic subterms means evaluation may not reduce the space to a normal form. ChopChop implements a function nonempty :: ExprSpace -> Bool that performs a fixpoint computation over the codata representation of its input. Again, because spaces are regular coterms, the fixpoint computation operates over a finite structure despite the fact that a space can represent infinitely many programs.

In our example, nonempty determines that the first two sub-spaces of the union in S’ are empty while the third one is non-empty, and hence the union is non-empty.

Putting it All Together

Together, the four components—lexing, parser derivatives, user-defined pruners, and the nonemptiness check—can compute realizability for our running example as:

⬇

nonempty (even_sum (odds S))

This pipeline is modular and requires minimal effort from the user: they define a grammar and supply pruners for each constraint. ChopChop takes care of the rest—automatically enforcing semantic constraints as the LM generates code.

3. Semantic Constrained Decoding as Realizability Checking

In this section, we formalize the problem of semantic constrained decoding and explain how it is equivalent to the problem of checking whether a synthesis problem is realizable—i.e., whether a regular tree grammar accepts any programs that satisfy a given input specification. After Section 3.1 establishes some basic definitions, Section 3.2 gives a general formulation of constrained decoding where the constraint is a predicate on strings. Section 3.3 defines the special case of semantic constrained decoding, where the predicate is induced by a constraint on ASTs. We also provide soundness and completeness theorems.

3.1. Preliminaries

Strings and Abstract Syntax Trees

Let $\Sigma$ be a finite alphabet of characters. A string is a sequence $\omega\in\Sigma^{*}$, and the completions of $\omega$ are the strings that begin with $\omega$. Let $\mathsf{AST}$ be a set of abstract syntax trees (of programs). Translation from strings to ASTs is defined by a function $\mathsf{parse}\colon\Sigma^{*}\rightarrow\mathsf{AST}\cup\{\bot\}$ that produces an AST from a string of characters (or $\bot$ if parsing fails).

Language Models and Decoding

Language Models (LMs) operate over short character sequences called tokens, rather than over individual characters. We define a token vocabulary $\mathbf{T}$, where a token $\tau\in\mathbf{T}$ is either a finite string of characters from $\Sigma$ or the special token $\mathsf{END}$. A token vocabulary $\mathbf{T}$ must be large enough to represent any string in $\Sigma^{*}$ as a sequence of tokens.

We formalize a language model $\mathsf{lm}\colon\mathbf{T}^{*}\to\mathbf{T}\to[0,1]$ as a function that takes in a prefix $\tau_{1},\ldots,\tau_{i-1}\in\mathbf{T}^{*}$ and returns a probability distribution over the next token $\tau_{i}\in\mathbf{T}$. Given a language model, we can iteratively generate a sequence of tokens, selecting each next token $\tau_{i}$ based on the model’s distribution, conditioned on the previously generated tokens $\tau_{1},\ldots,\tau_{i-1}$. This process is called decoding. Decoding can be done greedily (by choosing the most probable token at every step) or stochastically (e.g., via nucleus sampling (holtzman2020)). Decoding stops when an $\mathsf{END}$-terminated token sequence is produced.

3.2. Constrained Decoding

We begin with a general definition of constrained decoding (CD) that is not specific to semantic constraints. A string constraint $\Phi$ is a predicate on $\Sigma^{*}$ that accepts some set of strings. For example, $\Phi$ may accept the members of some context-free language. We say that a string $\omega\in\Sigma^{*}$ is completable with respect to $\Phi$ if there exists a completion of $\omega$ satisfying $\Phi$:

[TABLE]

A monitor for a string constraint $\Phi$ is a function $\mathsf{monitor}_{\Phi}:\Sigma^{*}\to\mathrm{bool}$ that checks whether an input string is completable with respect to $\Phi$. For a given string constraint $\Phi$, constrained decoding maintains the invariant that the currently generated sequence of tokens is completable with respect to a monitor for $\Phi$. Given a language model $\mathsf{lm}$, a string constraint $\Phi$, and a monitor for $\Phi$, Algorithm 1 outlines how constrained decoding operates in its general form.

To abstract over the choice of the decoding strategy, Figure 4 uses an opaque $\mathsf{worklist}$ data structure that stores all generated token sequences whose proper prefixes are completable, along with the sequences’ generation probabilities. In each iteration, the algorithm dequeues a sequence $\omega$ from the worklist. (Note that for sampling-based techniques dequeuing may be a probabilistic operation.) If $\omega$ is $\mathsf{END}$-terminated, we return $\omega[:-1]$ if $\omega[:-1]$ satisfies $\Phi$ and discard $\omega$ otherwise (lines 6-7). If $\omega$ is not $\mathsf{END}$-terminated, we check whether any completion of $\omega$ can satisfy $\Phi$ (line 8). If yes, we enqueue the possible continuations $\omega\tau$ for later review (lines 9-10). If no, we discard $\omega$.

3.2.1. Soundness and Relative Completeness of Constrained Decoding

The guarantees we can make about Algorithm 1 depend on the quality of $\mathsf{monitor}_{\Phi}$. A monitor is (i) sound if every prefix the monitor accepts is completable: $\mathsf{monitor}_{\Phi}(\omega)\Rightarrow\exists\omega^{\prime}\in\Sigma^{*}.\Phi(\omega\omega^{\prime})$; and (ii) complete if all completable prefixes are accepted by the monitor: $\mathsf{monitor}_{\Phi}(\omega)\Leftarrow\exists\omega^{\prime}\in\Sigma^{*}.\Phi(\omega\omega^{\prime})$. Constrained decoding is sound if every string produced by Algorithm 1 satisfies the constraint $\Phi$. Constrained decoding is complete if every string satisfying $\Phi$ can be returned by Algorithm 1 with non-zero probability.

Lemma 3.1 (Soundness).

Constrained decoding is sound if $\Phi(\omega)$ can be checked soundly.

This is easy to see, as the algorithm only returns outputs $\omega$ that pass the check $\Phi(\omega)$. Note that this condition ensures that Algorithm 1 is sound even when the monitor is unsound.

Unlike soundness, completeness often does not hold for common instantiations of $\mathsf{worklist}$ (e.g., greedy decoding, where the highest probability continuation of the previously dequeued string is always selected). However, we still want a relative characterization of completeness to ensure that constrained decoding cannot discard solutions we could achieve with unconstrained decoding. To this end, we define a decoding strategy as simply an implementation of $\mathsf{worklist}$. We say constrained decoding is complete up to a decoding strategy if under that implementation, Algorithm 1 can return every valid solution that unconstrained decoding can produce with at least as high probability.

We prove completeness up to two of the most popular decoding strategies, top-$p$ and top-$k$ sampling (though our proof methodology generalizes to other common strategies). Top-$k$ sampling is a decoding method where, at each step, the model considers only the $k$ most likely next tokens for its current prefix and randomly selects one based on their normalized probabilities. Top-$p$ sampling is similar, except instead of a fixed $k$ we use the smallest set of most probable tokens whose cumulative probability mass is above threshold $p$. Either of these sampling approaches could be implemented as instantiations of Algorithm 1 by setting dequeue to iterate over the worklist, only choose pairs where the token sequence has a maximal length, and sample from the appropriate subset after renormalizing probabilities.

Lemma 3.2 (Completeness up to Top-$p$ and Top-$k$ Sampling).

If $\mathsf{monitor}_{\Phi}$ is complete, then constrained decoding (Algorithm 1) is complete up to both top-$p$ and top-$k$ sampling.

Note that not all decoding strategies satisfy completeness up to decoding. In a greedy/deterministic beam search for example, discarding an incompletable prefix might cause the LM to explore a completable prefix it would ordinarily have neglected. This exploration may cause constrained decoding to find a different solution than unconstrained decoding would have originally found.

While complete monitors guarantee completeness up to common decoding strategies, sound monitors make search more efficient.

In existing approaches for syntactic constrained decoding, the string constraint $\Phi$ is limited to asserting membership in a context-free language. In this case, monitors can be sound and complete (greatgramma; syncode).

3.3. Semantic Constrained Decoding

Semantic constrained decoding is the special case of constrained decoding where the string constraint is defined as $\Phi=\phi\circ\mathsf{parse}$ for some predicate $\phi\colon\mathsf{AST}\to\mathrm{bool}$. We call $\phi$ a semantic constraint, We implicitly extend the domain of any such $\phi$ to $\mathsf{AST}\cup\{\bot\}\to\mathrm{bool}$ by setting $\phi(\bot)=\mathrm{false}$. For example, the semantic constraint in Section 2 checks whether an AST is an odd sum of even literals. The corresponding string constraint checks whether a string parses to such an AST.

Algorithm 1 requires a monitor for checking completability of the string constraint $\Phi$. For semantic constrained decoding, we have that

[TABLE]

The key insight of our approach is that we can re-express $\mathsf{completable}(\omega,\Phi)$ in terms of the space of ASTs a prefix $\omega$ represents. First, we define the prefix space of a string $\omega$ as the set of all parses of continuations of $\omega$:

[TABLE]

By changing the quantified variable to range over ASTs, completability can now be written as

[TABLE]

We are now asking if there exists a term in a given prefix space that satisfies a constraint $\phi$. Readers familiar with program synthesis will recognize this formulation as the standard shape of a synthesis problem. Specifically, such a query is an example of a realizability (unrealizability2020; popl23unrealizabilitylogic) problem, which asks whether a set contains a term that satisfies a given property.

[TABLE]

Expressing realizability entirely over spaces of ASTs removes the need for the string-level reasoning that has characterized prior constrained-decoding work (typespaper; monitors). All together, our definition of completability simplifies to:

[TABLE]

Consequently, a monitor for $\Phi$ can be implemented as $\mathsf{check\_realizable}_{\phi}\circ\mathsf{PrefixSpace}$, where $\mathsf{check\_realizable}_{\phi}$ is a potentially approximate procedure for checking realizability.

3.3.1. Soundness and Relative Completeness of Semantic Constrained Decoding

A realizability checker is (i) sound if every space it accepts is realizable: $\mathsf{check\_realizable}_{\phi}(T)\Rightarrow\exists t\in T.~\phi(t)$ and (ii) complete if every realizable space is accepted by the checker: ${\mathsf{check\_realizable}_{\phi}(T)\Leftarrow\exists t\in T.~\phi(t)}$.

Since $\mathsf{PrefixSpace}$ can be computed exactly, the following theorems follow immediately from Lemma 3.1 and Lemma 3.2:

Theorem 3.3 (Soundness of Semantic Constrained Decoding).

Semantic constrained decoding is sound if $\phi$ can be checked soundly.

Theorem 3.4 (Completeness up to Top-$p$ and Top-$k$ Sampling of Semantic Constrained Decoding).

If $\mathsf{check\_realizable}_{\phi}$ is complete, then semantic constrained decoding is complete up to both top-$p$ and top-$k$ sampling.

Section 2 showed an example of a sound and complete realizability checker for the constraint being enforced. In Section 5, we present two more realistic examples: a sound and complete realizability checker for the problem of equivalence-guided decoding, and a complete444For this problem one can prove that no sound and complete realizability checker exists (system_f_untypable) realizability checker for type-safe decoding.

4. ChopChop: Semantic Constrained Decoding via Coinduction

The key idea of semantic constrained decoding is that one can define pruners on spaces of programs, which are defined at the level of abstract syntax. To create a programmatic interface for defining pruners, we need a framework for constructing, manipulating, and performing analyses over possibly infinite program spaces. One framework for cleanly manipulating infinite objects is supplied by cocaml; the framework defines infinite objects with repeated structure (like program spaces) as regular codata and lets users compute recursive functions on regular codata (Section 4.1). We adopt this framework to represent and manipulate program spaces (Section 4.2). As we show in Section 4.3, framing program spaces as regular codata allows us to not only implement pruners over program spaces, but also gives an elegant way to construct prefix spaces. Finally, we describe how ChopChop implements this approach as an embedded DSL in Python (Section 4.4).

4.1. Programming with Regular Coinduction

Coinduction is a powerful technique for representing and manipulating infinite objects. We present a brief introduction to coinduction adapted from the running example used by cocaml.

Codata

Consider the usual datatype for integer lists:

⬇

data IList = INil

| ICons Int IList

The IList datatype includes finite lists like INil and ICons 1 (ICons 2 INil). However, IList also includes infinite streams like, e.g., ICons 1 (ICons 2 (ICons 3 ...)). Infinite members of a datatype are called coterms, or sometimes codata.

In general, it is not always possible to finitely represent a coterm. However, many coterms do admit compact representations. For example, the stream of all ones can be written as ones = ICons 1 ones. The stream ones is an infinite term, but it only has finitely many distinct subterms (i.e., 1 and ones). This property, called regularity, allows codata to be expressed with a finite representation. Alternatively, regular coterms can be depicted as cyclic term graphs, as shown by Figure 5.

Because regular codata can be finitely represented, we can compute their properties in finite time. For example, one cannot compute the set of integers contained in an arbitrary stream. However, a quick inspection of the definition of ones (or a fixpoint procedure over the term graph) reveals that ones contains no integers besides $1$. When we represent program spaces as regular codata later, we will use these nice properties to answer questions about, e.g., the nonemptiness of a program space.

Computations over Regular Codata

To describe operations on codata, we can define typical recursive functions on the structure of the datatype representing codata. For example, we can define the following function to collect the set of distinct integers appearing in a stream:

⬇

@fixpoint: EmptySet

elements :: IList -> Set Int

elements INil = EmptySet

elements ICons x xs = (add (elements xs) x)

Over an arbitrary infinite coterm t, it may not be possible to explicitly compute (elements t). However, one can do so when t is regular. The key observation is that, if t has only finitely many distinct subterms, we will only need to evaluate elements on finitely many distinct coterms. In general, functions that compute data from regular coterms can be evaluated as fixpoint computations over the coterm’s cyclic term graph. Throughout the paper, we distinguish such functions with the annotation @fixpoint, followed by the initial value for the fixpoint computation.

It is also possible to recursively define functions that produce regular coterms. In the case of streams, we might consider a function that adds $1$ to each element of the stream

⬇

addOnes :: IList -> IList

addOnes INil = INil

addOnes (ICons x l) = ICons (x + 1) (addOnes l)

If we apply addOnes to ones, we see that only finitely many distinct terms are generated:

⬇

addOnes ones = addOnes (ICons 1 ones)

= ICons 2 (addOnes ones)

Regular corecursive functions (i.e., functions that map regular coterms to regular coterms) can be computed explicitly over regular coterms with the techniques of cocaml. At a high level, their techniques work by memoizing the result of function expansions and producing a cycle upon encountering a previously seen call.

Of course, it is possible that the user may write a function that yields a coterm that is not regular. We do nothing to prevent this or otherwise enforce termination—nontermination is a wholly orthogonal problem to our purposes that has been studied in the literature on coinduction, for example in (capretta2005general). In practice, one can avoid most issues by (i) only writing recursive functions that call themselves on subterms of the input term and (ii) avoiding @fixpoint-annotated functions whose return types contain infinitely many values. Finally, our framework provides one special built-in function, isCyclic, that returns true if a regular coterm has cycles and false if it is just a tree.

4.2. Program Spaces as Coterms

In Section 2 we lifted the Expr datatype, which describes individual programs, to ExprSpace, which describes spaces of programs. Now, we generalize that principle to arbitrary program datatypes. First, we define a generic Program datatype (Figure 7(a)) that describes the structure of abstract syntax trees. It is parametric over a type parameter sym, which represents the different possible constructors for ASTs. We write Program this way to allow for manipulations over ASTs that are generic over the constructor. Often, we want to treat a datatype like Expr “as if it were” an instance of Program. That is, Expr is roughly the same as Program ExprSym, where ExprSym = Sum, ignoring constraints on arity of children. For notational convenience, we ignore this distinction and treat these two datatypes as the same.

We can abstract over ExprSpace in the same way we abstracted over Expr. Specifically, we can define a ProgramSpace (Figure 7(b)) as either: Empty, the empty space representing no programs; Union, a union of program spaces; Lit, a set of concrete literals described by a regular expression; or ASTNode, a product of program spaces under some AST constructor.

We will write most concrete program spaces in the style of ExprSpace for clarity, but generic algorithms on program spaces will be written over ProgramSpace.

As discussed in Section 2, we need to be able to decide whether a ProgramSpace represents the empty set. While Empty is obviously empty, determining emptiness of a coterm likeE = Union [E, E] requires a fixpoint computation. To solve this problem, we implement a simple function, nonempty, to check whether a space is empty:

⬇

@fixpoint: False

nonempty :: ProgramSpace sym -> ProgramSpace sym

nonempty Empty = False

nonempty Union children = any nonempty children

nonempty (Lit l) = regexNonempty l

nonempty ASTNode _ children = all nonempty children

Finally, when writing pruners it will be useful to convert a ProgramSpace representing only a single program into the corresponding element of type Program. Such spaces naturally arise when prefixes contain complete subexpressions. For this reason, we define a utility function collapse as:

⬇

collapse :: ProgramSpace sym -> Maybe (Program sym)

collapse x | isCyclic x = Nothing

collapse (Union [x]) = collapse x

collapse (Lit l)

| isSingleton l = Just (ASTLeaf (toString l))

collapse ASTNode sym [children] = do

collapsedChildren <- mapM collapse children

ASTNode sym collapsedChildren

collapse _ = Nothing

4.3. Parsers as Coterms

Recall from Section 2 that our lexer takes a string $\omega$ and returns a finite set of lexical prefixes. A lexical prefix is a sequence of complete lexemes followed by a possibly incomplete lexeme. The lexer is designed so that every lex of a completion of $\omega$ extends one of the lexical prefixes. The details of our lexing algorithm are discussed in Section A.2.

Once lexing is complete, we must perform parsing. We carry out parsing by following the parsing with derivatives technique introduced by parsingWithDerivatives. Intuitively, a parser is a function from strings to trees that represents the state of a parser after consuming some string $\omega$. Parsers support a derivative operation that advances the parser state by consuming a lexeme, analogous to Brzozowski derivatives for regular expressions (Brzozowski). Parsers, their derivative operation, and a method to convert a parser to a program space can be easily represented as codata and corecursive functions.

Intuitively, after consuming some prefix $\omega$, a parser (Figure 8) can be in one of a few possible states when it considers how to handle further lexemes.

• •

EmptyParser: The parser accepts no strings, meaning $\omega$ is not in the language that the parser recognizes.

• •

Choice ps: The parser accepts any string accepted by any parser in the list of parsers ps.

• •

ConstParser reg: The parser accepts any single lexeme in the regex reg.

• •

NullParser l: The parser has parsed the lexeme l but will consume nothing further.

• •

Seq a ps1 ps2: The parser is a sequential composition of parsers, where ps1 is the sequence elements whose parsing is complete and ps2 is the sequence of elements that remain. The action a describes how completed parses map to AST nodes.

4.3.1. Derivatives on Parsers

To advance the state of a parser, we define a corecursive derivative function d (Figure 9(a)). Given a lexeme $l$ and a parser $p$, the coterm d l p represents the parser that is obtained after the parser p consumes the lexeme $l$.

The definition of d recurses on the structure of the input parser p:

• •

If $p$ is an EmptyParser, then d p l returns EmptyParser.

• •

If $p$ is a NullParser, then d p l returns EmptyParser as $p$ cannot accept further input.

• •

If $p$ is a ConstParser, then d p l returns a constant parser storing $l$ if the regex for $p$ matches $l$; otherwise it returns EmptyParser.

• •

If $p$ is a Choice, then d p l returns a Choice of the derivative of its children.

• •

If $p$ is a Seq, then d p l derives the parser at the current position in the sequence and splits into a Choice of cases. If the derived parser can accept the empty string, we advance to the next parser in sequence by applying the nullability operator delta, which “completes” a parser by throwing away all parses that haven’t been fully matched. Otherwise, we update the sequence in place.

More details appear in parsingWithDerivatives and parsingWithZippers.

4.3.2. From Parsers to Program Spaces

Finally, we need to construct a program space reprsenting all programs our parser could emit. To do so, we define a corecursive function image (Figure 10) that recurses over the structure of the input parser p:

• •

If $p$ is an EmptyParser, then image returns the empty space.

• •

If $p$ is a Choice, then image returns a Union of the images of its children.

• •

If $p$ is a ConstParser, then image returns a Lit matching any lexeme $p$ could accept.

• •

If $p$ is a NullParser, then image returns a Lit matching only the lexeme $p$ has already accepted.

• •

If $p$ is a Seq, then image applies the Action to $p$. If the constructor for the action is None, we “skip” converting this layer of the parser—this option supports inlining trees for constructs like parenthesis specifically.

Together, the lexing, derivative-based parsing, and image construction enable ChopChop to track the evolving set of valid program completions at every step of generation. This coinductive representation forms the foundation for subsequent semantic pruning and realizability checking.

4.4. Implementation

We implemented ChopChop as an embedded domain-specific language (DSL) in Python that supports symbolic manipulation of coinductive structures. The backend draws inspiration from prior work on regular coinduction, such as CoCaml (cocaml), and makes extensive use of Python metaprogramming. We do not use CoCaml directly to ensure compatibility with the rest of our Python implementation. Notably, ChopChop defines two key decorators:

• •

@rewrite: Marks functions that construct coterms by symbolically rewriting recursive calls into a finite system of equations (if the recursion is regular).

• •

@fixpoint: Interprets a coterm via Kleene iteration to compute a fixed point over the coterm’s input.

Additionally, ChopChop incorporates domain-specific simplifications for program spaces. For instance, unions over parser states or AST spaces are simplified by removing empty branches—i.e., when nonempty returns false. For parser derivatives, we also implement the compaction optimization described in  (parsingWithDerivatives) to reduce the size of coterms.

5. Case Studies

We demonstrate the generality of our framework by instantiating it for two domains: enforcing semantic equivalence for a basic functional language and enforcing type safety for TypeScript.

5.1. Equivalence-Guided Decoding

In this case study, the LM is given expressions in a basic functional language and is asked to refactor them into equivalent programs. The language consists of basic arithmetic operators, identifiers, integer constants, function applications, and let bindings. For example, consider the following program that computes the distance between two points.

⬇

sqrt (pow (x2 - x1) 2 + pow (y2 - y1) 2)

A valid output for the LM might be:

⬇

let dx = x2 - x1 in

let dy = y2 - y1 in

sqrt (pow dy 2 + pow dx 2)

In general, program equivalence is not decidable; therefore, ChopChop uses e-graphs (egg) to reason about program equivalence approximately. An e-graph is a data structure for compactly representing spaces of equivalent programs. At a high level, an e-graph maintains a collection of equivalence classes of expressions. To build an e-graph, a user supplies an initial expression and a list of rewrite rules that define equivalences. For example, the rule $?x+?y\to?y+?x$ encodes commutativity of addition. A term like $f(a,b)+2$ can match the left-hand side of this rule, to be rewritten to $2+f(a,b)$. Initially, an e-graph only represents trivial equivalences (i.e., every equivalence class has only one member). Equivalence classes are then refined via a process known as equality saturation, which iteratively applies rules (up to a fixed budget) to subterms in the e-graph. Whenever a subterm matches a rule, the e-graph is modified by applying the rewrite and merging the equivalence classes of the rewritten subterm with the subclass of the original subterm. Crucially, e-graphs can compactly represent large sets of terms by sharing: instead of storing a term like $f(x,y)$ directly, an e-graph will add a layer of indirection so that the node $f$ has pointers to the equivalence classes of $x$ and $y$, rather than the expressions themselves.

For our case study, we define a set of basic rewrite rules for arithmetic expressions (ones with addition, subtraction, multiplication, and division; see Section A.4 for the full set of rules). We then use the egglog library (egglog) to build an e-graph. ChopChop then enforces the constraint that the output of an LM must be a program stored by this e-graph—i.e., ChopChop guarantees that the output term is equivalent up to rewrite.

Importantly, the set of terms an e-graph represents forms a regular tree language that can be represented by a finite tree automaton (suciu2025semantic). We use this property to build a semantic pruner whose goal is to only keep terms that appear in the automaton. In particular, we syntactically convert the automaton corresponding to the e-graph into a corresponding ProgramSpace coterm. Then we can define a function intersectSpaces to filter out non-equivalent programs from the prefix space.

While e-graphs can easily deal with let-free expressions, we need some extra care to make sure that let-expressions are taken into account by the e-graph. To handle let expressions, our pruner adopts a simple strategy: if we have not finished generating a let binding, we do not prune any programs—no matter what expression the let binds a variable to, we can always avoid using the variable in the final expression. If a let expression space contains a complete binding of form $x=e_{1}$ where $e_{1}$ is a complete expression (i.e., the LLM has generated a let binding), then we update the current e-graph with an additional rewrite rule $e_{1}\to x$. When generating the last expression under the let expression, we use the semantic pruner induced by this new e-graph. The pseudocode for our checker is shown below:

⬇

prune (Let b s1 s2) egraph = fromMaybe Empty do

x <- collapse b -- Wait for variable name to be generated

e1 <- collapse s1 -- Wait for binding for x to be generated

let egraph’ = updateEGraph egraph x e1

prune s2 egraph’ -- Recurse, adding extra rule e1 => x

prune s egraph = s ‘intersectSpaces‘ (eGraphToSpace egraph)

5.2. Type-Safe Decoding for TypeScript

In our second case study, we use ChopChop to implement a semantic pruner that enforces type safety for a subset of TypeScript that covers most core language features (branching, loops, variable declaration and reassignment, constant and mutable variables, and [recursive] function definitions). We study TypeScript because it is widespread (octoverse2022), and previous work has shown that small and mid-sized LMs often fail to produce type-safe TypeScript code (typespaper).

It is a folklore result that even for simply-typed lambda calculus, the set of well-typed terms is not a regular tree language. As a consequence, no pruner can remove exactly the ill-typed programs from a program space—the pruned space would not be representable as regular codata. Instead, we implement an overapproximate pruner that conservatively discards many ill-typed programs while ensuring that all well-typed programs are preserved.

Type Pruning

Our typesafety pruner is a corecursive function of the following form:

⬇

type_prune :: Environment -> Type -> ProgramSpace -> ProgramSpace

Much like a type checker, type_prune is parameterized by a typing environment and target type. However, it operates on program spaces instead of single programs: given an input space it returns an overapproximation of the subspace of well-typed programs. For example, for the program space (Union (Add x 6) false), the expression

⬇

type_prune {x: int} int (Union (Add x 6) false) = Add x 6

yields a program space containing (Add x 6), the only program that types to int when the variable x has type int. If we call type_prune with the empty environment and the target type $\top$ (i.e., the supertype of all types), we get an approximation of the set of well-typed closed programs—for the program space (Union (Add x 6) false), we would get false. Section A.3.1 discusses the full implementation of type_prune; we give an overview below.

Designing type_prune

We designed type_prune to be an analogue of checking in bidirectional type checking (bidirectional), which resolves typing judgements locally and is deterministic. For ground terms, we check their type against the target type and decide whether to keep them or prune them (yielding the Empty program space):

⬇

type_prune {x: int} int 6 = 6

type_prune {x: int} bool 6 = Empty

For most program constructors, a bidirectional type checker would check the types of the subterms to decide how to type the superterm. Similarly, our type pruner prunes each set of subterms and returns only the valid combinations:

⬇

type_prune {x: int} int (Add x 6) =

Add (type_prune {x: int} int x) (type_prune {x: int} int 6)

Like with bidirectional type checking, this approach gets complicated for function applications. Suppose F and X are program spaces, and consider type pruning the application of F to X—i.e., (type_prune {} int (App F X)). We would like to handle this case by pruning F and X to their expected types and combining the results. However, there are infinitely many valid combinations of types that programs in F and X could take, e.g., int -> int paired with int, or (bool -> int) -> int paired with bool -> int, and so on.

In bidirectional type checking, this multiplicity is resolved by first inferring the type of the function. When the type of the function is known, the argument can be checked against the function’s input type. Since F may represent infinitely many programs with infinitely many possible types, type inference on F may be insufficient to resolve the multiplicity. Instead, we wait until F resolves to a single AST (i.e., via collapse from Section 4.2). Before F resolves to a single AST, we type prune F to exclude functions that cannot return the target type, and we leave X unmodified. Once F resolves to a single AST, we can infer the type of that AST and use it as the basis of our pruning. For example, if F = foo, then

⬇

type_prune {foo: (int -> int) -> int} int (App foo X) =

App foo (type_prune {foo: (int -> int) -> int} int -> int X)

Type inference for single ASTs can be implemented in the usual way (e.g., (typescript_good_typesystem)). type pruning Empty always yields Empty, and type pruning a Union will type prune each child and union the results.

Despite the overapproximate handling of function application, our pruner is quite precise over program spaces that correspond to left-to-right program prefixes. For such spaces, F will always resolve to a concrete function before any of X is written. This left-to-right resolution means that we can always infer the type of F when we start writing X.

We note that ChopChop makes it more natural to implement an overapproximate type pruner than an underapproximate type pruner. The idea of waiting for a term to be completed is supported naturally by the collapse function. In contrast, writing an underapproximate pruner requires analyzing some subset of the combinations of function and argument types at the same time.

6. Evaluation

We evaluate the two instantiations of ChopChop presented in Section 5 to answer the following research questions:

1. RQ1)

Effectiveness. Does ChopChop make language models more effective at generating programs that satisfy semantic constraints? 2. RQ2)

Overhead. What is the computational cost (e.g., latency, token usage) of enforcing semantic constraints during generation?

6.1. Experiment Setup

We compare our semantic constrained decoders written in ChopChop to the following baselines:

• •

Unconstrained Decoding: The LM generates code without any constraints.

• •

Grammar-Constrained Decoding (GCD): The LM must produce syntactically valid programs (enforced via a grammar), but no semantic restrictions are applied. In ChopChop, grammar-constrained decoding corresponds to using the identity function as the pruner.

Benchmarks: Equivalence-Guided Decoding

We created 10 benchmark tasks in the basic functional language shown in Section 5.1, where the goal is to refactor a program into an equivalent one—e.g., factoring out subexpressions into let bindings. We use a fixed system prompt that specifies the grammar of the language and instructs the model to return only a refactored program555We also ran a variant of this benchmark where we included in the prompt the list of rewrite rules. The overall trends are similar; this data can be found in Section A.4. with no explanation. The exact prompt and the full list of benchmarks are shown in Section A.4. We count a response as correct if the LM produces a complete program that is equivalent to the input program, with no post-processing. Unconstrained decoding often fails to produce just the output code, despite being explicitly instructed to do so. Therefore, we also evaluate a variant where the prompt wraps outputs in triple backticks (‘‘‘) to encourage the model to delimit its code clearly. This variant avoids penalizing runs that fail only due to formatting. We refer to the two variants as No Delimit and Delimit, respectively.

Benchmarks: Type-Safe Decoding

For our second instantiation of ChopChop, we source the benchmarks from the TypeScript translations of the MBPP (mbpp) tasks from the MultiPL-E dataset (multiplE). We extract the 72/809 tasks that can be solved in our language fragment. Our prompting strategy mirrors that of typespaper, but we additionally provide context to the LM to instruct it to avoid language constructs outside our language fragment. Our full prompting strategy and benchmarks are included in Section A.3.2.

An example task is given below:

// Write a typescript function to find the next perfect square // greater than a given number. function next_Perfect_Square(N: number): number

We count a response as correct if the generated TypeScript program compiles. For the TypeScript evaluation, we also run the tool by typespaper for comparison (although we do not instruct the LM to avoid programs outside our language fragment since their tool supports a larger subset of TypeScript).

Models, Parameters and Hardware

We run all experiments using the instruction-tuned versions (i.e. models that are trained to follow instructions in the prompt) of the following models: DeepSeek-Coder-6.7b, CodeLlama-7B, and CodeLlama-13B. Each model is evaluated at five different sampling temperatures: ${0.01,0.3,0.5,0.7,1.0}$. These ranges of small-to-medium models and low-to-high temperatures lets us explore a range of model capability. We run all experiments on a Supermicro SYS-4029GP-TRT with two Intel(R) Xeon(R) Gold 6230 CPUs, 384 GB RAM, a 4 TB SSD, and eight Nvidia Geforce RTX 2080Ti GPUs.

Procedure

For each benchmark, model, decoder, and temperature, we run constrained decoding until either: the $\mathsf{END}$ token is generated or a 150 second timeout is reached. We only implement a naive sampling strategy where if a token is rejected, we backtrack by one token and re-sample with that token removed. Constrained decoders may fail if they use up their token or time budget without completing a valid program—especially if the LM repeatedly proposes unrealizable tokens that must be pruned. Unconstrained decoders may also fail to terminate if the model does not emit an $\mathsf{END}$ token withing the budget.

A run is considered successful if: (i) A complete program is emitted, and (ii) It satisfies the semantic constraints of the task (i.e., equivalence or type safety).

6.2. RQ1: Effectiveness

6.2.1. Quantitative Evaluation

Table 1 reports the number of successful runs for ChopChop and the two baselines—unconstrained decoding and grammar-constrained decoding—on all benchmarks. Across nearly all configurations, semantic constrained decoding delivers consistent and often dramatic improvements.

Equivalence-Guided Decoding

Unconstrained, most models perform very poorly on our benchmarks, with most failing to generate even a single semantically equivalent program. Several factors contribute to this: (i) We intentionally use small- and medium-sized models, which highlight the gains possible even for less capable models. (ii) The toy language used in the benchmarks is likely out-of-distribution for most pretrained LMs, which are tuned on real-world languages like Python and JavaScript. In particular, DeepSeek-Coder-6.7B frequently attempts to write Python, Lisp, or TypeScript code, and fails all benchmarks without semantic constraints as a result. (iii) Despite clear instructions, models frequently emit natural language explanations, markdown, or commentary—none of which are semantically valid outputs under our equivalence checker.

Because we define equivalence with respect to a reference set of rewrite rules, it is possible that these rules do not encode every possible equivalence a user might have in mind—e.g., in our benchmarks we treated all named functions as uninterpreted, but particular functions could have additional semantics associated with them. To mitigate this source of imprecision, we manually check the unconstrained and syntax-constrained data for false negatives (programs that could be considered equivalent, but are not proved equivalent by our rewrite rules). We only found 8 such instances out of the 600 total programs for these baselines.

Type-Safe Decoding

All three models often produce compiling code, except at high temperatures, where their performance degrades. The two CodeLlama models perform similarly, and the DeepSeek-Coder-6.7b model performs somewhat worse, especially at the highest temperature. Surprisingly, CodeLlama-7B slightly outperforms CodeLlama-13B at most temperatures. When aggregated across all temperatures, semantic constrained decoding consistently outperforms the baselines, improving the performance of DeepSeek-Coder-6.7b, CodeLlama-7B, and CodeLlama-13B by an average of 28.0%, 10.1%, and 23.2% across all temperatures, respectively. We also observe that grammar-constrained decoding alone actually performs worse than unconstrained generation. This effect is likely due to the fact that we limit the grammar to a small fragment of TypeScript and prevent programs that would compile, but are not in our supported fragment, from being generated. Additionally, we observe that typespaper performs slightly better than our semantic constrained decoding at medium temperatures and significantly better at the highest temperature. The reason for this discrepancy is that their tool supports a larger language fragment than we do, and the model tends to ignore the prompt and use forbidden language features as temperature increases.

6.2.2. Qualitative Evaluation

Next, we discuss some instances that show the strengths of semantic constrained decoding relative to GCD and unconstrained generation.

Equivalence

One interesting phenomenon is that while GCD ensures syntactic validity, it does not prevent models from creatively “embedding” invalid outputs within the grammar. For example, the text in 11(a) can be parsed (misleadingly) as a series of function calls due to the permissiveness of the grammar. This quirk allows LMs to “escape” into natural language. By contrast, semantic constrained decoding disallows such outputs because programs with undefined variables cannot be equivalent to the original. Next, we show a case where semantic constrained decoding prevents an inequivalent (but otherwise error-free) program from being generated. CodeLlama-7B under GCD returns the code in Figure 11(b) when given the program start + (end - start) * scale. This program needs to be extended with the suffix

• start to be correct. Semantic constrained decoding prevents the model from terminating the program string prematurely and would force it to continue (equivalence-constrained) generation.

TypeScript

Enforcing type safety prevents variable-name and function-name hallucinations, eliminating many errors that appear in the GCD and unconstrained modes. We observe that at high temperatures the unconstrained mode also struggles to correctly balance parentheses, and GCD often calls undefined functions when it wants to use forbidden language features (e.g., newArray(...) is used instead of new Array to try to construct an array). A more interesting (but rare) case type-constrained decoding prevents is mutation of variables declared const. Consider the code in Figure 11(c), produced with GCD. The variable divisors is declared constant on line 2, but it is mutated on line 9. In this case, the LM’s mistake on line 2 does not cause an observable error until later in the program. The type system implemented in our semantic pruner will prevent the assignment to divisors, but it will still allow line 2.

When irresolvable conflicts between the LM’s intention and the formal constraints of the decoder like Figure 11(c) occur, the LM is typically unable to recover because it has already “committed” to a solution. In the best case, this mistake results in continuations consisting of legal but useless code, such as whitespace or comments. In the absolute worst case, the LM will sometimes generate deeply nested arithmetic expressions that explode the size of our program space and slow our solver to the point of timing out. In general, constrained decoding is known to skew the LM token distribution and how to mitigate this problem is an active area of research (gad). Such adjustments are orthogonal to our purposes, so we do not consider them.

6.3. RQ2: Overhead

Table 2 shows the average overhead of semantic constrained decoding (in ms) per generated token. Overhead on decoding time range from tens to a couple hundred milliseconds per token, which is a very small price to pay for assurance provided by semantic constrained decoding. As a reference, on our hardware, CodeLlama-13B takes on average 81 ms to produce a token when unconstrained.

To better illustrate the source of the overhead, Figure 12 plots the distribution of the number of tokens that are tried before finding a realizable one, for CodeLLama-7B. Results for other models can be found in Section A.3.2. In general, even with semantic constrained decoding the first token tried is accepted most of the time. For instance, across all models, 96.4% of the tokens produced during semantic constrained decoding for TypeScript pass on the first try (similarly, 96.1% of tokens for GCD).

7. Related Work

Constrained decoding.

Constrained decoding techniques ensure the output of language models meets a given specification by throwing away invalid next tokens at each step. Grammar-constrained decoding, in which the constraint is given as a context-free grammar, has been well studied (syncode; geng2023grammarconstrained; willard2023efficient; wang2023grammar; greatgramma). A significant portion of ChopChop’s runtime is spent pruning tokens that fail simple syntactic validity. Integrating fast syntactic filtering tools such as LLGuidance (llguidance) as a pre-processing step could reduce this cost by eliminating invalid tokens early. Beyond syntax, more recent work has explored enforcing specific semantic constraints such as type safety (typespaper). Frameworks such as monitors (monitors) and completion engines (synchromesh) provide abstractions for providing more complex constraints by allowing a user to provide a monitor (written in a general-purpose language) that performs the decoding. The main difference between our work and those techniques is that they require the user to write checkers over strings. By contrast, ChopChop operates at the level of abstract syntax, abstracting away the syntactic component and allowing the user to define pruners at the level of program spaces, thus enabling new applications such as equivalence-guided decoding.

Algebraic approaches to parsing.

We build on a long line of work viewing parsers and grammars as algebraic, recursive structures (typedAlgebraicParsing; kleene). parsingWithDerivatives presents a functional approach to parsing based on applying Brzozowski derivatives to parser combinators. Zipper-based variants such as  (parsingWithZippers; zippy) reduce redundant traversals in the basic version of parsing with derivatives to improve efficiency. Integrating these techniques into our implementation could be another avenue to improve performance.

Regular coinduction.

Our implementation relies on regular coinduction to represent and manipulate cyclic program spaces. CoCaml (cocaml; cocaml_foundation) is a framework to unambiguously define and compute recursive functions over regular codata. Because some recursive functions admit more than one interpretation on codata, the CoCaml language allows users to define custom solvers to implement their desired semantics. We do not use the CoCaml language directly. However, our Python backend handles the computation of corecursive functions, which produce codata (e.g., our pruners), with a solver analogous to the corec solver presented in (cocaml). Our backend’s solver for @fixpoint-annotated functions, which compute concrete values over regular codata, is analogous to the fixpoint solver presented in (cocaml).

Well-behaved corecursion.

As discussed in Section 4.1, ChopChop does not prevent users from writing corecursive functions that will not terminate. Finding syntactic conditions for well-behaved corecursive functions is challenging in general. One closely related body of work is on techniques for determining productivity of corecursive functions (i.e., corecursive functions that are guaranteed to always eventually produce more of the infinite term they are computing (guarded_corecursion)). Famously, a sufficient condition for productivity is guarded corecursion, which stipulates that every recursive call to a function must appear under a datatype constructor (guarded_corecursion). This condition is often too restrictive, and a number of variants have been introduced to weaken it (beyond_guarded_corecursion1; beyond_guarded_corecursion2). In our case, productivity is necessary (but not sufficient) for regularity or termination of our CoCaml-like backend. For example, f: int -> Stream where f(j) = j::f(j+1) is a guarded function, and hence productive, but it is not regular and will not terminate in our backend.

Unrealizability and pruning in synthesis.

Our approach draws inspiration from the concept of unrealizability—the problem of determining whether no solution exists that satisfies a given specification (unrealizability2019). Existing approaches to proving unrealizability (unrealizability2019; unrealizability2020) typically focus on specific synthesis domains, leveraging domain insights to solve particular tasks. Pruning, for example based on types (myth) or examples (sygus), to remove infeasible portions of the search space is a well-established technique in program synthesis. Our work provides a framework to adapt these general methods from traditional synthesis towards constraining the output of LLMs.

Abstract interpretation.

A natural question to ask is whether analyses that use abstract interpretation (abstractinterpretation) to detect invalid programs can be encoded as pruners in ChopChop. In general, the complexity of the abstract domain affects how one can connect programs to abstract values.

When the set of abstract predicates is finite, blaze have shown how to connect programs in a search space with their corresponding abstract values using abstract finite tree automata (AFTA). In an AFTA, each state represents a predicate or abstract value, and the trees derivable from that state correspond exactly to the programs to which the abstract interpretation will assign the state’s abstract value. We can encode an AFTA by defining, for each state, a pruning function that encodes the transitions to that state. The example we used in Section 2 involving odd/even predicates is already a (simple) instantiation of such an encoding.

For more complex infinite abstract domains (e.g., numerical ones), assigning abstract values to parts of the program space becomes harder. Prior work in synthesis and unrealizability (unrealizability2020) shows that grammar-flow analysis (GFA) (gfa) provides a systematic solution to do so. GFA analyzes programs in a regular tree grammar (in our case, the program space) by performing dataflow analysis and assigning abstract values from a semilattice to each nonterminal. In a GFA, abstract transformers assigned to individual operations are lifted to grammars by interpreting the unions of productions as joins in the semilattice. By solving the “abstract” equations resulting from these interpretations, one can obtain a representation of the program space that matches the given abstract interpretation. While solving these equations can be challenging, prior work has identified cases where doing so is feasible (monotonic).

Bidirectional Typing

In a bidirectional typesystem (bidirectional), type checking and type inference are done simultaneously. As noted in Section 5.2, this style of typechecking can be naturally expressed as a pruner in ChopChop. Type checking corresponds to describing how to build, via a corecursive function, a well-typed space of programs from well-typed component subspaces. Type inference corresponds to performing an analysis on a space of programs via a fixpoint computation.

8. Conclusion

We introduced ChopChop, a new framework for semantic constrained decoding that allows one to impose semantic constraints directly on the abstract syntax trees representing programs (instead of their string syntax). ChopChop lets users program constraints by providing semantic pruners—recursive program operating over finite representations of the infinitely many programs the LM can produce on a given prefix. This flexibility enables new applications—e.g., constraining LMs to only output programs that are equivalent (up to rewrite rules) to a given input program.

ChopChop bridges the gap between formal methods and the outputs of language models. Looking forward, there are numerous opportunities to enhance the framework. In terms of programmability, users of ChopChop must directly define a pruner for the property they wish to enforce as a corecursive function on program spaces. Moreover, this function must return a space that is regular. There may be a better interface for programming pruners that abstracts away these details. In terms of performance, the current implementation of ChopChop is relatively unoptimized, incurring noticeable per-token overhead: future work could likely greatly improve the runtime performance.

Exploring new backends for reasoning about codata, such as term rewriting solvers (egg; egglog) or constrained Horn clauses (chc), could enable new applications. Finally, we envision better combinators for expressing semantic pruners and for automatically proving whether pruners over-approximate or under-approximate a user-provided constraint.

Acknowledgements.

The project is supported in part by a Microsoft Faculty Fellowship; a UCSD JSOE Scholarship; and NSF under grants Grant #CCF-2422214, Grant #CCF-2506134, Grant #CCF-2446711. This material is based upon work supported by the National Science Foundation Graduate Research Fellowship Program under Grant No. Grant #DGE-2038238. Any opinions, findings, and conclusions or recommendations expressed in this publication are those of the authors, and do not necessarily reflect the views of the sponsoring entities. Loris D’Antoni holds concurrent appointments as a Professor at the University of California San Diego and as an Amazon Scholar. This paper describes work performed at the University of California San Diego and is not associated with Amazon.

Data-Availability Statement

The code for this paper is available on GitHub. An artifact containing a Docker image is available on Zenodo (artifact).

Appendix A Appendix

A.1. Soundness and Completeness Proofs

We prove the main results of Section 3.2.1. We first prove Lemma 3.1:

Proof.

Let $\mathsf{lm}$, $\Phi$, and $\mathsf{check\_realizable}_{\Phi}$ be given. Suppose Algorithm 1 returns a string $\omega^{\prime}\in\Sigma^{*}$ which does not satisfy $\Phi$. The only way for $\omega^{\prime}$ to be returned is from Line 7. But we check that the output of Line 7 satisfied $\Phi$ on Line 6! By contradiction, no string $\omega^{\prime}\in\Sigma^{*}$ can be returned which does not satisfy $\Phi$. ∎

We next prove Lemma 3.2. The proof is identical for top-p and top-k sampling:

Proof.

Suppose $\omega$ is a valid solution that can be found with non-zero probability in unconstrained (top-p/top-k) decoding. Consider an execution of unconstrained decoding that occurs with non-zero probability and returns a solution $\omega$ that satisfies $\Phi$. Such an execution is guaranteed to exist because there are only finitely many executions that can return $\omega$. Let $\alpha=(\alpha_{1},\dots,\alpha_{n}=\omega\mathsf{END})$ be the sequence of elements dequeued during the execution. Since the search is non-backtracking (enqueueing $\omega\tau$ deletes all elements that don’t start with $\omega$), every $\alpha_{j}$ is a prefix of $\alpha_{j+1}$. In particular, every $\alpha_{j}$ for $j<n$ is realizable. If $\mathsf{check\_realizable}_{\Phi}$ is complete, then this exact execution is also possible in the constrained case with the same probability.

The probability of producing $\omega$ in the unconstrained case is the sum of the probabilities of producing each of the (finitely many) executions that produce $\omega$. Since constrained decoding can produce every execution that the unconstrained case can with the same probability, the probability that unconstrained decoding produces $\omega$ is at least as large as the probability that unconstrained decoding produces $\omega$. ∎

Note that Lemma 3.2 also applies to greedy decoding (i.e., top-k sampling for k=1).

A.2. Lexing

We open with a brief background on maximal munch lexing, the most widely used lexing formalism.

Maximal Munch Lexing

A maximal munch lexer (compilers_dragon_book) is instantiated by a collection of disjoint regular expressions, each of which corresponds to a different kind of lexeme. For example, we might give the regex [1-9][0-9]* to describe the set of strings representing integers, and the regexes true and false to describe the strings encoding keywords true and false, respectively. We call these regexes lexeme classes.

Given such a collection of disjoint regexes, a lex of a string $\omega$ is a partition $(\omega_{1},\dots,\omega_{n})$ of $\omega$ so that each $\omega_{j}$ matches one of the given regexes. These strings $\omega_{j}$ are called lexemes. The maximal munch lex of $\omega$ is the unique lex so that, for any other lex $(\omega_{1},\dots,\omega_{j},\omega_{j+1}^{\prime},\dots\omega_{m}^{\prime})$, we have $|\omega_{j}|\geq|\omega_{j+1}^{\prime}|$.

Lexing a Partial Program

Given a string $\omega$ that represents a partial program, our goal is to construct a representation of set of maximal munch lexes of all the strings that extend $\omega$. This will be the output we pass to the parser. For example, the string 1 + 3 can be extended to 1 + 34, whose maximal munch lex is [1, +, 34], or 1 + 3 + 4, whose maximal munch lex is [1, +, 3, +, 4]. To represent the set of maximal munch lexes of completions of $\omega$, we will build a partial lex $L$ like the following:

[TABLE]

Each element of $L$ is a lexical prefix – a sequence of lexemes that ends in a regex. A lexical prefix describes the set of prefixes that match it. So [1, +, 3] describes the lexes [1, +, 3, +], [1, +, 3, 5, 6], etc. And [1, +, 3[0-9]+] describes the lexes [1, +, 31, +], [1, +, 354, 6], etc. The partial lex $L$ describes the set of lexes that extend any one of its lexical prefixes. Our goal will be to produce $L$ from $\omega$ so that the lexes described by $L$ are exactly the longset match lexes of completions of $\omega$.

To build $L$ incrementally, we introduce a richer representation of $L$ that tells us how much of a regex has already been matched by $\omega$. For example, if I had a “print” lexeme, then

[TABLE]

could be the partial lex of both $\omega=\text{``print''}$ and $\omega=\text{``pri''}$. To resolve this, we add a $@$ annotation that tells us how much of a regex has been matched. Then, I can distinguish [print @] from [pri @ nt] Left of the $@$ is a string that has been explicitly matched by the end of $\omega$, and right of the $@$ is a regex that has not been matched yet.

To advance an annotated regex by a character $a$, we define $D_{a}(\text{{x @ y}})=\text{{xa @ }}D_{a}(\text{{y}})$ , where $D_{a}(\text{{y}})$ is the usual Brzozowski derivative of y with respect to $a$ (Brzozowski). For example,

[TABLE]

Given $\omega$, we will incrementally build a lexer state, a set of sequences of such annotated regexes x @ y like

[TABLE]

that projects to the desired $L$ when annotation symbols $@$ are removed.

The full algorithm to build $L$ is given in Algorithm 2. It very closely mirrors the naïve approach to maximal munch lexing (compilers_dragon_book). We iterate through $\omega$ character by character, constructing the lexer state $\tilde{L}$ incrementally. As we go, we discard the partial lexes from $\tilde{L}$ that fail maximal munch by not having the largest possible tokens from left to right. At the end of the algorithm, we remove the pointers and throw away “ignorable” tokens (e.g., whitespace and comments) to convert $\tilde{L}$ into $L$.

If there is a reserved whitespace character (e.g., ’ ’) and a class of lexemes that matches a single occurrence of that character (e.g., s+), then the lexer state $L$ that our algorithm produces describes exactly the set of maximal munch lexes of completions of $\omega$, up to the presence/absence of ignorable tokens like whitespace.

Theorem A.1 (Correctness of Partial Lexing).

Suppose every string in $\Sigma^{*}$ is expressible by some token sequence in $\mathbf{T}^{*}$. Suppose the regexes that each language token matches are disjoint. Suppose $\mathsf{lex}$ is a maximal munch lexer. Suppose there is an whitespace character in our language which matches the ignorable lexeme class and appear in no lexeme of any other class. Then for every LM token sequence $\omega\in\mathbf{T}^{*}$, the set of sequences of language token predicates $L=\mathsf{partial\_lex}(\omega)$ corresponds exactly to the maximal munch lexes of continuations of $\omega$ with whitespace tokens removed (i.e., $\langle\!\langle{L}\rangle\!\rangle^{\mathsf{lexerstate}}=\{\mathsf{lex}(\omega\beta)\mid\beta\in\mathbf{T}^{*}\}$).

Proof.

We first prove two properties of $\mathsf{compute\_lexer\_state}$.

Lemma A.2 (Property 1).

The concatenation of the left-hand sides of every lexical prefix in $\mathsf{compute\_lexer\_state}(\omega)$ is exactly $\omega$.

Proof.

The proof proceeds via straightforward induction on the length of $\omega$. When $\omega=\epsilon$, we have $\tilde{L}=\{()\}$. When $\omega^{\prime}=\omega a$, we know that every lexical prefix in $\tilde{L}$ on line 12 matches left-hand-sides with $\omega$. Each partial lex added by $\mathsf{extend\_lexer\_state}$ takes a derivative in $a$ of a lexical prefix from the input $\tilde{L}$. So, each partial lex in the output matches left-hand-sides with $\omega^{\prime}$. ∎

Lemma A.3 (Property 2).

For every $\omega$ and every $\omega^{\prime}\succeq\omega$, the maximal munch lex of $\omega^{\prime}$ is matched by exactly one lexical prefix in $\mathsf{compute\_lexer\_state}(\omega)$, including whitespace.

Proof.

The second property is proven by induction on the length of $\omega$ as well. When $\omega=\epsilon$, we have $\tilde{L}=\{()\}$ and the lex of any continuation of $\omega$ matches $()$. When $\omega^{\prime}=\omega a$, some prefix of length $m$ in $\tilde{L}$ on line 12 matches the lex of $\omega^{\prime}$. If the $m$th token of $\omega^{\prime}$ matches the lhs of the $m$th token of the lexical prefix exactly, then line 21 or line 23 adds a prefix $l$ with $m+1$ tokens that matches $\omega^{\prime}$. Similarly, if the $m$th token of $\omega^{\prime}$ is longer than the lhs of the $m$th token of the lexical prefix exactly, then line 25 adds a prefix $l$ with $m$ tokens that matches $\omega^{\prime}$. Regardless, this prefix $l$ cannot be removed by $\mathsf{remove\_nonmaximal\_munch\_lexes}$. If $l$ were removed, this would imply that one can write some other lexical prefix $l^{\prime}$ whose left-hand-sides match $\omega^{\prime}$ (by Property 1) but which is a maximal munch of $l$. But this would imply that our lex of $\omega^{\prime}$ is not a maximal munch lex of $\omega^{\prime}$ since there exists a better tokenization, a contradiction. So $\omega^{\prime}$ matches at least one lexical prefix in $\tilde{L}$. Moreover, $\omega^{\prime}$ matches at most one lexical prefix in $\tilde{L}$ because, for any two matches of $\omega^{\prime}$, one would necessarily munch the other. ∎

The final result follows from Properties 1 and 2. When we remove the annotations and whitespace from whichever lexical prefix matches the whitespace-containing $\omega^{\prime}\succeq\omega$, we get a lexical prefix matching the whitespace-lacking lex of $\omega^{\prime}$. So $\langle\!\langle{L}\rangle\!\rangle^{\mathsf{lexerstate}}\supseteq\{\mathsf{lex}(\omega\beta)\mid\beta\in\mathbf{T}^{*}\}$. For the other direction, let $l=[\alpha_{1},\dots,\alpha_{n}]$ be a lex that matches some lexical prefix in $\langle\!\langle{L}\rangle\!\rangle^{\mathsf{lexerstate}}$. Since that lexical prefix has left-hand-sides matching $\omega$, we know that $\omega$ must match a prefix of $l$ up to whitespace. Suppose

[TABLE]

where $ab=\alpha_{m}$. Then we can construct a completion of $\omega$ that lexes to $l$ by simply putting whitespace between each of the tokens following $\alpha_{m}$:

[TABLE]

So $\langle\!\langle{L}\rangle\!\rangle^{\mathsf{lexerstate}}\subseteq\{\mathsf{lex}(\omega\beta)\mid\beta\in\mathbf{T}^{*}\}$. ∎

A.3. TypeScript Typechecking

A.3.1. Details of Type Pruning

The main idea of our typepruner is presented in Section 5.2. Here, we provide our grammar, selected inference rules for single programs, and selected parts of the implementation of type_prune. We also provide some additional information on our use of bounded types.

We present our typescript grammar in Figure 15. Typing rules infering the types of individual TypeScript programs are presented in Figures 16 and 17. We use a terse, inference-only typesystem for individual programs that is used when pruning sets of programs. When we write, e.g., $\Gamma\vdash e\implies\texttt{bool}$, we mean that $e$ infers to a type that matches bool. Similarly, when we say $\Gamma\vdash s\implies\tau-()$, we mean that $s$ infers to a subtype of $\tau$ that does not contain the unit type. Note that our typing contexts $\Gamma$ assign types and a designation of mutable/immutable to variables. A much cleaner type system is given in typescript_good_typesystem, but this one suffices for our purposes. We borrow from typescript_good_typesystem the notion that statements type to their return types.

Part of the implementation of type_prune is given in Figure 14. As mentioned in Section 5.2, most cases like Add and Ternary can be handled by pruning and combining subterms. For cases like Apply, we prune f to have type ? -> tau until f collapses to a single AST. Once f collapses, we can infer its type and typeprune x appropriately.

In Section 5.2, we promised to explain our use of bounded types. Recall the function application rule from Section 5.2. There is a flaw in the behavior of that rule if we allow types of arbitrary size. If f unrolls to an application of itself (Apply (f _)), then the coterm that (type_prune gamma f (T -> tau)) represents may not be regular. In order to compute

⬇

(type_prune gamma f (T -> tau))

we must eventually type-prune a case of the form Apply ( f a ) against the type (T -> tau). If f is incomplete, then our definition of type_prune, asks us to compute

⬇

(type_prune gamma f (T -> T -> tau)).

This process continues infinitely, generating larger and larger types. Because infinitely many distinct calls to type_prune are made, we cannot represent the result as a regular coterm.

One solution is to simply return (Apply f x) when f is incomplete. This would mean that we do not typecheck a function until it is complete. For the purposes of constrained decoding, this is unsatisfactory; we ought to put some kind of restriction on the LM’s behavior as it generates the left-hand-sides of function applications. Worse, since the TypeScript syntax does not tell us whether an expression is the left-hand side of a function application until it is applied, many otherwise invalid expressions can fail to typecheck if we leave function calls uninspected. Instead, we simply bound the our types to depth 3. In our example above, the type T -> T -> T -> tau becomes T -> T -> T. This prevents type_prune from constructing infinitely many types and makes our analysis regular. However, we do sacrifice soundness for programs with deeply nested types (i.e., type_prune may accept a singleton set with an ill-typed program if trying to typecheck the program generates deeply-nested types). We did not find any such large types appearing in the LLM generated programs in practice.

The challenges in handling function application also explain why we implemented an overapproximate pruner, rather than an underapproximate pruner. For an underapproximate pruner, the obvious sound way to handle (Apply f x) is to consider a finite subset of the possible combinations of types (e.g., by only considering types up to some size bound, or inferring the possible types of f). While we do bound the size of our types to prevent nonterminating behavior, pruning f and x for each valid combination of types is expensive. More than that, it is unnecessary. Since LMs generate programs from left to right, f will always resolve to a concrete function before any of x is written. This means that we will always be able to infer the type of f when we start writing x. As a result, the only overapproximation that matters to constrained decoding is bounding the size of types. As explained above, we overapproximate types with depth greater than 3 (e.g., ((int -> ...) -> int) -> int) by types of depth 3 (e.g., ((T -> int) -> int) -> int). We did not find any such large types appearing in the generated programs in practice.

A.3.2. Benchmarks and Additional Data

Prompting

All TypeScript experiments used the following context in instruct mode. The context is borrowed from typespaper with the exception of the final 3 lines instructing the model to stay within our language subset.

You are an expert in typescript programming. Solve the given problem by writing solution code in typescript. When answering, insert the solution code in a ‘‘‘typescript...‘‘‘ block. Do NOT use arrays, strings, or lambdas! Do NOT use console.log or add tests! Do NOT throw errors!

Each benchmark consists of a comment describing the task and the function signature, e.g.,

//Write a typescript function to identify non-prime numbers. function is_not_prime(n: number): boolean

We use the comment as our prompt, and we use the signature as the prefix from which the LLM starts generating its solution, adding ‘̈“typescriptẗo the front. In our example, the prompt would be

//Write a typescript function to identify non-prime numbers.

and the LLM would begin generation by appending to the string

‘‘‘typescript function is_not_prime(n: number): boolean

Benchmarks

We ran our experiments on the following 72 benchmarks from the MBPP (mbpp) benchmarks available in the MultiPL-E dataset (multiplE):

mbpp_80_tetrahedral_number mbpp_392_get_max_sum mbpp_171_perimeter_pentagon mbpp_127_multiply_int mbpp_435_last_Digit mbpp_287_square_Sum mbpp_606_radian_degree mbpp_803_is_perfect_square mbpp_731_lateralsurface_cone mbpp_581_surface_Area mbpp_135_hexagonal_num mbpp_17_square_perimeter mbpp_77_is_Diff mbpp_126_sum mbpp_266_lateralsurface_cube mbpp_797_sum_in_range mbpp_3_is_not_prime mbpp_458_rectangle_area mbpp_441_surfacearea_cube mbpp_162_sum_series mbpp_448_cal_sum mbpp_738_geometric_sum mbpp_239_get_total_number_of_sequences mbpp_59_is_octagonal mbpp_638_wind_chill mbpp_577_last_Digit_Factorial mbpp_84_sequence mbpp_724_power_base_sum mbpp_641_is_nonagonal mbpp_279_is_num_decagonal mbpp_72_dif_Square mbpp_781_count_divisors mbpp_309_maximum mbpp_14_find_Volume mbpp_167_next_power_of_2 mbpp_600_is_Even mbpp_742_area_tetrahedron mbpp_432_median_trapezium mbpp_234_volume_cube mbpp_422_find_Average_Of_Cube mbpp_292_find mbpp_389_find_lucas mbpp_227_min_of_three mbpp_388_highest_Power_of_2 mbpp_271_even_Power_Sum mbpp_67_bell_number mbpp_274_even_binomial_Coeff_Sum mbpp_86_centered_hexagonal_number mbpp_574_surfacearea_cylinder mbpp_430_parabola_directrix mbpp_406_find_Parity mbpp_605_prime_num mbpp_264_dog_age mbpp_770_odd_num_sum mbpp_453_sumofFactors mbpp_244_next_Perfect_Square mbpp_93_power mbpp_291_count_no_of_ways mbpp_637_noprofit_noloss mbpp_293_otherside_rightangle mbpp_592_sum_Of_product mbpp_256_count_Primes_nums mbpp_479_first_Digit mbpp_267_square_Sum mbpp_58_opposite_Signs mbpp_103_eulerian_num mbpp_20_is_woodall mbpp_96_divisor mbpp_404_minimum mbpp_752_jacobsthal_num mbpp_765_is_polite mbpp_801_test_three_equal

Additional Results

We include the total number of guesses required per token for each of our three generation modes in Figure 18.

A.4. Equivalence-Guided Decoding

A.4.1. Benchmarks and Additional Data.

3 shows a variation of our equivalence-guided decoding benchmarks where the rules were added to the prompt for the LM.

Context.

The equivalence benchmarks use the following context. The last line is removed for the NO-DELIMIT experiments.

You are a code refactoring assistant for a simple functional language. The language consists of expressions which are either identifiers, integers, basic arithmetic operations, function application, and let expressions. The only binary operators are +, -, *, and /. All other functions (for example, sqrt or pow) are named--- ONLY use names appearing in the original program.

As examples, syntactically valid programs would include:

‘‘‘ let x = sqrt 42 in let y = pow (f x) 2 in y - 3 ‘‘‘

and

‘‘‘ f x + g y ‘‘‘

Your job is to refactor programs into equivalent ones which also have clear, readable style using let bindings when helpful. Never introduce new features not in the language. Never include comments or explanations. ONLY output code, then IMMEDIATELY stop. Never redefine variables in the original program or that have already been defined.

Start and end your solution with a codeblock using ‘‘‘.

Benchmarks.

We show the 10 benchmark programs we used below.

1. fetch_document (authorize_user_for_document ( authenticate_user current_user web_request) document_id)

2. sqrt (pow (x1 - x2) 2 + pow (y1 - y2) 2)

3. pow 10 (-15) * (66743 * m1 * m2) / (pow r 2)

4. add_watermark (apply_filter ( crop_image original_image selection) filter_type) watermark_image

5. start + (end - start) * scale

6. (sum (filter positive xs)) / (length (filter positive xs))

7. power / 1000 * hours * price_per_kwh

8. (-b + sqrt ((pow b 2) - 4 * a * c)) / (2 * a)

9. map toUpper (filter isAlpha s)

10. sqrt ((pow (a - ((a+b+c)/3)) 2) + (pow (b - ((a+b+c)/3)) 2) + (pow (c - ((a+b+c)/3)) 2)) / 3

Egglog file.

We show the Egglog file defining the rewrites for the initial e-graph below. It encodes basic arithmetic rules.

(datatype Math (Num i64) (Str String) (Var String) (Add Math Math) (Sub Math Math) (Neg Math) (Pow Math Math) (Sqrt Math) (Mul Math Math) (Div Math Math) (App Math Math))

(rewrite (Add a b) (Add b a))

(rewrite (Add (Num a) (Num b)) (Num (+ a b)))

(rewrite (Add (Add a b) c) (Add a (Add b c)))

(rewrite (Neg a) (Sub (Num 0) a))

(rewrite (Sub (Num 0) a) (Neg a))

(rewrite (Sub a b) (Add a (Mul (Num -1) b)))

(rewrite (Sub (Num a) (Num b)) (Num (- a b)))

(rewrite (Mul a b) (Mul b a))

(rewrite (Mul (Num a) (Num b)) (Num (* a b)))

(rewrite (Mul (Mul a b) c) (Mul a (Mul b c)))

(rewrite (Mul a (Add b c)) (Add (Mul a b) (Mul a c)))

(rewrite (Div a b) (Mul a (Div (Num 1) b)))

(rewrite (Mul a (Div (Num 1) b)) (Div a b))

(rewrite (Div (Num 1) (Mul b c)) (Mul (Div (Num 1) b) (Div (Num 1) c)))

(rewrite (Mul (Div (Num 1) b) (Div (Num 1) c)) (Div (Num 1) (Mul b c)))