规范引导解码：以符号可满足性逐步过滤LLM输出语法

大型语言模型（LLMs）可以生成结构化输出，但现有的约束解码方法主要强制语法，不能直接强制满足形式规范。我们引入了一种神经符号、规范引导的解码框架，它将 LLM 生成与符号推理相结合。在每个步骤中，该框架都会通过过滤掉无法扩展到满足规范的输出的值来细化解码语法。我们提出了一个仅前向变体，通过构造保证规范满足，以及一个回溯变体，当下游结果只留下 LLM 本身判断不合适的值时，修改早期的可行选择。该框架与模型无关，不需要重新训练，并且建立在现有语法约束解码机制的基础上。配置和约束求解基准测试表明，仅前向变体可靠地生成符合规范的输出，同时与拒绝采样相比减少了重复的 LLM 推理并产生适度的符号推理开销。回溯变体进一步减少了模型被迫选择其自身判断为不合适的值的情况，从而大大提高了对LLM自身所声明的提示解释的遵循程度。