@inproceedings{ma-hu-2025-logically,
    title = "Logically Constrained Decoding",
    author = "Ma, Franklin  and
      Hu, Alan J.",
    editor = "Valentino, Marco  and
      Ferreira, Deborah  and
      Thayaparan, Mokanarangan  and
      Ranaldi, Leonardo  and
      Freitas, Andre",
    booktitle = "Proceedings of The 3rd Workshop on Mathematical Natural Language Processing (MathNLP 2025)",
    month = nov,
    year = "2025",
    address = "Suzhou, China",
    publisher = "Association for Computational Linguistics",
    url = "https://preview.aclanthology.org/ingest-emnlp/2025.mathnlp-main.11/",
    pages = "150--167",
    ISBN = "979-8-89176-348-7",
    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."
}