Semantic prefix oracles improve error detection during llm code generation
Semantic Prefix Oracles for LLM Decoding: Contracts and Differential Validation
Programming LanguagesArtificial IntelligenceComputation and Language
Summary
Many computer programs fail when generated by AI because errors depend on complex meaning rules, not just grammar. The authors created a way to check these meaning rules as code is written, catching problems earlier without blocking recoverable paths. They tested their method with compilers and found it blocked invalid code more effectively than grammar-only methods. This new approach helps AI systems generate more correct code by understanding context better.
What this means in practice
- •For software developers: Detect semantic errors early during AI-assisted code generation to reduce invalid program outputs.
- •For compiler engineers: Improve compiler testing by validating generated code prefixes against semantic constraints for more precise error localization.
- •For language tool builders: Enhance programming language tooling by integrating semantic prefix checking to guide real-time code completion systems.$Commercial implications: Enables development of smarter code completion software that reduces programmer errors and increases productivity.
Authors
Paul Kronlund-Drouault
Abstract
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.