Logically Constrained Decoding (2025)

Abstract: Constrained decoding is a state-of-the-art technique for restrictingthe output of an Large Language Model (LLM) to obey syntactic rules,e.g., a regular expression or context-free grammar.In this paper, we propose a method for extending constrained decodingbeyond syntactic constraints, to enforcing formal, logical constraintsthat reflect some world model being reasoned about.We demonstrate proof-of-concept implementations for the game of chess,and for propositional resolution proofs:we constrain the LLM’s decoding such that the LLM is free to outputwhatever tokens it wants, as long as it does not make illegalmoves (chess) or unsound proof steps (resolution).We believe this technique holds promise for improving LLMs’ generationof precise, formal reasoning, as is particularly necessary formathematics.

## introduction proof is the quintessential distinguishing feature of mathematical discourse. like other forms of argumentation, the statements in a proof must be syntactically correct and semantically meaningful, and the overall text should lead to the desired conclusion. what makes proofs distinctive is that each statement must be sound, i.e., it must obey formal logical rules with respect to the preceding statements. this is akin to the moves in a game or puzzle: each step must be a legal move. many applications require such precise, correct, logical reasoning, underscoring the importance of research on nlp for mathematics. large language models (llms) have made extraordinary progress on mathematical reasoning, e.g., both openai and google deepmind recently announced gold-medal-level performance on international math olympiad problems @xcite . however, even leadingedge frontier models frequently make mistakes. in this paper, we do not concern ourselves with wild hallucinations, but rather focus on formally invalid reasoning: statements that, given the precise logic of the world model underlying the reasoning, are illegal or incorrect. for example, we pitted chatgpt-5 against the well-known chess engine stockfish @xcite in a casual game. 1 chatgpt played a solid opening, but stumbled a bit in the mid-game, reaching the position shown in fig. 1 with chatgpt (white) to play its 30th move. at this point, chatgpt attempted a flagrantly illegal move, presumably 1 the details of the game are unimportant, but for the curious: we used stockfish version 17.1, with default settings except a depth-limit of 15. chatgpt-5 played white, and stockfish played black. the moves played were: 1. e4 e5 2. nf3 nc6 3. bb5 a6 4. ba4 nf6 5. o-o nxe4 6. d4 b5 7. bb3 d5 8. dxe5 be6 9. c3 be7 10. re1 o-o 11. nbd2 bc5 12. nxe4 dxe4 13. qxd8 rfxd8 14. rxe4 bxb3 15. axb3 rd1+ 16. re1 rxe1+ 17. nxe1 nxe5 18. bf4 bd6 19. bxe5 bxe5 20. nd3 bd6 21. re1 a5 22. ra1 f6 23. kf1 kf7 24. ke2 c6 25. g3 bc7 26. b4 re8+ 27. kf1 a4 28. b3 axb3 29. ra7 re7, whereupon chatgpt attempted an illegal move. ## logically constrained decoding but what if we wish to enforce richer constraints than mere syntax? for example, we might wish to generate a program that obeys specified functional properties, or a mathematical proof that is logically sound. for such an application, syntactical constraints are insufficient, because there is an underlying world model, upon which the correctness or incorrectness of an output depends. for program correctness, this world model might include the values and types of program variables, assumptions on program paths, and the semantics of various operators. for mathematical proof, the underlying model might include constraints (assumed or derived) on the domains and interpretations of all formal symbols, and the status of assumptions and proof goals. in this paper, we propose the concept of logically constrained decoding. we retain the framework of constrained decoding, with its desirable attributes, but we seek to enforce formal, logical constraints that reflect some world model underlying the reasoning. the basic idea is actually very simple. the key insight is that the parser p in (normal, syntactic) constrained decoding is already doing logically constrained decoding, but just for a very limited, underlying world model. for regular expressions, the world model is just a finite automaton; for cfgs, a pushdown automaton. why not substitute a richer world model? the llm (if any), and allows any token that can lead to generating one of the complete legal moves. propositional resolution proofs are our second, more complex example. propositional proofs are the essence of mathematical proof, and as mentioned earlier, resolution lies at the core of practical, modern sat solvers. in this case, the state of the underlying world model is the set of clauses that were either given as assumptions, or have been proven already. a legal "move" is a resolvent of existing clauses. (we can also enforce that the move does not generate a duplicate of an existing clause, or a useless tautology like (x+x).) when the llm is trying to generate its next move, the symbolic constraint engine enforces that each additional token maintains that the generated output be a prefix of a legal resolvent. for example, given assumptions (1) (-1 + 2) (-2), the legal resolvents are (2) (generated by resolving (1) and (-1 + 2)), and (-1) (generated by resolving (-1 + 2) and (-2)). so, the llm is constrained foot_4 to generating a ( next, and then either a 2 or a -, and then if it had generated (2, it must generate a ) next, and if it had generated (-, it must generate a 1 next, etc. so, it is possible in theory to do logically constrained decoding for two small, but non-trivial problems. but is it efficient enough to improve the accuracy of real llms? that is a question that must be answered empirically. ## empirical results we now evaluate how well logically constrained decoding works on our two example world models. specifically, we explore (1) is it easily implementable in practice on real llms? (2) does it improve the quality of llm outputs on these problems in practice? and (3) what is the impact on the llms' token throughput? to answer the first question, we implemented logically constrained decoding for these two problems on several different llm families: qwen2.5 7b / 14b / 32b (qwen et al., 2025), llama 3.1 8b @xcite , gemma3 7b / 14b / 27b @xcite , phi4mini @xcite , and ministral-8b @xcite . we selected these models because they are open-source, and fit on our computing infrastructure. (our experiments were run on a shared cluster, using dell emc c4140 gpu compute nodes, with 8gb ram per core, and nvidia tesla v100 gpus with 16gb or 32gb.) all models are instruction fine-tuned. to account for numerical instability, gemma3 models were run with fp32, while others in fp16. 8-bit quantization was used for all gemma3 models and qwen2.5 32b. code was in python, using the huggingface transformers library @xcite . overall, we encounted no particular difficulties in implementing logically constrained decoding with these llms. our code is available on github foot_5 . we evaluate the effect on llm output quality in §4.1 for chess, and §4.2 for resolution proofs. in §4.3, we report on the effect of logically constrained decoding on llm performance (token throughput). ## conclusion and future work we have introduced logically constrained decoding, which lifts the concept of constrained decoding beyond syntactic constraints to enforcing logically correct output with respect to an underlying, formal world model. we have demonstrated proof-ofconcept implementations for chess and for propositional resolution proofs, on nine different llms. our technique guarantees that the small llms do not generate illegal outputs for the problems being solved, and enables them to generate correct outputs on problems that even state-of-the-art, proprietary frontier models solve incorrectly. the main line for future work is to expand the applicability of our technique to additional domains, such as code generation or richer proof systems (e.g., lean). the principle challenge is how to turn the logical constraints into something that can be enforced efficiently at the token level. for code generation, we are excited by the work of mündler et al. @xcite on constrained generation of type-safe programs. for mathematical proof, we are currently developing a more efficient technique for a more powerful proof system than resolution.