技术摘要：解码时语法 (Decode-Time Grammars)

1. 问题陈述

大语言模型（LLMs）正越来越多地用于为智能体（agents）和执行系统生成代码，在这些场景中，生成的输出会在没有人工审查的情况下被编译或执行。虽然这在主流语言中行之有效，但在低资源编程表面（low-resource programming surfaces）——如领域特定语言（DSLs）、自定义库 API 或命令行工具——方面仍然表现得非常脆弱。

这类环境中的一个反复出现的失效模式是幽灵引用（ghost reference）：即一个在语法上有效的标记（例如变量名、列名、API 函数或 CLI 选项），但在当前运行时环境 $\Gamma$ 中并不存在。

• 示例： 在 TileLang 内核中引用了从未声明过的缓冲区；在 SQL 模式（schema）中选择了不存在的列；或者调用了特定库版本中不可用的内建函数（intrinsic）。
• 根本原因： 这些错误通常源于负迁移（negative transfer），即模型将邻近方言、旧版本 API 或不同工具接口的知识应用到了目标环境中。
• 现有补救措施的局限性：
  • 固定语法： 标准的语法约束解码（如 CFG）虽然能确保语法有效性，但将引用位置视为开放类（例如 identifier），从而允许了既有效又无效的名称。
  • 模型侧补救措施： 提示词工程（Prompting）、微调或重试机制可以降低错误的概率，但无法从模型的支持集（support set）中移除无效的后续内容。它们依赖于模型“倾向于”选择正确的路径，但这在错误的路径本身也非常流畅且高概率时是不够的。

2. 方法论：解码时语法

本文引入了解码时语法，这是一个根据运行时环境 $\Gamma$ 在生成过程中动态实例化语法片段（grammar fragments）的框架。

核心机制

1. 运行时环境 ($\Gamma$)： 当前状态的一个快照，包含作用域内的名称、类型（sorts）、形状（shapes）、模式条目、API 成员或工具状态。$\Gamma$ 随着声明的生成而演进。
2. 语法片段与细化顺序： 系统不使用单一的固定语法，而是使用一组按细化关系 ($\sqsubseteq$) 排序的语法片段。
   • 片段的范围从粗粒度（例如接受任何标识符）到细粒度（例如仅接受 $\Gamma$ 中声明的名称）。
   • 每个区域的策略 $\pi(s, \Gamma)$ 根据预期的类型 $s$ 和当前环境，为特定的“空缺处”（生成过程中的一个类型化位置）选择合适的片段。
3. $\tau_\Gamma$ 算子（收紧）： 这是关键机制。它将一个开放的引用位置转换为一个 $\Gamma$-类型化的插槽（$\Gamma$-typed slot）。
   • 该插槽的候选集恰好是 $\Gamma$ 中可用的名称（例如 Gamma.names(sort=Buffer)）。
   • 这些候选者被编译成一个转义后的交替项（例如 "A" | "B" | "C"），并在解码该区域前注入到 Token 级识别器中。
4. 自扩展生成： 当模型生成声明时，这些声明会被提取并添加到 $\Gamma$ 中，然后再对后续的引用空缺进行解码。这确保了引用受到已生成前缀的约束。

系统架构

其实现方案 gproj 由两个部分组成：

• TemplateInductor（离线）： 利用小规模语料库上的反统一化（anti-unification）技术来诱导语法片段和策略。它通过使用语料库正例和自动生成的负例（包括挖掘出的幽灵引用）来验证片段是否通过“硬门禁（hard gate）”，以确保可执行性和正确性。
• gproj Executor（在线）： 一个在线掩码执行器，负责维护 $\Gamma$、查询策略 $\pi$、通过 $\tau_\Gamma$ 实例化片段，并将生成的语法编译为 LLM 解码器的 Token 掩码（例如 XGrammar）。

3. 核心贡献与形式化结果

理论贡献

• 无幽灵安全性（No-Ghost Soundness）： 本文证明，对于任何将引用位置实现为 $\Gamma$-类型化插槽的片段，生成的字符串在作用域层面是构造安全的（scope-safe by construction）。每一个发出的引用都保证在 $\text{dom}(\Gamma)$ 中。
• 细化保持性（Refinement Preservation）： 本文证明，如果一个较松的片段是安全的，那么任何更紧的细化（通过 $\tau_\Gamma$）都会保持这种安全性。这使得系统可以在不重新引入错误的情况下，在不同的片段强度之间进行切换。
• 动态支持的必要性（命题 3）： 本文证明，对于无界标识符空间，没有任何一组具有固定引用支持的预编译有限族语法能同时满足安全性（无幽灵引用）和非阻塞性（允许所有有效续接）。
  • 启示： 必须在解码过程中基于前缀合成精确的引用支持。静态预编译在处理声明一致性语言时在理论上是不够的。

实践贡献

• 分工明确： 该方法将受环境约束的正确性（由掩码处理）与开放式的程序决策（由模型处理）分离。掩码保证了引用的有效性，而模型则负责选择算法、策略或意图。
• 归纳流水线： 一种从小型语料库自动生成所需语法片段和策略的方法，使得该方法无需手动进行语法工程即可应用于新的 DSL。

4. 实验评估结果

系统在 TileLang（张量内核 DSL）、SQL（Spider 数据集）、P4（数据平面语言）和 CLI 工具（git, FFmpeg）上进行了评估，使用的模型参数规模从 0.6B 到 236B 不等。

• 消除幽灵引用：
  • 在所有测试表面中，使用 $\tau_\Gamma$ 的 $\Gamma$-类型化分支 通过构造实现了 0% 的幽灵引用。
  • 相比之下，开放标识符分支（自由解码）在 TileLang、SQL 和 P4 中均出现了幽灵引用，导致 100% 的失败，且该现象与模型大小无关（从 0.6B 到 236B 均如此）。
  • 示例： 在 SQL 任务中，开放标识符导致 0% 的执行匹配率；而 $\Gamma$ 约束解码实现了 100% 的匹配。
• 模型无关性： 这种保证可以跨越模型规模进行传递。即使是 236B 的前沿模型（DeepSeek-V4-Flash），在没有掩码的情况下也无法生成有效的引用，而 0.6B 的模型在有掩码的情况下却能成功。
• 与替代方案对比：
  • 提示词/重试： 在 SQL 任务中，通过提供 Schema 并重试最多 4 次，虽然达到了 90% 的执行匹配率，但仍产生了 5 个幽灵列。而掩码机制在单次尝试中就实现了 100% 匹配且 0 幽灵。
  • 成本： 该方法会带来一定的开销。相对于无约束解码，端到端吞吐量平均减少了 17.3%。相对于标准约束解码（XGrammar），gproj 降低了 10.6–17.8% 的吞吐量。
• 离线归纳： TemplateInductor 成功为复杂的表面（如 AscendC 算子、FFmpeg 过滤器）归纳出了有效的片段，而这些片段并非手工编写，这验证了“归纳 + 硬门禁”工作流的有效性。

5. 重要性与主张

作者声称，解码时语法提供了一个精确、稳定的正确性切片，这与模型能力是正交的。

• 机械保证： 它将引用安全性从一种概率性的结果（取决于模型质量）转变为一种构造层面的保证。
• 可扩展性： 通过将“语义草图”（模型的工作）与“受环境约束的引用”（掩码的工作）分离，该系统允许较弱的模型在低资源环境下生成有效的代码，否则这些模型会产生幻觉。
• 理论必要性： 关于静态语法无法同时满足安全性与非阻塞性的证明，确立了所提议的运行时实例化方法的必要性。

作者将这项工作定位为不是解决全程序语义正确性（如算法逻辑或终止性）的方案，而是一种鲁棒的机制，用于消除在受限环境中困扰代码生成的特定类别的机械可枚举错误（即未定义符号）。