Semantic framework improves safety checks while generating code
AGDecode: Semantic Attribute Grammar Derivatives for Safety-Constrained Decoding of Large Language Models
Software EngineeringProgramming Languages
Summary
Generating correct and safe computer code automatically is very challenging because programs must follow complex rules. The authors designed AGDecode, a system that carefully guides code generation to ensure many detailed safety checks, like avoiding null pointer errors and division by zero, are always met. Their method works by encoding rules as constraints and checking these with logic solvers during generation, balancing safety and efficiency. The system was tested on real C programs and showed it can enforce important safety properties without slowing down code generation too much.
What this means in practice
- •For software engineers: Generate C programs with built-in semantic safety checks to prevent common runtime errors during code synthesis.
- •For security auditors: Automatically verify that generated code adheres to path-sensitive safety properties to reduce vulnerabilities in software.
Authors
Rajan Maghera, Asher Tempest Arya, Aren A. Babikian, Marsha Chechik, Maryam Mehri Dehnavi
Abstract
Large language models (LLMs) are increasingly used for code generation, motivating techniques that guarantee the structural and semantic correctness of generated programs. Constrained decoding enforces correctness during generation by restricting token choices to those that admit at least one valid completion. While existing approaches can enforce syntactic constraints and selected semantic properties such as type safety, they either target specific properties or rely on operational pruning mechanisms that are difficult to generalize to data-dependent, inductive program properties. We present AGDecode, a programmable framework for semantic constrained decoding based on least-fixed-point semantics. AGDecode extends attribute grammars to partially constructed syntax trees, and reduces semantic constrained decoding to a realizability problem over such trees. The framework compiles semantic specifications into systems of relational constraints that are discharged by external verification oracles, such as SMT and CHC solvers, cleanly separating language semantics from constraint-solving machinery. We prove that our approach is sound and complete relative to an ideal verification oracle. In practice, solvers inevitably encounter uncertain queries; conservatively, our system can reject tokens for soundness or speculatively continue to generate until later queries resolve the entire generation. We mechanize the core metatheory in Rocq and evaluate the framework on semantic-constrained generation of C programs, enforcing path-sensitive safety properties including null-pointer safety, division-by-zero freedom, and initialized-variable usage. Our results demonstrate that solver-backed semantic constrained decoding can enforce rich semantic guarantees while incurring modest computational overhead at regular program boundaries.