Specification-Guided Generation for Large Language Models

📄 arXiv: 2610.41511v1 📥 PDF

作者: Alessandro Previti, Konstantinos Vandikas, Mario Alviano, Mats Carlsson, Albin Larsson Forsberg, Alexandros Nikou, Athanasios Karapantelakis, Aneta Vulgarakis

分类: cs.AI

发布日期: 2026-10-30

💡 一句话要点

提出神经符号框架以解决大语言模型的规范满足问题

🎯 匹配领域: 支柱九：具身大模型 (Embodied Foundation Models)

关键词: 大语言模型 规范引导 神经符号推理 约束解码 输出生成

📋 核心要点

  1. 现有的约束解码方法主要关注语法，无法直接满足正式规范，导致生成输出的有效性不足。
  2. 本文提出了一种神经符号的规范引导解码框架，通过结合LLM生成与符号推理来解决规范满足问题。
  3. 实验表明，提出的仅向前变体能可靠地产生符合规范的输出，并减少了重复推理的次数，提升了效率。

📝 摘要（中文）

大语言模型（LLMs）能够生成结构化输出，但现有的约束解码方法主要侧重于语法，无法直接满足正式规范。本文提出了一种神经符号的规范引导解码框架，将LLM生成与符号推理相结合。在每一步，该框架通过过滤掉无法扩展为满足规范的输出的值来细化解码语法。我们展示了一种仅向前的变体，通过构造保证规范满足，以及一种回溯变体，当早期可行选择的下游后果仅留下LLM自身认为不合适的值时，修正这些选择。该框架与模型无关，无需重新训练，并基于现有的语法约束解码机制。实验结果表明，仅向前的变体可靠地产生符合规范的输出，同时相比于拒绝采样减少了重复的LLM推理，并且仅增加了适度的符号推理开销。回溯变体进一步减少了模型被迫选择自身认为不合适的值的情况，从而显著改善了对LLM对提示的解释的遵循。

🔬 方法详解

问题定义：本文旨在解决大语言模型生成输出时无法直接满足正式规范的问题。现有的约束解码方法主要关注语法，未能有效处理规范满足的需求。

核心思路：提出的框架结合了神经网络生成与符号推理，通过在每一步过滤不符合规范的值，确保生成的输出能够满足预设的规范。

技术框架：框架包含两个主要变体：仅向前的变体和回溯变体。仅向前的变体在构造时保证规范满足，而回溯变体则在发现不合适的选择后进行修正。

关键创新：最重要的创新在于提出了一种模型无关的解码框架，能够在不需要重新训练的情况下，基于现有的语法约束解码机制进行有效的规范满足。

关键设计：框架设计中，采用了过滤机制来细化解码语法，并通过符号推理来减少不合适选择的影响，确保生成的输出符合LLM的解释。

📊 实验亮点

实验结果显示，仅向前的变体在生成符合规范的输出方面表现出色，相比于拒绝采样方法，减少了重复推理次数，并且符号推理的开销保持在适度水平。回溯变体进一步降低了模型选择不合适值的频率，显著提高了输出的质量。

🎯 应用场景

该研究的潜在应用领域包括自动化配置生成、约束求解和智能助手等。通过确保生成输出符合特定规范，能够提升系统的可靠性和用户体验，具有重要的实际价值和广泛的应用前景。

📄 摘要（原文）

Large language models (LLMs) can generate structured outputs, but existing constrained-decoding methods mainly enforce syntax and cannot directly enforce satisfaction of a formal specification. We introduce a neuro-symbolic, specification-guided decoding framework that combines LLM generation with symbolic reasoning. At each step, the framework refines the decoding grammar by filtering out values that cannot be extended to an output satisfying the specification. We present a forward-only variant that guarantees specification satisfaction by construction, and a backtracking variant that revises earlier feasible choices when their downstream consequences leave only values that the LLM itself judges unsuitable. The framework is model-agnostic, requires no retraining, and builds on existing grammar-constrained decoding mechanisms. Experiments on configuration and constraint-solving benchmarks show that the forward-only variant reliably produces specification-compliant outputs while reducing repeated LLM inference compared with rejection sampling and incurring modest symbolic-reasoning overhead. The backtracking variant further reduces cases in which the model is forced to select values that it has itself judged unsuitable, thereby substantially improving adherence to the LLM's stated interpretation of the prompt.