CRANE: Reasoning with constrained LLM generation

TL;DR

This work tackles the conflict between enforcing formal constraints in LLM outputs and preserving reasoning capability. It provides a theoretical analysis showing that highly restrictive grammars limit expressivity to TC^0 and proposes augmenting grammars to include reasoning steps, enabling CRANE to balance constraint satisfaction with flexible reasoning. The CRANE algorithm adaptively switches between unconstrained reasoning and constrained generation using explicit delimiters, achieving state-of-the-art improvements on symbolic and logical benchmarks (GSM-symbolic and FOLIO) over both constrained and unconstrained baselines. The results demonstrate how reasoning-augmented constrained decoding can deliver syntactically correct and semantically sound outputs with practical performance gains. This approach has meaningful implications for deploying LLMs in tool-augmented and formal-language tasks where both correctness and reasoning are critical.

Abstract

Code generation, symbolic math reasoning, and other tasks require LLMs to produce outputs that are both syntactically and semantically correct. Constrained LLM generation is a promising direction to enforce adherence to formal grammar, but prior works have empirically observed that strict enforcement of formal constraints often diminishes the reasoning capabilities of LLMs. In this work, we first provide a theoretical explanation for why constraining LLM outputs to very restrictive grammars that only allow syntactically valid final answers reduces the reasoning capabilities of the model. Second, we demonstrate that by augmenting the output grammar with carefully designed additional rules, it is always possible to preserve the reasoning capabilities of the LLM while ensuring syntactic and semantic correctness in its outputs. Building on these theoretical insights, we propose a reasoning-augmented constrained decoding algorithm, CRANE, which effectively balances the correctness of constrained generation with the flexibility of unconstrained generation. Experiments on multiple open-source LLMs and benchmarks show that CRANE significantly outperforms both state-of-the-art constrained decoding strategies and standard unconstrained decoding, showing up to 10% points accuracy improvement over baselines on challenging symbolic reasoning benchmarks GSM-symbolic and FOLIO.

Figures (3)

• Figure 1: An example from the GSM-symbolic dataset (variables in blue) where unconstrained generation produces syntactically incorrect output, while constrained generation provides a syntactically valid but incorrect answer. CRANE, however, generates a correct answer.
• Figure 2: CRANE adaptively switches between constrained LLM generation and unconstrained LLM generation based on start and end delimiters (in this example << and >>). Using these delimiters, CRANE dynamically tracks which windows (highlighted in the figure) of the LLM generation constraints should be applied to.
• Figure 3: Accuracy (%) of Qwen2.5-Math-7B-Instruct By Method and Number of Shots on GSM-Symbolic

Theorems & Definitions (16)

• Definition 2.1: Deterministic LLM Step
• Definition 2.2: Deterministic Unconstrained Decoding
• Definition 2.3: Deterministic Constrained Decoding under Grammar
• Definition 2.4: Turing Machine
• Definition 2.5: Boolean Circuit
• Proposition 3.0
• Lemma 3.0
• Proposition 3.0
• Lemma 3.1: Constant depth circuit for $\mathcal{L}_{f}$
• proof