$\texttt{SEM-CTRL}$: Semantically Controlled Decoding

TL;DR

SEM-CTRL tackles the challenge of producing outputs that are both syntactically correct and semantically valid from off-the-shelf LLMs. It couples Answer Set Grammar-based semantic constraints with token-level Monte Carlo Tree Search to prune the decoding space and optimize for task goals, guaranteeing correctness by construction. Empirically, SEM-CTRL enables small models to rival or surpass larger reasoning models across synthetic grammar synthesis, combinatorial reasoning, and planning tasks, while maintaining strong semantic guarantees. The approach has practical implications for deploying reliable LLMs in domains requiring strict correctness and domain knowledge, reducing generation costs through principled search and caching.

Abstract

Ensuring both syntactic and semantic correctness in Large Language Model (LLM) outputs remains a significant challenge, despite being critical for real-world deployment. In this paper, we introduce $\texttt{SEM-CTRL}$, a unified approach that enforces rich context-sensitive constraints and task- and instance-specific semantics directly on an LLM decoder. Our approach integrates token-level MCTS, which is guided by specific syntactic and semantic constraints. The constraints over the desired outputs are expressed using Answer Set Grammars -- a logic-based formalism that generalizes context-sensitive grammars while incorporating background knowledge to represent task-specific semantics. We show that our approach guarantees correct completions for any off-the-shelf LLM without the need for fine-tuning. We evaluate $\texttt{SEM-CTRL}$ on a range of tasks, including synthetic grammar synthesis, combinatorial reasoning, and planning. Our results demonstrate that $\texttt{SEM-CTRL}$ allows small pre-trained LLMs to efficiently outperform larger variants and state-of-the-art reasoning models (e.g., o1-preview) while simultaneously guaranteeing solution correctness.

Figures (4)

• Figure 1: Overview of method showing: (a) Blocksworld planning task with initial and goal states. (b) asg fragment showing syntax and semantic rules. Curly braces {…} denote parse tree semantic constraints $\Psi_{PR}$, with domain rules and state encoding $\Psi_{B}$ under "Background". (c) Partial parse tree of a valid solution sequence. (d) mcts search over the token space, with correct (green / ✓), suboptimal (orange / $-2$), and invalid paths (red / $\times$). States are simplified to show the generated token at each node instead of the entire sequence. Blue arrow shows mcts-parse tree correspondence; each node maps to a valid parse tree as constraints are computed per step.
• Figure 2: Prompt template for the 3$\times$3 Sudoku task, showing the system message that defines the task and grammar, followed by example interactions.
• Figure 3: Prompt template for the Blocksworld planning task, showing the system message that defines predicates and action restrictions, followed by example interactions.
• Figure 4: Answer Set Grammar for the language $a^nb^nc^n$. The grammar uses ASP annotations (shown in bold) to enforce equal lengths of $a$'s, $b$'s, and $c$'s sequences.

Theorems & Definitions (3)

• Definition 3.1: Syntactic Control
• Definition 3.2: Context-Sensitive Control
• Definition 3.3: Semantic Control