CRANE: Reasoning with constrained LLM generation

Code generation, symbolic math reasoning, and other tasks require LLMs to pro-duce outputs that are both syntactically and semantically correct. ConstrainedLLM generation is a promising direction to enforce adherence to formal gram-mar, but prior works have empirically observed that strict enforcement of formalconstraints often diminish the reasoning capabilities of LLMs. In this work, wefirst, provide a theoretical explanation for why constraining LLM outputs to veryrestrictive grammars that only allow syntactically valid final answers reduce thereasoning capabilities of the model. Second, we demonstrate that by augmentingthe output grammar with carefully designed additional rules, it is always possibleto preserve the reasoning capabilities of the LLM while ensuring syntactic andsemantic correctness in its outputs. Building on these theoretical insights, wepropose a reasoning-augmented constrained decoding algorithm, CRANE, whicheffectively balances the correctness of constrained generation with the flexibilityof unconstrained generation. Experiments on multiple open-source LLMs andbenchmarks show that CRANE significantly outperforms both state-of-the-art con-strained decoding strategies and standard unconstrained decoding, showing up to a10% improvement over baselines on challenging symbolic reasoning benchmarks.