ABS: Enforcing Constraint Satisfaction On Generated Sequences Via Automata-Guided Beam Search
Extracted source text · arXiv 2506.09701
\documentclass{article}
% if you need to pass options to natbib, use, e.g.:
% \PassOptionsToPackage{numbers, compress}{natbib}
% before loading neurips_2025
% ready for submission
\usepackage[preprint]{neurips_2025}
% to compile a preprint version, e.g., for submission to arXiv, add add the
% [preprint] option:
% \usepackage[preprint]{neurips_2025}
% to compile a camera-ready version, add the [final] option, e.g.:
% \usepackage[final]{neurips_2025}
% to avoid loading the natbib package, add option nonatbib:
% \usepackage[nonatbib]{neurips_2025}
\usepackage[utf8]{inputenc} % allow utf-8 input
\usepackage[T1]{fontenc} % use 8-bit T1 fonts
\usepackage{hyperref} % hyperlinks
\usepackage{url} % simple URL typesetting
\usepackage{booktabs} % professional-quality tables
\usepackage{amsfonts} % blackboard math symbols
\usepackage{nicefrac} % compact symbols for 1/2, etc.
\usepackage{microtype} % microtypography
\usepackage[table]{xcolor}
\definecolor{lightgreen}{RGB}{200,255,200}
\definecolor{lightred}{RGB}{255,200,200}
\usepackage{amsmath}
\usepackage{comment}
% Use the postscript times font!
\usepackage{times}
\usepackage{soul}
\usepackage{url}
%\usepackage[hidelinks]{hyperref}
\usepackage[utf8]{inputenc}
\usepackage[small]{caption}
\usepackage{graphicx}
\usepackage{amsmath}
\DeclareMathOperator*{\argmax}{arg\,max}
\DeclareMathOperator*{\argmin}{arg\,min}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{booktabs}
\usepackage{algorithm}
\usepackage{algorithmic}
\usepackage{tikz}
\usepackage{comment}
\usepackage{xspace}
\usepackage{subfigure}
\usetikzlibrary{automata,positioning}
\newtheorem{example}{Example}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}[theorem]{Lemma}
\newtheorem{definition}{Definition}
\newcommand{\eg}[1]{\textcolor{blue}{EG: #1}}
\newcommand{\ltlf}{$\text{LTL}_f$\xspace}
\newcommand{\centered}[1]{\begin{tabular}{l} #1 \end{tabular}}
\newcommand{\model}[1]{\texttt{TRIDENT} }
\newif\iflong
\longfalse
\title{TRIDENT: Temporally Restricted Inference via DFA-Enhanced Neural Traversal}
% The \author macro works with any number of authors. There are two commands
% used to separate the names and addresses of multiple authors: \And and \AND.
%
% Using \And between authors leaves it to LaTeX to determine where to break the
% lines. Using \AND forces a line break at that point. So, if LaTeX puts 3 of 4
% authors names on the first line, and the last on the second line, try using
% \AND instead of \And before the third author name.
\author{%
Vincenzo~Collura \\
%\thanks{Use footnote for providing further information
%about author (webpage, alternative address)---\emph{not} for acknowledging
%funding agencies.} \\
University of Luxembourg \\
Luxembourg \\
\texttt{vincenzo.collura@uni.lu} \\
% examples of more authors
\And
Karim~Tit \\
University of Luxembourg \\
Luxembourg \\ \texttt{karim.tit@uni.lu} \\
\And
Laura~Bussi \\
University of Luxembourg \\
Luxembourg \\
\texttt{laura.bussi@uni.lu} \\
\And
Eleonora~Giunchiglia \\
Imperial College \\
London \\
\texttt{e.giunchiglia@imperial.ac.uk} \\
\And
Maxime~Cordy \\
University of Luxembourg \\
Luxembourg \\
\texttt{maxime.cordy@uni.lu} \\
% Coauthor \\
% Affiliation \\
% Address \\
% \texttt{email} \\
% \AND
% Coauthor \\
% Affiliation \\
% Address \\
% \texttt{email} \\
% \And
% Coauthor \\
% Affiliation \\
% Address \\
% \texttt{email} \\
% \And
% Coauthor \\
% Affiliation \\
% Address \\
% \texttt{email} \\
}
\begin{document}
\maketitle
\begin{abstract}
Large Language Models (LLMs) and other neural architectures have achieved impressive results across a variety of generative and classification tasks. However, they remain fundamentally ill-equipped to ensure that their outputs satisfy temporal constraints, such as those expressible in Linear Temporal Logic over finite traces (\ltlf). In this paper, we introduce \model{}: a general and model-agnostic inference-time algorithm that guarantees compliance with such constraints without requiring any retraining. \model{} compiles \ltlf{} formulas into a Deterministic Finite Automaton (DFA), which is used to guide a constrained variant of beam search. At each decoding step, transitions that would lead to constraint violations are masked, while remaining paths are dynamically re-ranked based on both the model’s probabilities and the DFA’s acceptance structure. We formally prove that the resulting sequences are guaranteed to satisfy the given \ltlf{} constraints, and we empirically demonstrate that \model{} also improves output quality. We validate our approach on two distinct tasks: temporally constrained image-stream classification and controlled text generation. In both settings, \model{} achieves perfect constraint satisfaction, %being in par with the state of the art for what concerns standard metrics.
while comparison with the state of the art shows improved efficiency and high standard quality metrics.
\end{abstract}
% \begin{comment}
% and demonstrate that MAP inference under minimal unary constraints (such as positional equality) is NP-hard even for simple first-order Markov chains. This complexity result reveals fundamental limits on the tractability of constrained inference, challenging common assumptions about Tractable Probabilistic Models. \end{comment}
\section{Introduction}
\input{paper/introduction.tex}
\section{Problem Statement and Notation}\label{sec:notation}
\input{paper/statementAndNotation}
% \section{Background}\label{sec:back}
%\input{background.tex}
\section{The \model{} Algorithm}\label{sec:contrib}
\input{paper/contribution.tex}
\section{Theoretical Analysis}\label{sec:theor}
\input{paper/theoretical}
\section{Experimental Evaluation}\label{sec:exper}
\input{paper/experiments.tex}
\section{Related Work}\label{sec:related}
\input{paper/related.tex}
\section{Conclusions}\label{sec:conclusions}
\input{paper/conclusions.tex}
\bibliographystyle{unsrtnat}
\bibliography{paper/DFALayer}
%\input{paper/checklist}
\newpage
\appendix
\section{Proofs}
\input{paper/proofs.tex}
\section{Hardware for Experiments}
\input{paper/hardware.tex}
\section{Ordered Fashion MNIST}
\label{ordered_fashion_mnist}
\input{paper/ordFMAppendix.tex}
\section{Ordered CommonGen}
\input{paper/ordCGAppendix.tex}
%\input{algorithms.tex}
\end{document}
% MC: reworked introduction. Experiments and results still have to be updated.
Machine-learning systems -- propelled by deep neural networks, transformers, and large language models -- have become the de-facto engines behind vision, language, and decision-making applications that impact millions of lives every day. The growing spread of these methods, however, poses several challenges. One is their oftentimes unexpected behavior, as they often offer little assurance that their predictions obey essential domain-specific requirements. This is an open problem that different communities have tried to tackle in orthogonal ways.
Neurosymbolic AI methods express requirements as logical constraints and introduce these constraints either in the loss function~\citep{xu2018semantic,LTN,diligenti2017sbrnn} (to nudge the predictions to be compliant) or as an additional layer~\citep{giunchiglia2021jair,ahmed2022spl,manhaeve2018deepproblog} (to restrict the output space to the space defined by the constraints, making the model compliant by design). A limitation of these methods, however, is that they do not support temporal constraints, which would enable specifying requirements over the temporality of output sequences. For example, in the text generation domain, temporal requirements may impose that not only a specific set of words should appear (a problem considered by previous methods~\citep{Lin2020}), but also that they should appear in a given order. The satisfaction of these requirements is essential to enhance consistency and, as later demonstrated in our experiments, it enables a general improvement of the quality of the generated sequences.
In the specific case of LLMs, constrained text generation methods were designed to either (i) constrain the beam search with logical constraints~\citep{Lu2021,Lu2022}, (ii) use auxiliary models to steer the generation~\citep{krause2021gedi,zhang2024ctrlg}, or (iii) treat constraints as conditioning and sample from the posterior~\citep{Miao19sampling,loula2025smc}. While these methods can theoretically support temporal requirements, their capability in doing so has not been studied. However, our analyses reveal that there is no method that simultaneously (i) guarantees the satisfaction of the constraints, (ii) does not require finetuning/training an additional model, (iii) has low latency and, most importantly, (iv) retains a high quality of the generated text.
To overcome all these limitations, we propose \model{}: a model-agnostic method able to constrain any autoregressive model with temporal constraints. Specifically, we express constraints in Linear Temporal Logic on Finite Traces (\ltlf), which offers an adequate balance between expressivity and computational tractability. Given an \ltlf{} formula, our method builds an equivalent Deterministic Finite Automaton (DFA), which by design represents the set of sequences accepted by the formula. This DFA can be executed on the model outputs to determine whether or not the sequence satisfies the temporal constraint. More importantly, we compile the transition matrix of the DFA and develop a novel Beam Search process guided by this matrix. This enhanced Beam Search guides the model to avoid producing outputs that violate the temporal constraint and enforces its satisfaction by the end of the generation.
We demonstrate the wide applicability of our method through two different use cases: image sequence classification and constrained text generation.
% MC: I stopped there. We have to clarify the evaluation criteria, mention baselines, and summarize results with numbers.
The results on image classification show that we can improve the accuracy while also enforcing constraint satisfaction. We then test our method on the challenging constrained text generation task, and in particular on the CommonGen challenge, and we compare our results with all the state-of-the-art methods (e.g.,~\citep{zhang2024ctrlg}). Our results confirm that not only are we able to guarantee the satisfaction of the constraints, but we also improve on or closely match state-of-the-art results on quality metrics. Finally, we show that \model{} has a low overhead compared to its competitors and produces high-quality results with a significantly lower computational footprint, as evidenced by our shorter runtimes for a fixed number of beams. The code for the experiments will be made available on github and is now in the supplementary materials.
%MC: imo we can remove this
\begin{comment}
The rest of the paper is organized as follows. In Section~\ref{sec:notation} we introduce the notation and problem statement. In Section~\ref{sec:contrib} we present the \model{} algorithm. Section~\ref{sec:theor} presents some theoretical results. In Section~\ref{sec:exper} we present the experimental evaluation of the algorithm on image classification and constrained text generation. In Section~\ref{sec:related} we give an overview of the related literature. In Section~\ref{sec:conclusions} we draw conclusions and highlight possible future work.
%In Section~\ref{sec:back} we introduce background and notation about \ltlf and automata.
\end{comment}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% PREVIOUS VERSIONS
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Machine-learning systems—propelled by deep neural networks,
% transformers, and large language models—have become the de-facto engines behind vision, language, and decision-making applications that touch millions of lives every day. Nevertheless, the growing spread of these methods poses several challenges. One among many is their oftentimes unexpected behaviour, as they often offer little assurance that their predictions obey the domain-specific requirements. This is an open problem that different communities have tried to tackle in orthogonal ways. For example, in the neurosymbolic AI community requirements are often expressed as logical constraints that are either introduced in the loss function~\citep{xu2018semantic,LTN,diligenti2017sbrnn} to nudge the predictions to be compliant, or in a layer~\citep{giunchiglia2021jair,ahmed2022spl,manhaeve2018deepproblog} which modifies the output space of the model to be same as the space defined by the constraints, thus making the model compliant by design. More recently, this problem has seen a surge of interest in the language generation domain, as LLMs often struggle to comply with strict directives. In the constrained text generation domain, people have followed three main streams: (i) some methods~\citep{Lu2021,Lu2022} constrain the beam search with logical constraints, (ii) some other~\citep{krause2021gedi,zhang2024ctrlg} use auxiliary models to steer the generation and (iii) the remaining ones~\citep{Miao19sampling,loula2025smc} treat constraints as conditioning and sample from the posterior. The limitations of the methods from the neurosymbolic AI community is that they cannot support temporal constraints, while in the constrained text generation domain there is no method that simultaneously (i) guarantees the satisfaction of the constraints, (ii) does not require finetuning and/or training of an additional model, (iii) has low latency, and most importantly (iv) retains a high quality of the generated text.
% In this paper, we propose \model{}: a model-agnostic method able to constrain any autoregressive model with temporal constraints expressed in Linear Temporal Logic on Finite Traces (\ltlf) and has all the properties listed above. Given an \ltlf{} formula, our method builds an equivalent Deterministic Finite Automaton (DFA) which is used to calculate: (i) the paths on the DFA that lead to {\sl deadlock states}, i.e., non-accepting states of the automaton that have no outgoing transitions, and (ii) the distance to to the closest accepting state. Informally, if we reach an accepting state in the automaton then the constraints are satisfied. This formulation allows us to modify the beam search in order to avoid the deadlock states, and to select ``promising paths'' that lead to constraint satisfaction. To prove the generality of our method, we test it on two very different scenarios. In the first we have to classify images belonging to a stream such that the predictions conform with the constraints. We compare our approach... and the results show that... We then test our method on the challenging constrained text generation task, and in particular on the CommonGen challenge and we compare our results with all the state-of-the-art methods (e.g.,~\citep{zhang2024ctrlg}). Our results confirm that not only we are able to guarantee the satisfaction of the constraints, but we are also able to improve the scores... Finally, we also show that our method introduces very low overhead when compared to its competitors and is able to produce very high quality results even with low exploration abilities (i.e., with small beam size).
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% EG: I wrote an alternative beginning of the intro. It is just a draft, feel free to improve/modify/delete it.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% \begin{comment}
% In recent years, the rise of machine learning methods has deeply impacted society. The spreading of tools based on neural networks has dramatically changed how we perform different tasks, and enhanced new, efficient, and effective approaches to difficult problems. Let us think e.g. of image classification, or text generation. Neural Networks are used to perform all of these and other crucial tasks in everyday life.
% \end{comment}
% In recent years, the rise of machine learning methods has deeply impacted society. The spreading of tools based on neural networks has dramatically changed how we perform different tasks, and enhanced new, efficient, and effective approaches to difficult problems. In particular, the impact of Deep Neural Networks, unsupervised methods, transformers, and Large Language Models is changing many aspects of everyday life. A growing number of people and companies rely on such methods to efficiently perform critical tasks that range over a variety of domains, as e.g. computer vision or Natural Language Processing.
% Nevertheless, the growing spread of these methods poses several challenges. Among these, ensuring their trustworthiness is a major one. Indeed, many applications involve critical aspects in safety and society: a typical example of this is image classification, which is used in safety-critical applications like autonomous driving, where a prediction error may result in a cost in human lives. But this is not the only case where we may need to enforce some warranty on the output of a machine learning method. A recent example is that of text generation, where the presence of toxic language in the training data can result in content affected by ethnic or gender bias. Hence, in order to avoid such situations, it may be the case that we want the output of a network to satisfy a certain constraint. This issue was addressed in many recent works, for example for what concerns constrained output generation using Large Language Models~\citep{Lu2021,Lu2022,Zhang2023,Zhang2024} and multi-label classification problems with formally expressed requirements, as introduced in~\cite{manhaeve2018deepproblog,ahmed2022spl,Giunchiglia2023}.
% The task of constrained text generation has been recently studied, and the community proposed some benchmarks, like e.g. CommonGen~\footnote{\href{https://inklab.usc.edu/CommonGen/index.html}{https://inklab.usc.edu/CommonGen/index.html}}~\citep{Lin2020}, to test the ability of LLMs to generate natural sentences containing a given set of words. The usual approach to the problem is to mask at each step all the outputs that may violate the constraint. This is a greedy approach, that can penalize tokens that would not break the constraint, while unnaturally leading to sentences that satisfy the constraint, but does not make sense semantically. Our aim is to provide a method that leads to constraint satisfaction, while generating sentences having good sense.
% In this paper we propose a novel, general algorithm to constrain a Neural Network's output over temporal requirements. Existing work mainly addresses constraints expressed using Propositional Logic. This limits their applicability to problems where the temporal axis is not considered, i.e. the evolution of data over time is not taken into account. In our case, we also consider the temporal dimension. A prominent example of this is video stream analysis, where the output of the network at time $t$ may be somehow related to the output at time $t-1$. In our method, we first state the formula to enforce using Linear-Time Temporal Logic on Finite Traces (\ltlf). Given such formula, we build the associated, accepting automaton and we apply it as a further layer to the network. The output is then further refined using a variant of Beam Search, that takes into account the distance in the DFA from the current state to an accepting one to compute the most promising paths. This allows us to avoid outputs that violate the formula, and to select ``promising paths'' that lead to constraint satisfaction. It is worth noting that our approach supports any requirements over NNs' generated output that can be expressed as regular languages: throughout the paper, we will show applications to image streams classification using CNNs, as well as to constrained text generation using LLMs.
Let $f_\theta$ be a neural network with learnable weights $\theta$. In this paper, we suppose that the network generates a finite sequence of $n$ outputs of maximum length $T$ (note that $T$ might vary from one sequence to another), which we will denote by $x_{1:n}$, with $n \le T$. This is a reasonable assumption, as in many tasks (including text generation), neural networks are trained with sequences of finite length. Similarly, we refer to the sequence produced up to the $t$-th time step as $x_{<t}$. Given a sequence $x_{1:n}$, $x_t \in \mathcal{X}$ represents the $t$-th element of the sequence, while $\mathcal{X}$ is the set of possible values that for every sequence and for every $t=1, \ldots, n$, $x_t$ can take. %Given the outputs of the neural network,
Finally, we denote by $p_\theta(x_t \mid x_{<t})$ the probability of emitting the output $x_t$ given the already generated sequence $x_{<t}$.
Our objective is to ensure that, given a neural network $f_\theta$, every sequence $x_{1:n}$ generated by $f_\theta$ is compliant with specified temporal requirements. We assume these requirements to be expressed as an \ltlf{}~\citep{Vardi2013} formula $\phi$ over the set of atomic propositions $\mathcal{A}$. Each atomic proposition might correspond to one of the possibles values of the outputs, and hence given a sequence $x_{1:n}$, we have for example that $x_t \models a$ iff $a \in x_t$. However, sometimes---like in the text generation case---we might not want to write the requirements over the outputs, i.e., the tokens, but rather on higher level concepts, i.e., the words. In these cases, each atomic proposition corresponds to a {\sl concept} $c \in \mathcal{C}$, where $\mathcal{C}$ is user-defined. Given the set of all the output sequences $\mathcal{X}^*$ and the set $\mathcal{C}^*$, we assume that there exists an injective function $\nu:\mathcal{X}^* \to \mathcal{C}^*$ such that $\nu(x_{1:n}) = c_{1:k}$. In the text generation case, indeed, given a sequence of tokens $x_{1:n}$ we can always deterministically compute the set of words $c_{1:k}$. In the remaining of the paper, we will assume that each atomic proposition corresponds to a concept, and that if they directly correspond to the outputs then $\nu(x_{1:n}) = x_{1:n}$.
% $x_{1:n}$ and an injective function $\nu$,
% Each of the atomic propositions corresponds to a concept $c \in \mathcal{C}$, where $\mathcal{C}$ represents
% Given a sequence of outputs $x_1, \ldots, x_n$, we suppose there exists an function $\nu: \mathcal{X}^* \to \mathcal{C}^*$
%each corresponding to one of the possible values the neural network can emit at every time step $t$.
\begin{definition}
Let $\mathcal{A}$ be a finite set of atomic propositions. \ltlf formulas are generated by the grammar:
\[
\phi ::= \top \mid a \mid \lnot \phi \mid \phi \, \land \, \phi \mid \mathsf{X} \, \phi \mid \phi_1 \, \mathsf{U} \, \phi_2, \qquad \qquad a \in \mathcal{A}.
\]
\end{definition}
%In the above definition $\top$ stands for {\sl true}, $\mathsf{X} \, \phi$ stands for {\sl next} $\phi$ and $\phi_1 \, \mathsf{U} \, \phi_2$ stands for $\phi_1$ {\sl until} $phi_2$.
\ltlf is interpreted on \emph{finite traces}, namely finite words (or sequences) $w$ on the alphabet of $2^\mathcal{A}$. $length(w)$ is the length of the trace, with $length(w) \in \mathbb{N}$. We denote by $w(t)$ the element $t$th of the sequence with $0 \leq t \leq length(w) - 1$.
\begin{definition}
The satisfaction of a formula $\phi$ at a given instant $t$ is defined via the following set of equations:
\[
\begin{array}{l c l c l c l l}
w,t \models \top \ \forall t .\ 0 \leq t < length(w); \qquad \qquad \qquad \!\!\!\!
w,t \models \lnot \phi \iff w,t \not \models \phi; \\
w,t \models a \ \text{ for } \ a \in \mathcal{A} \iff a \in w(t); \qquad \quad \quad
w,t \models \phi_1 \land \phi_2 \iff w,t \models \phi_1 \ \text{ and } \ w,t \models \phi_2;\\
w,t \models \mathsf{X} \phi \iff w,t+1 \models \phi;\\
w,t \models \phi_1 \, \mathsf{U} \, \phi_2 \iff \exists j .\ j < length(w), \ w,j \models \phi_2 \ \text{ and } \ \forall k .\ t \leq k < j \Rightarrow w,k \models \phi_1.
\end{array}
\]
\end{definition}
We say that a formula $\phi$ is \emph{satisfied} in $w$ (noted $w \models \phi$) iff $w,0 \models \phi$. %EG: do we need the defintion of valid? we did not define the word interpretation.
%and that $\phi$ is \emph{valid} if it is true in all interpretations.
% When defining an \ltlf formula, the set of atomic propositions we can use is the set of \emph{concepts}. We distinguish a concept $c \in C$, with $C \subseteq \mathcal{A}$ from an output $x_t$ as these may differ in practice: consider, for instance, the task of constrained text generation. A constraint will express the fact that some words must appear in the generated sentence, but outputs are tokens. We thus have to formally define a map from tokens to concepts.
% \begin{definition}
% Let $\mathcal{X}^*$ be the set of all output sequences, $C^*$ the set of all concept sequences. We define $\nu : \mathcal{X}^* \to C^*$ as $\nu(x_1,...,x_n) = c_1,...,c_k$, the sequence of concepts obtained by concatenating outputs $x_1,...,x_n$.
% \end{definition}
% By this definition, we have that $x_{1:T} \models \phi \iff \nu(x_{1:T}) \models \phi$.
More formally, given a neural network $f_\theta$, and a set of constraints expressed as an \ltlf{} formula $\phi$ over the atomic propositions $\mathcal{A}$, we target the problem of ensuring that for every sequence $x_{1:n}$ generated by $f_\theta$, we have $\nu(x_{1:n}) \models \phi$.
Now for a given sequence and its corresponding maximum length $T$, let $\mathcal{X}^T$ be the set of all sequences of length $T$. Then, the mathematical formulation of the problem as an optimization program is the following:
\begin{equation}\label{eq:MAP}
\begin{aligned}
x^*_{1:T} = \underset{x_{1:T} \in \mathcal{X}^T, \nu(x_{1:T}) \models \phi}{\text{argmin}} - \Sigma_{t = 1}^T \log p_{\theta}(x_t \mid x_{<t}),
\end{aligned}
\end{equation}
which corresponds to the \textit{Maximum A Posteriori} (MAP) inference problem under \ltlf{} constraints.
%where $\mathcal{X}^*_{<T}$ indicates the set of all possible sequences with length up to $T$.
%for $\phi$ a given constraint and given length $T$ of the output sequence.
%Note that for non-autoregressive models, as for instance CNNs, we can state the problem equivalently as:
\begin{comment}
\begin{equation*}
\begin{aligned}
x^*_{1:T} = \underset{x_{1:T} \in \mathcal{L}, x_{1:T} \models \phi}{\text{argmin}} - \Sigma_{t = 1}^T log \ P_{NN}[x_t]
\end{aligned}
\end{equation*}
\end{comment}
% Given a \ltlf{} formula $\phi$, it is always possible to build a Deterministic Finite Automaton (DFA) $A_\phi$ that accept exactly the set of finite sequences satisfying $\phi$.
% \begin{definition}
% A DFA is a 5-tuple $(Q,2^\mathcal{A},\delta,q_0,F)$, where $Q$ is the set of all states, $2^\mathcal{A}$ is the alphabet of input symbols, $\delta : Q \times 2^\mathcal{A} \to Q$ is the transition function, $q_0$ is the initial state, $F$ is the set of accepting states.
% \end{definition}
% Let $w = w_0,...,w_n$ be a sequence in the alphabet $2^\mathcal{A}$: we say that a DFA \emph{accepts} $w$ iff there is a sequence of states $s_0,...,s_n$ such that $s_0 = q_0$, $s_{i+1} = \delta(s_i,w_{i+1})$ for $0 \leq i < n$, $s_n \in F$.
% \begin{definition}
% We are given a NN $N$, input data $I$ and an \ltlf formula $\phi$. Let $x_{1:T}$ be the output sequence generated by $N$ from data $I$, and $m : X \Rightarrow P$ a function that maps outputs to atomic propositions. a set of atomic propositions, with $C \subseteq P$. We want $m(x_1)...m(x_T) \models \phi$.
% \end{definition}
\begin{comment}
In this section, we introduce the notation and formal statement of the problem that we aim to address.
Along all the paper, we denote a logical constraint by $\phi$, and the corresponding automaton by $A_\phi$. We indicate as \emph{deadlock states} non-accepting states of the automaton that have no outgoing transitions (i.e. states that are only reachable via traces that falsify $\phi$). Greek letters $\alpha, \beta, \gamma...$ denote parameters of a Neural Network (NN for short) $N$. By lower case $t$ we denote an instant in task execution. The $t^{th}$ output emitted by the network is denoted by $x_t$, while the sequence of length $T$ is indicated as $x_{1:T}$. Similarly, we denote the sequence produced up to time $t$ as $x_{<t}$. We denote by $C$ a set of \emph{concepts} output by a network, where $c \in C$ can be, for instance, a class in an image classification task or a word in the task of text generation. We thus have that, for $P$ a set of atomic propositions, $C \subseteq P$. We denote the probability of emitting output $x_t$ by $P_{NN}(x_t \mid x_{<t})$. Note that we distinguish $x_t$ from an output concept $c$: this is due to the fact that these two may differ. Indeed, in the case of text generation, the $t^{th}$ output is a token, while a concept $c$ is a word. We will go into details on this when addressing the problem of constrained text generation. Upper case $T$ thus denotes the length of the sequence of outputs emitted by the network, while the sequence of concepts might be shorter. We formulate the problem statement according to these considerations.
\end{comment}
\begin{comment}
\subsection{Problem description}
Let us look in more detail at the problem of analyzing image sequences. In this case, the input of the Neural Network is a stream of images, that we denote by $S$. For each image $s \in S$, the network $N$ makes some predictions and outputs a probability vector. We want this probability vector to be constrained to have $0$ probability for classes that are not allowed to be detected in the image.
%Intuitively, we want the output of the network to be constrained by the formula $\phi$.
Let us consider again the semaphore example: as long as the semaphore is red in image $s_{i-1}$, we want the output probability to be $0$ for the class $yellow$ on image $s_i$. Of course, this is enough if we consider the task of classifying images. It is easy to see that generative tasks, such as text generation, also involve less formal requirements. In particular, we do not want only the constraint to be fulfilled, but also the text to have good quality and to make sense from a common sense perspective. We will see in the following how we can enforce this on the output by means of heuristics.
The problem can be thus described as follows:
\medskip
\begin{definition}
We are given a NN $N$, a sequence of inputs $s_1,...,s_n$, and an \ltlf formula $\phi$. We consider the set of predictions $P$ as atomic propositions. Let $p_1,...,p_{n-1}$ be a sequence of atomic propositions classified by $N$ on $s_1,...,s_{n-1}$. We want $o_n(p) = 0$ for $o_n(p)$ the output probability of prediction $p$ on input $s_n$ if the trace $p_1,...,p_{n-1},p$ falsifies $\phi$.
\end{definition}
\end{comment}
\begin{comment}
\begin{figure}[t]
\centering
\begin{minipage}{.5\textwidth}
\begin{center}
\begin{tikzpicture}[shorten >=1pt,node distance=2.5cm,on grid,auto]
\node[state,initial,accepting] (1) {$1$};
\node[state] (2) [right=of 1] {$2$};
\node[state] (3) [right=of 2] {$3$};
\path[->]
(1) edge[bend left] node {$r \land \lnot g$} (2)
edge [loop above] node {$g \lor \lnot r$} ()
(2) edge[bend left] node {$g$} (1)
edge [loop above] node {$r \land \lnot g$} ()
edge node {$\lnot g \land \lnot r$} (3)
(3) edge [loop above] node {$\top$} ();
\end{tikzpicture}
\end{center}
\end{minipage}%
\begin{minipage}{0.5\textwidth}
\begin{center}
\begin{tabular}{ |p{0.5cm}||p{0.5cm}|p{0.5cm}|p{0.5cm}| }
\hline
& $r$ & $g$ & $y$\\
\hline
1,1 & 0 & 1 & 1\\
\hline
1,2 & 1 & 0 & 1\\
\hline
2,2 & 1 & 0 & 0\\
\hline
2,3 & 0 & 0 & 1\\
\hline
3,3 & 1 & 1 & 1\\
\hline
\end{tabular}
\end{center}
\end{minipage}
\caption{A DFA accepting traces that make the formula $\mathsf{G}(r \to r \, \mathsf{U} \, g)$ true, and the corresponding matrix.}\label{fig:semaphore}
\end{figure}
\end{comment}
\newcommand{\disttoaccept}{\texttt{dist}_{\phi}}
In this section, we present our method to constrain the output of an auto-regressive model over a given \ltlf formula $\phi$. Our procedure can be divided into two fundamental steps: (i) the static {\sl DFA-compilation step}, where we take the \ltlf{} formula, compile it into a Deterministic Finite Automaton (DFA), and then compile it into a transition matrix, and (ii) the dynamic {\sl DFA-Enhanced Beam Search} where the Beam Search is guided both by the model's prediction and the DFA.
\begin{figure}[t]
\centering
\begin{minipage}{.61\textwidth}
\begin{center}
\includegraphics[width=1.0\textwidth]{paper/figs/AutomatonExample.pdf}
\end{center}
\end{minipage}%
\begin{minipage}{0.39\textwidth}
\begin{center}
\renewcommand{\arraystretch}{1.4}
\begin{tabular}{|@{}>{\centering\arraybackslash}m{0.45cm}@{}|
@{}>{\centering\arraybackslash}m{1.1cm}@{}|
@{}>{\centering\arraybackslash}m{2.1cm}@{}|
@{}>{\centering\arraybackslash}m{1.1cm}@{}|}
\hline
& Cat & Politician & EOS\\
\hline
s1 & 1, s3 & 3, s2 & 1, s4\\
\hline
s2 & 1, s5 & 3, s2 & 1, s4\\
\hline
s3 & 1, s3 & 3, s5 & 1, s4\\
\hline
s4 & 1, s4 & 3, s4 & 1, s4\\
\hline
s5 & 1, s5 & 3, s5 & 1, s6\\
\hline
s6 & 1, s6 & 3, s6 & 1, s6\\
\hline
\end{tabular}
\vspace{0.5em}
\footnotesize
Distances: $s_1\!=\!5$, $s_2\!=\!2$, $s_3\!=\!4$, $s_4\!=\!\infty$, $s_5\!=\!1$, $s_6\!=\!0$
\end{center}
\end{minipage}
\caption{A DFA equivalent to the formula in Example \ref{par:semaphoreExample} and the corresponding matrix. The deadlock state is s4 (red) and the acceptance state is s6 (green). For easier visualization, edges with more than one true atomic proposition have been cut off, as it is never the case that two words are generated at the same time. We also omitted negated atomic propositions when there is at least another true one. %To understand Example 1, these will not be necessary as an LLM can only predict one output at a time.
The rows of the transition matrix represent states and the columns represent concepts. In each cell, the first element is the number of outputs needed for an LLM to generate the concept (1 for cat, 3 for politician and 1 for EOS). The second element is the state reached after generating the concept.}
\label{fig:semaphore}
\end{figure}
\subsection{DFA Compilation Step}
The first step is to compute the DFA equivalent to the formula. Given an \ltlf{} formula $\phi$, it is always possible to build a DFA $A_\phi$ that accepts exactly the set of finite sequences satisfying $\phi$~\citep{ltlf_compilation}. Each DFA can then be represented as a transition matrix.
\begin{definition}
A DFA is a 5-tuple $(Q,2^\mathcal{A},\delta,q_0,F)$, where $Q$ is the set of all states, $2^\mathcal{A}$ is the alphabet of input symbols, $\delta : Q \times 2^\mathcal{A} \to Q$ is the transition function, $q_0$ is the initial state, and $F$ is the set of accepting states.
\end{definition}
Let $w = w_0,...,w_n$ be a sequence in the alphabet $2^\mathcal{A}$: we say that a DFA \emph{accepts} $w$ iff there is a sequence of states $s_0,...,s_n$ such that $s_0 = q_0$, $s_{i+1} = \delta(s_i,w_{i+1})$ for $0 \leq i < n$, $s_n \in F$. On the contrary, we will say that a state is a {\sl deadlock state} if it is a non-accepting state from which no accepting state is reachable via any sequence of transitions.
In our settings, we work on finite traces whose length $T$ is not known at the time the temporal logic formula is compiled into an automaton. Instead, $T$ is provided only later, at runtime, when the trace is generated and checked. As a result, the automaton must be constructed to operate correctly on traces of any finite length, without relying on a specific bound. This places our approach within the framework of Linear Temporal Logic on Finite Traces (\ltlf), rather than Bounded Linear Temporal Logic (B-LTL), where the bound $T$ is assumed to be known and is used to constrain the semantics of temporal operators when compiling to an equivalent automaton. For each state $q$, we also calculate the set $\mathcal{R}_{q}$ of states that are reachable from $q$, and then associate to each pair $(q, q')$, %where for every $q' \in \mathcal{R}_{q}$
a number representing the distance from $q$ to the closest accepting state computed using the Dijkstra algorithm~\citep{dijkstra1959note}. The full pipeline is summarized in (\ref{pipeline}).
%Differently from a simple transition matrix, ours does not just encode which how to reach a state from another, but it also incorporates the information on how the distance to the closest accepting state changes when we move from each state to the next. In particular, given
% Notice that by definition the distance
\begin{example}\label{par:semaphoreExample}
Consider a simple formula \ltlf defining the rules that an LLM must follow when generating a text. We want the words \emph{cat} and \emph{politician} to appear at least once before the End Of Sequence (EOS). The desired formula $\phi$ is
\protect\(
\left( (\lnot \text{eos} \mathbin{U} \text{cat}) \land \mathsf{F}(\text{cat}) \right)
\land
\left( (\lnot \text{eos} \mathbin{U} \text{politician}) \land \mathsf{F}(\text{politician}) \right)
\land
\mathsf{F}(\text{eos})
\).
The automaton that accepts $\phi$ and the corresponding transition matrix are shown in figure \ref{fig:semaphore}. With the transition matrix, it is then simple to calculate the distance from each state to an acceptance state using Dijkstra's algorithm.
\end{example}
\begin{equation}
\label{pipeline}
\phi: \text{\ltlf Formula}
\underbrace{\longrightarrow}_{ \text{LTLf2DFA Comp.}}
\mathcal{G}_{\phi}:\mathrm{\text{DFA graph } }
\underbrace{\longrightarrow}_{\text{Djikstra Alg.}}
\mathrm{ \disttoaccept: \text{Distance to accep. states} }
\end{equation}
\begin{comment}
\begin{figure}[t]
\centering
\begin{minipage}{\textwidth}
\begin{center}
\includegraphics[width=\textwidth]{paper/figs/AutomatonExample.pdf}
\end{center}
\end{minipage}
\end{figure}
\end{comment}
\newcommand{\copyz}{Z}
\begin{algorithm}[t]
\caption{Pseudo-Code of the \model{} Beam Search Algorithm}\label{alg:TRIDENT}\begin{algorithmic}[1]
\STATE \textbf{Input:} Prompt $x_0$, Function $p_{\theta}$, DFA transition function $\delta$, distance function to accepting states $\disttoaccept: Q \mapsto \mathbb{R}_+ \cup {+\infty}$, number of beams $k$, Ramping Push Up parameters $\alpha_{min}, \gamma$
\STATE Initialize beams with initial sequence $x_0$, score and state $\mathcal{B} \gets \{(x_0, s=0, q_0)\}$
\FOR{$t = 1$ to $T$}
\STATE Compute next outputs scores $Z \gets \log p_{\theta}(\mathcal{B}) \in \mathbb{R}^{k \times |\mathcal{X}|}$
%\STATE Make a copy $\copyz$ of $Z$
\FOR{beam $i = 1$ to $|\mathcal{B}|$}
\STATE Fetch output sequence $x_{<t}$ and current score $s_i$ of beam $i$
\STATE Fetch current state $q_i$ of beam $i$ and its distance from an accepting state $d_i$
\STATE Compute push strength $\alpha_i \gets \textsc{RampPushUp} (\alpha_{min},d_i,T-t,\gamma)$ (see Eq. (\ref{eq:ramp}))
\FOR{output $x = 1$ to $|\mathcal{X}|$}
\STATE $q' \gets \textsc{NextState}(q_i, x,x_{<t})$
\STATE $q'' \gets \textsc{BestQuasiNextState}(q_i, x, x_{<t})$
\IF{$\disttoaccept(q') > T - t$}
\STATE $\copyz[i, x] \gets -\infty$
\ELSIF{$\disttoaccept(q') < d_i$}
\STATE $\copyz[i, x] \gets \alpha_i \cdot \max (Z[i, :]) + (1{-}\alpha_i + 2\alpha_i\epsilon) \cdot Z[i, x]$
\ELSIF{$\disttoaccept(q'') < d_i$}
\STATE $\copyz[i, x] \gets \alpha_i \cdot \max (Z[i, :]) + (1{-}\alpha_i + \alpha_i\epsilon) \cdot Z[i, x]$
\ENDIF
\STATE Compute score of $[x_{<t},x]$: $\copyz[i,x] \gets \copyz[i,x] + s_i$
\ENDFOR
\ENDFOR
\STATE Select top-$k$ sequences according to $\copyz$, update $\mathcal{B}$ with new sequences, scores and states
\ENDFOR
\STATE Re-rank sequences in $\mathcal{B}$ according to their natural log-likelihood for $f_\theta$
\RETURN First sequence in $\mathcal{B}$
\end{algorithmic}
\end{algorithm}
\subsection{DFA-Enhanced Beam Search}
The intuition behind the DFA-Enhanced Beam Search is twofold: on one hand, we want to ensure that the model does not end up in a deadlock state, while on the other, we want to promote the exploration of the DFA towards accepting states.
% Information about the DFA is then added as a ``further layer'' to the network. %We know the length of the sequence to be emitted to be $T$.
% In particular, we consider the distance from any state in the DFA to the closest accepting state as the relevant information to avoid deadlock states. Using these distances in our modified Beam Search, on the one side we can prune outputs leading to such states, and promote on the other side NN outputs that lead to states at smaller distances from an accepting state.
%\paragraph{Avoidance of deadlock states}
%We propose an algorithm to constrain the output of a NN $N$ that exploits the DFA construction starting from an \ltlf formula $\phi$. In a DFA, we call a \emph{deadlock state} a state with no outgoing transitions.
% Remember that an output sequence $t$ satisfies a formula $\phi$ iff the execution of $t$ in the corresponding DFA terminates in an accepting state. It is trivial that sequences reaching a deadlock state cannot satisfy $\phi$, namely there is no path leading from such a deadlock state to an accepting state.
% During the compilation phase, for each state $q_i$, we calculate the set $\mathcal{R}_{q_i}$ of states that is reachable from $q_i$, and then associate to each pair $(q_i, q)$, where for every $q \in \mathcal{R}_{q_i}$ a number which represents the distance from $q$ to the its closest accepting states using the Dijkstra algorithm~\citep{dijkstra1959note}. During the beam search, at every step $i$, we can fetch the current state $q_i$ and we can then calculate the most promising next steps to take by simply taking all the pairs $(q_i, q)$ for $q \in \mathcal{R_{q_i}}$ and checking which are associated with the lowest distance.
At every step $k$, we fetch the current state $q_k$ and then calculate the most promising next steps to take by simply taking all the pairs $(q_k, q)$ for $q \in \mathcal{R}_{q_k}$ and checking which are associated with the lowest distance. For each state $q$ we will refer to the distance from $q$ to the closest accepting state as $d_q$. Notice that in the simplest cases we consider the cost of passing through an edge $=1$, but different applications might lead to different weights. For example, in the case of LLMs, we compute the cost of each edge as the minimum number of outputs required to build its transition label's concepts. It is easy to see that since we only add an output to our beam if its distance to the closest accepting state $d_q$ is $d_q \leq T - k$, then we will never add a deadlock state $q$ as $d_q = +\infty$.
% Notice that by definition the distance
% At each step $k$, we consider the distance from an accepting state associated with each state that is reachable via a transition from the current one. This is precomputed via the Dijkstra algorithm~\citep{dijkstra1959note}. Since there is no path leading from a deadlock state to an accepting one, the distance of deadlocks from any accepting states is $+ \infty$ by the algorithm, and of course $+ \infty > T - k$. Considering only candidates at distance $d_q \leq T - k$ is thus enough to rule out deadlock states from the search.
\begin{comment}
We can exploit this fact to rule out paths leading to deadlock states when performing Beam Search: if fewer than $T$ outputs are left to be generated, then we must stay within $T$ states of accepting states. It is clear that deadlock states do not satisfy this requirement and are thus to be avoided. This ensures our first goal, as we avoid states that for sure will lead to the violation of the constraint $\phi$.
Roughly speaking, we compute the transition matrix for the automaton accepting traces that make the formula $\phi$ true. Then we build a constraint matrix, that we denote by $M_C$, setting to $- \infty$ the pairs $(source,concept)$ such that $\delta(source,concept) = d$ for $d$ a deadlock state. We call a \emph{concept} an element from a set $P$ of atomic propositions, that may vary depending on the task. In the case of CNNs, the set of concepts $P$ contains the predictions that can be output by the network. In the case of LLMs, instead, the set $P$ contains the vocabulary of all the words in a given language. This further layer is then used to guide a customized beam search towards an accepting state, ensuring that a sequence of output concepts $X_{1:T}$ is such that $X_{1:T} \models \phi$.
\textbf{Building the DFA Layer}
Our aim is to perform a sum between the output vector and the column indexed by the considered state in the matrix $M_C^T$. This sets any transitions leading to a deadlock to $- \infty$. The constraint matrix $M_C$ is computed by first removing from $M$ all the rows indexed by pairs $(s,t)$, for $t$ a deadlock state. Then, rows indexed by pairs having the same $s$ state are collapsed into one row performing a logical $or$. In this way, if the atomic proposition $p$ does not cause a transition from state $s$ it is marked as $0$, otherwise with $1$. Finally, we transform $0$ into $- \infty$ and $1$ into $0$.
%For now, we will assume that the constructed DFA is already minimized, thus having only deadlock states with no deadlock components (e.g. cycles). A more general description of the algorithm is left as future work.
%Intuitively, this corresponds to only allowing transitions to non-deadlock states. Finally, we transform $0$ into $- \infty$ and $1$ into $0$, in order to get a suitable vector to be summed to the output vector. The detailed algorithm used to build the constraint matrix is reported in the Appendix as Algorithm~\ref{alg:DFALayer}.
\begin{lemma}[Correctness of the generated matrix]\label{theorem:constrMatrix}
Let $q$ be a state, $d$ be a deadlock state and $p$ such that $\delta(q,p) = d$. Then $M_C[q][p] = - \infty$.
\end{lemma}
\end{comment}
%\paragraph{Constraining the output}
%Let us now consider the subset of concepts that appear in a formula $\phi$: we denote this by $\mathcal{C}_\phi \subseteq \mathcal{A}$.
%When analyzing outputs of $f_\theta$, we must identify when a sequence of outputs represents a concept (that is, a transition label in the automaton), and promote or prune sequences containing concepts $c \in \mathcal{C}$ based on the resulting distance from an accepting state.
Recall that we defined an output match function $\nu : \mathcal{X}^* \to \sl \mathcal{C}^*$. Such a function is not bijective, but we can assume the existence of a \emph{canonical} function $\mu : \mathcal{C}^* \to \mathcal{X}^*$ that, given a sequence of concepts $c_1,...,c_k$ returns a canonical sequence of $f_\theta$'s outputs $x_1,...,x_n$ such that $\mu(c_1, \ldots,c_k) = x_1, \ldots, x_n$. We thus define a predicate:
\begin{comment}
However, this must be done iteratively by interpreting subsequences of outputs, in order to promote also those sequences that \emph{can be extended} to a concept $c \in C_\phi$. We thus define a partial interpretation function $[\![ .]\!] : \mathcal{X}^* \to W$ such that:
\begin{equation*}
([\![x_1...x_n]\!]) = \begin{cases}
w &\text{if $\nu(x_1...x_n) = w \in W$}\\
\bot &\text{otherwise}
\end{cases}
\end{equation*}
\end{comment}
%$$extends(x_1...x_n) = [\![x_1...x_n]\!] = \bot \land (\exists x_k...x_t \in \mathcal{X}^* . [\![x_1...x_nx_k...x_t]\!] \in \mathcal{C}_\phi)$$
$$\textsc{compatible}(x_{1}, \ldots, x_n ,c) \iff \exists . \text{\sl suffix} \in \mathcal{X}^* . \ \mu(c) = x_{1}, \ldots, x_n \text{\sl suffix}$$
We can now use this predicate to check if a sequence of outputs may lead to a transition in the future. We want to select the best candidate among states that are reachable from the current one. We assume to have a function $\textsc{last}(x_{<t})$ that, given the output history, returns the last (possibly incomplete) output suffix. We can thus compute the best candidate quasi-next state as:
$$\textsc{BestQuasiNextState}(\text{\sl current}, x, x_{<t}) =$$
$$\text{arg}\!\min_{q \in Q} \{ d_q \mid \exists c \in \mathcal{C}. \ \textsc{compatible}(\textsc{last}(x_{<t})x, c) \land \delta(\text{\sl{current}},c) = q \}$$
% Where $d_q$ is the distance of $q$ from an accepting state. For each state, $d_q$ is simply computed via the Dijkstra algorithm on the graph underlying the DFA, where costs are computed according to the task. For instance, in the case of CNNs, the cost of each edge is $1$, as $\nu(x_{1:n}) = x_{1:n}$ In the case of LLMs, we compute the cost of each edge as the minimum number of outputs required to build a transition label concept on it.
We now need a function that computes the actual next state. Note that, in the case of text generation, we are also interested in generating words that do not appear in the constraint, in order to get a sentence of common sense. We thus extend the set of atomic propositions $\mathcal{A}$ with a special value {\sl noMatch}, that represents the fact that the computed word does not match any concept, and we recompute the automaton accordingly. We define a function $\textsc{NextState}(\text{\sl {current}},x,x_{<t})$ as follows:
\begin{equation*}
\textsc{NextState}(\text{\sl {current}},x,x_{<t}) = \begin{cases}
\delta(\text{\sl {current}},c) &\text{if $\nu(\textsc{Last}(x_{<t})x) = c \in \mathcal{C}$}\\
\delta(\text{\sl {current}}, \text{\sl {noMatch}}) &\text{otherwise}
\end{cases}
\end{equation*}
The detailed pseudocode of the modified Beam Search is reported in Algorithm~\ref{alg:TRIDENT}, while a graphical representation referring to Example \ref{par:semaphoreExample} can be found in Figure \ref{fig:beamsearch}.
\begin{comment}
We can now produce a constrained output by considering the accepting condition of the DFA. Every time the Neural Network generates an output, we keep track of the associated DFA state. The generated output represents the label of a transition from one state of the automaton to another; then we can update the state of the NN accordingly. By considering distances to an accepting states, we can avoid transitions leading to utting transitions to deadlock states is not enough to guarantee the constraint to hold. Consider the case of image streams analysis: it can still be the case that the network misclassifies an image, thus leading to an incorrect state and compromising the correctness of the following outputs. On the other hand, blindly applying the constraint can lead to unnatural outputs, for instance, in the case of constrained text generation. We thus need to rule out paths leading to the constraint not being satisfied while maximizing the probability of ``good'' paths, namely paths that may lead to the constraint being fulfilled in the future, still having good natural probability to be generated by the NN. In the task of constrained text generation, this point is crucial: indeed, blindly forcing the constraint to be fulfilled immediately would lead to unnatural sentences, only containing the sequence of words that are required to appear. More formally, we end up with the following optimization problem:
\end{comment}
\begin{comment}
To deal with this problem, we implemented a modified version of the beam search algorithm. More precisely, we take into account both the natural probability of the network to output a certain \emph{concept}, as well as the need for the constraint to be satisfied. At each step, we select a set of candidate \emph{state changers}, namely labels that cause a transition from one state of the automaton to another. From these, we select candidates that have a high natural probability of being emitted by the NN, and we prune those being at a distance greater than $T$ to an accepting state. At step $k$, we use a parameter $\alpha_i$ to weight the NN probabilities and the distance from an accepting state in the DFA. In the following section, we explain how we can guide the output towards a sequence satisfying the formula $\phi$. The detailed pseudocode of the algorithm is reported in the Appendix.
\end{comment}
\textbf{Ramping Push Toward Accepting States}
\label{subsec:ramping}
We introduce a dynamic mechanism for encouraging the model to follow transitions in the DFA that move it closer to an accepting state. At each decoding step \(t\) and for each beam
$i$, we define a coefficient \(\alpha_i \in [\alpha_{\min}, 1]\) that controls how much we bias the logits of promising outputs toward the maximum logit. The coefficient \(\alpha_i\) increases as the number of decoding steps left \(T - t\) approaches the current DFA distance to acceptance \(d_i\). Let:
\begin{equation}
\label{eq:ramp}
\textsc{RampPushUp} (\alpha_{min},d_i,T-t,\gamma) = \alpha_{\min} + (1 - \alpha_{\min}) \cdot \min\left(1, \left( \frac{d_i}{T - t}
\right)^\gamma
\right),
\end{equation}
where \(\gamma > 0\) controls the sharpness of the transition. This schedule ensures that the model explores freely when there is slack (i.e., \(T - t \gg d_i\)) and ramps up pressure when approaching a deadline. We show the soundness of the resulting algorithm in the next section.
\begin{figure}[t]
\centering
\begin{minipage}{\textwidth}
\begin{center}
\includegraphics[width=0.9\textwidth]{paper/figs/dfa_enhanced_beam_search2.pdf}
\end{center}
\end{minipage}
\caption{Illustration of the DFA-Enhanced Beam Search applied to Example \ref{par:semaphoreExample}, with 3 beams, $\alpha$=0.5 and $\gamma$=1, It shows the outcomes of the NextState and QuasiNextState functions and how deadlocks are avoided.}
\label{fig:beamsearch}
\end{figure}
In this section we provide formal statements concerning the computational complexity of our inference tasks, soundness of our DFA-guided inference method, and comparison with existing work (Ctrl-G). Proofs of the stated theorems are reported in the Appendix.
\subsection{Soundness and Complexity of DFA-Enhanced Beam Search}
We first recall the nature of the problem at hand, explicted in Eq. (\ref{eq:MAP}), which is a constrained Maximum A Posteriori (MAP) inference problem over the output distribution of an auto-regressive neural model. MAP inference under logical constraints is known to be NP-hard in general, even when the model is a Bayesian network with treewidth 1~\citep{roth96}. Our setting considers more expressive temporal constraints (LTL$_f$) and long sequences over symbolic outputs, making exact inference intractable. Thus, we develop a structured approximate inference method that is sound and tractable in practice.
\begin{theorem}[Soundness of DFA-Guided Beam Search with Ramping \(\alpha\)]\label{theorem:soundness}
Let \( \phi \) be an LTL$_f$ constraint over a sequence of concepts, $q_0$ the initial state of the associated DFA, and suppose that: \\ (i) At decoding step \(0\), the initial DFA state \(q_0\) is at distance \(d_0\) from an accepting state with \(d_0 \leq T \), where \(T\) is the maximum length of the output sequence. \\
(ii) At decoding step \(t\), the scheduler ramps up, for each beam $i$, \(\alpha_i\) as described in Section~\ref{subsec:ramping}. \\
(iii) At each step, we prune any transition to a DFA state \(q_{k+1}\) such that \(d_{q_{t+1}} > T - t\). \\
Then the DFA-guided beam search produces a sequence \(x_{1:T}\) such that \(x_{1:T} \models \phi\), whenever it exists.
\end{theorem}
While our approach does not guarantee optimality, it ensures that only feasible paths are explored and valid completions are prioritized, yielding a sound and efficient decoding algorithm.
\paragraph{Complexity of DFA Beam Search}
The DFA-guided beam search procedure has polynomial-time complexity in the number of decoding steps \(T\), beam width \(B\), and output space of size \(|\mathcal{X}|\), assuming a fixed-size DFA. Specifically, each decoding step processes at most \(B \cdot |\mathcal{X}|\) candidates, applies DFA filtering and scoring, and retains the top \(B\). Thus, overall complexity is \(O(T \cdot B \cdot |\mathcal{X}|)\).
\paragraph{Limitations: DFA Compilation Overhead}
The LTL$_f$ formula \(\phi\) is first compiled into a deterministic finite automaton (DFA), using tools such as LTL2DFA~\citep{ltlf_compilation}. This compilation step may introduce an exponential blowup in the size of the automaton relative to the size of the formula, as shown by \citet{double_expo}. While this step is performed only once (offline), it may limit scalability to highly complex constraints with deep temporal structures.
\subsection{Theoretical Comparison with the State of the Art}
\paragraph{Comparison with Ctrl-G}
One way to address this problem, proposed by \cite{zhang2024ctrlg}, is to distill the model $f_{\theta}$ into Markov models to hopefully obtain a tractable representation. Unfortunately, the next result shows that even in the simplest case, the constrained MAP inference task is NP-hard.
\begin{theorem}[Complexity of Markov Chains MAP Inference with Unary Constraint]
\label{theorem:MCMAP}
MAP inference on Markov Chains with a unary equality constraint is NP-hard.
\end{theorem}
Thus, even for the simplest class of probabilistic graphical models—first-order Markov Chains—and with minimal constraints (e.g., a constraint of the form \(y_\beta = t\)), MAP inference remains NP-hard. While MAP inference for Hidden Markov Models (HMMs) is solvable in polynomial time via the Viterbi algorithm, this tractability relies on the assumption that the emission matrix is dense. In practice, however, this is often not the case for LLMs, whose output distributions are extremely sparse. Consequently, approximating LLMs with HMMs~\citep{zhang2024ctrlg} does not, in general, guarantee tractability for constrained decoding, even for very simple logical constraints.
\textbf{Comparison with Sampling Methods}
Sampling-based approaches~\citep{Miao19sampling, ahmed2025resampling, loula2025smc} enforce constraints by modifying or resampling sequences guided by logic or learned distributions. While they offer flexibility and can handle complex, soft constraints, they often lack generality or require expensive sampling or approximations. In contrast, our method provides a structured and efficient solution for a wide range of constraints (including temporal logic). Finally, we note that while both MAP inference and exact constrained sampling are intractable in general, in many cases sampling is actually in the \#P class of problems \citep{valiant,roth96}.
\begin{comment}
\begin{theorem}[Complexity of Exact Constrained Sampling]
\label{theorem:sharpp}
Given an LTL$_f$ formula \(\phi\), sampling exactly from the constrained conditional distribution \(P_{f_{\theta}}(x_{1:T} \mid \phi)\) is \#P-hard, even when the probabilistic model factorizes as independent variables.
\end{theorem}
\end{comment}
We report on experiments assessing the benefits of our approach applied to two tasks. In all tasks, to produce the transition matrix representing the temporal formula, we exploit the MONA software~\footnote{\href{https://www.brics.dk/mona/}{https://www.brics.dk/mona/}, copyright 1997-2020 Aarhus University.} and the LTLf2DFA software~\citep{Fuggitti2019}, under license LGPLv3+. All the experiments run on a machine with a Intel® Xeon® 20 cores and a NVidia L40S GPU with 48 GB of VRAM.
%\subsection{Experimental setting and implementation}
\subsection{Constrained Image Sequence Classification}
% Please add a topic sentence like: "We first conduct experiments to demonstrate the applicability of our method to a simple sequential image selection problem."
We start from Fashion-MNIST, which consists of $28 \times 28$ images of clothes~\footnote{\href{https://github.com/zalandoresearch/fashion-mnist}{https://github.com/zalandoresearch/fashion-mnist.}, MIT License}. Images in the training set are labeled with integer numbers representing the item type (e.g. 0 corresponds to ``t-shirt/top'', 1 corresponds to ``trousers'' etc.). From the test set of this dataset, we derived our customised dataset called Ordered Fashion MNIST. This contains the Fashion MNIST images ordered in sequences that respect the \ltlf constraints we defined and reported in the Appendix (Section \ref{ordered_fashion_mnist}) of the paper. These constraints define which clothes cannot be worn in the same outfit and the order in which they must be worn. For example, the sequence [trousers, t-shirt/top, sneakers, sandals] is not allowed since sneakers and sandals cannot be worn at the same time, but neither is the sequence [sandals, trousers, t-shirt/top] since sandals cannot be worn before trousers. For this task, we trained the CNN on the Fashion MNIST training set. Details on the CNN architecture and training parameters are in the Appendix (Section \ref{ordered_fashion_mnist}). The CNN has an accuracy of 91.03\% and a sequence accuracy (the ratio of sequences that are correctly classified) of 64.09\% on the Ordered Fashion MNIST dataset. Instead, using the same model with \model{}, we reached with 10 beams an accuracy of up to 95.58\% and a sequence accuracy of up to 80.66\%. Detailed results per number of beams from 2 to 10 are shown in Figure \ref{fig:cnn}, where we observe progressive improvements as the number of beams increases.
\begin{figure}[t]
\centering
\begin{minipage}{.45\textwidth}
\begin{center}
\includegraphics[width=\textwidth]{paper/figs/accuracy_comparison.pdf}
\end{center}
\end{minipage}%
\hfill
\begin{minipage}{0.45\textwidth}
\begin{center}
\includegraphics[width=\textwidth]{paper/figs/sequence_accuracy_comparison.pdf}
\end{center}
\end{minipage}
\caption{On the left the accuracy referring to single labels as the number of beams increases, on the right the accuracy referring to the correct classification of entire sequences as the number of beams increases. The dotted lines refer to the CNN without the use of \model{}.}\label{fig:cnn}
\end{figure}
\subsection{Constrained Text Generation}
We present two experiments on constrained text generation with LLMs. For both datasets, \model{} operates deterministically, and we compute the usual quality metrics in the literature: BLEU \citep{papineni2002bleu}, ROUGE \citep{lin-2004-rouge}, CIDEr \citep{cider} and SPICE \citep{spice}.
\textbf{CommonGen.} For the first experiment we use the CommonGen dataset ~\citep{Lin2020}, a standard evaluation task for constraint text generation released under MIT License. In this task, a set of common concepts is provided (e.g., {dog, frisbee, catch, throw}) and the goal for the LLM is to generate a coherent sentence describing a scenario using all the given concepts (e.g., “A man throws a frisbee, and his dog catches it”).
We compare our results with those obtained in relevant previous work, such as \cite{zhang2024ctrlg, zhang2023gelato, meng2022_nado}. In particular, we use the scores reported in the first two cited papers. Moreover, to ensure a fair comparison, we apply \model{} to the same models they employed: GPT2-large \cite{gpt2} (MIT License) as the unsupervised model, and GPT2-large fine-tuned by \cite{zhang2023gelato} on the training set of CommonGen as the supervised model. For this task we selected the best parameters on the training set and then applied these parameters to the validation set. The results in Table \ref{metricscomparison} show that, for both models, \model{} exceeds the current state of the art in two quality metrics (ROUGE-L and BLEU-4), is competitive in the remaining two (CIDEr and SPICE) and achieves 100\% constraint satisfaction (``Coverage''). Importantly, as shown in table \ref{timecomparison}, \model{} is systematically faster than Ctrl-G -- the best competing method -- when using the same number of beams and maximum token generation length.
\begin{table}[t]
\centering
\small
\caption{Performances on validation set only. The \model{} is run with: number of beams=64, $\alpha$=0.5 and $\gamma$=1, for both supervised and unsupervised model. Ctrl-G uses the HMM with 32768 hidden states the authors provided in their paper. Best scores are in bold, while second bests are
underlined.}
\begin{tabular}{llccccc}
\toprule
\textbf{Method} & & \textbf{ROUGE-L} & \textbf{BLEU-4} & \textbf{CIDEr} & \textbf{SPICE} & \textbf{Coverage} \\
\midrule
\rowcolor{gray!15}
\multicolumn{7}{l}{\textit{Unsupervised}} \\
InsNet (\cite{insnet}) & & - & 18.7 & - & - & \textbf{100.0} \\
NADO (\cite{meng2022_nado}) & & - & 26.2 & - & - & 96.1 \\
GeLaTo (\cite{zhang2023gelato}) & & 44.3 & 30.3 & 15.6 & \underline{30.2} & \textbf{100.0} \\
Ctrl-G (\cite{zhang2024ctrlg}) & & \underline{45.2} & \underline{32.1} & \textbf{16.0} & \textbf{30.8} & \textbf{100.0} \\
\textbf{\model{}} & & \textbf{48.7} & \textbf{47.9} & \underline{15.7} & 29.3 & \textbf{100.0}\\
\midrule
\rowcolor{gray!15}
\multicolumn{7}{l}{\textit{Supervised}} \\
NADO & & 44.4 & 30.8 & 16.1 & \underline{32.0} & 88.8 \\
GeLaTo & & \underline{46.2} & \underline{34.0} & \textbf{17.2} & \textbf{32.2} & \textbf{100.0} \\
\textbf{\model{}} & & \textbf{49.7} & \textbf{49.5} & \underline{16.2} & 29.7 & \textbf{100.0}\\
\bottomrule
\end{tabular}
\label{metricscomparison}
\vspace{1em}
\caption{Runtimes comparison across different beam sizes ($\pm$ standard error), with max length $T=32$. \model{} is used with $\alpha$=0.5 and $\gamma$=1, and the Ctrl-G uses the HMM with 32768 hidden states. Both use the fine-tuned GPT2 model.}
\begin{tabular}{lcccccc}
\toprule
\textbf{Method} & \textbf{4} & \textbf{8} & \textbf{16} & \textbf{32} & \textbf{64} & \textbf{128} \\
\midrule
\textbf{\model{}} & \textbf{0.74} $\pm$ {\scriptsize 0.007} & \textbf{0.81} $\pm$ {\scriptsize 0.006} & \textbf{1.33} $\pm$ {\scriptsize 0.010} & \textbf{2.22} $\pm$ {\scriptsize 0.019} & \textbf{4.42} $\pm$ {\scriptsize 0.041} & \textbf{9.45} $\pm$ {\scriptsize 0.084} \\
Ctrl-G & 3.49 $\pm$ {\scriptsize 0.011} & 3.70 $\pm$ {\scriptsize 0.014} & 4.25 $\pm$ {\scriptsize 0.024} & 5.43 $\pm$ {\scriptsize 0.053} & 8.05 $\pm$ {\scriptsize 0.102} & 12.01 $\pm$ {\scriptsize 0.161} \\
\bottomrule
\end{tabular}
\label{timecomparison}
\end{table}
\textbf{Ordered CommonGen.}
In our second experiment, we introduce Ordered CommonGen, a variant of CommonGen with a temporal constraint that the generated sentence must include all provided concepts in a specified order. For example, given the ordered set {\textit{dog, frisbee, catch, throw}}, a valid output would be: “The dog eagerly chased the frisbee trying to catch it after its owner threw it.”. This ordering constraint increases task difficulty and makes the setting well-suited for evaluating temporal constraint satisfaction. We derived this dataset from the CommonGen validation split by removing repeated concept sets and reordering the remaining ones to match the concept order in their reference sentence. The prompt, adapted from CommonGen Lite, is provided in Appendix~\ref{prompt}.
We compare \model{} applied to LLAMA 8B model with OpenAI models: GPT-3.5, GPT-4, GPT-4o, and the o1 reasoning model~\cite{brown2020language,openai2024gpt4technicalreport,openai2024gpt4ocard,openai2024openaio1card}. In Table~\ref{oderedcommongencomparison}, despite using a much smaller and locally deployed model, \model{} outperforms the large models on two metrics (BLEU-4 and CIDEr) and remains competitive on the others. It is also the only approach that achieves 100\% constraint satisfaction—consistent with its sound design—whereas GPT-3.5, GPT-4, and GPT-4o fall significantly short and the advanced o1 model achieves 99.8\% coverage.
\begin{comment}
For the second experiment we introduce a variation of CommonGen, which we call Ordered CommonGen. In this setting, the generated sentence must not only include all the provided concepts but also preserve their given order. For example, given the ordered set \{dog, frisbee, catch, throw\}, a valid sentence could be: “The dog eagerly chased the frisbee trying to catch it after its owner threw it.” This adds an additional constraint that makes the generation task more challenging and well-suited for testing the satisfaction of temporal constraints. We derived this dataset from the CommonGen validation set, removing the concept sets that appeared several times and reordering the remainder according to the order in which they appear in the target sentence. We provide the prompt used for this task, derived from the one used in CommonGen lite, in appendix \ref{prompt}.
We decided to compare \model{} with various GPTs, namely: OpenAI's GPT 3.5, 4, 4o and the o1 reasoning model (\cite{brown2020language}, \cite{openai2024gpt4technicalreport}, \cite{openai2024gpt4ocard}, \cite{openai2024openaio1card}).
The results reported in table \ref{oderedcommongencomparison} show that TRIDENT outperforms very large models in two of the four quality metrics and is competitive in the other two, even though it uses a model with 8 billion parameters and can hence easily be used locally. It also achieves 100\% in constraint satisfaction, something models such as GPT 3.5, 4 and 4o are not even close to doing, even surpassing one of the most advanced reasoning models of the moment, namely o1, which has a coverage of 99.8\%.
\end{comment}
\begin{table}[t]
\centering
\small
\caption{Performances on Ordered CommonGen. \model{} use LLAMA 8B with number of beams=64, $\alpha$=0.25, $\gamma$=1. The best scores are in bold, while the second best are underlined.}
\begin{tabular}{llccccc}
\toprule
\textbf{Method} & & \textbf{ROUGE-L} & \textbf{BLEU-4} & \textbf{CIDEr} & \textbf{SPICE} & \textbf{Coverage} \\
\midrule
GPT 3.5 & & 42.2 & 24.9 & \underline{13.5} & 40.8 & 64.5 \\
GPT 4 & & 42.2 & 23.7 & 12.4 & 40.7 & 83.3 \\
GPT 4o & & \underline{42.7} & \underline{25.2} & 13.4 & \textbf{42.2} & 73.9 \\
o1 & & \textbf{43.1} & 24.3 & 12.9 & 41.3 & \underline{99.8} \\
LLAMA 8B + \textbf{\model{}} & & 40.0 & \textbf{25.6} & \textbf{13.6} & \underline{41.7} & \textbf{100.0}\\
\bottomrule
\end{tabular}
\label{oderedcommongencomparison}
\end{table}
\paragraph{Neurosymbolic AI.} Neurosymbolic AI~\cite{} is a growing filed of interest in machine learning due to the ability of its methods to reconcile neural perception with symbolic reasonings~\citep{raedt_survey,third_wave}. While the field is quite vast, the neurosymbolic solutions that are the closest to our method are those that try to incorporate symbolic background knowledge in the form of constraints into neural models~\citep{dash_informed_ml_review,giunchiglia2022ijcai}. These methods can be divided in two groups: those that give a probabilistic semantics to the constraints~\citep{manhaeve2018deepproblog,xu2018semantic,krieken2023anesi} and those that give a fuzzy semantics~\citep{LTN,giunchiglia2024ccn+,diligenti2012SBR}. Another way to categorize the methods in the field is by whether they incorporate the constraints in the loss function~\citep{LTN,xu2018semantic,fischer2019DL2,krieken2022_analyzing} or they change the final output space of the model~\citep{manhaeve2018deepproblog,giunchiglia2021jair,ahmed2022spl,pryor2023NeuPSL,hoernle2022multiplexnet,misino2023tvael}. The first can be used to nudge via the loss the network to satisfy the constraints, while the second can guarantee the constraints satisfaction.
\paragraph{Constrained Text Generation.} The work done in constrained text generation has been developing on multiple orthogonal axes. \textit{1. Search based decoding.} These approaches act at inference time and constrain the beam search with logical constraints. For example, in~\citep{Lu2021,Lu2022}, the authors decide which beams to expand taking into account not only the LLM's prediction but also the degree of satisfaction of the constraints reported for every sequence.
%The method was further developed in~\cite{Lu2022}, using a look-ahead mechanism and the well known A$^*$ algorithm to find the most likely sequences that satisfy the constraints.
%The advantages of these approaches is that (i) they are intuitive and (ii) they can be used in conjunction with any pre-trained model, however, in the worst case scenario the number of partial states to explore might be exponential in the vocabulary size.
\textit{2. Auxiliary Classifier Guidance.} The works that follow this line aim to guide the base model with an auxiliary one. %GeDi~\cite{krause2021gedi} uses two small, class-conditional LLMs to compute a Bayes-factor weight that is multiplied into the base model’s logits, steering generation toward the desired attribute while leaving the architecture unchanged. NADO~\cite{}, on the other hand,
GeDi~\citep{krause2021gedi}, FUDGE~\citep{Yang2021_fudge} and NADO~\citep{meng2022_nado} steer generation with class-conditional or token-level predictors. However, they provide no hard guarantees and might require task-specific supervision. On the contrary, GeLaTo~\citep{zhang2023gelato} provides the guarantee as it distills the base LLM into a hidden-Markov model, which computes the probability that the remaining suffix can still contain a set of keywords and then multiplies this value into the LLM's logits. Ctrl-G~\citep{zhang2024ctrlg} is the recent extension of GeLato, which allows for any constraint that can be captured in a DFA (instead of propositional logic). \textit{3. Probabilistic Sampling} treats constraints as conditioning and samples from the posterior. This line was pioneered by~\citep{Miao19sampling} with Metropolis–Hastings token edits that provide unbiased samples under lexical constraints. This idea has then been further explored in the works of ~\citet{ahmed2025resampling,loula2025smc}.
%, where the model generates a full sample, and re-weights and resamples only the local factorisation that is relevant to the constraint.
% in~\cite{Lu2021}, the authors propose an approach based on propositional logic to constrained text generation, using LLMs. The proposed method performs a beam search on the strings that might satisfy a given constraint. It then selects the best candidates and uses beam-based search to find an approximately optimal solution. Such an approach was further refined in~\cite{Lu2022}, using the well known A* algorithm. This method is shown to be effective in terms of quality of the generated output, but it does not scale well as the number of constraints grow. Another interesting approach is the one proposed in~\cite{Zhang2023} and~\cite{Zhang2024}. In these works, the authors first distill a Hidden Markov Model from a Language Model, and then they condition the model on the constraint. Focusing on the distilled HMM simplifies the computation of the conditioned probability, and makes constrained text generation more effective.
We introduced \model{}, a DFA-guided method to constrain the output of a Neural Network. By using \ltlf, we are able to address temporal requirements, thus widening the set of possible case studies w.r.t. other existing methods. Our algorithm is proved to be sound, while not optimal, and can easily be adapted to different applications. Comparison with the state of the art shows significant improvements in both efficiency and quality of the generated output. The introduced method can be used for multiple purposes, with a positive societal impact, like detoxification of LLMs' output. On the other hand, we are also aware that our method may be misused and a potential issue could be its use to enforce instead the usage of toxic words by LLMs.
\subsection{Soundness of the \model{} algorithm}
\newcommand{\defeq}{\overset{\text{\tiny def}}{=}}
\begin{comment}
We start by proving the correctness of the generated constraint matrix $M_C$ (Theorem~\ref{theorem:constrMatrix}).
\begin{proof}[Correctness of the generated matrix]
Suppose we are in a state $s$, and we have an outgoing transition $\delta(s,p) = s'$, with $s'$ a deadlock state. Such transition is marked in the transition matrix as $M[(s,s')][p]$. But since $s'$ is deadlock, $M[(s,s')]$ is removed from the matrix. Take now the column indexed by $p$, and suppose that the logical $or$ of remaining elements $M[(s,\_)][p]$ is $1$. Then there is $s''$ such that $\delta(s,p) = s''$. But since the automaton is deterministic, it must hold $s'=s''$, and since we removed $M[(s,s')]$ from the transition matrix, we end up in a contradiction.
\end{proof}
We start by proving that DFA-Guided Beam Search avoids deadlock states, thus leading to a sequence that never falsifies the constraint $\phi$ (Lemma~\ref{lemma:beam})
\begin{proof}[Deadlock States Avoidance of DFA-Guided Beam Search]
It suffices to observe that deadlock states are at distance $d_{q_{k+1}} = + \infty$ to any accepting states. Then transitions leading to deadlock states are pruned from the set of candidates, and such states are never reached.
Let us suppose that, at step $k+1$, a concept $c$ leading to a deadlock state has probability according to the LLM $p_{k+1}$. Before selecting the beams, with state of the network $q$, we compute probability of each beam as $P_{k+1} = p_{k+1} + M_C[q][c]$. By construction, $M[q][c] = - \infty$. Hence $P_{k+1} = - \infty$, and $c$ cannot be selected as a candidate beam. Hence the constraint is not violated.
We first proceed by induction on the length of the sequence to show that there is an accepting path of length at most $T$. Let $T = 0$: then the sequence is empty and trivially sound.
Let us now consider $T > 0$. Let us call $\pi$ a path in the DFA, $\pi(i)$ the $i^{th}$ state traversed by the path. We assume the following as the inductive hypothesis: given $m < T$, with state of the DFA $q$, either
\begin{itemize}
\item $x_{1:m} \models \phi$ or,
\item $x_{1:m} \not \models \phi$ and $\forall \pi . \ \pi(0) = q \implies \exists i . \ \pi(i) \in F \land i \leq T - m$.
\end{itemize}
Take now the sequence $x_{m:T}$ with $T - m = n$. By the inductive hypothesis, also $x_{m:T}$ satisfies the condition above. Consider the concatenation $x_{1:m} \bullet x_{m:T}$: we have that $\forall \pi . \ \pi(0) = q \implies \exists i . \ \pi(i) \in F \land i \leq T - (n+m) = 0$, namely there is a path leading to an accepting state of length at most $T$.
It now remains to show that, at each step, the distance from such an accepting state always decreases. At step $t$, given state of the network $q$, our algorithm performs the following operations:
\begin{itemize}
\item for each atomic proposition $p$ such that $\delta(q,p) = q'$, if $\delta(q',p') = q'$ forall $p'$, then logits corresponding to $p$ are set to $-\infty$. This corresponds to pruning paths of length $1$ leading to a deadlock state;
\item take $f$ an accepting state, $d(s,f)$ the distance between a state $s$ and $f$. For each atomic proposition $p$ such that $\delta(q, p) = q'$ with $d(q',f) < d(q,f)$ we set the corresponding logit $\hat{l} = min\{ l \}_{l \in beam}$.
\end{itemize}
It is easy to see that distance decreasing paths are always explored by the beam search algorithm. Hence, at the end of the sequence, the constraint $\phi$ is satisfied.
\end{proof}
\end{comment}
\begin{comment}
\begin{proof}[Proof Sketch]
We proceed by induction on sequence length. Initially, at step $t=0$, the set of sequences is trivially sound (empty sequence). Let us call $\pi$ a path in the DFA, $\pi(i)$ the $i^{th}$ state traversed by the path. We assume the following as the induction hypothesis. At time $t-1$, with state of the network $q$, a sequence $s$ in the beam is such that either:
\begin{itemize}
\item $s \models \phi$
\item $s \not \models \phi$, and $\forall \pi . \ \pi(0) = q \implies \exists i . \ \pi(i) \in F$.
\end{itemize}
Let us consider an atomic proposition $\hat{p}$ such that $\delta(q, \hat{p}) = \hat{q}$, with $\delta(\hat{q}, a) = \hat{q} \ \forall a \in P$, namely $\hat{p}$ leads to a deadlock state. At time $t$, the algorithm sets to $- \infty$ the logits corresponding to $\hat{p}$.
At step $t$, any potential prediction leading to a deadlock DFA state receives a logit of $-\infty$, removing it from consideration. Thus, every sequence selected at step $t$ can still reach an accepting state. By induction, at the final step, every surviving sequence must satisfy the constraint by construction.
\end{proof}
\end{comment}
We prove here that our method is sound (Theorem~\ref{theorem:soundness}).
\begin{proof}[Proof of Theorem \ref{theorem:soundness}. (Soundness of the \model{} algorithm)]
We prove that the algorithm is sound by induction on the length $t$ of the sequence.
More precisely, we propose the following inductive hypothesis $$\mathcal{H}_t: \text{for all beams } (x_{<t}, s, q) \in \mathcal{B}_t, d_{q_t} \leq T - t.$$ The base case is $t=0$: the initial beam only contains the prompt $x_0$, the initial state of the DFA $q_0$, and the distance $d_0$ from an accepting state. By the hypothesis of the theorem, we have $d_0 \leq T$ and thus $\mathcal{H}_0$ is verified.
Let us now assume that $\mathcal{H}_t$ is true, for $t\in[1,T-1]$.
%that all the sequences in $\mathcal{B}$ at time $t$ can be extended to an accepted sequence.
At line 12 of the algorithm:
\begin{itemize}
\item if a transition leads to a state $q'$ such that $d_{q'} > T - t$ then it is impossible to complete an accepting sequence within the remaining steps. But this choice is excluded by setting $Z[i,x] \leftarrow - \infty$.
\end{itemize}
This ensures that no sequence in $\mathcal{B}$ is extended to a non-accepting sequence.
Indeed, at line 22:
\begin{itemize}
\item we choose the top $k$ beam extensions among the valid ones with respect to their score (denoted by $Z$ in the pseudo-code), i.e. among those having distance $d_{q'_{t+1}} \leq T - (t+1)$, since invalid outputs have $-\infty$ as a score. In the case where we have less than $k$ valid beam extensions, then we pad the remaining beams with copies of the valid beams. We know that at least one valid extension exists for each beam, since we assume that $\mathcal{H}_t$ is true.
\end{itemize}
Thus we have shown that $\mathcal{H}_{t+1}$ is true whenever $\mathcal{H}_t$ is true. By induction, $\mathcal{H}_T$ is true.
At time $T$, the algorithm returns the best sequence among those included in $\mathcal{B}_T$. But, by $\mathcal{H}_T$, every sequence in $\mathcal{B}_T$ has distance $0$ from an accepting state, and hence terminates in an accepting state. Thus the algorithm is sound.
\end{proof}
\subsection{Complexity of MAP Inference on Markov Chains}
\begin{proof}[Proof of Theorem~\ref{theorem:MCMAP}]
We show NP-hardness by providing a polynomial-time reduction from the \emph{Constrained Shortest Path (CSP) problem with uniform arc lengths} to the \emph{MAP inference problem on time-homogeneous Markov chains under a unary constraint}.
\paragraph{Step 1: CSP Formulation.}
Consider a directed graph \(G = (V, E)\), where each arc \((i,j)\in E\) has an associated cost \(c(i,j)\geq 0\) and a length \(b(i,j)\in\mathbb{N}\). We focus on the special case where all arcs have the same length, specifically \(b(i,j) = 1\) for all \((i,j)\in E\). Given vertices \(s, t \in V\) (source and target) and an integer bound \(\beta \geq 1\), the CSP problem seeks a path of exact length \(\beta\) from \(s\) to \(t\) that minimizes total cost:
\[
\min_{x_{1:\beta} \in V^\beta,\; x_1 = s,\; x_\beta = t,\; (x_k,x_{k+1})\in E} \sum_{k=1}^{\beta-1} c(x_k,x_{k+1}).
\]
This uniform-length CSP variant is known to be NP-hard~\citep{Erzin2022}.
\paragraph{Step 2: MAP Inference Problem Formulation.}
In the MAP inference setting, we have a time-homogeneous Markov chain over a state space \(S\), an initial distribution \(\mu\), and transition matrix \(P\). Given a unary constraint specifying the state at time \(\beta\), i.e., \(X_\beta = t\), the MAP inference problem is:
\[
x_{1:\beta}^{*} = \argmax_{x_{1:\beta}\in S^\beta,\; x_\beta = t} \mu(x_1)\prod_{k=1}^{\beta-1}P(x_{k+1}\mid x_k).
\]
\paragraph{Step 3: Reduction from CSP to MAP Inference.}
Given a CSP instance \((G,c,s,t,\beta)\), construct a MAP inference instance as follows:
\begin{enumerate}
\item \textbf{State space.} Define the state space as \(S = V\cup D\), where \(D = \{d_i \mid i\in V\}\) is a set of newly introduced dummy states, with one dummy state per original vertex.
\item \textbf{Initial distribution.} Set \(\mu(x) = \delta_{x,s}\), ensuring the chain always starts at the source vertex \(s\).
\item \textbf{Transition probabilities.} First, define an extended cost function \(\tilde{c}: V\times S \to [0,+\infty]\) by:
\[
\tilde{c}(i,j)=\begin{cases}
c(i,j), & (i,j)\in E\\[4pt]
-\log(Z_{\max}-Z_i), & j = d_i\\[4pt]
+\infty, & \text{otherwise}
\end{cases}
\]
where for each vertex \(i\in V\), we set:
\[
Z_i=\sum_{j\in V} e^{-c(i,j)}, \quad Z_{\max}=\max_{i\in V}Z_i.
\]
With these definitions, we set the transition probabilities for all \(i \in V\) as:
\[
P(j\mid i)=\frac{e^{-\tilde{c}(i,j)}}{Z_{\max}}, \quad j\in S.
\]
This ensures that all transitions from states in \(V\) are properly normalized, as:
\[
\sum_{j\in S}P(j\mid i)=\frac{Z_i+(Z_{\max}-Z_i)}{Z_{\max}}=1,\quad\forall i\in V.
\]
\item \textbf{Absorbing states.} Explicitly set the target vertex \(t\) and all dummy states \(d_i\) as absorbing states:
\[
P(t\mid t)=1,\quad P(j\mid t)=0\text{ for }j\neq t,\quad\text{and}\quad P(d_i\mid d_i)=1,\quad P(j\mid d_i)=0\text{ for }j\neq d_i.
\]
Thus, any path entering a dummy state or \(t\) remains there indefinitely.
\item \textbf{Unary constraint.} Set the unary constraint as \( \phi \equiv X_\beta = t\).
\end{enumerate}
\paragraph{Step 4: Correctness and Equivalence.}
Consider any path \(x_{1:\beta}\) that satisfies the constraint \(X_\beta = t\). If the path ever enters a dummy state \(d_i\), it will remain there indefinitely (absorbing), contradicting the constraint \(X_\beta = t\). Thus, any feasible path must stay entirely within \(V\).
For feasible paths \(x_{1:\beta}\in V^\beta\), we have:
\begin{align*}
P(x_{1:\beta})& =\prod_{k=1}^{\beta-1}\frac{e^{-\tilde{c}(x_k,x_{k+1})}}{Z_{\max}}=Z_{\max}^{-(\beta-1)}\cdot e^{-\sum_{k=1}^{\beta-1}\tilde{c}(x_k,x_{k+1})} \cdot \delta_{x_1,s} \\ & \underset{(x_{1:\beta}\models \phi)}{\operatorname{=}} Z_{\max}^{-(\beta-1)}\cdot e^{-\sum_{k=1}^{\beta-1}c(x_k,x_{k+1})}
\end{align*}
Hence, the MAP objective is exactly equivalent to minimizing the total cost:
\[
\argmin_{x_{1:\beta}\in S^\beta,\; x_\beta = t}-\log P(x_{1:\beta})=\argmin_{x_{1:\beta} \in V^\beta,\; x_1 = s,\; x_\beta = t,\; (x_k,x_{k+1})\in E} \sum_{k=1}^{\beta-1} c(x_k,x_{k+1}),
\]
recovering precisely the original CSP objective.
\paragraph{Step 5: Complexity and Conclusion.}
The construction described above clearly runs in polynomial time (adding one dummy state per vertex and computing simple exponentials). Thus, we have demonstrated a polynomial-time reduction from the CSP problem (known NP-hard) to the MAP inference problem under unary constraints in a Markov chain.
\end{proof}
All the experiments were run on a machine equipped with the following infrastructure: Intel® Xeon® Silver 4416+ CPU, 20 Cores, 40 Threads, 2.00/3.90 GHz; NVidia L40S GPU, 48 GB GDDR6, 18176 CUDA Cores, 142 RT Cores, 568 Tensor Cores.
For this task, we trained a CNN model on the Fashion MNIST training set for 7 epochs using a batch size of 64 and a learning rate of 0.002. The model consists of two convolutional blocks followed by three fully connected layers, incorporating Dropout and Layer Normalization. The convolutional layers use 2×2 and 5×5 filters, each followed by MaxPooling operations. The final classification layer applies a Softmax activation for 10-class classification. We used CrossEntropyLoss as the loss function, and the Adam optimizer for training.
\subsection{Natural Language Constraints}
We report here all the constraints enforced on the Ordered Fashion-Mnist dataset, expressed in natural language. The \ltlf formulation of each constraint is reported below.
\begin{itemize}
\item If you wear a T-shirt/top, you will not be able to wear a Shirt, Dress, or another T-shirt/top.
\item If you wear Trousers, you will not be able to wear a Dress or another Trouser.
\item If you wear a Pullover, you will not be able to wear a Dress, T-shirt/top, Shirt, or another Pullover.
\item If you wear a Dress, you will not be able to wear a T-shirt/top, Shirt, Trouser, Pullover, or another Dress.
\item If you wear a Coat, you will not be able to wear a T-shirt/top, Shirt, Pullover, Dress, or another Coat.
\item If you wear Sandals, you will not be able to wear Sneakers, Trousers, Ankle boots, or another pair of Sandals.
\item If you wear a Shirt, you will not be able to wear a T-shirt/top, Dress, or another Shirt.
\item If you wear Sneakers, you will not be able to wear Sandals, Trousers, Ankle boots, or another pair of Sneakers.
\item If you wear a Bag, you will not be able to wear a T-shirt/top, Shirt, Dress, Pullover, Coat, or another Bag.
\item If you wear Ankle boots, you will not be able to wear Sandals, Trousers, Sneakers, or another pair of Ankle boots.
\item You must wear at least one of the following: T-shirt/top, Pullover, Shirt, or Dress.
\item You must wear at least one of the following: Trouser or Dress.
\item You must wear at least one of the following: Sandal, Sneaker, or Ankle boot.
\end{itemize}
\subsection{\ltlf Constraints}
The listed formulas must be interpreted as being conjoined via the logical AND operator (\(\land\)). That is, the complete specification is given by:
\[
\varphi = \varphi_1 \land \varphi_2 \land \dots \land \varphi_{13}
\]
where each \(\varphi_i\) corresponds to the respective in the list:
\begin{itemize}
\item $G(t\_shirt\_top \to \neg F\, Shirt) \land G(t\_shirt\_top \to \neg F\, Dress) \land G(t\_shirt\_top \to WX\, G\, \neg t\_shirt\_top)$
\item $G(Trouser \to \neg F\, Dress) \land G(Trouser \to WX\, G\, \neg Trouser)$
\item $G(Pullover \to \neg F\, Dress) \land G(Pullover \to \neg F\, t\_shirt\_top) \land G(Pullover \to \neg F\, Shirt) \land G(Pullover \to WX\, G\, \neg Pullover)$
\item $G(Dress \to \neg F\, t\_shirt\_top) \land G(Dress \to \neg F\, Shirt) \land G(Dress \to \neg F\, Trouser) \land G(Dress \to \neg F\, Pullover) \land G(Dress \to WX\, G\, \neg Dress)$
\item $G(Coat \to \neg F\, t\_shirt\_top) \land G(Coat \to \neg F\, Shirt) \land G(Coat \to \neg F\, Pullover) \land G(Coat \to \neg F\, Dress) \land G(Coat \to WX\, G\, \neg Coat)$
\item $G(Sandal \to \neg F\, Sneaker) \land G(Sandal \to \neg F\, Trouser) \land G(Sandal \to \neg F\, Ankle\ boot) \land G(Sandal \to WX\, G\, \neg Sandal)$
\item $G(Shirt \to \neg F\, t\_shirt\_top) \land G(Shirt \to \neg F\, Dress) \land G(Shirt \to WX\, G\, \neg Shirt)$
\item $G(Sneaker \to \neg F\, Sandal) \land G(Sneaker \to \neg F\, Trouser) \land G(Sneaker \to \neg F\, Ankle\ boot) \land G(Sneaker \to WX\, G\, \neg Sneaker)$
\item $G(Bag \to \neg F\, t\_shirt\_top) \land G(Bag \to \neg F\, Shirt) \land G(Bag \to \neg F\, Dress) \land G(Bag \to \neg F\, Pullover) \land G(Bag \to \neg F\, Coat) \land G(Bag \to WX\, G\, \neg Bag)$
\item $G(Ankle\ boot \to \neg F\, Sandal) \land G(Ankle\ boot \to \neg F\, Trouser) \land G(Ankle\ boot \to \neg F\, Sneaker) \land G(Ankle\ boot \to WX\, G\, \neg Ankle\ boot)$
\item $F(t\_shirt\_top \lor Pullover \lor Shirt \lor Dress)$
\item $F(Trouser \lor Dress)$
\item $F(Sandal \lor Sneaker \lor Ankle\ boot)$
\end{itemize}
Each experiment in Ordered CommonGen has a prompt and a set of ordered concepts, given as a constraint on the output. A sample prompt for experiments is reported below.
\subsection{Prompt}
\label{prompt}
\# Instruction
Given several concepts (i.e., nouns or verbs), write a short and simple sentence that contains *all* the required words in the given order.\\
The sentence should describe a common scene in daily life, and the concepts should be used in a natural way.
\# Examples
\#\# Example 1\\
- Concepts: "dog, frisbee, catch, throw"\\
- Sentence: The dog eagerly chased the frisbee trying to catch it after its owner threw it.
\#\# Example 2\\
- Concepts: "apple, place, tree, pick"\\
- Sentence: I found an apple in a place near a tree and I picked it up.
\# Your Task
- Concepts: **Concepts**\\
- Sentence:
\subsection{\ltlf Constraints example}
The listed formulas should be interpreted as being conjoined via the logical AND operator ($\land$).
Therefore, the complete specification is given by:
\[
\varphi = \varphi_1 \land \varphi_2 \land \cdots \land \varphi_5
\]
where each $\varphi_i$ corresponds to the respective formula in the list below. This represents an example with 3 concepts.
\begin{itemize}
\item $((\neg(secondword \lor dot)\ U\ firstword) \land F(secondword))$
\item $((\neg(thirdword \lor dot)\ U\ secondword) \land F(thirdword))$
\item $((\neg(eos \lor dot)\ U\ thirdword) \land F(eos))$
\item $G(dot \to X\ eos)$
\item $G(firstword \lor secondword \lor thirdword \lor dot \lor eos \lor nomatch)$
\end{itemize}
\begin{thebibliography}{47}
\providecommand{\natexlab}[1]{#1}
\providecommand{\url}[1]{\texttt{#1}}
\expandafter\ifx\csname urlstyle\endcsname\relax
\providecommand{\doi}[1]{doi: #1}\else
\providecommand{\doi}{doi: \begingroup \urlstyle{rm}\Url}\fi
\bibitem[Xu et~al.(2018)Xu, Zhang, Friedman, Liang, and den
Broeck]{xu2018semantic}
Jingyi Xu, Zilu Zhang, Tal Friedman, Yitao Liang, and Guy~Van den Broeck.
\newblock A semantic loss function for deep learning with symbolic knowledge.
\newblock In \emph{Proceedings of International Conference on Machine
Learning}, 2018.
\bibitem[Donadello et~al.(2017)Donadello, Serafini, and Garcez]{LTN}
Ivan Donadello, Luciano Serafini, and Artur~D'Avila Garcez.
\newblock Logic tensor networks for semantic image interpretation.
\newblock In \emph{Proceedings of the 26th International Joint Conference on
Artificial Intelligence}, IJCAI'17, page 1596–1602. AAAI Press, 2017.
\newblock ISBN 9780999241103.
\bibitem[Diligenti et~al.(2017)Diligenti, Roy\-chowdhury, and
Gori]{diligenti2017sbrnn}
Michelangelo Diligenti, Soumali Roy\-chowdhury, and Marco Gori.
\newblock Integrating prior knowl\-edge into deep learning.
\newblock In \emph{Proceedings of {International Conference on Machine Learning
and Applications}}, 2017.
\bibitem[Giunchiglia and Lukasiewicz(2021)]{giunchiglia2021jair}
Eleonora Giunchiglia and Thomas Lukasiewicz.
\newblock Multi-label classification neural networks with hard logical
constraints.
\newblock \emph{Journal of Artificial Intelligence Research}, 72, 2021.
\bibitem[Ahmed et~al.(2022)Ahmed, Teso, Chang, den Broeck, and
Vergari]{ahmed2022spl}
Kareem Ahmed, Stefano Teso, Kai{-}Wei Chang, Guy~Van den Broeck, and Antonio
Vergari.
\newblock Semantic probabilistic layers for neuro-symbolic learning.
\newblock In \emph{Proceedings of Neural Information Processing Systems}, 2022.
\bibitem[Manhaeve et~al.(2018)Manhaeve, Dumancic, Kimmig, Demeester, and
De~Raedt]{manhaeve2018deepproblog}
Robin Manhaeve, Sebastijan Dumancic, Angelika Kimmig, Thomas Demeester, and Luc
De~Raedt.
\newblock {DeepProbLog: N}eural probabilistic logic programming.
\newblock In \emph{Proceedings of Neural Information Processing Systems}, 2018.
\bibitem[Lin et~al.(2020)Lin, Zhou, Shen, Zhou, Bhagavatula, Choi, and
Ren]{Lin2020}
Bill~Yuchen Lin, Wangchunshu Zhou, Ming Shen, Pei Zhou, Chandra Bhagavatula,
Yejin Choi, and Xiang Ren.
\newblock Commongen: A constrained text generation challenge for generative
commonsense reasoning, 2020.
\newblock URL \url{https://arxiv.org/abs/1911.03705}.
\bibitem[Lu et~al.(2021)Lu, West, Zellers, Le~Bras, Bhagavatula, and
Choi]{Lu2021}
Ximing Lu, Peter West, Rowan Zellers, Ronan Le~Bras, Chandra Bhagavatula, and
Yejin Choi.
\newblock {N}euro{L}ogic decoding: (un)supervised neural text generation with
predicate logic constraints.
\newblock In Kristina Toutanova, Anna Rumshisky, Luke Zettlemoyer, Dilek
Hakkani-Tur, Iz~Beltagy, Steven Bethard, Ryan Cotterell, Tanmoy Chakraborty,
and Yichao Zhou, editors, \emph{Proceedings of the 2021 Conference of the
North American Chapter of the Association for Computational Linguistics:
Human Language Technologies}, pages 4288--4299, Online, June 2021.
Association for Computational Linguistics.
\newblock \doi{10.18653/v1/2021.naacl-main.339}.
\newblock URL \url{https://aclanthology.org/2021.naacl-main.339/}.
\bibitem[Lu et~al.(2022)Lu, Welleck, West, Jiang, Kasai, Khashabi, Le~Bras,
Qin, Yu, Zellers, Smith, and Choi]{Lu2022}
Ximing Lu, Sean Welleck, Peter West, Liwei Jiang, Jungo Kasai, Daniel Khashabi,
Ronan Le~Bras, Lianhui Qin, Youngjae Yu, Rowan Zellers, Noah~A. Smith, and
Yejin Choi.
\newblock {N}euro{L}ogic a*esque decoding: Constrained text generation with
lookahead heuristics.
\newblock In Marine Carpuat, Marie-Catherine de~Marneffe, and Ivan~Vladimir
Meza~Ruiz, editors, \emph{Proceedings of the 2022 Conference of the North
American Chapter of the Association for Computational Linguistics: Human
Language Technologies}, pages 780--799, Seattle, United States, July 2022.
Association for Computational Linguistics.
\newblock \doi{10.18653/v1/2022.naacl-main.57}.
\newblock URL \url{https://aclanthology.org/2022.naacl-main.57/}.
\bibitem[Krause et~al.(2021)Krause, Gotmare, McCann, Keskar, Joty, Socher, and
Rajani]{krause2021gedi}
Ben Krause, Akhilesh~Deepak Gotmare, Bryan McCann, Nitish~Shirish Keskar,
Shafiq~R. Joty, Richard Socher, and Nazneen~Fatema Rajani.
\newblock Gedi: Generative discriminator guided sequence generation.
\newblock In Marie{-}Francine Moens, Xuanjing Huang, Lucia Specia, and
Scott~Wen{-}tau Yih, editors, \emph{Findings of the Association for
Computational Linguistics: {EMNLP} 2021, Virtual Event / Punta Cana,
Dominican Republic, 16-20 November, 2021}, 2021.
\bibitem[Zhang et~al.(2024)Zhang, Kung, Yoshida, Broeck, and
Peng]{zhang2024ctrlg}
Honghua Zhang, Po-Nien Kung, Masahiro Yoshida, Guy Van~den Broeck, and Nanyun
Peng.
\newblock Adaptable logical control for large language models.
\newblock In \emph{Proceedings of NeurIPS}, 2024.
\bibitem[Miao et~al.(2019)Miao, Zhou, Mou, Yan, and Li]{Miao19sampling}
Ning Miao, Hao Zhou, Lili Mou, Rui Yan, and Lei Li.
\newblock {CGMH:} constrained sentence generation by metropolis-hastings
sampling.
\newblock In \emph{Proceedings of {AAAI}}, pages 6834--6842, 2019.
\bibitem[Loula et~al.(2025)Loula, LeBrun, Du, Lipkin, Pasti, Grand, Liu, Emara,
Freedman, Eisner, Cotterell, Mansinghka, Lew, Vieira, and
O'Donnell]{loula2025smc}
Joao Loula, Benjamin LeBrun, Li~Du, Ben Lipkin, Clemente Pasti, Gabriel Grand,
Tianyu Liu, Yahya Emara, Marjorie Freedman, Jason Eisner, Ryan Cotterell,
Vikash Mansinghka, Alexander~K. Lew, Tim Vieira, and Timothy~J. O'Donnell.
\newblock Syntactic and semantic control of large language models via
sequential monte carlo.
\newblock In \emph{Proceedings of ICLR}, 2025.
\bibitem[{De Giacomo} and Vardi(2013)]{Vardi2013}
Giuseppe {De Giacomo} and Moshe~Y. Vardi.
\newblock Linear temporal logic and linear dynamic logic on finite traces.
\newblock In \emph{Proceedings of the Twenty-Third International Joint
Conference on Artificial Intelligence}, IJCAI '13, page 854–860. AAAI
Press, 2013.
\newblock ISBN 9781577356332.
\bibitem[De~Giacomo et~al.(2022)De~Giacomo, Favorito, Li, Vardi, Xiao, and
Zhu]{ltlf_compilation}
Giuseppe De~Giacomo, Marco Favorito, Jianwen Li, Moshe~Y. Vardi, Shengping
Xiao, and Shufang Zhu.
\newblock Ltlf synthesis as and-or graph search: Knowledge compilation at work.
\newblock In Lud~De Raedt, editor, \emph{Proceedings of the Thirty-First
International Joint Conference on Artificial Intelligence, {IJCAI-22}}, pages
2591--2598. International Joint Conferences on Artificial Intelligence
Organization, 7 2022.
\newblock \doi{10.24963/ijcai.2022/359}.
\newblock URL \url{https://doi.org/10.24963/ijcai.2022/359}.
\newblock Main Track.
\bibitem[Dijkstra(1959)]{dijkstra1959note}
Edsger~W. Dijkstra.
\newblock A note on two problems in connexion with graphs.
\newblock \emph{Numerische mathematik}, 1\penalty0 (1):\penalty0 269--271,
1959.
\bibitem[Roth(1996)]{roth96}
Dan Roth.
\newblock On the hardness of approximate reasoning.
\newblock \emph{Artificial Intelligence}, 82\penalty0 (1):\penalty0 273--302,
1996.
\newblock ISSN 0004-3702.
\newblock \doi{https://doi.org/10.1016/0004-3702(94)00092-1}.
\newblock URL
\url{https://www.sciencedirect.com/science/article/pii/0004370294000921}.
\bibitem[De~Giacomo and Vardi(2015)]{double_expo}
Giuseppe De~Giacomo and Moshe~Y. Vardi.
\newblock Synthesis for ltl and ldl on finite traces.
\newblock In \emph{Proceedings of the 24th International Conference on
Artificial Intelligence}, IJCAI'15, page 1558–1564. AAAI Press, 2015.
\newblock ISBN 9781577357384.
\bibitem[Ahmed et~al.(2025)Ahmed, Chang, and den Broeck]{ahmed2025resampling}
Kareem Ahmed, Kai-Wei Chang, and Guy~Van den Broeck.
\newblock Controllable generation via locally constrained resampling.
\newblock In \emph{Proceedings of {ICLR}}, 2025.
\bibitem[Valiant(1979)]{valiant}
L.G. Valiant.
\newblock The complexity of computing the permanent.
\newblock \emph{Theoretical Computer Science}, 8\penalty0 (2):\penalty0
189--201, 1979.
\newblock ISSN 0304-3975.
\newblock \doi{https://doi.org/10.1016/0304-3975(79)90044-6}.
\newblock URL
\url{https://www.sciencedirect.com/science/article/pii/0304397579900446}.
\bibitem[Fuggitti(2019)]{Fuggitti2019}
Francesco Fuggitti.
\newblock Ltlf2dfa, mar 2019.
\newblock URL \url{https://doi.org/10.5281/zenodo.3888410}.
\bibitem[Papineni et~al.(2002)Papineni, Roukos, Ward, and
Zhu]{papineni2002bleu}
Kishore Papineni, Salim Roukos, Todd Ward, and Wei-Jing Zhu.
\newblock Bleu: a method for automatic evaluation of machine translation.
\newblock In \emph{Proceedings of the 40th annual meeting of the Association
for Computational Linguistics}, pages 311--318, 2002.
\bibitem[Lin(2004)]{lin-2004-rouge}
Chin-Yew Lin.
\newblock {ROUGE}: A package for automatic evaluation of summaries.
\newblock In \emph{Text Summarization Branches Out}, pages 74--81, Barcelona,
Spain, July 2004. Association for Computational Linguistics.
\newblock URL \url{https://aclanthology.org/W04-1013/}.
\bibitem[Vedantam et~al.(2015)Vedantam, Lawrence~Zitnick, and Parikh]{cider}
Ramakrishna Vedantam, C.~Lawrence~Zitnick, and Devi Parikh.
\newblock Cider: Consensus-based image description evaluation.
\newblock In \emph{Proceedings of the IEEE Conference on Computer Vision and
Pattern Recognition (CVPR)}, June 2015.
\bibitem[Anderson et~al.(2016)Anderson, Fernando, Johnson, and Gould]{spice}
Peter Anderson, Basura Fernando, Mark Johnson, and Stephen Gould.
\newblock Spice: Semantic propositional image caption evaluation.
\newblock In Bastian Leibe, Jiri Matas, Nicu Sebe, and Max Welling, editors,
\emph{Computer Vision -- ECCV 2016}, pages 382--398, Cham, 2016. Springer
International Publishing.
\newblock ISBN 978-3-319-46454-1.
\bibitem[Zhang et~al.(2023)Zhang, Dang, Peng, and Broeck]{zhang2023gelato}
Honghua Zhang, Meihua Dang, Nanyun Peng, and Guy Van~den Broeck.
\newblock Tractable control for autoregressive language generation.
\newblock In \emph{Proceedings of ICML}, 2023.
\bibitem[Meng et~al.(2022)Meng, Lu, Peng, and Chang]{meng2022_nado}
Tao Meng, Sidi Lu, Nanyun Peng, and Kai{-}Wei Chang.
\newblock Controllable text generation with neurally-decomposed oracle.
\newblock In \emph{Proceedings of {NeurIPS}}, 2022.
\bibitem[Radford et~al.(2019)Radford, Wu, Child, Luan, Amodei, Sutskever,
et~al.]{gpt2}
Alec Radford, Jeffrey Wu, Rewon Child, David Luan, Dario Amodei, Ilya
Sutskever, et~al.
\newblock Language models are unsupervised multitask learners.
\newblock \emph{OpenAI blog}, 1\penalty0 (8):\penalty0 9, 2019.
\bibitem[Lu and Peng(2021)]{insnet}
Sidi Lu and Nanyun Peng.
\newblock On efficient training, controllability and compositional
generalization of insertion-based language generators.
\newblock \emph{CoRR}, abs/2102.11008, 2021.
\newblock URL \url{https://arxiv.org/abs/2102.11008}.
\bibitem[Brown et~al.(2020)Brown, Mann, Ryder, Subbiah, Kaplan, Dhariwal,
Neelakantan, Shyam, Sastry, Askell, et~al.]{brown2020language}
Tom Brown, Benjamin Mann, Nick Ryder, Melanie Subbiah, Jared~D Kaplan, Prafulla
Dhariwal, Arvind Neelakantan, Pranav Shyam, Girish Sastry, Amanda Askell,
et~al.
\newblock Language models are few-shot learners.
\newblock \emph{Advances in neural information processing systems},
33:\penalty0 1877--1901, 2020.
\bibitem[OpenAI(2024{\natexlab{a}})]{openai2024gpt4technicalreport}
OpenAI.
\newblock Gpt-4 technical report, 2024{\natexlab{a}}.
\newblock URL \url{https://arxiv.org/abs/2303.08774}.
\bibitem[OpenAI(2024{\natexlab{b}})]{openai2024gpt4ocard}
OpenAI.
\newblock Gpt-4o system card, 2024{\natexlab{b}}.
\newblock URL \url{https://arxiv.org/abs/2410.21276}.
\bibitem[OpenAI(2024{\natexlab{c}})]{openai2024openaio1card}
OpenAI.
\newblock Openai o1 system card, 2024{\natexlab{c}}.
\newblock URL \url{https://arxiv.org/abs/2412.16720}.
\bibitem[Raedt et~al.(2020)Raedt, Dumancic, Manhaeve, and Marra]{raedt_survey}
Luc~De Raedt, Sebastijan Dumancic, Robin Manhaeve, and Giuseppe Marra.
\newblock From statistical relational to neuro-symbolic artificial
intelligence.
\newblock In \emph{Proceedings of International Joint Conference on Artificial
Intelligence}, 2020.
\bibitem[d’Avila Garcez and Lamb(2023)]{third_wave}
Artur d’Avila Garcez and Luis~C. Lamb.
\newblock {Neurosymbolic AI: The 3rd wave}.
\newblock \emph{Artificial Intelligence Review}, 2023.
\bibitem[Dash et~al.(2022)Dash, Chitlangia, Ahuja, and
Srinivasan]{dash_informed_ml_review}
Tirtharaj Dash, Sharad Chitlangia, Aditya Ahuja, and Ashwin Srinivasan.
\newblock A review of some techniques for inclusion of domain-knowledge into
deep neural networks.
\newblock \emph{Scientific Reports}, 12\penalty0 (1), 2022.
\bibitem[Giunchiglia et~al.(2022)Giunchiglia, Stoian, and
Lukasiewicz]{giunchiglia2022ijcai}
Eleonora Giunchiglia, Mihaela~Catalina Stoian, and Thomas Lukasiewicz.
\newblock Deep learning with logical constraints.
\newblock In \emph{Proceedings of International Joint Conference on Artificial
Intelligence}, 2022.
\bibitem[van Krieken et~al.(2023)van Krieken, Thanapalasingam, Tomczak,
Harmelen, and Teije]{krieken2023anesi}
Emile van Krieken, Thiviyan Thanapalasingam, Jakub~M. Tomczak, Frank~Van
Harmelen, and Annette~Ten Teije.
\newblock A-ne{SI}: A scalable approximate method for probabilistic
neurosymbolic inference.
\newblock In \emph{Proceedings of Neural Information Processing Systems}, 2023.
\bibitem[Giunchiglia et~al.(2024)Giunchiglia, Tatomir, Stoian, and
Lukasiewicz]{giunchiglia2024ccn+}
Eleonora Giunchiglia, Alex Tatomir, Mihaela~Catalina Stoian, and Thomas
Lukasiewicz.
\newblock {CCN+:} {A} neuro-symbolic framework for deep learning with
requirements.
\newblock \emph{International Journal of Approximate Reasoning}, 171, 2024.
\bibitem[Diligenti et~al.(2012)Diligenti, Gori, Maggini, and
Rigutini]{diligenti2012SBR}
Michelangelo Diligenti, Marco Gori, Marco Maggini, and Leonardo Rigutini.
\newblock Bridging logic and kernel machines.
\newblock \emph{Machine Learning}, 2012.
\bibitem[Fischer et~al.(2019)Fischer, Balunovic, Drachsler{-}Cohen, Gehr,
Zhang, and Vechev]{fischer2019DL2}
Marc Fischer, Mislav Balunovic, Dana Drachsler{-}Cohen, Timon Gehr, Ce~Zhang,
and Martin Vechev.
\newblock {DL2: T}raining and querying neural networks with logic.
\newblock In \emph{Proceedings of International Conference on Machine
Learning}, 2019.
\bibitem[van Krieken et~al.(2022)van Krieken, Acar, and van
Harmelen]{krieken2022_analyzing}
Emile van Krieken, Erman Acar, and Frank van Harmelen.
\newblock Analyzing differentiable fuzzy logic operators.
\newblock \emph{Artificial Intellegence}, 302:\penalty0 103602, 2022.
\bibitem[Pryor et~al.(2023)Pryor, Dickens, Augustine, Albalak, Wang, and
Getoor]{pryor2023NeuPSL}
Connor Pryor, Charles Dickens, Eriq Augustine, Alon Albalak, William~Yang Wang,
and Lise Getoor.
\newblock Neupsl: Neural probabilistic soft logic.
\newblock In \emph{Proceedings of International Joint Conference on Artificial
Intelligence}, 2023.
\bibitem[Hoernle et~al.(2022)Hoernle, Karampatsis, Belle, and
Gal]{hoernle2022multiplexnet}
Nicholas Hoernle, Rafael{-}Michael Karampatsis, Vaishak Belle, and Kobi Gal.
\newblock {MultiplexNet: T}owards fully satisfied logical constraints in neural
networks.
\newblock In \emph{Proceedings of Association for the Advancement of Artificial
Intelligence}, 2022.
\bibitem[Misino et~al.(2022)Misino, Marra, and Sansone]{misino2023tvael}
Eleonora Misino, Giuseppe Marra, and Emanuele Sansone.
\newblock {VAEL: Bridging Variational Autoencoders and Probabilistic Logic
Programming}.
\newblock In \emph{Proceedings of Neural Information Processing Systems}, 2022.
\bibitem[Yang and Klein(2021)]{Yang2021_fudge}
Kevin Yang and Dan Klein.
\newblock {FUDGE:} controlled text generation with future discriminators.
\newblock In \emph{Proceedings of {NAACL-HLT}}, pages 3511--3535, 2021.
\bibitem[Erzin et~al.(2022)Erzin, Plotnikov, and Ladygin]{Erzin2022}
Adil Erzin, Roman Plotnikov, and Ilya Ladygin.
\newblock Constrained shortest path and hierarchical structures, 2022.
\newblock URL \url{https://arxiv.org/abs/2204.04960}.
\end{thebibliography}