AGDecode: Semantic Attribute Grammar Derivatives for Safety-Constrained Decoding of Large Language Models

1 Introduction

• LLMs provide no native guarantees of structural or semantic invariants, motivating constrained decoding that restricts choices to continuations admitting a valid completion.Syntactic constraints are well explored, while semantic constrained decoding has addressed selected properties such as type safety and variable scoping.Source: §1 · p. 1
• Existing semantic decoders can be tied to a single property or require lookahead over every permissible token continuation, limiting generalization to broader constraints.The cited type-safety approach evaluates checking logic over an incremental string representation [Mündler et al. 2025].Source: §1 · pp. 1–2
• Forcing complex data states into structural trees requires many unique symbols and causes state-space explosion, making coterms ill-suited to bit-precise arithmetic and path conditions.These data-dependent safety properties are naturally expressed over reachable states as a least fixed point.Source: §1 · p. 2
• Operational pruning in ChopChop couples language semantics with the execution oracle, making pruners black boxes that prevent global logical optimizations.Its coinductive coterms also fit data-dependent inductive invariants poorly because representing distinct bit-precise states requires separate structural symbols.Source: §1 · p. 2
• AGDecode models semantic constrained decoding over incomplete syntax trees and delegates relational-constraint realizability queries to external verification oracles.This separates semantic specifications from checking machinery and supports inductive properties through least-fixed-point semantics.Source: §1 · p. 3
• The framework is proved sound and complete relative to ideal evaluation, while uncertain oracle results can be handled by retrospectively verifying speculative tokens.The approach uses solvers such as SMT and CHC backends.Source: §1 · p. 3

2.1 Semantic Constrained Decoding

• A semantic monitor strengthens derivative parsing by accepting a token only when a continuation satisfies both the grammar and semantic specification.Derivative parsing advances the parser state as characters are consumed; a nonempty derivative alone guarantees syntactic continuations, not semantic validity.Source: §2.1 · pp. 3–4

2.2 Attribute Grammars

• Attribute grammars attach declarative attributes and semantic rules to grammar symbols, connecting program syntax to properties such as expression types.Unlike a context-free grammar, the example grammar can require compatible operand types and specify type promotion.Source: §2.2 · p. 4, §2.2.1 · p. 4

2.2.1 Synthesized attributes.

• In an S-attributed grammar, expression types depend on child attributes and are synthesized bottom-up; a partial promotion result explicitly marks disallowed additions.The example promotes integers to floats and disallows string addition.Source: §2.2.1 · pp. 4–5, Figure 1 · p. 5

2.2.2 Inherited attributes.

• Inherited attributes carry contextual information such as a symbol table downward, while synthesized attributes pass updates upward and between statements.The expression’s inherited symbol table supports variable lookups; declaration rules update it and pass the result along.Source: §2.2.2 · pp. 5–6

3 Overview

• AGDecode lifts attribute evaluation to incomplete parse trees and represents their semantic validity as a realizability problem over relational constraints.Unexpanded structural non-terminals become typed holes, while instantiated productions contribute local semantic rules to the residual system.Source: §3 · p. 6, §3.1 · p. 7

3.1 Residual Relational Constraint System

• Typed structural holes keep attributes dependent on unexpanded syntax symbolic, so a valid completion reduces to finding a satisfiable path through the residual relational system.Structural choice variables distinguish production alternatives; the oracle checks whether a valid path exists, with conservative or speculative handling when solvers return unknown.Source: §3.1 · pp. 7–8

3.2 Symbolic Refinement and Rule Transformations

• Refinement narrows structural holes as characters are consumed and transforms the residual constraints; in the example, only the string-literal production satisfies the required String type.The other production choices are unsatisfiable because string addition is disallowed.Source: §3.2 · pp. 9–10, Figure 5 · p. 9

3.2.1 Partial Lexemes.

• Partial lexemes use over-approximating lexical holes until a token boundary freezes the lexeme into a solid terminal with exact localized constraints.The refinement chain requires each abstract prefix to subsume all possible concrete completions.Source: §3.2.1 · p. 10

3.3 Generalizing Semantics as Constrained Horn Clauses

• AGDecode lowers recursive relational summaries into constrained Horn clauses, enabling semantic constraints to use general logical theories such as arrays, bitvectors, and datatypes.The example clause relates a non-terminal’s evaluation to its children and the promotion relation.Source: §3.3 · p. 10

4 Declarative Semantics of Incomplete Residual Attribute Grammars

• The framework compiles partial-tree semantics into static relational constraints, allowing an oracle to prune semantically invalid search spaces early.The section proves this formulation sound and monotonic relative to evaluation over complete ground trees.Source: §4 · pp. 10–11

4.1 Residual Attribute Grammars

• Residual Attribute Grammars replace opaque semantic functions with a typed term algebra so semantic constraints can be reasoned about symbolically.Attribute equations are expressed as well-typed terms over computation symbols and attribute projections.Source: §4.1 · p. 11

4.2.1 Syntax: Partial Derivation Trees.

• Partial derivation trees represent unexpanded grammar regions as typed holes that can be refined into complete trees.Their concretizations are the complete ground trees that refine the partial tree.Source: §4.2 · p. 12, §4.2.1 · p. 12

4.2.2 Semantics: Residual Relational Constraint Systems.

• Residual relational constraint systems preserve semantic constraints at unresolved holes and defer their evaluation until structural concretization.The system acts as a relational semantic interface bounded to the partial syntax tree.Source: §4.2.2 · pp. 12–13

4.3 Compiling Structure to Semantic Constraints

• Global compilation maps production equations and partial-tree structure into a residual relational constraint system.Production equations become position-indexed constraints, with holes retained as placeholders for unexpanded regions.Source: §4.3 · pp. 13–14

4.4 Core Equivalence and Soundness Meta-Theorems

• For complete ground trees, compiled-constraint satisfiability is strictly equivalent to traditional functional attribute evaluation.For partial trees, unsatisfiability implies that every concretization is invalid.Source: §4.4 · p. 14

5 Semantic Constrained Decoding via Language Derivatives

• The derivative framework converges monotonically and guarantees soundness and completeness of real-time semantic pruning.An unsatisfiable derivative constraint system rules out every complete tree extending that prefix, while valid trees remain satisfiable at every yielded-character prefix.Source: §5 · p. 14, §5.3 · p. 16

5.1 Lexical Hole Semantics and Character Derivatives

• Lexical holes accumulate characters until a generated lexeme satisfies its terminal category, at which point the hole becomes a concrete terminal node.An unfinished lexical prefix remains a placeholder while it is a valid prefix of the terminal language.Source: §5.1 · p. 15

5.2 Semantic Derivatives of Partial Trees

• The derivative operator updates a sequence hole to represent valid remaining grammar-symbol sequences after consuming the next character.The framework also defines structural nullability to test whether a sequence of holes can derive the empty string.Source: §5.2 · p. 15

5.3 Meta-Theorems

• Derivative constraints preserve viable prefixes: unsatisfiability excludes all valid completions, whereas every prefix of a valid tree remains satisfiable.Structural path-consistency constraints prevent the oracle from satisfying semantic constraints through incompatible derivations.Source: §5.3 · p. 16, §5.2 · p. 16

6.1 Constrained Horn Clauses and Background Theories

• The encoding maps residual relational constraints to CHCs over a decidable background theory, such as linear integer arithmetic, bitvectors, or algebraic datatypes.Tree positions and semantic attributes are flattened into arguments of uninterpreted relational predicates.Source: §6.1 · p. 17

6.2 Inductive Rule Compilation

• Inductive Horn clauses make a parent relation depend on its children, the selected production, and local semantic attribute equations.Terminal nodes instead emit base facts from attributes computed from their lexeme strings.Source: §6.2 · p. 17

6.2.1 Derivative Memoization.

• A cyclic logical alias represents repeated derivative states and safely approximates infinite derivative unrolling without spurious least-fixed-point models.The alias binds the current position’s validity to that of the cached ancestor across semantic attributes.Source: §6.2.1 · pp. 17–18

6.3 Queries and Meta-Theorems

• CHCs encode semantic validation as a reachability query over structural choices, requiring a valid completion with no semantic errors.An unsatisfiable query means no valid structural completion exists and the prefix can be pruned.Source: §6.3 · p. 18
• Unknown or timeout oracle results require a mode choice: conservative rejection is sound but incomplete, while speculative acceptance is not immediately sound.The framework’s soundness and completeness are relative to the underlying oracle.Source: §6.3 · p. 18
• The CHC translation has a valid least-fixed-point model exactly when the declarative derivative system for the prefix is satisfiable.This supplies a formal connection between the relational encoding and prefix-level semantic validation.Source: §6.3 · pp. 18–19

7.1 Case Study: Safety Constraints for C

• The C case study covers null-pointer dereferences, division by zero, and uninitialized-variable accesses using path-sensitive data theories.The grammar mapping includes pointers, dereferences, and array subscripting, but omits a memory model.Source: §7.1 · p. 19

7.2 Experimental Setup

• The evaluation maps 77 memory- and pointer-focused cases from HumanEval C++ to C and tests CodeLLaMA-13B at three temperatures in speculative mode.Each SMT query has a five-second timeout; unknown or timed-out queries are treated as successful verification during generation.Source: §7.2 · p. 20

7.3.1 RQ1: Effectiveness.

• AGDecode monitored safety conditions across multiple paths; array subscripting could retreat to a null check, while pointer dereferences usually led to doomed generations.Removing assert(arr) caused the monitor to disallow the final decoder token [ in the illustrated example.Source: §7.3.1 · p. 20, Figure 6 · p. 20

7.3.2 RQ2: Overhead.

• About 21.7%-25.4% of queries timed out; invalid-query medians were 0.001s-0.002s, while valid-query quartiles ranged from 0.235s to 2.564s.Table 1 summarizes latency distributions across valid and invalid generations.Source: §7.3.2 · pp. 20–21, Table 1 · p. 21
• Verification latency depended on queried program structure rather than total program length, and statement-boundary checks were presented as feasible where character- or token-level checks might not be.Partially generated expressions can create many scenarios and contribute to timeouts; completed statements can yield simpler constraints.Source: §7.3.2 · pp. 21–22, Figure 7 · p. 21

7.4 Limitations

• The evaluation is bounded by its grammar and specifications, omits a full memory model, and lacks backtracking to identify which speculatively accepted token to replace.The authors state that this scope cannot enforce robust memory safety across unconstrained C programs.Source: §7.4 · p. 22

7.5 Contrasting With A Coinductive Approach

• AGDecode sends relational constraints to an external oracle, separating approximation choices from front-end semantics, while trading invariant-synthesis completeness for automated data-theory reasoning.The authors report no direct empirical comparison with ChopChop on this path-sensitive C safety benchmark.Source: §7.5 · p. 23

• Syntactic constrained decoding checks grammar-valid continuations but does not enforce contextual or semantic requirements.AGDecode instead checks whether a prefix can be completed into a program satisfying a property.Source: §8 · p. 24
• Existing semantic approaches include type-specific decoding and programmable pruning, while AGDecode separates constraint checking from semantics by delegating to external solvers.The cited programmable pruning approach encodes constraints in the pruners themselves, coupling checking and semantics and adding representational overhead.Source: §8 · p. 24
• Formal verification and repair generally act after complete output, whereas AGDecode applies formal methods during token generation; search samples candidates rather than enforcing validity during generation.Source: §8 · p. 24

• AGDecode reduces semantic constrained decoding to realizability over partially constructed syntax trees and compiles specifications into relational constraints for external SMT and CHC solvers.Source: §9 · p. 24
• The framework is sound and complete relative to an ideal verification oracle, and experiments demonstrate path-sensitive safety enforcement during C generation.The conclusion identifies significant token-level tail latency and motivates batching and speculative validation.Source: §9 · p. 24
• The authors plan to explore using the SMT oracle to guide next-token choice and adding backtracking for iterative refinement of generated output sections.Source: §9 · p. 25