PaperlayerView exact revision on arXiv

Source-linked AI summary

Semantic Prefix Oracles for LLM Decoding: Contracts and Differential Validation

Paul Kronlund-Drouault

arXiv:2609.35425v1cs.PLcs.AIcs.CL

TL;DR

Syntax-only constraints cannot express semantic failures involving scope, typing, and declaration effects. The paper executes semantic constraints during parsing and reports zero false prunes across every prefix of 65 compiler-valid programs.

  • Problem

    Syntax-only constraints cannot express consequential program-generation failures involving scope, type compatibility, and declaration effects.

    Source: §1 · p. 1

  • Method

    Aufbau encodes semantic rules as constraints over evidence graphs and solves them during Earley descent, rejecting prefixes with stable contradictions.

    Source: §2.1 · p. 2, §2.2 · p. 3

  • Results

    Zero false prunes occurred across every prefix of 65 compiler-valid programs in differential validation against production compilers.

    Source: §7 · p. 10

  • Takeaways & Limitations

    Dead-end freedom is guaranteed only for grammars meeting surface-productivity, type-coverage, and left-to-right-flow conditions; token-level lifting additionally assumes vocabulary coverage.

    Source: §7 · p. 10

    The rejection proof is not a mechanized proof of the code, and finite hand-selected validation cohorts do not establish optimized-engine verdict correspondence at every token boundary.

    Source: §4.1 · p. 6, §6 · p. 10

Abstract

from arXiv · show

Constrained decoding can enforce regular or context-free output formats, but many program-generation failures are semantic: scope, typing, and declaration effects depend on context. We present semantic grammar specifications, a declarative formalism that attaches such constraints to a context-free surface and executes them during Earley descent. Our implementation enforces \emph{safe pruning}: it rejects only prefixes whose semantic contradictions cannot be repaired by any continuation. A separate, grammar-dependent, \emph{dead-end freedom} property guarantees the existence of a realizable witness for each remaining branch. We give simple sufficient conditions based on surface productivity, type coverage, and left-to-right constraint flow. Our finite-lambda, core ML, and C-like fragments satisfy them, while the STLC instance used in our experiments does not: plain STLC can violate type coverage, and we show how restricting its type universe recovers it. A tokenizer-lifting lemma carries character-level witnesses to token sequences under an explicit vocabulary-coverage hypothesis. We validate the implementation differentially against production compilers (\texttt{ocamlc}, \texttt{cc}). Across every prefix of 65 compiler-valid programs we observe zero false prunes. The semantic oracle localizes 25/30 invalid programs mid-stream, against 0/30 for a syntax-only oracle, and agrees on 42/42 recursion probes. A twelve-model generation study, including a matched semantic-versus-syntactic ablation for nine models, finds nonnegative observed semantic-minus-syntactic point estimates for every model-language pair, with maxima of $+15.2$ points on STLC task correctness and $+14.3$ points on ML validity.

1 Introduction

Syntax-only grammars cannot express consequential contextual failures such as scope, typing, and declaration effects. The paper presents semantic prefix constraints and asks when they can safely prune continuations and how their implementation can be validated.

1 Introduction

  • Safe pruning preserves every prefix with a semantically valid completion, while dead-end freedom guarantees a completion for every retained prefix.The two guarantees are distinct and require different hypotheses.Source: §1 · p. 1
  • For example, semantic constraints mask true after “let x : Int =” even though that assignment is syntactically valid in the context-free grammar.The annotation fixes the demanded type, while the boolean literal has a fixed type.Source: §1 · p. 2
  • Aufbau executes declarative typing rules during Earley descent and rejects a path only after a stable semantic contradiction.The language-parametric format attaches typing rules to a context-free surface; safe pruning is an oracle property, while dead-end freedom depends on the grammar.Source: §1 · p. 2
  • Across every prefix of 65 compiler-valid programs, there were zero false prunes; the semantic oracle localized 25/30 invalid programs mid-stream versus 0/30 for syntax-only constraints.The implementation was also differentially validated against production compilers, and agreed on 42/42 recursion probes.Source: §1 · p. 2

2 The Constraint Model

The constraint model combines a context-free surface with semantic evidence evaluated incrementally during parsing. It proves safe pruning for every instance and gives sufficient grammar conditions for the stronger guarantee of dead-end freedom.

2.1 Grammar Specifications

  • A semantic grammar specification is a context-free grammar with semantic rules attached to nonterminals; a semantic prefix grammar additionally meets three conditions for witness construction.Production bindings annotate evidence used by rules without changing the context-free structure.Source: §2.1 · p. 2
  • The language-parametric IR represents semantic rules with constructor patterns and shared holes, not built-in notions of types or functions.Ascription and first-order unification express equality, membership, and structural matching.Source: §2.1 · p. 2, §2.2 · p. 3

2.2 Evidence and Constraint Graphs

  • Each parsed node carries status, a possible type term, context effects, and bindings that become resolved only after the parser passes the child.Rules connect evidence into a graph; Aufbau builds and solves it during Earley descent, and only exact nodes export declarations to right siblings.Source: §2.2 · p. 3
  • Fixed-prefix evaluation and finite-candidate masking are decidable when reachable zero-consumption left-corner dependencies are acyclic and every reachable nonterminal is productive.The checks rule out unbounded evidence elaboration on a finite span and unproductive reachable syntax.Source: §2.2 · p. 3

2.3 Verdicts: Safe Pruning and Dead-end Freedom

  • Aufbau never rejects a prefix with a witness: rejection requires a stable contradiction on every compatible branch.Stable contradictions persist under extension; ambiguity is existential, so a prefix is Lost only if every compatible branch is Lost.Source: §2.3 · pp. 3–4
  • Surface productivity, type coverage, and left-to-right constraint flow together suffice to make every Live prefix completable.The proof completes the leftmost unfinished position repeatedly, using the first condition for syntax and the latter two for typed expressions.Source: §2.3 · p. 4
  • Finite-lambda, core ML, and C-like fragments meet the coverage conditions, but the experimental STLC and tool DSL instances do not.Restricting STLC to finitely many base types with literals restores coverage, but the reported STLC experiments did not use that restriction; the tool DSL lacks a closed docs value.Source: §2.3 · p. 4

2.4 Worked Example

  • In the worked example, a pending body leaves the graph open and Live, while looking up y in a context containing only x:int yields a stable contradiction.A complete term resolves x in the fixed context and closes the graph.Source: §2.4 · p. 4

3 Aufbau, P7, and the Instances

Aufbau executes semantic grammar rules during Earley parsing, and P7 uses its prefix oracle to guide token decoding. The language instances differ in their guarantees and boundaries, while tokenizer lifting connects character-level witnesses to token sequences under explicit assumptions.

3.1 Architecture

  • P7 submits candidate tokens to Aufbau’s prefix oracle, which excludes Lost tokens, commits Live tokens, and ends decoding on Satisfied.The language definition is lowered to Aufbau’s semantic grammar IR and executed inside an Earley parser.Source: §3.1 · p. 4
  • The mask preserves model stop tokens mid-derivation and prunes rather than repairs, so it can leave well-formed output that still fails grading.The evaluation therefore counts abandonments rather than hiding them.Source: §3.1 · p. 5
  • Under exact spelling and vocabulary coverage, every character-level witness factors into a finite token sequence, lifting witness reachability to token decoding.Regular derivatives carry the oracle state across tokens that end inside a terminal recognizer.Source: §3.1 · p. 5

3.2 Language Instances

  • Finite Lambda satisfies the stated productivity, type-coverage, and left-to-right-flow conditions, unlike experimental STLC, whose unrestricted base types permit Live prefixes without witnesses.Finite Lambda restricts base types to Int, Bool, and Float with literals; STLC retains safe pruning but has no dead-end-freedom claim.Source: §3.2 · p. 5
  • Core ML is a strict OCaml subset accepted without translation; its universal assert false inhabitant covers reachable expression-type demands, and checking-mode let rec uses a fixed signature.The fragment supports differential prefix validation against ocamlc.Source: §3.2 · p. 5
  • The C-like fragment supports typed declarations, functions, control flow, arithmetic, and pointers, but does not guarantee full C compiler acceptance or diagnostics-free output.Its return-type check postdates the generation study, whose C results use the earlier grammar.Source: §3.2 · pp. 5–6
  • C-like dead-end freedom rests on realizable demanded types and productive statements, while separate differential checks assess compatibility with cc.Scalar literals realize scalar types, and casts from scalar literals realize pointer types admitted by the grammar.Source: §3.2 · p. 6
  • The tool DSL uses a fixed typed registry across three surface dialects, threading each turn’s bindings into later decoding, but its harness checks supplied witnesses rather than dead-end freedom.With empty context, a summarize call can be Live yet lack a docs argument witness; the 51-case harness injects demanded-type bindings and checks acceptance.Source: §3.2 · p. 6

4 Empirical Findings

The evaluation separates compiler-based oracle validation from generation effects and exploratory measurements. Differential tests found no observed false prunes, while matched generation comparisons showed nonnegative semantic-minus-syntactic estimates across tested model-language pairs.

4.1 Differential Prefix Validation

  • 0/65 compiler-valid programs were falsely pruned at any prefix (40 ML, 25 C), with a pooled Wilson 95% upper bound of 5.6%.The finite cohorts validate selected ML and C implementation behavior, rather than exhaustively establishing correctness.Source: §4.1 · pp. 6–7
  • 25/30 invalid programs were localized mid-stream, versus 0/30 for syntax-only; all 42 recursion probes agreed with ocamlc.In caught cases, the Lost position trailed the start of the compiler diagnostic span by 2.3 characters pooled.Source: §4.1 · p. 7
  • Validation time grew mildly superlinearly, with the largest 450-token C and 65-application STLC inputs staying under ∼130 ms.Across four stress families, log–log slopes were roughly 1.1–1.4.Source: §4.1 · p. 7, Figure 3 · p. 7

4.2 Constrained Generation

  • Mixed mode tracked full chain-of-thought within a few points while emitting 28–36 tokens instead of 1,100–2,000.It confines the mask to a late emission block after free reasoning.Source: §4.2 · p. 7
  • Across nine models that ran both ablation arms, every observed semantic-minus-syntactic model-language point estimate was nonnegative; largest lifts were +15.2 points on STLC task correctness and +14.3 on ML validity.Source: §4.2 · pp. 7–8
  • On C, direct and syntax-only masks both raised pooled validity from 53% to 80% (+27 points); the semantic increment was zero and not significant.These C results predate the return-type check added to the grammar; rerunning the semantic arm is future work. On STLC, direct masking was slightly negative pooled (44% to 40%), while mixed mode reached 55%.Source: §4.2 · p. 8

4.3 Exploratory Observations

  • Rejected first choices were associated with higher pre-mask entropy, while semantic constraints reduced average admissible tokens from 26.3 to 16.8 on ML and raised forced positions from 9% to 13%.The branching measure is model-free and conditioned on the evaluated corpus; on C, the semantic oracle admitted 7.1 tokens per position against 11.4.Source: §4.3 · pp. 8–9, Figure 6 · p. 9
  • In unpaired tool episodes, constrained Qwen3.5-4B-Base completed 57% (8/14) against 22% (4/18) unconstrained, while fluent 4B was level at 69% against 71%.Rates varied with surface form: fluent 4B reached 88% on S-expressions against 50% on XML under the same typing rules.Source: §4.3 · p. 9

5 Related Work

Prior work constrains syntax, incrementally checks incomplete programs, and explores semantic pruning; this paper positions its semantic layer and contract analysis alongside those approaches.

Syntactic constrained decoding

  • Syntax-focused systems constrain membership in fixed regular or context-free languages, but do not carry context-dependent state such as scope, types, and declaration effects.The paper identifies its contribution as the semantic layer above Earley parsing and the contract analysis that survives tokenization.Source: §5 · p. 9

Semantic constraints

  • ChopChop frames semantic pruning as realizability, while this work presents its declarative class as an instance of that general framework.ChopChop’s type pruner is over-approximate and consistent only to type depth three.Source: §5 · p. 9

Language-specific semantic constraints

  • Mündler et al. [11] report a stronger per-language TypeScript result, whereas this work emphasizes a declarative ML fragment and reusable definitions for C-like and tool-DSL instances.The related-work discussion distinguishes per-language engineering from instances generated without new pruner code.Source: §5 · p. 10

Grammar formalisms and validation

  • The formalism combines attribute grammars, definite-clause grammars, and unification-based grammar, restricting effects to keep prefix verdicts decidable and analyzable.Its differential test checks every prefix against an oracle that grades whole programs with an independent compiler.Source: §5 · p. 10

Editors, holes, incremental typing

  • Incremental typing work treats incomplete programs as typed holes or recovers from broken text; this paper instead prunes extensions of prefixes without stable contradictions.The paper characterizes Pending as a parsed hole and Live as weaker than Hazel’s typing.Source: §5 · p. 10

6 Discussion and Limitations

The guarantees and empirical findings have explicit scope limits: proofs depend on grammar conditions, while validation and generation experiments cover finite, selected settings.

Formal limitations

  • Dead-end freedom is established for finite-lambda, core ML, and C-like fragments, but not claimed for tool DSLs or the experimental STLC instance.Unrestricted STLC violates type coverage; token reachability also assumes exact spelling and vocabulary coverage.Source: §6 · p. 10

Empirical limitations

  • Generation uses one greedy attempt per task and small hand-selected validation corpora, while language metrics differ and some comparisons are exploratory rather than causal.The C generation cells predate the return-type check in c.auf.Source: §6 · p. 10

7 Conclusion

The conclusion separates safe pruning from grammar-dependent dead-end freedom and reports finite compiler-compatibility and generation results. It frames these results as bounded evidence, not exhaustive proof.

Validation

  • Zero false prunes occurred across every prefix of 65 compiler-valid programs, while 25/30 invalid programs were caught mid-stream versus 0/30 by syntax-only decoding.The conclusion describes these as finite compatibility results for the shipped engine, not an exhaustive correctness proof.Source: §7 · p. 10

Contracts and scope

  • Surface productivity, type coverage, and left-to-right constraint flow suffice for dead-end freedom in finite-lambda, ML, and C-like fragments, but not the experimental STLC and tool instances.A tokenizer-lifting lemma requires an explicit vocabulary-coverage hypothesis.Source: §7 · p. 10

Generation results and next steps

  • The matched ablation reports positive observed typing-rule lift on ML, while every matched C difference is zero and can be explained by format control alone.The conclusion lists behavioral ML/C grading, covered finite-lambda generation, broader corpora, and mechanization as next steps.Source: §7 · p. 10
Loading 2609.35425v1…