CRANE: Reasoning with constrained LLM generation
Authors: Debangshu Banerjee
Tarun Suresh
Shubham Ugare
Sasa Misailovic
Gagandeep Singh
Venue: ICML 2025 poster (2025)
Keywords: LLM reasoning
Constrained Decoding
Grammar Guided Generation.
Primary area: deep_learning->large_language_models
TL;DR: A constrained decoding algorithm that combines reasoning capabilities with structural correctness.

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.

CRANE:
Reasoning with constrained LLM generation
Debangshu Banerjee"
Tarun Suresh Shubham Ugare' Sasa Misailovic'
Gagandeep Singh'
Abstract
Jiang et al., 2024), logical solvers (Pan al., 2023; Olaus- son et al., 2023), and theorem provers (Wu et al., 2022; Yang et al., 2023). These tools impose specific syntactic and semantic constraints on their inputs, requiring LLMs to produce outputs in the correct format. For instance, if an LLM provides output to a specific logical solver (Han et al., 2024), the output must be parsable by that solver. Similarly, Wolfram Alpha (wolfram, 2024) translates user queries about mathematical problems into domain-specific language (DSL) to utilize symbolic solvers. However, as highlighted in recent studies ( (Ugare et al., 2024b; Lundberg et al., 2023; Poesia et al., 2022), pre-trained L.M outputs do not always comply with downstream tools' input re- quirements. Constrained decoding algorithms (Ugare et al., 2024b; Poesia et al., 2022) address this issue by project- ing the LLM output onto user-specified formal constraints (e.g., syntactic rules defined by context-free grammar G),, thereby ensuring that the input requirements of downstream tasks are satisfied.
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 direc- tion to enforce adherence to formal grammar, but prior works have empirically observed that strict enforcement of formal constraints often dimin- ishes the reasoning capabilities of LLMs. In this work, we first provide 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 augment- ing the output grammar with carefully designed additional rules, is always possible to preserve the reasoning capabilities of the LLM while en- suring syntactic and semantic correctness in its outputs. Building on these theoretical insights, constrained
As illustrated in Fig. 1, constrained decoding improves the syntactic correctness of L.M outputs (e.g., generating a well-formed mathematical expression). However, does not guarantee functional correctness (e.g., ensuring the ex- pression correctly answers the user's query). Recent works such as Tam et al. (2024) have empirically observed that imposing constraints on LLM outputs can, in some cases, reduce functional correctness for specific tasks. Tam et al. (2024) attributes this reduction in functional accuracy to decline in the LLM's reasoning capabilities under con- strained decoding. This observation raises the following open questions:
we propose a decoding algorithm, CRANE, which effectively balances the correctness of constrained generation with the flexibility of unconstrained generation. Experiments multiple open-source LLMs and benchmarks show that CRANE significantly out- performs both state-of-the-ar constrained decod- ing strategies and standard unconstrained decod- ing, showing up to 10% points accuracy improve- ment over baselines on challenging symbolic rea- soning benchmarks GSM-symbolic and FOLIO.
RQ1: Do LLMs truly lose reasoning capabilities under constrained decoding?
1. Introduction
RQ2: How can we leverage the benefits of constrained decoding in reducing syntax errors while preserving the unconstrained reasoning capabilities of LLMs?
Transformer-basee based large language models (LLMs) are widely used in AI systems that interact with traditional soft- ware tools like Python interpreters (OpenAI, 2024; Chen et al., 2023) for code generation (Suresh et al., 2024a;b;
First, we need formally identify the root cause of the reduction in functional accuracy of end- to-end systems when a pre-trained LLM operates under constrained generation. Unlike the empirical observations in (Tam et al., 2024), we seek a formal justification for this reduction that is not limited to specific LLMs used in experiments but extends to any LLM,, including more
Key Challenges:
Equua contribution 'Department of Computer Science, Uni- versity Illinois Urbana-Champar Champaign, USA. Correspondence to: Debangshu Banerjee <db21 @illinois.edu>.
Proceedings of the ndnd International Conference Machine Learning, Vancouver, Canada. PMLR 267, 2025. Copyright 2025 by the author(s).

---

CRANE: Reasoning with constrained LLM generation
Question: [name] hires [vehicle] from (start hour (end hour]. He gets ffree_hours] hours free. The first pald hour Is Sjfirst hour cost) and each hour after that (multiplier] cost. How much did he pay?
Unconstrained with CoT: "Reasoning Text... The final answer <<first hour_ _ost__ostt (int((end_hon ficlend__our-- hour start hour hotal seconds(] / 3600) free hours 1)
* multiplier first_hour htt_hhouur_st>t... cost>>..
Syntax error
Constrained: <<(int(end_ _hour- -tart_hhool sourt_hoor-- free_hours) fors__hurr_ae cost + free free_hours first_hour_ee (int(end_houee hour start_hour) free_hours 1)* multiplier* first_ fet_hhorr_cstt>>
CRANE:
"Reasoning Text ..." The final answer is
cest_hour_costt
<<first_ Barrs_hou_____ _osstcosst_______ + (int(end_ cont@ed_houur-a start_hour free_hours 1) multiplier first_hour_comm cost>>.
Functionally incorrect
Syntactically and Functionally Correct
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 correct answer.
powerful ones developed in the future.
eration for producing structurally correct outputs. This allows the model to produce syntactically valid outputs while enabling the LLM to reason. Our detailed exper- iments on multiple open-source L.LMs and benchmarks demonstrate that CRANE significantly outperforms both SOTA constrained decoding strategies and standard un- constrained decoding, showing up to 10% improvement over baselines on challenging symbolic reasoning bench- marks GSM-symbolic (Mirzadeh et al., 2024)) and FO- LIO (Han et al., 2024).
Second, we must design cost-efficient decoding strategies that address the shortcomings of existing constrained decod- ing methods while improving functional accuracy. In this work, we do not consider task-specific fine-tuning of LLMs, as fine-tuning for each task is compute-intensivee Unlike constrained decoding, fine-tuning does not guarantee that the LLM output adheres to formal constraints.
Contributions: We make the following contributions to improve the functional accuracy of the end-to-end system:
Next, we provide the notations and necessary background constrained decoding, including the definition of Turing machines and relevant circuit complexity classes.
We theoretically show that LLMs with a constant number of layers, which are known be capable of simulating n steps of any given Turing machine M with (n) rea- soning steps (Merrill & Sabharwal, 2024), can only solve problems within relatively restrictive circuit complexity class when constrained to generate outputs that always conform to restrictive grammar G defining only the valid output strings. This demonstrates that, for restrictive gram- mar, constrained decoding reduces the problem-solving capabilities of LLMs.
2. Preliminaries
Notations:
In the rest of the paper, we use small case letters (x) for constants, bold small case letters (x) for strings, capital letters X for functions, for string concatenation, |ar] to denote the length of the string æ. We use I.I.M to refer to transformer-basee LLMs with a fixed number of layers.
We theoretically show that the loss of expressivity of LLMs under constrained decoding arises because the out- put grammar G is too restrictive to accommodate the inter- mediate reasoning steps required to compute the answer. We further demonstrate that augmenting the grammar G with specific additional production rules enables the LLM generate the intermediate reasoning steps while ensur- ing that the final output always adheres the intended output structure. With the augmented grammar Ga, the LLM retains its expressivity under constrained decoding.
2.1. Constrained LLM Decoding
Autoregressive language models L decode output iteratively by generating tokens from probability distribution over the vocabulary V. The distribution derived by applying the softmax function to the model's scores S. Common decoding methods include greedy decoding, temperature sampling, and beam search. Constrained LLM decoding extends this process by excluding specific tokens at certain positions, such as avoiding harmful words or adhering to user-defined output grammar for languages like JSON or SQL (Poesia et al., 2022; Ugare et al., 2024c; Willard & Louf, 2023). At each decoding step, a binary mask m e (0, (0,1) generated by function fm. specifies valid tokens
We propose a simple and cost-efficient decoding strat- egy. CRANE (Constrained Reasoning Augmented Generation). CRANE effectively alternates between un- constrained generation for reasoning and constrained gen-
2

---

CRANE: Reasoning with constrained LLM generation
(m, 1) and excluded tokens (m; 0). Decoding is then performed the masked probability distribution O softmax(S), where C denotes element-wise multiplication.
models used to analyze resource requirements (e.g. time and space complexity) and the hardness of computation problems. Formally, Turing machine is defined as: Definition 2.4 (Turing Machine). A Turing machine M with k work tapes and an output tape is a 8-tuple
2.2. Deterministic LLM Decoding
CRANE is compatible with various decoding strategies, both constrained and unconstrained, allowing the output of L to be stochastic. However, following existing works (Hahn, 2020; Merrill & Sabharwal, 2023; Li et al., 2024) and for simplicity in the theoretical setup in Section 3, we assume that the output of L on any input string x is deter- ministic in both constrained and unconstrained settings.
M K, b, Q qu: F,
where Σ is the finite input alphabet, I' is the finite tape 1 E is a special blank symbol, alphabet with Σ _ r, E T
Q is a finite set of states, qo Q is the initial state, ó (Q \ F) x pk+2 + Q P x (0,+1, 11,++111k+ -1)*-2 is the transition function (where - 1, 0 represent moving the tape head left, right, or staying in place, respectively), and F C Q is the set of halting states.
Similar to prior works (Merrill & Sabharwal, 2023; 2024), we model single autoregressive step as a deterministic function Cy that predicts the next token given a specific input. Formally,
Let Σn denote the set of all finite strings over the input alphabet E. Given an input string s E Σ", the computation of Mon is a sequence of configurations starting from the initial configuration. Each configuration 7y is a tuple containing the current state q E Q, the contents of the input tape, the k work tapes, the output tape, and the current head positions of all k + 2 tapes. For each configuration, " (i E N), the transition function ó computes the next configuration 7h+1 based on the current state q and the values on the k + 2 tapes at the current head positions. It updates the head positions, writes the output tape (possibly leaving it unchanged if no new symbol is written), and advances to the next configuration. For each i, computation of 7++1 from 7.2 defines a single step of the Turing machine.
Definition 2.1 (Deterministic LLM Step). A single autore- gressive step of an LLM is modeled as a deterministic func- tion Cy: : V* - V. where V the finite vocabulary and V* represents the set of all finite strings over V. For an input string 2 V*, the LLM predicts the next token (x)).
Definition 2.2 (Deterministic Unconstrained Decoding). For an input string x, the deterministic output string y selected from the output distribution of a LLM using decoding algorithm (e.g., greedy decoding) is denoted as [(x) where L V - V*. L(x) is the most likely output sequence according to learned distribution on æ.
The output y = L(x) is computed iteratively with ly/ au- toregressive steps defined by Ly. For each 1 Sis S
The computation of M on input s halts if M reaches a halting state g E F. If M halts, the output corresponding to is written on the output tape. Additional details about the computation of the Turing machine are in Appendix A.
ly), and the recurrence relation 2/ (x) L (i- 1) (x) (x) (C) (z))
(1))
where _ (x)) x and denotes string concatenation. Here, x.y- = -- (x)) Similarly, under constrained decoding with grammar G we define:
Before discussing existing expressivity results for constant- layer LLMs, we briefly introduce relevant uniform constant- depth circuit complexity classes, e.g. logspace uniform- TC which provide an upper bound on the computational power of LLMS that do not employ reasoning steps, as seen in methods like Chain-of-Thought (Wei et al., 2022).
Definition 2.3 (Deterministic Constrained Decoding un- der Grammar). Under constrained decoding with formal grammar G, the output string yG is selected from the con- strained output distribution and is denoted as yc = Lx)).. The output of i-th constrained autoregressive step with G is (i) (1) Vg f (z) and yG (1yl)) (z).
Definition 2.5 (Boolean Circuit). A Boolean circuit is computational model for evaluating Boolean functions over fixed-length binary strings. It is represented as a directed acyclic graph (DAG), where the leaf nodes correspond to input binary variables or their negations, and the internal nodes perform operations from a predefined set of opera- tions B (e.g., AND (A), OR (V), etc.). One more marked nodes in the graph represent the circuit's 's output.
The constrained output ye is always in the grammar ye E (G) where T.G) is the language defined by G. For sound- constrained decoding algorithms,, if the unconstrained out- put = ((x) in the grammar y E L(G,, the constrained output remains unchanged, i.c., L(x) = Lx(x).
The structure of the DAG specifies the computation of the Boolean function by propagating input values through the graph. The complexity of a circuit is determined by its size (the number of nodes) and depth (the longest path in the graph). Since a single circuit only defines a boolean
2.3. LLM Expressivity
We discuss the notations and background related to Turing machines, and relevant uniform circuit complexity classes. Turing machines are popular mathematical computation
3

---

CRANE: Reasoning with constrained LLM generation
function for fixed-length inputs, family of circuits is re- quired-one for each input length-to characterize com- putational problem where input lengths vary. Unlike Turing machines, whose computation does not depend on input length, circuit families have a separate circuit for each input length, which can differ entirely. This non-unifommity can lead to degenerate cases where non-uniform circuit fam- ilies solve undecidable problems (Arora & Barak, 2009). To address this issue, complexity theorists enforce unifor- mity conditions, requiring circuits for different input sizes to be related, resulting in uniform circuit families. For further details and formal definitions of circuit classes, re- fer to (Arora& & Barak, 2009). In this work, we focus on constant-depth, polynomial-sized logspace-uniform thresh- old eircuits (TCC),, where B contains only threshold gates formal definition is in Appendix B).
LLM with constant number of layers on an input of length n. can be simulated by logspace-uniform conttant-depth threshold circuit family. This result allows the LLM to use floating- poaaingg-pintttii numbers with log(n) precision when process- ing inputs of size n, ensuring that the precision scales with n and preventing floating-port representation issues for large n. We denote such LLMs as log-precision LLMs.
Let t0 denote the output after the i-th autoregressive step of an LLM L under constrained decoding with output grammar G on input x. Then, we have x y = _/0 (z), and for any i, y is always a valid prefix of string in L(G), i.e. there exists a (possibly empty) string at)) such that y (a E L(G). Now, for any output grammar Ge where the output set O = L(G²) is finite, we show that the output La. (I) for any input z of size |x| - n can be computed using constant-depth threshold circuits.
3. Expressivity of Constrained Decoding
Proposition 3.1. For any oe-preciison LLM L with con- stant layers there exists a logspace-uniforn thershold circuit T Th, such that LG. (x) Th,(w) (x) holds for all inputs I with size |z| and E N.
First, we show that any constant-layer layer LLM L under con- strained decoding loses expressivity. We identify the class of problems and the corresponding output grammars G such that when imposed on the outputs of any constant-layer LLM, the problems cannot be solved unless there is a col- lapse in fundamental complexity classes that are widely believed to be unequal (e.g.. TC" 7 NL).
Proof: The formal proof is in Appendix C.
From Proposition 3.1, it follows that for any decision prob- lem under constrained decoding, an LLM can only solve problems within the logspace-uniform TC" class (constant- depth threshold circuits). Consequently, any decision prob- lem believed to lie outside this class cannot be solved un- der constrained decoding. The previously mentioned st- connectivity problem is known to be NL-complete (Arora & Barak, 2009). This implies that unless TC" = NL, no LLM under constrained decoding can solve st-connectivity. Additionally, (Li et al., 2024; Merrill & Sabharwal, 2024) show that given any Turing machine M there exists a log- precision LLM with a constant number of layers that can simulate (t())) steps of M using (t(nn) autoregressive steps, where t(n) denotes polynomial in the input size n.
3.1. Limitation of Constrained Decoding
Next, we present the high-level idea behind Proposition 3.1 that shows the limitation of constrained LLM decoding when the output grammar is too restrictive. We consider problems where the number of possible outputs is finite, and thus the set of all possible outputs O can be expressed as a simple regular language. Consequently, Ge that encodes the output set O, i.e., O = L(G., where L(G2) denotes the language defined by the grammar G.. For instance, any decision problem (yes/no answer) such as st-comnectivity that asks for vertices and in directed graph, if is reach- able from can be answered within single-bit output i.e. T(GG.) {0, 1}. This implies that constrained decoding with the output grammar Ge allows only a single autoregres- sive step for any L on all inputs.
Lemma 3.2. For any Turing machine M with tape alphabet r, there exists a constant depth LLM Lm with finite vocabu- lary I C VM and log pee-preission that can simulate t(m) steps of M with t(n) autoregressive steps.
series of existing works (Hahn, 2020; Hao et al., 2022; Merrill et al., 2022; Merrill & Sabharwal, 2023) establish that, under suitable assumptions, single autoregressive step on an input with length n for any constant-depth LLM can be represented as a constant-depth circuit. Since, for de- cision problems, the constrained decoding step permits only a single autoregressive step, any LLM can only solve prob- lems within the corresponding cireuit complexity class. We build on the most recent result from (Merrill & Sabharwal, 2023), which shows that a single autoregressive step of any
Proof: The proof follows from Theorem 2 in (Merrill & Sabharwal, 2024) further details in Appendix C.
Proposition 3.1 and Lemma 3.2 together imply that there ex- ist problems, such as st-connectivity, an LLM can solve that in an unconstrained setting but cannot be solved under con- strained decoding (unless logspace-unifee unifor TC = NL).
3.2. Reasoning with Augmented Grammar
The reduction in LLM expressivity under constrained de- coding, as established in Proposition 3.1, arises primarily because the language of all valid output strings, T.(2)),
'NL refers to nondeterministic log-space
4

---

CRANE: Reasoning with constrained LLM generation
is too restrictive and does not permit large (non-constant)
[0, 10,+1,11 denote either staying in place (0), moving left (-1), or moving right (+1) by a single position. Since the set of states Q. the tape alphabet I', and the number of tapes k are all constants, the total number of possible encodings is also constant. Let T denote the set of all possible configu- ration encodings, i.e., I = {Tm)..... Yuy J. where = -[]] Given I' is finite and enumerable, we can define the rules of the augmented grammar G. accordingly as follows.
reasoning chains. This naturally leads to the question of whether it is possible to augment any output grammar G with additional production rules to construct an augmented grammar G. that can accommodate reasoning steps while preserving the expressivity of L even under constrained decoding. At the same time, G, should remain nontriv- ml-aming it should not accept all possible strings, as in the unconstrained setting- -so that it aligns with the practi- cal objective of constrained decoding: guiding the LLM to generate syntactically and semantically valid outputs.
G. + RyG; Ra - SRari S - T()
7())
To achieve this, we enforce that the augmented grammar G. always follows the structure G2 + RG, where the nonterminal symbol R captures the reasoning steps, and G represents the final output. This guarantees that for any string E L(Ga), the final answer extracted from r always belongs to the original output grammar G, i.e., a E [(G), with r serving as the reasoning sequence leading up to the final output.
The set of reasoning strings in I. essentially define a regular language over the configuration encodings I. Let, for any input with size [x] a given Turing machine M halts and compute the output (xx) in t(n) steps that are polynomial in n. Then there exist La compute (x) with (n) autoregressive steps under constrined decoding with the augmented grammar G. - RM Suppose, LM,G. (z) denotes the output of the LLM Las on input x under con- strained decoding with grammar G2 then
Formally, we show that for any Turing machine M and a grammar G containing all valid outputs of M, there exists an LLM Lar with a constant number of layers and log- precision, along with an augmented grammar G. in the specified format, such that LM can simulate t(n) steps of M using (n) autoregressive steps under constrained decoding with G.. Here n E N and (nn) is a polynomial over n. The augmented grammar Go may not be unique, and we provide one such construction.
Proposition 3.3. For any Turing machine M with tape alphabet I, there exists constant depth LLM Las with finite vocabulary I C Vas and log precision such that for any input x with |x|| = LMM.G, (x) + M(x) with E VM assuming M halts on x in t(n) steps.
Proof: The proof is in Appendix C.
At high level, Las simulates the Turing machine M by computing the encoded representations T of the machine's 's configurations 7/2 at each step and storing them within the reasoning component (i.c., the string r) of the output. Dur- ing each autoregressive step, L generates the next configu- ration based on the transition function M and appends its encoding to the reasoning sequence. This process continues until Mf reaches a halting state, which point LM produces the final output a, which belongs to L(G). For any given M, we define the rules RM that can parse the encodings y of all possible configurations y. This ensures that the output La. (x:) represents the full
4. CRANE Algorithm
Given any Turing machine M, Proposition 3.3 establishes that constrained decoding with the augmented grammar G. a specific LLM LM simulate the computation of M. However, this result does not directly translate into a practical constrained decoding algorithm that preserves the expressivity of general L.LMs. The construction assumes a specific LLM LM with the vocabulary Var and knowl- edge of the particular Turing machine M for defining the rules Ry- In practice, we require an efficient approach that can be applied to diverse open-source LLMs, various grammars, and different constrained decoding algorithms. Importantly, we know that enforcing the output grammar G from the beginning can limit expressivity. Instead, we im- pose grammar constraints judiciously to avoid restricting the LLM's s reasoning capabilities. For example, in the case of a aassoning-augment output of the form लエ -.. -T(()) (xx, we apply constrained decoding only from the t(n) + 1-th autoregressive step onward, ensuring that the reasoning pro- cess remains unrestricted while the final answer adheres to the desired grammar.
augmenttd sequence, i... 71 ...... Te(m)) (xx,, where (zx is the final output of M on input æ of size n after 1(n) computational steps. The encodings TI...., Te(n)) correspond to the configurations "1...., (mm)). as described below.
We begin by defining the vocabulary Var for LM, which contains all tape symbols! 1' of M along with a finite set of auxiliary symbols y that encode the corresponding config- urations 7. Similar to prior works (Merrill & Sabharwal, 2024), each configuration encoding 7 represents the cur- rent state q, the symbols at the current head position of k ++2 2 tapes (input, output and & work tapes), and the head movement directions (0, +1, - for each tape. Directions
The primary challenge here is deciding when to transition between an unconstrained generation for reasoning and a
5

---

CRANE: Reasoning with constrained LLM generation
constrained generation. For instance, grammar for general- purpose programming languages such as Python can allow any text string at the start (e.g. program starting variable names) making it hard to detect the end of reasoning string. To avoid this, we augment the output grammar with specific delimiter symbols S1 and S2 that mark the start and end of the constrained generation. We incentivize the LLM to generate these delimiters via explicit instructions in the prompt and few-shot examples. This aligns with common penerol-purpose LLMs that already use specific delimiters such as backticks
Algorithm 1 CRANE Algorithm
1: Input: LLM, tokens, CSD (constrained decoder), G (output grammar), S1 (start delimiter), Sz (end delim- iter)
2: Output: Output string
3: G' + S,GS,
CSD.NIITIALIZE(())
pointer (enkesk)
6: isConst ned <- False
7: while True do
for programs like python, SQI., and (<<, >>) to enclose math-expression blocks. This approach allows a simple and cost-efficient approach for detecting the transitions to and from constrained decoding. For the construction in the previous section, in this setup, we will generate the string S1 .M (x) -S where the reasoning is generated unconstrained and the LLM moves constrained
8: currGen + (etookeniiieaakem/pooineer :I)
9: if Si E currGen then
10:
isConstrained + True
11: else
isConstzained +- False 13: if i isConstrained then
12:
14:
constrained <- extactConntaaine(((urreee
mode after seeing the symbol Si. However, in practical
15:
4~ ((oeen)t @ CSD(conStrained)
cases, the delimiters may be generated multiple times (ie. for intermediate operations), even during the reasoning step.
16:
else
17:
t, ~ (tokens)
Therefore, upon encountering the end symbol S2, we switch back to unconstrained generation avoid unnecessarily restricting the output.
18: tokens <- tokens + 4
19: if t, BOS then
20: break
21: if isConstrained then
22: constrained + constrained + detokenizze(t) if conntrainee..edsswit( then pointer + (token)))))
This can be represented as <<n1 mult n1 + (total n1 mult n1)>>. Simplifying this expression, we get <<total - n1 (1 + mult)>>, The number of (color3) {obi}s is the total number of (obi]s minus the number of (colort) and (color2) (obils, which is <<total
23:
24:
25:
return (etokennize(okknn))
Current Constrained Window
If S] is not present, the next token is computed directly without any constraints applied. Additionally, if the current constrained window ends with S2, the pointer is updated the length of the current token sequence, effectively switch- ing back to unconstrained generation until S is generated again. Figure 2 further illustrates LLM generation with CRANE. The underlined portion of the LLM generation represents currGen, and the current constrained window is highlighted in yellow.
Figure 2. CRANE adaptively switches hetween constrained L.M generation and unconstrained L.M 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.
We implement our approach into the CRANE algorithm (Algo 1), which extends standard autoregressive LLM gen- eration. CRANE takes arbitrary I.LM, constrained de- coding algorithm (denoted as CSD), output grammar G, and symbols S, and S2 as input. It first initializes CSD with G", the output grammar augmented with S₁ and Sg. CRANE starts unconstrained generation and maintains a pointer that marks the start of the current window of LLM gen- eration following the last constrained generation. In each iteration, the algorithm checks if S present the current generation window currGen, which is the portion of the sequence from the current pointer position onwards. If S is detected, CRANE switches to constrained generation mode. In this mode, the current constrained window (the portion of currGen that is in G') is extracted, and the next token sampled based on the constraints defined by the CSD.
5. Evaluation
In this section, we evaluate CRANE on a math reasoning task (GSM-Symbolic (Mirzadeh et al., 2024)) and a logical reasoning task (FOLIO (Han et al., 2024)) and demonstrate significant improvement over both unconstrained and SOTA constrained generation baselines.
Experimental Setup. We run experiments 48-core Intel Xeon Silver 4214R CPU with 2 NVidia RTX A5000 GPUs, CRANE is implemented using PyTorch (Paszke et al., 2019) and the HuggingFace transformers library (Wolf et al., 2020). Our primary baseline for unconstrained gen- eration is Chain-of of-Thoughtt (CoT) Prompting (Wei et al.,
6

---

CRANE: Reasoning with constrained LLM generation
2022), which enables LLMs to decompose and reason about problem through series of intermediate steps before out- putting the final answer. Furthermore, we run constrained semantic generation for GSM-Symbolic (Mirzadeh et al.,
Accuracy (%6 an G5M-Symbolic c Dwwnn?.5 -a-----------srrettt
35
Constrated
CVUE
Accuracy 19
25
2024) with the ITERGEN library (Ugare et al., 2024a) and use the SYNCODE framework for FOLIO (Han et al., 2024) evaluation. In all experiments, CRANE initialized with the same constrained decoders and uses the same constraints as the constrained generation baselines.
20
10
5
GSM-Symbolic: We first evaluate CRANE on GSM- Symbolic (Mirzadeh et al., 2024), a dataset consisting of math word problems designed to assess LLMs' mathemati- cal reasoning skills. In the word problems, names and nu- merical values are replaced with symbolic variables, and the LLMs are tasked with generating correct symbolic expres- sion solutions (see Appendix D.1 for examples). To evaluate correctness, we extract the final expressions from the LLM generations and verify if they are functionally equivalent to the ground truth expressions with the Z3 solver (De Moura & Bjørner, 2008).
Number of few Shots (k)
Figure 3. Accuracy (%) of Wrren..5-Mat-7B--nnsiii By Method and Number of Shots on GSM-Symbon
As shown in the table, CRANE consistently improves func- tional correctness across all evaluated models. For exam- ple, with the -wwe2.5-Maah-7BB-- Bith--BB-Instruc model, CRANE achieves 38% accuracy, outperforming both constrained generation and unconstrained generation with CoT, which achieves 29% accuracy. Moreover, CRANE significantly enhances the syntactic correctness of generated expressions compared to unconstrained generation. Notably, none of the expressions generated using CRANE contain syntax errors, whereas 10% of the expressions from unconstrained generation with CoT do. Although, for several instances, CRANE produces slightly more syntax errors than a purely constrained generation, it offers substantial improvement in functional correctness over this baseline.
We compare CRANE against three baselines: (1) uncon- strained generation without chain-of-thought prompting, (2) unconstrained generation with CoT, and (3) constrained gen- eration. We use ITERGEN for the constrained generation baseline and also initialize CRANE with ITERGEN. For ITERGEN and CRANE, we enforce syntactic constraints via the context- free grammar provided in Appendix D.5.1 and apply the semantic constraint ensuring that generated expressions contain only valid problem -eelined variables. Since IEERGEN uses selective rejection sampling enforce semantic constraints, we also include comparisong against unconstrained generation with sampling in Table 4 in the Appendix. For CRANE, we use << and >> for the delime- ters S1 and S2, respectively. We evaluate Qwen2.5-1.5B: Instruct (Qwen, 2024), Qwen2.55-Math-7B-nntt 2024), Qwen2.5-Coder Bonder-7B-Instieee In-strruct (Qwen, 202ma, 3.1-8B-Instru (Llama, 2024), DeepSeet-RI--Disill-ONee 7B (DeepSeek-AI et al., 2025). DeepSeck-RI-Distill Llama-8B (DeepSeek-AI et al., 2025), Qwen2.5-Coder- 14B-Instruct (Qwen, 2024),
Ablation Study on Few-shot examples: We evaluate CRANE and baselines on varying numbers of few-shot examples in the prompt and display the results for Qwen2.5- Math-7B-Instruce in Figure 3. Results for all models presented in Table 3 in the Appendix. CRANE consis- tently achieves higher accuracy on GSM-Symbolic than the baselines for all evaluated numbers of few-shot examples.
(Qwen,
FOLIO:
We further evaluate CRANE on the validation split of FOLIO dataset, which comprises 203 expert- written natural language reasoning instances and corresponding first-order logic (FOL) annotations. We evaluate the ability of LLMs correctly translate the natural language reason- ing instances into FOL formulas and leverage Prover9 (Mc- Cune, 2005-2010) a FOL solver to verify the correctness of the LLM-generated FOL formulas.
14B (DeepSeek-AL et al., 2025), and QwQ-32B (Team, 2025). We use greedy decoding with a maximum new token limit of 600 and prompt the LLMs with the 8-shot examples from GSM-Symbolic (Mirzadeh al., 2024) (the prompts can be found in Appendix D.I).
Table compares the performance of CRANE with the baseline methods. The Accuracy (%) column reports the percentage of functionally correct --g-errerrtted expres- sions, Parse (%) indicates the percentage of syntactically valid expressions (i.e., expressions without invalid opera- tions), and Tokens provides the average number of tokens generated.
We compare CRANE against crammar-constriine genera- tion with SYNCODE using the Prover9 grammar (Appendix D.5.2). The Prover9 grammar divides FOL formulas into Predicates, Premises, and Conclusions and allows interme- diate reasoning in comments (an example can be found in Appendix D.2). We also compare CRANE against un- constrained generation with COT. For all approaches and models, we run greedy decoding with maximum new to-
7

---

CRANE: Reasoning with constrained LLM generation
kens limit of 800 and use 2 few-shot examples in the prompt. We also compare CRANE against unconstrained CoT with temperature sampling in Table 5 in the Appendix.
ing the LLM's expressivity by reasoning chains.
LLM Expressivity: (Strobl et al., 2024) provides a detailed survey of existing results from the perspective of formal language theory and complexity classes. A series of existing works (Hahn, 2020; Hao et al., 2022; Merrill et al., 2022; Merrill & Sabharwal, 2023) establish that, under suitable assumptions, a single autoregressive step on an imput of any length for constant-depth LLM can be represented as constant-depth Boolean circuit. (Merrill & Sabharwal, 2024; Li et al., 2024) show that the expressivity of LLMs significantly improves under popular reasoning approaches like Chain of Thought (Co'T) (Wei et al., 2022), where LLMs take intermediate steps before generating the final answer. To the best of our knowledge, there is no prior work on LLM expressivity under grammar constraints.
Appendix table 2 presents the results of our experiment. The Accuracy (%) column in the table reports the percentage of functionally correct FOL translations while the Compiles (%) column reports the percentage of FOL formulas ex- tracted from LLM output that are syntactically valid and compile into a Prover9 program. CRANE outperforms the unconstrained and constrained generation baselines for all models evaluated.
Limitation: Our work has the following limitations. First, Proposition 3.1 only demonstrates a reduction expressiv- ity when the language L(G2) is finite. This leaves open the question of whether Proposition 3.1 can be extended to grammars G where L(G) is infinite. Second, CRANE for constrained decoding relies on existing tools (Ugare et al., 2024b) that require access to output logits, rendering CRANE inapplicable to models that do not expose logits.
7. Conclusion
In conclusion, tasks requiring both syntactic and seman- tic correctness, such as code generation and symbolic math reasoning, benefit significantly from constrained de- coding strategies. However, strict enforcement of con- straints can hinder LLM reasoning capabilities. Theoret- ically, we demonstrate why restrictive grammars dimin- ish reasoning and show that augmenting grammars with carefully designed rules preserves reasoning while main- taining conrectness. Building on these insights, our pro- posed reasoning-angmented constrained decoding algo- rithm, CRANE, achieves state-of-the-art performance, with up to 10% improvement on symbolic reasoning benchmarks such as GSM-symbolic and FOLIO, effectively balancing the strengths of constrained and unconstrained generation.
6. Related Works
Constrained LLM Decoding: Recent works have intro- duced techniques to enforce LLM generations to adhere to context-free grammar using constrained decoding (Ugare et al., 2024c; Willard & Louf, 2023; Seurer-Kellnee al., 2024; Melcer et al., 2024a). Additionally, Poesia et al. (2022); Ugare et al. (2024a) have extended grammar- chaamar-guided generation to incorporate task-specific semantic constraints. These approaches demonstrate that constrained decoding can improve the syntactic and semantic quality of LLM outputs for various structured generation tasks.
More recently, Tam et al. (2024) demonstrated that con- strained structured generation can negatively impact the quality of generated outputs. Similarly, Park et al. (2024) showed that greedily masking out tokens that do not lead to a valid string during next-token prediction can distort the output distribution, causing it to deviate from the true distri- bution of all grammatically valid outputs of C for given input. To mitigate the distortion introduced by the greedy masking approach, these "grammar aligned" methods (Park et al., 2024; Melcer et al., 2024b) use a tric to track previ- ous generations, reducing generation divergence iteratively. However, they are computationally expensive and require a large no. of resamplings per prompt to converge.
In contrast, our work focuses on the fundamental question of the theoretical expressivity of any constant layered con- strained I.I.M, even under an ideal constrained decoding algorithm, and uses the insights to propose a practical so- lution. We propose an adaptive constrained decoding ap- proach that can support various constrained decoding meth- ods, including grammar-aligned techniques while presery-
8

---

CRANE: Reasoning with constrained LLM generation
Table I. Comparison of CRANE and baselines with different models GSM-Symholic.
Model
Method
Acc. (%)
Parse (%)
Tokens
Unconstrained w/o CoT
21
97
23.34
Constrained
22
97
25.29
Qwen2.5-1.5B-Instne
Unconstrained CoT
26
90
128.97
CRANE
31
100
131.3
Unconstrained w/o CoT
94
17.92
Constrained
35
99
25.28
Owen2.5-Coder::7B-mme
Unconstrained CoTT
37
88
138.38
CRANE
39
94
155.32
Unconstrained w/o CoT
27
89
25.7
Constrained
29
99
26.81
Bren2.5-Math-BB-Insse
Unconstrained CoT
29
82
155.26
CRANE
38
94
158.86
Unconstrained w/o CoT
21
73
128.38
Constrained
26
98
35.97
Unconstrained CoT
30
95
163.55
CRANE
33
95
170.22
Unconstrained w/o CoTT
18
89
21.64
Constrained
20
99
17.21
DeepSeek-Ro PoepSeck-RI-iisee Distill-Qwenn
Unconstrained CoT
24
89
212.24
CRANE
29
92
235.78
Unconstrained w/o CoT
12
77
29.2
Constrained
96
16.89
Unconstrained CoT
21
250.83
CRANE
31
92
268.82
Unconstrained w/o CoT
42
93
18.52
Constrained
42
96
25.62
Qwen2.5-Coder- 14B-Instrude
Unconstrained CoT CRANE
42
95
157.71
45
95
158.54
Unconstrained w/o CoT
29
82
20.9
Constrained
30
91
30.48
DeepSeek-RR--isstill- -I-ii-till--ieeennnn 14B
Unconstrained CoT CRANE
32
87
233.42
93
244.98
Unconstrained w/o CoT
37
80
54.93
Constrained
38
91
34.2
QwQ-32B
Unconstrained CoT
43
87
222.62
CRANE
46
88
237.98

---

CRANE: Reasoning with constrained LLM generation
Impact Statement
Zhang, Y., Shi, Y., Xiong, Y., He, Y., Piao, Y., Wang, Y., Tan, Y., Ma, Y., Liu, Y., Guo, Y., Ou, Y., Wang, Y., Gong, Y., Zou, Y., He, Y., Xiong, Y., Luo, Y., You, Y., Liu, Y., Zhou, Y., Zhu, Y. X., Xu, Y., Huang, Y., Li, Y., Zheng, Y. Zhu, Y., Ma, Y., Tang, Y., Zha, Y., Yan, Y., Ren, Z. 7 Ren, Z., Sha, Z., Fu, Z., Xu, Z., Xie, Z., Zhang, Z., Hao, Z., Ma, Z., Yan, Z., Wu, Z., Gu, Z., Zhu, Z., Liu, Z., Li, Z. Xie, Z., Song. Z.. Pan, Z., Huang, Z., Xu, Z., Zhang, Z., and Zhang, Z. Deepseek-rl: Incentivizing reasoning capability in ilms via reinforcement learning, 2025. URL https: https://arxinn wwwpxii.rrggbb////oee
This paper introduces research aimed at advancing the field of Machine Learning. We do not identify any specific so- cictal consequences of our work that need to be explicitly emphasized here.
References
Arora, S. and Barak, B. Computational Complexity; A Modern Approach. Cambridge University Press, USA, 1st edition, 2009. ISBN 0521424267.
12948.
Hahn, M. Theoretical limitations of self-attention in neural sequence models. Transactions of the Association for Computational Linguistics, 8:156-171, 2020. doi: 10. 1162/tacl a 00306. URL. org org/ 2ttp/2220.ccccc1m
Beurer- Kellner I.., Fischer, M., and Vechev, M. Guiding Ilms the right way: Fast, non-invasive constrained gener- ation, 2024.
Chen, W. Ma, X., Wang, X., and Cohen, W. W. Pro- gram of thoughts prompting: Disentangling computation from reasoning for numerical reasoning tasks. Transac- tions on Machine Learning Research, 2023. ISSN 2835- 8856. URL https: http//ppeerevveeeeee net/ forum? id=Yf24ZPtåzd,
Han, S., Schoelkopf, H., Zhao, Y., Qi. Z., Riddell, M., Zhou, W., Coady, J., Peng. D., Qiao. Y., Benson, L.,, Sun, L., Wardle-Solano, A., Szabo, H., Zubova, E.,, Burtell, M., Fan, J., Liu, Y., Wong, B., Sailor, M., Ni, A., Nan, L., Kasai, J. Yu, T., Zhang, R., Fabbri, A. R., Kryscinski, W., Yavuz, S., Liu, Y., Lin, X. V., Joty, S., Zhou, Y., Xiong, C., Ying, R., Cohan, A., and Radev, D. Folio: Natural language reasoning with first-order logic, 2024. URL /ttps://arxiie org/ abs/ 22t.//222..00 00840.
De Moura, L. and Bjorner, N. Z3: an efficient smn solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, AACAS'OS/ETAPS pp. 337-340, Berlin, Heidelberg, 2008. Springer-Verlee ISBN 3540787992.
Hao, Y., Angluin, D., and Frank, R. Formal language recognition by hard attention transformers: Perspectives from circuit complexity. Transactions of the Associa- tion for Computational Linguistics, 10:800-810, 07 2022. ISSN 2307-387X. doi: 10. 10.1162/aac URL 100 11 http://1..1122/tacl..e. 00490.
DeepSeek-AI, Guo, D., Yang, D., Zhang, H., Song, J., Zhang, R., Xu, R., Zhu, Q.. Ma, S., Wang, P., Bi. X., Zhang, X., Yu, X., Wu, Y., Wu, Z. F., Gou, Z., Shao, Z., Li, Z., Gao, Z., Liu, A., Xue, B., Wang, B., Wu, B., Feng, B., Lu, C., Zhao, C., Deng, C., Zhang, C., Ruan,
C., Dai, D.. Chen, D., Ji, D., Li, E., Lin, F., Dai, F., Luo, F., Hao, G., Chen, G., Li, G., Zhang. H., Bao, H., Xu, H., Wang, H., Ding, H., Xin, H., Gao, H., Qu, H., Li, H., Guo, J., Li, J., Wang. J., Chen, J., Yuan, J., Qiu, J., Li, J., Cai, J. L., Ni, J., Liang, J., Chen, J., Dong, K., Hu, K., Gao, K., Guan, K., Huang, K., Yu, K., Wang, L., Zhang, I.., Zhao, I., Wang, I., Zhang, I.., Xu, I., Xia, L., Zhang, M.. Zhang, M., Tang, M.. Li, M., Wang. M., Li, M., Tian, N., Huang, P., Zhang, P., Wang, Q., Chen, Q., Du, Q., Ge, R., Zhang. R., Pan, R., Wang. R., Chen, R. J. Jin, R. L., Chen, R., Lu, S., Zhou, S., Chen, S. Ye, S., Wang, S., Yu, S., Zhou, S., Pan, S., Li, S. S., Zhou, S., Wu, S. Ye. S., Yun, T., Pei, T.. Sun, T., Wang, T., Zeng, W., Zhao, W., Liu, W., Liang, W. Gao, W. Yu, W. Zhang, W. Xiao, W. L., An, W., Liu, X., Wang, X., Chen, X. Nie, X., Cheng, X., Liu, X., Xie, X., Liu, x., Yang, X. X., Su, X., Lin, X., Li, X. Q. Jin, X., Shen, X., Chen, X., Sun, X., Wang. X., Song, X., Zhou, X., Wang, X., Shan, X., Li, Y. K., Wang. Y. Q., Wei, Y. X., Zhang, Y., Xu, Y. Li, Y., Zhao, Y., Sun, Y., Wang, Y., Yu, Y.,
Jiang, J.. Wang. F., Shen, J., Kim, S., and Kim, S. A survey large language models for code generation, 2024. URL https: / /arxivvvvvvv////a///a///aaaav/// www//oog//aa...ooooo 2406 00515.
Li, Z., Liu, H., Zhou, D., and Ma. T. Chain of thought em- powers transformers to solve inherently serial problems. In The Twelfth International Conference on Learning Representations, 2024. URL 3wwhttdddddddddyee
Llama. The llama herd of models, 2024. URL https: //arxiv.org/ orgg 2407 21783.
Lundberg, S., Ribeiro, M. T. A. p., and et. al. Guidance- ai/guidance: A guidance language for controlling large language models., 2023. URI. https://githon
com/ ht///uudaance aaance-ai/geee aiuiiid
McCune, W http: kttp://www. /ttp://wwww.oooo cs unm. htt////cccccc/ceeeeeeee 2005-2010.
Prover9 and mace4.
10

---

CRANE: Reasoning with constrained LLM generation
Melcer, D., Fulton, N., Gouda, S. K., and Qian, H. Con- strained decoding for fill-intthe-middee code language models via efficient left and right quotienting of context- sensitive grammars, 2024a. URL https: arxiv. org/abs/ 2ttp/bbb/4422.1102 2402.
Paszke, A., Gross, S., Massa, F., Lerer, A., Bradbury, J., Chanan, G., Killeen, T., Lin, Z.., Gimelshein, N., Antiga, L., Desmaison, A., Kopf, A., Yang, E., DeVito, Z., Raison, M., Tejani, A., Chilamkurthy, S., Steiner, B., Fang, L., Bai, J., and Chintala, S. Pytorch: An imperative style, Segh-performance deep learning library. In Advances in Neural Information Processing Systems 32, pp. 8024- 8035. Curran Associates, Inc., 2019.
Melcer, D., Gonugondla, S.. Perera, P., Qian, H., Chiang, W.-H., Wang, Y., N., Garg. P., Ma, X., and Deoras, A. Approximately aligned decoding, 2024b. URL https:
// //arxiv.com orgg abs/244 011.0.... 0. 01103.
Poesia, G., Polozov, A., Le, V., Tiwari, A., Soares, G., Meek, C., and Gulwani, S. Synchromesh: Reliable code generation from pre-trained language models. In International Conference on Learning Representations, 2022. URL https: /openreviwww net/ formm? id id-KmtVD97J43e
Merrill, W. and Sabharwal, The parallelism tradeoff: Limitations of log-precision transformers. Transactions of the Association for Computational Linguistics, 11:531- 545, 2023. doi: 10.1162/tacl URL https: //acl antho logy org/ 2023. tacl-1.31/.
Merrill, W. and Sabharwal, A. The expressive power of transformers with chain of thought. In The Twelfth International Conference on Learning Representations, 2024. URL https:ttp/..... www.r/veeeeeeeeeeeeeeeeeeeee net/ forum? JN-NJNGG
Qwen. Qwen2.5: A party foundation models, September 2024. URL https: /tt////wweee qwenlm. github io/blog/ qwen2.5/.
Strobl, L., Merrill, W., Weiss, G., Chiang, D., and Angluin, D. What formal languages can transformers express? a survey. Trans. Assoc. Comput. Linguisties, 12:543-561, 2024. URL https: //tp::///oooooo /tttpp/////....r//1111//// 00663.63.
Merrill, W., Sabharwal, A., and Smith, N. A. Sat- urated transformers are constant-depth threshold cir- cuits. Transactions of the Association for Computa- tional Linguistics, 10:843-856, 2022. doi: 10.1 org/
4.00493. URL https: 2022. tacl-1.49.
Suresh, T., Reddy, R. G., Xu, Y., Nussbaum, Z., Mulyar, A., Duderstadt, B., and Ji, H. Cornstack: High-quality contrastive data for better code ranking, 2024a. URL pttps://arxiv.. wwgp:os//////////a///// 01007.
Mirzadeh, I., Alizadeh, K., Shahrokhi, H., Tuzel, O., Ben- gio, S., and Farajtabar, M. Gsm-symbolic: Understand- ing the limitations of mathematical reasoning in large language models, 2024. URL https: http///axvvvv.o// org/ abs/24 0 05229.
Suresh, T., Ugare, S., Singh, G., and Misailovic, S. Is watermarking Ilm generretd code robust?, 2024b. URL bttps://arxiin org abs 2403. 1.983.
Olausson, T., Gu, A., Lipkin, B., Zhang, C., Solar-Lezama, A., Tenenbaum, J., and Levy, R. Line: A neurosymbolic approach for logical reasoning by combining language models with first-order logic provers. In Proceedings of the 2023 Conference on Empirical Methods in Natu- ral Language Processing. Association for Computational Linguistics, 2023. doi: 10.18663/v 005533/11/2022 http:////222eeee .mwpppmma.....mi.....mmm... 313. URL http: //dx dxx doi. owg/10..//..o..... 18653/v1/ 2023. wwwwp-main..m..me. 31
Tam, Z. R., Wu, C.-K., Tsai, Y.-L., Lin, C.-Y., Lee, H.-y.. and Chen, Y.-N. Let me speak freely? a study on the impact of format restrictions on large language model performance. In Dernnncourt, F., Preofiuc-Pietro, D., and Shimorina, A. (eds.), Proceedings of the 2024 Confer- ence on Empirical Methods in Natural Language Pro- cessing: Industry Track, pp. 1218-1236, Miami, Florida, US, November 2024. Association for Computational Linguistics. doi: 10.18663w.1/2224.cmmmp. inddutisstty.... 91. URL https: https:://acaatthaaeeee org 2024. mmmlp-industry..o 91/.
OpenAL. Opneai tools, 2024. URL httss::::/ppl cwm/ htt.//cc..c///ooo/ http://ocs/asassstttttssaaaaaaaa
Pan, L., Albalak, A., Wang, X., and Wang, W. Y. Logic- Im: Empowering large language models with symbolic solvers for faithful logical reasoning, 2023. URL / //axiivv... org/ abs/2b05 12295.
Team, Q. Qwq-32h: Embracing the power of reinforce- ment learning, March 2025. URL https: hels:///qwen/ /wwnnmm github ht/pio////////oo//oooo -wg-p
Ugare, S., Gumaste, R., Suresh, T., Singh, G., and Mi- sailovic, S. Itergen: Iterative structured Ilm gener- ation, 2024a. URL https://axxvv.org/// abs/ 1410.07280
Park, K., Wang. J., Kirk-aaik,,,,,k,, T., Polikarpova, N.,
and D' Antoni, L. Grammar-aligned decoding, 2024. URL https: http///rxxiii// vxv.. www./oog///////oooooo.oo abs/2405 21047.

---

CRANE: Reasoning with constrained LLM generation
Ugare, S., Suresh, T., Kang, H., Misailovic, S., and Singh, G. Syncode: Llm generation with grammar augmentation, 2024b.
Ugare, S., Suresh, T., Kang, H., Misailovic, S., and Singh, G. Syncode: Lim generation with grammar augmen- tation, 2024c. URL https: https://aaxiiii /ttp://aaxvvvooooo org abs/ 9403.01632
Wei, J., Wang, X., Schuurmans, D., Bosma, M., Ichter, B., Xia, F., Chi, H., Le, Q. V., and Zhou, D. Chain-of- thought prompting elicits reasoning in large language models. In Proceedings of the 36th International Confer- ence on Neural Information Processing Systems, NIPS '22, Red Hook, NY, USA, 2022. Curran Associates Inc. ISBN 9781 111387188.8.
Willard, B. T. and Louf, R. Efficient guided generation for large language models, 2023.
Wolf, T., Debut, L., Sanh, V., Chaumond, J.. Delangue,
C., Moi, A., Cistac, P. Rault, T., Louf, R., Funtow- icz, M., Davison, J., Shleifer, S., von Platen, P., Ma, C., Jernite, Y., Plu, J., Xu, C., Le Scao, T., Gugger, S., Drame, M., Lhoest, Q., and Rush, A. Transform- ers: State-of-the-art natural language processing. In Liu, Q. and Schlangen, D. (eds.), Proceedings of the 2020 Conference on Empirical Methods in Natural Language Processing: System Demonstrations, pp. 38-45, Online, October 2020. Association for Computational Linguisties. URL https: doi: 10. 10011865//1120020mmmmp-eee emnlp-demos 6.
wolframm Wolfram alpha, 2024.
URL https:// com/.
Wu, Y., Jiang, A. Q., Li, W., Rabe, M. N., Staats, C. E., Jamnik, M., and Szegedy, C. Autoformalization with large language models. In Oh, A. H., Agarwal, A., Belgrave, D., and Cho, K. (eds.), Advances in Neural Information Processing Systems, 2022. URL https: //operreiiew /et/foormm debTiieeb.IBB..
Yang. K., Swope, A. M.. Gu, A., Chalamala, R., Song, P., Yu, S., Godil, S., Prenger, R., and Anandkumar, A. Leandojo: Theorem proving with retrieval-augmeentd language models, 2023. https: /aaaaaivvvorr................ 2tss/2366.16226.
12

---

CRANE: Reasoning with constrained LLM generation
A. Turing Machine Computation
A Turing machine processes an input string x E Σ Its configuration consists of finite state set Q, an input tape co. work tapes cI,...,C Cb. and an output tape Cx+1- Additionally, each tape T has an associated head position h,-
Initially, the machine starts in the initial state qo Q with the input tape og containing x, positioned at index O, and surrounded by infinite blank symbols (6). The head on the input tape is set to hi O, while all other tapes contain only blank symbols bs and have their heads positioned at 0.
At each time step i, if qi & F (F is a set of halting states), the configuration updates recursively by computing:
( Yo+1, Co.... (.42) = 8(g,, 14.
where 8 is the transition function. The machine updates each tape by setting (h+) = 7.. leaving all other tape cells unchanged. The head position for each tape is updated as h2- h + d².. If q: F, the Turing machine halts and outputs the sequence of tokens on the output tape, starting from the current head position and continuing up to (hut not including) the first blank symbol (6). A Turing machine can also function as a language recognizer by setting the input alphabet > = = 1} and interpreting the first output token as either 0 or 1.
B. Thershold Circuit Class
TC is class of computational problems that can be recognized by constant-depth, polynomial-size circuits composed of threshold gates. A threshold gate, such Oçk. outputs if the sum of its input bits is at most ks, while 0z* outputs I if the sum is at least k. These circuits also include standard logic gates like A, V, and as special cases of threshold functions. Since TC circuits can simulate AC circuits a polysize, constant-depth (Λ, V,j,iij-i family), they are at least as powerful as ACO in the computational hierarchy. The circuit families we have defined above are non-uniform, meaning that there is no requirement for the circuits processing different input sizes to be related in any way. In degenerate cases, non non-uniform circuit families can solve undecidable problems making them an unrealizable model of computation (Arora Barak, 2009). Intuitively, uniform circuit family requires that the circuits for different input sizes must be "somewhat similar" to each other. This concept is formalized by stating that there exists resource-constraie given the input 1", can generate serialization of the corresponding circuit C, for that input size. Specifically, logspace uniform T family can be constructed by logspace-bounde Turing machine from the string 1
Turing machine that,
C. Proofs
Lemma C.I (Constant depth circuit for Lz)- For any log-precision constant layer transformer-based LLM C with finite vocabulary V, single deterministic auto-regressive step (z)x) operating any input of size N with x E V can be simulated by grespace-unifort threshold circuit family of depth C where C' is constant.
Proof. The construction is from Theorem 2 in (Merrill & Sabharwal, 2023).
Proposition 3.1. For any log-precision LLM L with constant layers there exists logspace-uniform thershold circuit Thn such that La, (x) = Th, (x) holds for all inputs with size |x = n and n. E N.
Proof. The language L(Ga) is finite; therefore, for any string E L(G2), the length satisfies |s| S N, where N is constant. Consequently, for any input æ, the output yG La has a constant length, i.e., lval < N. The number of autoregressive steps is also bounded by N.
From Lemma C. each unconstrained autoregressive computation (x) can be simulated by a constant-depth threshold circuit C. This implies that (z G.) can also be simulated by a constant-depth threshold eircuit since it only involves an additional multiplication by a constant-sized precomputed Boolean mask {0, 1 1 (see Section 2).
Given that the number of autoregressive steps is constant N, and each step can be simulated by a constant-depth circuit C, we can simulate all N steps using depth N x C' circuit by stacking the circuits for each step sequentially. For uniformity, we are just stacking together a constant number of constant depth circuits we can do it in a log-space bounded Turning machine M.
Note that this proof holds only because T..).) allows only constant-size strings in the output.
13

---

CRANE: Reasoning with constrained LLM generation
Lemma 3.2. For any Turing machine M with lape alphabet I, there exists consiant depth LLM LM with finite vocabulary T VM and log-precision that can simulate t(n) steps of M with t(n) autoregressive steps.
Proof. The construction follows from Theorem 2 (Merrill & Sabharwal, 2024).
In this construction, the deterministic Turing machine run captured by sequence of ,,,... Ta(os) capturing the state entered, tokens written, and directions moved after each token before generating the output M (z). Then any imput the z the output ( = Ti, Pt(n) Mxx) (assuming M halts within on within t(n) steps where n = |z] and t(n) is polynomial over n).
Proposition 3.3. For any Turing machine M with tape alphabet r, there exists constant depth LLM LM with finite vocabulary I C Vι and log precision such that for any input with |x| = LM.G. (x) - with E VM assuming M halts on x in t(n) steps.
Proof. Las (x)) = - M[]) M We show that (x) E L(Ga). Ga + RMG. Since, G is output grammar of M then Mx) L(G). For all S i < t(n) 7V I. Then, 71 ... P((n) I E L(RM).
Then (x) E I(Ga) then under constrained decoding the output LM (z) remains unchanged and (M) LM.G. (z) (2) where r 7i "(())
14

---

CRANE: Reasoning with constrained LLM generation
D. FOLIO Results
Table Comparison of CRANE and baselines with various models on FOLIO.
Model
Method
Acc. (%)
Compiles (%)
Tokens
Unconstrained CoT
18.72
54.19
629.59
Qwen2.5-Mathh77 TB-nstuuu
Constrained
28.08
76.85
679.44
CRANE
31.03
75.86
690.17
Unconstrained CoT
36.95
70.94
350,64
Qwen2.5-7B-Instruuc
Constrained
37.44
87.68
775.62
CRANE
42.36
87.68
726.88
Unconstrained CoT
32.02
57.14
371.52
1.1-a--3.--BB-mme 1-8t-rrttttt
Constrained
39.41
86.21
549.75
CRANE
46.31
85.71
449.77
D.1. GSM-Symbolic Examples and Prompt
M Problem Solution Examples:
Usestion: A fog bank rolls in from the ocean: to cover a city. it takes (#) minutes to cover every (d) miles of the city. the city mf how many minutes will it take foz the tog bank to cover the whole olty?
from oceanfront the opposita inland edge,
Answer: y//dvt
Vuestion: [name) makes [drink] using teaspeons of suger and cups of the ratio of [m]:in). if she used total of [x] teaspsons of sugar and cups of water, calculate the number of teaspocnfula augar used.
(m+x) (m+n))
Listing 1. Problem Solution Examples for GSM-Symbolic
GSM-Symbolie Prompt:
You expert in solving grade school math tasks. You will be presented with grade-school math word problem with symbolic variables and be aaked to solve it.
Defoze answering you should reasen about the problem (using the <ceasenings field in the response described nelowi. Intermediate symbolic expreastons generated during reasoning should be wrapped in cc 25.
chen, output the symbolic expression wrapped in that use numbers as well as the vari aalia defined in the question on. You are only al lowed to use the following operations:
the question. The expressions
//, 9, (), int().
You will always reapond in the format described below: <ressoning> The final answer is <csymbelic expression>s
let's think step
10
chare [t] trees the (gl. warkers will there will be [tf) trees. How many trees did the [gl workers plant today?
trees in the (g) today. After they done,
12
Let's think step by step. Initielly, there are [t] trees. After planting, there are [tf] crees. The number of trees planted is <etf tos, The final answer <eLf 1>s.
13
14
there are (o) cars in the parking lot and (nc] more cars arrive, hew many cars are in the parking lot??
15
Let's think step by step. Initielly, there are (e) cars. (ne) cars asrive, tosal becomes <<c ness. the final answer is exe + ne>>.
17
18
:pl) had (chl) (ol) and (p2) had (ch2) (ol). if they (a) (ol), how many pieces they have left in total?
20
let's think step by atep. Initially, (pl) had (ch1) foll, and (p2) had (ch2) (oll, making Lotel of <echl ch2s>. After esting (a) (ol), the remaining is <schl ch2 2>>.
ch2
final
21
:pl) had (11) (ol). (pl) (g) (o1) (p2). How many [ol] does [pi] have left?
15

---

CRANE: Reasoning with constrained LLM generation
24
Let's think step by atep. (p1) started with (11) (o1), Arser giving (g) 1o1] (p2), (p1) has <<11 [ol] left. the final onswer in <el1 g>>.
25
:p1) does (p1) have new?
foll,
Christmas, (pl: got [um) fol; (p2) (Ld) 1ol) from (p3). many [ol;
27
28
Tet's s think step by step. [p1] started with (t) [ol]. (p1) recetved (tm) (o1) from (p2) and [td] [o1] Irom (p3), The total is eet 1 im tas, The final anawes is eet i La>s,
30
Chere were (o) (ol) in the server room, (nc] more foll were inatalled each day, from [dl] to (d2), Now server
many (ol) new
31
32
Let's step by step. Initially, thare wore (e) 1o1). [nc] [ol] were addad each day for <<d2
122 days, which is <ene (d2 dl 1122. The total is <se - ld2 dl 1)22, The tinal answer is <<p nc + (d2 d1 1132.
34
:p1) had [gb1) (ol), On (daylh, (p1) Lost (11) fol), On (day2), (pl) lost (12) more. Now many {ol] does (p1)
at the end of [day2]?
35
16
Tet''s think step by step. Initia 1y, [pt] had (gbl] (o1). After losing (11) (o1) on Iday1 ), (pll <cgbl 11>2, After losing (12) (o1) on (day2), the total is <cabl 11 125>, The rinal anawer is <eghl
1285.
38
:p1) has Sim). (pl) bough: iek [el) for $(p) each. Now much money does (pl) have left?
40
Let's think stop by step. Initially, (pl] had 5im). [pl] spent <<q p>> on (g) [ol]. The remaining money 18 sem q po2. The rinal answer cem q p22.
41
42
iquestion
Listing 2. CoT Prompt Template For GSM-Symbolic Evaluation
You are an expert in solving grade school math tasks. You will be presented with grade school math word problem with symbolic variables
Only output symbolic expression wrapped in use numbers as well as the variables defined in the question. You are only allowed to use the following aperationss t, 7, /1, 8, O), (I.
answers question. expression must
You will always respond in the format described below: ecsymbolic expression>>
igl. ig) workers will plant trees in (g) today. they are done, there will be [tf) trees. How many trees did the [g] workers plant today?
are trees
10
<ctE
(o) in the packing lot [nc] more cars arrive, how many care are parking ESS
11
lct?
13
14
<<a no>>
15
16
:p1) had (chl) (ol) and (p2) had (eh2) (ol). If they ate (8) (ol), how many pieces they have left
in total?
18
<<chl + ch2 - 2>>
19
20
:p1) had (11) (o1). (pl) gave (g) [o1) to (p2). How many [ol] does (pl] have 1ett?
22
<<l1
23
[pt] has [0]1. For Christmas, (pt) got [bm) (p2) [td] [ol] from (p3). How many [o1]
does (pl) have now?
25
26
<ct tm Ed>>
27
28
chere [c) (ol) the (loc). (nz) more (ol) were installed each day, from (dl) to (d2). How many
(c1) are now in the (loc]?
<<a 30
(d2 dl 11>>
32
:p1) had [gb1] (ol). On (daylh, (pl) 2ost (11) (o1). On (day2), (pl) l08t (12) more. How many (ol) does (p1) have at the end of (day2]?
33
34
<<gb1 11 1255
36
(pl] has (m)) (pt) bought (g) [o1) for ((p) each. Row much money doea (p1) have lefc?
37
<cm 38
16

---

CRANE: Reasoning with constrained LLM generation
qqustiion]
Listing Prompt Template For GSM-Symbolic Evaluation Without CoT
D.2. FOLIO Examples and Prompt
FOLIO Problem Solution Examples:
Que
People in this club who pe:form in achool talent shows of:en actend and are very engaged with achool events.
People in this club either pertorm in school talent ahows often or ase inactive and disinterested community members.
People in this club who chaperone high school dances All paople in this club who are insctive and disintarestad members of their commenity chaperone high school
students who attend the school.
All young children and Leenagers in this elub who wish Lo further their academic cazeers and educat onal opportunt are atudents who attend the school.
Bonnie is in this club and she either both attends and is very engaged with school events and student who attends the school or is net someone who both attends and is very engaged with school student who attends the scheol.
events and is
Based on the above information, is the following statement true, false, or uncertain? Bonnie performs talent
in
++#
10
11
FOL Solution:
12 Predicates:
inclub
is member of the club.
14
Perform(X) :: x performs in school talent shows.
ALLend(x) :::
16
Engaged(x) ::: x is very engaged with schsol evects.
17
(nactIve(x ::: is an inactive and distreesdt community nember.
18
Chaperone (x)
chaperones high school dances.
19
Student (x) ::: x is student who attends the school.
Kish
wishes furthar their anademic
educstionsl opportanities.
21
Premises:
:Forail] (InClub(x) (and)
(x)) ::: People in club who perform in school talent shows often attend and are very engaged with school events.
(x) [and] Eagaged (implies)
23
:Forall] x (InClub (xt (implies) (Perform (xor) Inactive(x))1 ::: People in this elub either perfozn. insctive and disincerested community members.
in school talent shows often
24
[forail] x (Intlub (x) (and] Chaperone (x) (implias) [not] (x)) 1:: People in this club who students
chaperone high school dances
the school.
25
: [ooaall] x (InClub(x) (and) Inactive (x) [implies) Chaperone (x) 11: All people in this club who ace community cheperone high school dances.
inactive and disinterested members
26
:forall] x (inClub (x) (and] (Xoung(x) [or] Teenager (x)) (and] kish [implies] Seudert (x)) ::: All club
young Idren and teeragers students who attend the school.
to further their academtc carears
educational opportunities
27
[forall] x (InSlub (implies) (Attond (x) (and) Engaged (X)) (xor) |nct (Attand (x) (ard) (x)) and) [Student (xor] Student
Bonnle
this
either both actenda
is very engaged with school events and is student who attends the school or is not someone who very engaged with
attends
events
28
conclusion:
unClub (bonnie) (and] Perforn (bonnie) 11: Bornie performs school talent ahows often.
30
11
An answer: Uncertain
Listing 4. Problem Solution Examples for FOLIO
FOLIO Prompt:
a problem description and a queation. The task is to parse the problem and the question into first erder logie Formulas.
The grammar of the first-order logic formula is defined as follows:
() loginal conjunction
exprl and expr2: expr1 (and] expr2
2) logioal diajunation of expr1 and expr2: expr1 (or) expr?
logical exclusive junction
expil
expr2: exprl (xor] exp:2
4) logical negation of expel: (act)exprl
5) exprl impliea expr2: ex9rl (implies) exprž
5) if and only if expr2: exprl :iff) expr2
7) logical universal quansification: (forall) x
10 loginal existential suantification: (existal These the ONLY operations in granmor,
"1
13 Answer the question EXACTLY like the examples.
14
17

---

CRANE: Reasoning with constrained LLM generation
15
Problem:
16
All people who regularly drink coffee dependent caffeine. Foople either regularly drink coffee or joke about being addicted to caffeine. No one who jokes about being addicted to caffeine is unaware that
either student and unaware neither student asr unawere that caffeine is a drug. if Rina is not person dependent on student,
drug.
caffeine drug,
person dependent on caffeine and soudens, neither a person dependent on caffeine nor student. Queation:
caffeine
is
17
18
Rased the above information, peraon wao jokes about being addicted to caffeine or 1a unaware that caffeine 1s a drug.
lowing statement true, false, uncertain? Rina eithar
20
take steps: first, we define necessary predicates premisea, finally, we the question 'Rina is either person who Jokes about being addicted to caffeine or is unaware that caffeine is a drug." in the conclusion. Now, we will write only the logic progzam, nothing
22
Predicales:
Dependent (x) :::
person depeadent caffeins. (xinka 1:: regularly drinks coffee.
24
(x) 1:: jokes abous being addicted caffeine.
26
Unaware(x)
unaware that caffeine is drug.
27
Student (x) 1:: x a student.
Premises:
29
:forall) x (Drinks (x) (implies) Dependent (x)) ::: All people who regularly drink coffee are dependent
on
30
[forall] x (Drinks(x) (xor] (x)) People either regularly drink caffee or jake about heing
addicted to catteine.
31
[Forall) x (Jokes (implies) (nna)enaaae)(
No who jekes about being addicted to caffeine
is unsware that caffeine is drug.
(Studant(rinn) [and] Unaware (rina)) (xor) [not] (Student (rina) (rinas) Rina either student and unsware that ceffeine is drug, or neither student nor unavaze thas caffeine is drug.
33
conclusion:
34
Jokes trinal (xorl Unaware (zina) #:: Riea is either a person who jokes about being addicted to caffeine that caffeine is drug.
35
36
37
Problem:
38
rivisavv Vanhoda was
condustor specialized the performance Renaissance Baroque music. Any choral conductor is muaician. Some musicians love music, roalaavv Venhoda published book in 1946 called Method SLudying Gregozian Chant.
39
Question:
40
Based on the above information, is the following statement true, false, or uncertain? Kiroslav Venhoda loved music.
41
**#
43
We take three steps: Ciret, define the necessary predicates premiaes, and rinally, we encode the question "Miroslav Venhoda loved music. in the cenclusion. Now, we will write only the logic program, nething else.
44
Predicates:
46
ChhoralConducter ::: x is charol conductor. muatcian.
47
ansiotan 1::
48
Love y)
loves
49
Author y) 1:2 x is the auther of y.
Book (x)
book.
51
Publiah 1x, y) 111 x is published in year y. Specialize yl 11: specializes y.
53
Promi ses:
54
Czech (miroalav) land) ChoralConductor (miraal land) Smeiiallaeemirrll.. renaiesance) (and] opeciellizemiizzsleey tmiros,av, baroque) Miroslav Venhoda Czech choral conductor who specialized in the perfermance Renaissance and Baroque music.
{ [forall] (ChoralConductortas [implies] Musician
charal conductor
musinian.
56
texists] x (Musician (x) (x) (and) Love 1x, music)] ::: Some muaicians love muaic. (and] Authoz iniroslav, me-hocorStudy hechoooBBudyyingsserrriiia LnggregorianChann.. [and] year1946) 1is Mivoslav Vanhoda published book in 1946
Publ ish
ing.sttuyyynnnggrrrrrro called Method of Studying Gregorian Chant.
58
Cenclusion:
59
Love (miroslav, musicl s:: Miroslav Venhoda loved music.
61
iquestionl
Listing 5. Prompt Template Used For FOLIO Evaluation
18

---

CRANE: Reasoning with constrained LLM generation
D.3. Case Study For GSM-Symbolic
Question: iname) hizes a [vehicle) Erom (start_ to hend_hour). He gets hours) hours free. The first paid hour is $ifirat_hour_coat, and each hour after that [multiplier] the much did ne pay?
Constrained:
free_houra ficet_hour_eost 1 (int hend start_hour) free_houss 11 multiplier firat_hou:_coat
<<(int (end_ start_hour) - tree_hourgs
Unconstrained with col: Let's think step by step. the total time hired is from (start_hour) to end_hour), which ia <<int (and_hour start_hour) sotall_sealll_ddaaeoe the [Trre_houra! free houra, the pald hours are csint (lend_hour start, hott_hoorr..tttl.... final enswer
360013>
()
3600) free_houe hoursssr tatal_secondz 3600) free_hours 11 multiplier first_hour_costt>>
sffirst_hour_cot
tend hour start_houz).
CRANE: Let's think step by step, The total time hired from (start_hour] (eur_ totaling int hour start_hoori2> hours, Subtracting [free_hours! free hours, the paid hours are <eint start_hour) free_hours>>. auditional hour costs (maitipller) Limes that. The Sinal answer is ecficst_houc_coat (inL end_hour start_hour) free_hours 1) multiplier fiest_hour_costt
irirat_hour_cost
Listing 6. Case Study for GSM-Symbolic
CRANE effectively alternates between constrained and unconstrained generation to produce intermediate expressions, the final answer, and to maintain the reasoning capabilities of the LLM. In contrast, unconstrained generation with CoT results in syntactically incorrect expression, while constrained generation produces a syntactically valid but incorrect expression.
D.4. Sampling Ablation for GSM-Symbolic
In our GSM-Symbolic case study, we use IterGen as the constrained generation baseline and initialize CRANE with IterGen. Both IterGen and CRANE employ selective rejection sampling to filter tokens that do not satisfy semantic constraints. For comparison, we also run unconstrained generation using temperature sampling and evaluate its performance against CRANE. Specifically, Qwen2.5-1.55 1..52.5-..BB-nstruure and Llama-3.1 ---B-BBBBBBBB--- --sttunntt we generate three samples with unconstrained generation at temperature of 0.7 and compute pass@ 1/2/3 metrics.
As shown in Table 4, CRANE with greedy decoding achieves higher accuracy than pass @ 1/2/3 for unconstrained generation with Chain-of-Thoughh (CoT) and temperature sampling unconstrained generation with CoT and temperature sampling achieves p accuracy of 35% -2% higher than CRANE-it generates approximately 4 times as many tokens as CRANE.
1...n..5--.BB-ntttttrt Although, for Llama-3.1 1e------Inssteee
D.5, Grammars
D.5.1. GSM-SYMBOLIC GRAMMAR
start:
*C" "C" expr space? ">" ">*
expr: expr space? space?
expr space? *-" space? term Lecn
term:
torm space? space? factor space? */" space? Lecn space? *//* space? factor space? *g" space? factor factor space?
11
12
13
factor:
*_* space? facter TYPE "(" space? expr space? *>*
14
primary space?
16
primary: VARIABLE
18
19
"(" space? expr space? ")*
21
-YPR,4: *int*
23
space:
25
Simport CNAME >> VARIABLE
26
simport common. NUMBER
19

---

CRANE: Reasoning with constrained LLM generation
Listing 7. GSM-Symbolic Grammar
D.5.2. PROVER9 GRAMMAR
start: predicata_cection premiss_sscction conclasion_sectior.
peciicateesectiige "Bredicales:" pred_catt__Geiiniiionl
sremise_sections "Bremises:" premiset
conclusion_section:: "Conclusion:" conclusions
sendicaat_defiiittte PREDICATE "( VA8 ("," vAR) "!" COMMENT
define_predicate
promises se: quantified expr COMMENT => define dofine_premise premise
conclusion: quantiried_exp:
define_concluston
10
guentified_exp:: quantifiez VAR expression *)* expression
12
quentifier: "[foroll)" -> forall "(axista)" +> exiats
14
expression: himplicasion_expr 15
Pbimo_icatinn ialooiication_exp. implicaLion_ent expt ("(if[)* bimplication expp)) ifr
17
2implication
xor_exp= ("Aimplies)* implicationeexp// -> imply 2xor_expr: or_expr ("[xcr]" xor_expr)?
18
19
3or 2or_expri and_expr ("Ior)* or_expr]?
or
20
Pand_exprs seq_expr ("(and)* and_expr1
>> and
2nog_oxpr: "(not]" quantified__xppr
neg
22
atom
24
2atom: PREDICATE """ VAR ("," VAR) "j" -> predicate "1" exenta ")"
26
27
Varisble names begin with à lowercase letter
28
VAR.-1: [[a-z] 28-2--0----111
/10-9]+/
29
Predicate names begin capital
31
PREUICATE.-1: [[a-2] (a-zA-20-9)+/
33
COMMENT: Ant
34
Simport
36
Bignore WS
Listing 8. Prover9 Grammar
20

---

CRANE: Reasoning with constrained LLM generation
Table 3. Comparison of CRANE and baselines on GSM-Symbolic based on accuracy, no. of tokens, and average time.
Model
k
Method
Acc. (%)
Parse (%)
Tokens
Unconstrained w/o CoT
20
98
18.23
Constrained
21
95
34.28
Qwen2.5-14 1.52255-1.B-Instrrre
Unconstrained CoT
130.74
CRANE
96
140.52
Unconstrained w/o CoT
18.23
Constrained
18
96
34.28
Qwen2.5-1.55 1.55tttttt
Unconstrained CoT
24
94
130.74
CRANE
30
98
140.52
Unconstrained w/o CoT
21
97
23.34
Constrained
22
97
25.29
Qwen2.5-1.55 1-5---nsrttt
Unconstrained CoT
128.97
CRANE
131.3
Unconstrained CoT
17.22
Constrained
36
99
18.61
Owen2.55Cooder-7BBBnnttt
Unconstrained CoT
32
84
148.87
CRANE
37
96
155.65
Unconstrained w/o CoT
36
96
16.89
Constrained
36
100
18.81
CCoder-B-IIntruuee
Unconstrained CoT
89
151.29
CRANE
97
163.21
Unconstrained w/o CoT
94
17.92
Constrained
99
25.28
Unconstrained CoT
37
88
138.38
CRANE
39
94
155.32
Unconstrained w/o CoT
20
66
115.22
Constrained
26
95
26.99
Swen2.5-Math-7B-nnss
Unconstrained CoT
28
72
190.51
CRANE
89
195.65
Unconstrained w/o CoT
22
83
Constrained
98
27.08
Bren2.5-Math-7B...
Unconstrained CoT
28
76
184.35
CRANE
37
88
194.77
Unconstrained w/o CoT
27
89
25.7
Constrained
29
99
26.81
Owen2.5-Math-7B-mm
Unconstrained CoT
29
82
155.26
CRANE
94
158.86
Unconstrained CoT
61
157.36
Constrained
45.58
Unconstrained CoT
29
84
198 64
CRANE
35
94
206.85
Unconstrained w/o CoT
18
68
131.5
Constraincd
24
96
37.38
-lama-3.1-BBInnttee
Unconstrained CoT
26
92
172.21
CRANE
179.95
Unconstrained w/o CoT
73
128,38
Constrained
35.97
1imma-..--B-Innstte
Unconstrained CoT
30
95
163.55
CRANE
33
95
170.22
21

---

CRANE: Reasoning with constrained LLM generation
Table 4. Comparison of CRANE and greedy and sampling baselines with different models on GSM-Symbolic.
Model
Method
pass @ 1/2/3 (%)
Parse (%)
Tokens
Unconstrained w/o CoT (Greedy) Unconstrained w/o CoT (L 0.7)
21
97
23.34
15/19/22
88/96/98
20.19/39.76/60.5
Constrained (Greedy)
22
97
25.29
Owen2.5-1.5B-Insteee
Unconstrained CoT (Greedy)
26
90
128,97
Unconstrained CoT 0.7)
21/25/30
78/91/96
066.22/292.96/444.6
CRANE
31
100
131.3
Unconstrained w/o CoT (Greedy)
21
73
128.38
Unconstrained CoT (t= 0.7)
15/21/25
51/74/84
106.88/232.75/33
75/3669.89 86
Constrained (Greedy)
26
98
35.97
Llama-3.1-4 1iima-3.1-8B-Inaaee 1-88-Insttrctt
Unconstrained CoT (Greedy)
30
95
163.55
Unconstrained CoT (t= 0.7)
24/29/35
89/98/98
196.01/403.68/606
CRANE (Greedy)
33
95
170.22
Table Comparison of CRANE and greedy sampling baselines with different models on FOLIO.
Model
Method
pass 1/2/3 (%)
Compile (%)
Tokens
Unconstrained CoT (Greedy) Unconstrained CoT (t (t=00 0.7)
36.95
70.94
350.64
16.75/28.57/34
11166/55666688.477
401.5/800.19/1219..22
Qwen2.5-7B-Insthee
Constrained (Greedy)
37.44
87.68
775.62
CRANE (Greedy)
42.36
87.68
726.88
Unconstrained CoT (Greedy) Unconstrained CoT (.7)
32.02
57.14
371.52
14.29/22.66/22
33,99/46.88 8/57
435.35/877.33/1307.44
1-ama-3.1-8--nmee
Constrained (Greedy)
39.41
86.21
$49.75
CRANE (Greedy)
46.31
85.71
449.77
22


Reviews:
[{"review_id": "DoEDpQSxh2", "reviewer": "Reviewer_jTKi", "summary": "The paper examines the expressivity of large language models (LLMs) under grammar constraints. It first demonstrates that there are problems LLMs can solve without constraints but fail to solve when under grammar constraints. The paper introduces the CRANE algorithm, which first generates an unconstrained reasoning chain and then imposes constraint grammar within specific generated symbols.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Dear reviewer jTKi,\n\nThanks for your constructive feedback.\n\n> Q1. The paper provides a theoretical explanation of why COT is essential for LLMs across various tasks.  However, COT has recently become a widely adopted technique. The proposed method integrates CoT with output constraints and thus has limited novelty.\n\n**R1:** Although Chain-of-Thought (CoT) is a popular technique, to the best of our knowledge, we are the first to formally show that constrained decoding with restrictive grammars can limit the ability of large language models (LLMs) to perform CoT. This, for the first time, provides a theoretical justification for earlier empirical evidence [1] showing that the functional accuracy of LLMs for certain tasks decreases under constrained decoding. More importantly, we show that the lack of expressive power arises only when the output grammar is overly restrictive, and this limitation can be easily mitigated by augmenting the output grammar with additional production rules for any given task. This insight leads to our proposed adaptive decoding algorithm, CRANE, which improves performance over both baseline constrained and unconstrained decoding methods.  \n\nOur primary contribution is not just the combination of CoT with constrained decoding but:  \n1. Identifying and formally establishing the potential limitations of constrained decoding with restrictive grammars for any LLM, including more advanced models developed in the future.  \n2. Providing both -- a theoretical augmented grammar construction for any task (Turing Machine) and a simple, practical algorithm—CRANE—that simultaneously preserves reasoning capabilities and reduces structural errors (syntax and semantic errors) in generated outputs, thereby enhancing overall LLM performance.  \n\n[1] \"Let Me Speak Freely? A Study on the Impact of Format Restrictions on Performance of Large Language Models\", Proceedings of the 2024 Conference on Empirical Methods in Natural Language Processing: Industry Track.", "claims_and_evidence": "The claims are sound and well-supported.\n- The paper claims that an LLM with a constant number of layers cannot solve all problems. The authors first give an example of a st-connectivity problem, which is NL-complete but has constraints of single output digit 0 or 1. Then, they prove that the LLM can not solve it with the constraint unless the logspace-uniform class TC0=NL.\n- The experiments can validate the effectiveness of the proposed algorithm. The results show the proposed method significantly outperforms all baselines with different LLMs while achieving a comparable grammar pass rate with constrained grammar.", "methods_and_evaluation_criteria": "The paper uses accuracy and the grammatically correct rate to evaluate the methods. It is sound to inspect whether the methods follow the required grammar.", "theoretical_claims": "The proofs of Proposition 3.1 and 3.3 are correct.", "experimental_designs_or_analyses": "The experimental designs are sound. The paper evaluates the method on Math and Logic datasets and compares it with baseline with constraints and COT.", "relation_to_broader_scientific_literature": "The theoretical claims may inspire further works on LLM expressivity under constraints and design inference methods for certain grammars.", "essential_references_not_discussed": "The paper cites sufficient related works.", "other_strengths_and_weaknesses": "Weakness:\n- The paper provides a theoretical explanation of why COT is essential for LLMs across various tasks. However, COT has recently become a widely adopted technique. The proposed method integrates COT with output constraints and thus has limited novelty.", "other_comments_or_suggestions": "n/a", "questions_for_authors": "n/a", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "Dc0PKa8AbA", "reviewer": "Reviewer_ssfH", "summary": "The paper introduces CRANE (Constrained Reasoning Augmented Generation), a decoding algorithm for grammar-constrained large language model (LLM) generation that aims to balance syntactic correctness with reasoning capabilities. The work first provide a theoretical explaination for why constrained generation diminish the expressive power of LLMs. It then proposes an augmented grammar soltuion that allow intermediate reasoning steps to occur unrestricted first before restricted generation. The approach is demonstrated to improve both syntactic correctness and functional correctness.\n\n## update after rebuttal\nThe rebuttal addresses my questions. I remain positive on the paper.", "questions": "", "limitations": "", "rating": 3, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Dear reviewer ssfH,\n\nThanks for the constructive feedback. We have included additional experiments with different delimiters and larger and newer reasoning models. All experiments below use the same setup as Section 5. In all cases, CRANE consistently outperformed the baselines. We will add these results in the revised version.  \n\n> Q1. Experiments with different delimiters. \n\n**R1:** We use `<<` and `>>` as the delimeter for GSM-Symbolic following the original paper (see Figure 1) [1]. We will make this detail more clear in the revised version of the paper. \n\nFurthermore, to highlight CRANE's effectiveness across different delimeters, we have performed an ablation study on the GSM-symbolic dataset. We use ``## ##`` and ``!! !!`` in place of `<< >>` and report comparison against unconstrained CoT, which always performed the best among all three baselines. \n\n| Delimeter | Model | Method | Acc. (%) | Parse (%) | Tokens |\n| -------- | -------- | -------- |-------- |-------- | -------- |\n| || Unconstrained CoT | 20 | 61 | 156.13 |\n| |Qwen2.5-1.5B-Instruct | **CRANE** | **23** | 96 | 165.24 |\n| || Unconstrained CoT | 27 | 70 | 164.29 |\n| ``## ##``| Qwen2.5-Math-7B-Instruct | **CRANE** | **35** | 93 | 162.73 |\n| || Unconstrained CoT | 23 | 80 | 150.34 |\n| |Qwen2.5-1.5B-Instruct | **CRANE** | **26** | 92 | 162.21 |\n| || Unconstrained CoT | 24 | 81 | 198.53 |\n| ``!! !!``| Qwen2.5-Math-7B-Instruct | **CRANE** | **32** | 89 | 255.79 |\n| | | | | | |\n\n> Q2. Experiments with larger and advanced reasoning models.\n\n**R2:** We add experiments for newly released reasoning and larger models on GSM-symbolic. CRANE consistently outperforms the baselines on all models. \n\n\n| Model | Method | Acc. (%) | Parse (%) | Tokens |\n| -------- | -------- | -------- |-------- |-------- |\n| | Unconstrained w/o CoT | 18 | 89 | 21.64 |\n| | Constrained | 20 | 99 | 17.21 |\n| | Unconstrained CoT | 24 | 89 | 212.24 |\n| DeepSeek-R1-Distill-Qwen-7B | **CRANE** | **29** | 92 | 235.78 |\n| | Unconstrained w/o CoT | 12 | 77 | 29.2 |\n| | Constrained | 13 | 96 | 16.89 |\n| | Unconstrained CoT | 21 | 87 | 250.83 |\n| DeepSeek-R1-Distill-LLaMA-8B | **CRANE** | **31** | 92 | 268.82 |\n| | Unconstrained w/o CoT | 42 | 93 | 18.52 |\n| | Constrained | 42 | 96 | 25.62 |\n| | Unconstrained CoT | 42 | 95 | 157.71 |\n| Qwen2.5-Coder-14B-Instruct | **CRANE** | **45** | 95 | 158.54 |\n| | Unconstrained w/o CoT | 29 | 82 | 20.9 |\n| | Constrained | 30 | 91 | 30.48 |\n| | Unconstrained CoT | 32 | 87 | 233.42 |\n| DeepSeek-R1-Distill-Qwen-14B | **CRANE** | **38** | 93 | 244.98 |\n| | Unconstrained w/o CoT | 37 | 80 | 54.93 |\n| | Constrained | 38 | 91 | 34.2 |\n| | Unconstrained CoT | 43 | 87 | 222.62 |\n| QwQ-32B | **CRANE** | **46** | 88 | 237.98 |\n| | | | | |\n\n> Q3. Advances in Reasoning Models and Grammar-Constrained Generation\n\n**R3:** CRANE's effectiveness is maintained with the latest reasoning models. Larger, more advanced reasoning models are still susceptible to syntactic and semantic errors. Additionally, when recent reasoning models generate lengthy reasoning traces, enforcing output constraints from the start—as done in baseline constrained decoding algorithms—significantly degrades LLM performance.\nCRANE addresses both of these challenges by dynamically enforcing constraints. Notably, with DeepSeek-R1-Distill-LLaMA-8B, CRANE achieves the highest performance gains, improving by 10%  points.\nTherefore, for future reasoning models that generate reasoning traces and require final results to provably satisfy structural constraints, CRANE remains a valuable tool. \n\n\n> Q4. Finite Grammars.\n\n**R4:** Both the gsm-symbolic and FOLIO grammars permit infinite strings. The experiments demonstrate that CRANE significantly enhances the performance of practical LLMs, even when the output grammar allows infinite strings. Finite output grammars $G$ are just a special case used to theoretically establish the negative result, highlighting the limitations of constrained decoding when using highly restrictive grammars for **any** constant-layer LLM. Overall, CRANE remains a valuable framework for improving the performance of practical LLMs, even with infinite output grammars.  \n\nOn the other hand, Proposition 3.3 already provides a positive result for the ideal setting. It shows that an **ideal LLM** (with perfect parameter values) can always simulate any Turing machine using constrained decoding alone. This is possible when the output grammar $G$ is augmented with additional rules, as done in $G_a$. However, the currently available LLMs may not possess the perfect set of parameters.\n\n> Q5. Typos.\n\n**R5:** Thanks for pointing this out. We will fix them in the revised version. \n\n[1] \"GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models\", ICLR, 2025.", "claims_and_evidence": "+ Claims are generally well-supported by theoretical propositions and empirical evaluation. Specifically, \nthe work shows improvements on two benchmark datasets compared to baseline approaches.", "methods_and_evaluation_criteria": "+ The evaluation methods are appropriate. The work evaluate its approach on two symbolic reasoning datasets (GSM-symbolic, and FOLIO) and uses evaluation tools such as Z3 solver and Prover9 for validation the correctness.", "theoretical_claims": "+ The author presents clearly the limitation of prior work on providing only empirical studies. This work instead provide theoretical studies on why constrained generation limits the reasoning capability of the LLM. The theoretical analysis seems sound.", "experimental_designs_or_analyses": "The experimental designs seem sound. The proposed approach is compared to relevant approaches on two benchmarks using multiple LLM models.", "relation_to_broader_scientific_literature": "The work clearly relates to prior works on constrained decoding. \nIt provides two main key contributions based on its position: \n1. The theoretical analysis explaining the limited reasoning capability from constrained generation \n2. A simple yet effective approach to tradeoff between constrained generation and reasoning.", "essential_references_not_discussed": "+ the work comprehensively cites relevant prior works. \n- Many reasoning approaches are proposed to allow LLMs tackle more complex tasks. The work could discuss how these reasoning-related work affect the proposed approach.", "other_strengths_and_weaknesses": "+ clear theoretical contributions \n+ simple yet effective approaches to improve grammar-constrained LLM generation \n- focusing on grammars with finite languages seems to significantly limit the applicable scope of the work as the heavyweight usage of LLM is on code generation for common (e.g., rust) and domain-specific languages, which are likely all infinite. This could be the reason why the work focuses on the selected two benchmarks.", "other_comments_or_suggestions": "Minor typo: \n\nline 373: comparisong against --> comparison against \nline 498: Opneai tools --> OpenAI tools", "questions_for_authors": "1. Does the choice of the delimiter symbols (S1 and S2) affect the performance of CRANE? Currently, it is << and >> for the delimeters. Have the authors try other symbol choices? \n\n2. The models evaluated are all relatively small. Have the authors try larger models which could have better reasoning capability to begin with? Does the proposed approach see diminishing gain? \n\n3. Can the authors explain how would advances in reasoning models affect the grammar-constrained generation? In particular, the effectiveness of CRANE?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}, {"review_id": "ApXcuzvw2z", "reviewer": "Reviewer_6Prs", "summary": "The authors prove that constrained LLM generation diminishes the capabilities of\nLLMs. The (not precise) essence of this result is that\n1. Under constrained decoding, logspace-uniform threshold circuits (in $TC^0$)\n   can obtain the same outputs (solve the same problems) as LLMs.\n2. Under unconstrained decoding, LLMs can simulate Turing machines (in $NL$).\nBecause these two computational models belong to different complexity classes,\nit follows that there are problems (like st-connectivity) which LLMs can solve\nin an unconstrained setting and cannot solve in a constrained setting, (unless\n$TC^0 = NL$).\n\nThe second part establishes that augmenting the grammar to allow unconstrained\ndecoding for reasoning (then following by the constrained decoding) allows one\nto obtain constrained output and simulate the same Turing machine as an\nunconstrained LLM.\n\nTo bring this result to the realm of practical applicability, the paper proposes\nCRANE, a method to interleave constrained and unconstrained LLM decoding using\nan augmented grammar. Parts that require constrained decoding are generated\nbetween specific symbols (like << and >>), and there can be multiple such parts.\n\n## Update after rebuttal\n\nI would like to thank the authors for their insightful comments. I will maintain my score.", "questions": "", "limitations": "", "rating": 4, "confidence": null, "soundness": null, "presentation": null, "contribution": null, "strengths": "", "weaknesses": "", "quality": null, "clarity": null, "significance": null, "originality": null, "strengths_and_weaknesses": "", "was_revised": false, "final_justification": "", "rebuttal": "Dear reviewer 6Prs,\n\nThanks for your constructive feedback.\n\n> Q1. In CRANE, these two are freely interleaved with multiple constrained decoding parts. Do the results in Proposition 3.3 generalize naturally to this case? Is it always true that the final answer is at the end?\n\n**R1:** Proposition 3.3 shows that an ideal LLM (i.e., with a perfect set of parameters) can use constrained decoding with the augmented grammar $G_a$ (without any unconstrained steps) to simulate the steps of a given Turing machine and produce the final output only at the end. This result also naturally extends to CRANE, which interleaves unconstrained and constrained generation using $G' \\to S_1GS_2$, where $G$ is the output grammar and $S_1, S_2$ are delimiters. The only modification needed in the proof is to configure the ideal LLM from Proposition 3.3 to wrap the final output in delimiters $S_1$ and $S_2$. In this case, the ideal LLM with CRANE can simulate the Turing machine’s steps and write the answer at the end. We will include a formal proof in the revised version of the paper.  \n\nPractical LLMs may not have the specific set of parameters for the theoretical construction as in the ideal LLM and may not strictly follow this ideal format, where the output is generated only at the end. Instead, they may generate multiple strings that are parsable within the grammar (e.g., syntactically valid mathematical expressions). In such cases, following the common practice for CoT [1,2,3], for both CRANE and unconstrained reasoning, we greedily select the last parsable string to compute the functional accuracy. It is possible that the final answer is not generated at the end, and better selection algorithms could further improve the functional accuracy of CRANE. However, we leave this for future work.  \n\nNevertheless, our experiments demonstrate that CRANE, even with this simple selection strategy, outperforms direct final answer generation (whether in constrained or unconstrained modes) and unconstrained reasoning. \n\n[1] \"Large Language Models are Zero-Shot Reasoner\",  Advances in Neural Information Processing Systems 35 (NeurIPS 2022)\\\n[2] \"GSM-Symbolic: Understanding the Limitations of Mathematical Reasoning in Large Language Models\", The Thirteenth International Conference on Learning Representations (ICLR 2025)\\\n[3] https://huggingface.co/datasets/apple/GSM-Symbolic#answer-extraction-heuristic \n\n\n> Q2. Doesn't the grammar of the constrained generation also need to be modified to include the delimiters, like in C.5.1? \n\n**R2:** The constrained decoding algorithm must be initialized with the augmented grammar that includes the delimiter symbols. We mentioned this in the pseudocode (Algorithm 1, lines 3 and 4). The grammars in C.5.1 also include the delimiter symbols. For example, line 916 of the GSM-Symbolic grammar includes `<<` and `>>`. We will update the paper to clarify this detail. \n \n> Q3. Typos and writing suggestions.\n\n**R3:** Thanks for pointing this out. We will fix them in revised version of the paper.", "claims_and_evidence": "The theoretical results are proven. The empirical results are strong and\ndemonstrate the effectiveness of the proposed CRANE algorithm.", "methods_and_evaluation_criteria": "The benchmarks are appropriate and state-of-the-art.", "theoretical_claims": "I couldn't verify the proofs of the theoretical claims.", "experimental_designs_or_analyses": "I'm not sure what the ablation study on few-shot examples ablates, I don't see anything that's ablated.", "relation_to_broader_scientific_literature": "The paper is related to the literature of constrained decoding. The theoretical\npart is also related to complexity theory and the relationship between LLMs and\ncomputational models like boolean circuits or the Turing machines.", "essential_references_not_discussed": "I think the RICHES framework (https://arxiv.org/abs/2407.00361v1) is somewhat\nrelated in that it interleaves unconstrained decoding with exact retrieval keys,\nand the present work interleaves unconstrained and constrained decoding.", "other_strengths_and_weaknesses": "I really liked the discussion about the limitations.", "other_comments_or_suggestions": "- this part could be made more exact, it sounds like one can choose whether to use to\n  use just unconstrained or just constrained strategies: \"CRANE is compatible\n  with various decoding strategies, both constrained and unconstrained\"\n- Typo in Proposition 3.1: thershold\n- This could be rephrased: \"This approach allows a simple and cost-efficient approach\"\n- Typo on line 373: comparisong", "questions_for_authors": "In Proposition 3.3, there is just one reasoning part before the single\nconstrained decoding part. In CRANE, these two are freely interleaved with\nmultiple constrained decoding parts. Do the results in Proposition 3.3\ngeneralize naturally to this case? Also, is it always true that the final answer\nis at the end? Why?\n\nThe paper says that CRANE works with an arbitrary LLM and constrained decoding\nalgorithm. How do these generate the start and end delimiters? I have seen that\nthe delimiters are in the prompt, but doesn't the grammar of the constrained\ngeneration also need to be modified to include the delimiters, like in C.5.1?", "summary_of_paper": "", "summary_of_recommendation": "", "technical_quality": "", "clarity_of_presentation": "", "potential_impact": "", "robotics_focus": "", "quality_of_limitations": "", "questions_for_rebuttal": "", "reasons_to_accept": "", "reasons_to_reject": "", "questions_to_authors": "", "extra_scores": {}}]

Author rebuttal:

Meta-review: This paper first posts a theoretical analysis on the observation that grammar-guided constraint-decoding for LLMs would reduce the reasoning capabilities, by proving that the computational model under constraint and unconstraint decoding belong to different complexity class, thus there must be problems that can be solved with unconstraint decoding that inherently can not be solved with constraint decoding. To mitigate this issue, it proposes CRANE, a decoding algorithm that interleave constrained and unconstrainted LLM decoding with the augmented grammar. Experiments are conducted on GSM-Symbolic (math) and FOLIO (logical reasoning domains), and show that the proposed method is effective in improving the reasoning capabilities of LLMs. The theoretical analysis on constraint decoding is valuable and the experiments are well-designed to showcase the effectiveness of the proposed CRANE method. Concerns on generalizability to larger models are adequately addressed during the rebuttal phase by experimenting on large models. The remaining concern of this work is relatively limited scope for the experiments. As the main goal is to improve LLM reasoning in general and the theoretical analysis is also towards general LLM reasoning, the experiments are only conducted on two domain (math and logical reasoning), and only one dataset for each domain. I would suggest the authors to augment the experiments with more domains, or at least more datasets for each domain (e.g., there are plenty other math reasoning datasets out there) to provide better empirical support.
Decision: Accept (poster)