用于LLM解码的语义前缀预言机：契约与差分验证
Semantic Prefix Oracles for LLM Decoding: Contracts and Differential Validation
浏览论文内容
中文总结 AI 辅助
本文提出语义文法规范，在Earley下降中执行语义约束实现安全剪枝，并通过差分验证表明其能有效定位无效程序，提升生成正确性。
中文摘要 AI 辅助
约束解码可以强制实施正则或上下文无关的输出格式，但许多程序生成失败是语义性的：作用域、类型和声明效应依赖于上下文。我们提出语义文法规范，这是一种声明式形式体系，将此类约束附加到上下文无关表面，并在Earley下降过程中执行它们。我们的实现强制执行“安全剪枝”：它仅拒绝那些语义矛盾无法通过任何延续修复的前缀。一个独立的、依赖文法的“死端自由”属性保证了每个剩余分支都存在可实现的见证。我们给出了基于表面生产力、类型覆盖和从左到右约束流的简单充分条件。我们的有限lambda、核心ML和类C片段满足这些条件，而实验中使用的STLC实例则不满足：普通STLC可能违反类型覆盖，我们展示了如何通过限制其类型宇宙来恢复该属性。一个分词器提升引理在显式词汇覆盖假设下将字符级见证提升为token序列。我们针对生产编译器（ocamlc、cc）进行差分验证实现。在65个编译器有效程序的每个前缀上，我们观察到零次错误剪枝。语义预言机在30个无效程序中定位了25个，而仅语法预言机为0个，并在42个递归探测上达成一致。一项包含九种模型的匹配语义与语法消融的十二模型生成研究发现，每个模型-语言对的观察到的语义减语法点估计均为非负，STLC任务正确性最大值为+15.2点，ML有效性最大值为+14.3点。
英文摘要
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.
发表机构
- ENS de Lyon（里昂高等师范学院）
- Unsuspicious Industries（Unsuspicious Industries公司）
- Université de Lille（里尔大学）
机构由 AI 辅助整理，请以论文原文为准。
