PaperlayerView exact revision on arXiv

Source-linked AI summary

CRANE: Reasoning with constrained LLM generation

Debangshu Banerjee, Tarun Suresh, Shubham Ugare, Sasa Misailovic, Gagandeep Singh

arXiv:2502.09061v4cs.PLcs.LG

TL;DR

LLMs need to meet downstream formal input constraints, but restrictive grammars can limit reasoning, and a model-general explanation has been sought. The paper analyzes this limitation and proposes CRANE, which augments grammars to allow intermediate reasoning while preserving valid final outputs. Across its reported experiments, CRANE outperforms constrained and unconstrained decoding, with improvements up to 10% on symbolic reasoning benchmarks.

  • Problem

    LLM outputs must satisfy downstream formal input constraints, while a model-general formal explanation of reasoning loss under restrictive decoding is sought.

    Source: §1 · p. 1

  • Method

    CRANE augments output grammars to permit intermediate reasoning and alternates unconstrained reasoning with constrained generation of structurally correct outputs.

    Source: §1 · p. 2

  • Results

    Up to 10% improvement over baselines on symbolic reasoning benchmarks accompanies CRANE’s reported outperformance of state-of-the-art constrained and standard unconstrained decoding.

    Source: §7 · p. 8

  • Takeaways & Limitations

    For tasks requiring syntactic and semantic correctness, reasoning-augmented constraints can balance output correctness with reasoning flexibility.

    Source: §7 · p. 8

    The expressivity analysis concerns constant-layer, log-precision LLMs and relies on suitable assumptions for single-step circuit simulation.

    Source: §3.1 · p. 4

Abstract

from arXiv · show

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.

1. Introduction

LLMs must satisfy downstream format constraints, but restrictive constrained decoding can preserve syntax while undermining functional correctness. The paper analyzes this reasoning limitation and introduces CRANE, which combines reasoning flexibility with constrained output generation.

1. Introduction

  • Constrained decoding can produce syntactically valid outputs without guaranteeing functional correctness, while unconstrained outputs may fail downstream format requirements.Figure 1 contrasts malformed unconstrained output, a valid but incorrect constrained answer, and CRANE’s correct answer.Source: §1 · p. 1, Figure 1 · p. 2
  • The paper asks whether constrained decoding reduces reasoning capabilities and how syntax-error reduction can be retained without sacrificing unconstrained reasoning.It seeks a formal explanation extending beyond the particular LLMs studied empirically.Source: §1 · p. 1
  • CRANE augments restrictive output grammars with rules for intermediate reasoning, then alternates unconstrained reasoning with constrained generation of structurally correct outputs.The approach is presented as a cost-efficient decoding strategy that avoids task-specific fine-tuning.Source: §1 · p. 2
  • Up to 10% improvement over baselines on GSM-symbolic and FOLIO accompanies CRANE’s reported advantage over state-of-the-art constrained and standard unconstrained decoding.The reported experiments cover multiple open-source LLMs and benchmarks.Source: §1 · p. 2

2. Preliminaries

The preliminaries establish notation and define constrained and deterministic decoding, then introduce Turing machines and circuit complexity as background for analyzing LLM expressivity.

2. Preliminaries

  • The paper uses LLM to mean a transformer-based model with a fixed number of layers and introduces notation for strings, functions, concatenation, and string length.These conventions apply throughout the paper.Source: §2 · p. 2

2.1. Constrained LLM Decoding

  • Constrained decoding masks the next-token distribution so only tokens permitted by the grammar or other specified constraints can be generated.A binary mask marks valid tokens with 1 and excluded tokens with 0.Source: §2.1 · pp. 2–3

2.2. Deterministic LLM Decoding

  • The paper models deterministic decoding as iterative next-token prediction and defines constrained output under grammar G, which remains unchanged when unconstrained output already belongs to G.The theoretical setup assumes deterministic outputs for simplicity, although CRANE can support stochastic decoding strategies.Source: §2.2 · p. 3

2.3. LLM Expressivity

  • Turing machines provide a stepwise computation model, while circuit families characterize fixed-length Boolean computations; the paper focuses on logspace-uniform TC0.Circuits are described by their size and depth, and uniformity relates circuits across input lengths.Source: §2.3 · pp. 3–4

3. Expressivity of Constrained Decoding

Restrictive output grammars can reduce a constant-layer LLM’s expressivity by limiting decision problems to a circuit complexity class. An augmented grammar can preserve multi-step reasoning while requiring the final answer to satisfy the original grammar.

3.1. Limitation of Constrained Decoding

  • For finite output sets, a restrictive grammar can force a decision problem’s constrained decoding to a single autoregressive step.For example, the yes/no output set {0, 1} is a regular language, and its grammar permits only one generation step.Source: §3.1 · p. 4
  • Under constrained decoding, constant-layer LLMs solving decision problems are limited to logspace-uniform TC0; st-connectivity is therefore unsolvable unless TC0 = NL.The unconstrained model can simulate polynomial-step Turing-machine computations, so this is a loss of expressivity relative to unconstrained generation.Source: §3.1 · p. 4

3.2. Reasoning with Augmented Grammar

  • An augmented grammar of the form Ga → RG permits reasoning before the final answer while ensuring that answer belongs to the original output grammar G.The reasoning component R can encode successive machine configurations; the final output remains in L(G).Source: §3.2 · p. 5
  • For any Turing machine and polynomial runtime t(n), a constant-layer, log-precision LLM with a suitable augmented grammar can simulate t(n) steps under constrained decoding.The construction stores encoded configurations in the reasoning sequence and emits the machine’s final output after halting.Source: §3.2 · p. 5

4. CRANE Algorithm

CRANE applies grammar constraints selectively, leaving reasoning generation unconstrained and constraining delimited output windows. It uses start and end delimiters to switch modes during generation.

4. CRANE Algorithm

  • CRANE leaves reasoning unrestricted and applies the output grammar only after the start delimiter, so the final answer can be constrained without restricting earlier reasoning.The transition point is marked by a start symbol S1; the final answer is enclosed by delimiters in the described setup.Source: §4 · pp. 5–6
  • Start and end delimiters mark the windows where grammar constraints apply, allowing CRANE to switch between constrained and unconstrained generation.The end delimiter returns generation to unconstrained mode, including when delimiters occur for intermediate operations.Source: Figure 2 · p. 6, §4 · p. 6
  • CRANE initializes the constrained decoder with an augmented grammar, then checks each generation window for the start delimiter to determine whether to constrain the next token.If the end delimiter is reached, CRANE updates its pointer and resumes unconstrained generation until another start delimiter appears.Source: §4 · p. 6

5. Evaluation

CRANE improves functional correctness on GSM-Symbolic and FOLIO over constrained and unconstrained baselines, while maintaining syntactic correctness. The evaluation also tests performance across few-shot counts and reports the method’s scope limitations.

GSM-Symbolic

  • GSM-Symbolic tests symbolic math expressions against ground truth using Z3; CRANE is compared with unconstrained generation, CoT, and constrained generation.The evaluation uses eight-shot prompts and greedy decoding with a 600-token limit.Source: §5 · p. 7
  • 38% accuracy with Qwen2.5-Math-7B-Instruct: CRANE exceeds constrained generation and unconstrained CoT, each at 29%.CRANE also reaches 31% accuracy with Qwen2.5-1.5B-Instruct, 5 points above CoT and 9 above constrained generation.Source: §5 · p. 7, Figure 3 · p. 7
  • CRANE has no syntax errors in its GSM-Symbolic expressions, while unconstrained CoT has errors in 10%; it can have slightly more errors than purely constrained generation.The reported table distinguishes functionally correct expressions (Accuracy) from syntactically valid expressions (Parse).Source: §5 · p. 7

Ablation Study on Few-shot examples

  • CRANE maintains higher GSM-Symbolic accuracy than the baselines at every evaluated number of few-shot examples.The displayed comparison uses Qwen2.5-Math-7B-Instruct; results for all models are in the appendix.Source: §5 · p. 7, Figure 3 · p. 7

FOLIO

  • FOLIO evaluation uses 203 expert-written validation instances, translating natural-language reasoning into FOL and checking formulas with Prover9.The comparison includes SYNCODE-constrained generation and unconstrained CoT; all use greedy decoding, an 800-token limit, and two few-shot examples.Source: §5 · pp. 7–8
  • CRANE outperforms unconstrained and constrained generation baselines on FOL translation accuracy for every evaluated model.Accuracy measures functionally correct translations; Compiles measures formulas that are syntactically valid and compile into a Prover9 program.Source: §5 · p. 8

Limitations

  • The theoretical result is limited to finite constrained languages, and CRANE requires access to output logits.The authors leave extension to infinite grammars open; models that do not expose logits are inapplicable.Source: §5 · p. 8

6. Related Works

Prior work uses grammar constraints to improve structured-output quality, while some studies report quality or distributional costs. This paper combines an expressivity analysis with an adaptive decoding approach intended to preserve reasoning.

Constrained LLM Decoding

  • Grammar-constrained generation enforces context-free grammars, and task-specific semantic constraints extend it to improve structured-output quality.Prior approaches are applied across structured generation tasks.Source: §6 · p. 8
  • Prior studies report that constrained generation can reduce output quality, while greedy token masking can distort the distribution over valid strings.Grammar-aligned methods use a trie to reduce divergence iteratively, but require costly resampling.Source: §6 · p. 8

LLM Expressivity

  • The paper studies theoretical expressivity under grammar constraints, a question the authors say prior LLM-expressivity work had not addressed.The cited background covers constant-depth circuit views and the expressivity gains associated with Chain-of-Thought reasoning.Source: §6 · p. 8

Constrained LLM Decoding

  • The proposed adaptive constrained decoding supports multiple constrained-decoding methods and uses reasoning chains to preserve LLM expressivity.Source: §6 · p. 8

7. Conclusion

The paper argues that restrictive grammars can hinder reasoning and that carefully augmented grammars can preserve reasoning while maintaining output correctness. CRANE applies these insights and is reported to improve symbolic-reasoning benchmark performance.

Conclusion

  • CRANE achieves state-of-the-art performance, with up to 10% improvement on GSM-symbolic and FOLIO, balancing constrained and unconstrained generation.The conclusion frames grammar augmentation as a way to preserve reasoning while maintaining syntactic and semantic correctness.Source: §7 · p. 8

8. Impact and Ethics

The impact statement identifies no specific societal consequences requiring emphasis. The accompanying appendix material describes Turing-machine computation and threshold circuit classes.

8. Impact and Ethics

  • The authors identify no specific societal consequences of this work that need explicit emphasis.Source: §8 · p. 11

A. Turing Machine Computation

  • A Turing machine updates its configuration step by step, halts in a final state, and outputs tokens from its output tape.The appendix describes the input, work, and output tapes and their head positions.Source: A. Turing Machine Computation · p. 14

B. Thershold Circuit Class

  • TC0 consists of constant-depth, polynomial-size threshold-gate circuits; logspace uniformity requires a logspace-bounded machine to generate each circuit from its input size.Source: B. Thershold Circuit Class · p. 14

C. Proofs

This section presents proof constructions concerning finite-output grammars and LLM computation, alongside a FOLIO evaluation-prompt example. It covers how bounded generation length permits constant-depth threshold-circuit simulation and how computation traces can be included without changing the machine’s result, and shows facts and a conclusion encoded as predicates and premises.

C. Proofs

  • For finite-output grammar Gc, the output length and autoregressive-step count are constant, so the constrained computation has a logspace-uniform constant-depth threshold-circuit simulation.The proof stacks a constant number of constant-depth circuits and notes this argument depends on Gc allowing only constant-size output strings.Source: C. Proofs · p. 14
  • For any Turing machine M, a constant-depth LLM can simulate t(n) steps using t(n) autoregressive steps and emit the recorded trace before M(x).The construction assumes M halts within t(n) steps, where t(n) is polynomial in the input length.Source: C. Proofs · p. 15
  • A constant-depth LLM can emit a computation trace r followed by M(x), and augmented constrained decoding leaves that output unchanged when M halts.The trace records the machine’s states, written tokens, and moves; the proof shows it and M(x) belong to the augmented grammar.Source: C. Proofs · p. 15

C.2. FOLIO Examples and Prompt

  • The FOLIO prompt example represents facts about Miroslav Venhoda as predicates and premises, then states that he loved music as the conclusion.The example is labeled “Listing 5. Prompt Template Used For FOLIO Evaluation.”Source: §C.2 · p. 19

C.3. Case Study For GSM-Symbolic

The case study contrasts CRANE’s reasoning with constrained and unconstrained outputs, illustrating how it combines intermediate reasoning with a final expression. [p20]

C.3. Case Study For GSM-Symbolic

  • The displayed unconstrained CoT example also derives paid hours by subtracting free hours from the total rental time.The passage’s unconstrained example uses a total-seconds-to-hours conversion in its reasoning.Source: §C.3 · p. 20
  • The CRANE example computes the rental duration, subtracts free hours, then adds the first-hour cost and priced additional hours.Its final expression is first_hour_cost + (int(end_hour - start_hour) - free_hours - 1) * multiplier * first_hour_cost.Source: §C.3 · p. 20
  • CRANE alternates constrained and unconstrained generation, while unconstrained CoT produces a syntactically incorrect expression and constrained generation a valid but incorrect one.The case study presents CRANE as producing intermediate expressions and a final answer while maintaining the model’s reasoning capabilities.Source: §C.3 · p. 20

C.4. Sampling Ablation for GSM-Symbolic

In GSM-Symbolic sampling comparisons, CRANE’s greedy decoding beats unconstrained CoT temperature sampling on Qwen2.5-1.5B-Instruct, while Llama-3.1-8B-Instruct trades higher pass@3 for more tokens. The supplied grammar specifies arithmetic expressions and their operators.

C.4. Sampling Ablation for GSM-Symbolic

  • The sampling comparison uses three unconstrained temperature-sampled generations at t = 0.7 for Qwen2.5-1.5B-Instruct and Llama-3.1-8B-Instruct.The study computes pass@1/2/3 and compares against CRANE initialized with IterGen.Source: §C.4 · p. 20
  • 35% pass@3 accuracy for unconstrained CoT temperature sampling on Llama-3.1-8B-Instruct is 2% higher than CRANE, but uses approximately 4 times as many tokens.On Qwen2.5-1.5B-Instruct, CRANE with greedy decoding achieves higher accuracy than unconstrained CoT temperature-sampling pass@1/2/3.Source: §C.4 · p. 20

C.5.1. GSM-SYMBOLIC GRAMMAR

  • The GSM-Symbolic grammar permits arithmetic expressions with addition, subtraction, multiplication, division, floor division, modulo, negation, int calls, numbers, and variables.Expressions may also be parenthesized.Source: §C.5.1 · p. 20

C.5.2. PROVER9 GRAMMAR

The supplied Prover9 grammar defines the structure of predicate, premise, and conclusion sections and the logical expressions they contain. The accompanying table captions identify comparisons on GSM-Symbolic and FOLIO.

C.5.2. PROVER9 GRAMMAR

  • The Prover9 grammar structures output into predicate, premise, and conclusion sections, with quantified expressions and logical connectives.It specifies predicate definitions, premises, conclusions, quantifiers, and connectives including iff, implies, xor, or, and, and not.Source: §C.5.2 · p. 21
  • Table 3 compares CRANE and baselines across models on GSM-Symbolic using accuracy, token count, and average time.Source: Table 3 · p. 22
  • Tables 4 and 5 compare CRANE with greedy and sampling baselines on GSM-Symbolic and FOLIO, respectively.Source: Table 4 · p. 23, Table 5 · p. 23

Related papers

Loading 2502.09061v4…