\section{Introduction}
The use of \emph{recurrent neural networks} (\emph{RNN}s)~\cite{dnn}
is on the rise. RNNs are a particular kind of deep neural networks
(DNNs), with the useful ability to store information from previous
evaluations in constructs called \emph{memory units}. This
differentiates them from \emph{feed-forward neural networks}
(\emph{FFNNs}), where each evaluation of the network is performed
independently of past evaluations.  The presence of memory units
renders RNNs particularly suited for tasks that involve context, such
as machine translation~\cite{DeChLeTo18}, health
applications~\cite{LiKaElWe16}, speaker recognition~\cite{WaWaPaLo18},
and many other tasks where the network's output might be affected by
previously processed inputs.

Part of the success of RNNs (and of DNNs in general) is attributed to
their very attractive generalization properties: after being trained
on a finite set of examples, they generalize well to inputs they have
not encountered before~\cite{dnn}. Unfortunately, it is known that
RNNs may react in highly undesirable ways to certain inputs. For
instance, it has been observed that many RNNs are vulnerable to
\emph{adversarial inputs}~\cite{CiAdNeKe17,SzZaSuBrErGoFe13}, where
small, carefully-crafted perturbations are added to an input in order
to fool the network into a classification error. This example, and
others, highlight the need to \emph{formally verify} the correctness
of RNNs, so that they can reliably be deployed in safety-critical
settings. However, while DNN verification has received significant
attention in recent years
(e.g.,~\cite{BuTuToKoMu18,ChNuHuRu18,ChNuRu17,Eh17,GeMiDrTsChVe18,GoAdKeKa20,HuKwWaWu17,KaBaDiJuKo17,Marabou,LoMa17,NaKaRySaWa17,TjXiTe19,WaPeWhYaJa18,WuOzZeIrJuGoFoKaPaBa20}),
almost all of these efforts have been focused on FFNNs, with very
little work done on RNN verification.

To the best of our knowledge, the only existing general approach for
RNN verification is via \emph{unrolling}~\cite{AkKeLoPi19}: the RNN is
duplicated and concatenated onto itself, creating an equivalent
feed-forward network that operates on a sequence of $k$ inputs
simultaneously, as opposed to one at a time. The FFNN can then be
verified using existing verification technology. The
main limitation of this approach is that unrolling
increases the network size by a factor of $k$ (which, in real-world applications,
can be in the hundreds~\cite{WaWaPaLo18}).
Because the complexity of FFNN verification is known to
be worst-case exponential in the size of the network~\cite{ReluPlex}, this reduction gives
rise to FFNNs that are difficult to verify --- and is hence applicable
primarily to small RNNs with short input sequences.

Here, we propose a novel approach for RNN verification, which affords
far greater scalability than unrolling.  Our approach also
reduces the RNN verification problem into FFNN verification, but does
so in a way that is independent of the number of inputs that the RNN
is to be evaluated on. Specifically, our approach consists of two main
steps: (i) create an FFNN that \emph{over-approximates} the RNN, but
which is the same size as the RNN; and (ii) verify properties over this
over-approximation using existing techniques for FFNN verification.
Thus, our approach circumvents any duplication of the network or its
inputs.

In order to perform step (i), we leverage the well-studied notion of
\emph{inductive invariants}: our FFNN encodes time-invariant
properties of the RNN, which hold initially and continue to hold after
the RNN is evaluated on each additional input. Automatic inference of
meaningful inductive invariants has been studied extensively
(e.g.,~\cite{NgAnRuHi17,ShDiDiAi11,SiDaRaNaSo18}), and is known to be
highly difficult~\cite{PaImShKaSa16}. We propose here an approach for
generating invariants according to \emph{predefined templates}. By
instantiating these templates, we automatically generate a candidate
invariant $I$, and then: (i) use our underlying FFNN verification
engine to prove that $I$ is indeed an invariant; and (ii) use $I$ in
creating the FFNN over-approximation of the RNN, in order to prove the
desired property. If either of these steps fail, we refine $I$ (either
strengthening or weakening it, depending on the point of failure), and
repeat the process. The process terminates when the property is proven
correct, when a counter-example is found, or when a certain timeout
value is exceeded.

We evaluate our approach using a proof-of-concept implementation,
which uses the Marabou tool~\cite{Marabou} as its FFNN verification
back-end. When compared to the state of the art on a set of benchmarks
from the domain of speaker recognition~\cite{WaWaPaLo18}, our approach
is orders-of-magnitude faster. Our implementation, together with our benchmarks
and experiments, is available online~\cite{RNNCode}.

The rest of this paper is organized as follows.  In
Sec.~\ref{sec:background}, we provide a brief background on DNNs and
their verification. In Sec.~\ref{sec:method}, we describe our approach
for verifying RNNs via reduction to FFNN verification, using
invariants. We describe automated methods for RNN invariant inference
in Sec.~\ref{sec:invariant_generation}, followed by an evaluation of
our approach in Sec.~\ref{sec:evaluation}. We then discuss related
work in Sec.~\ref{sec:relatedWork}, and conclude with
Sec.~\ref{sec:conclusion}.

\section{Background}
\label{sec:background}

\subsection{Feed-Forward Neural Networks and their Verification}

An FFNN $N$ with $n$ layers consists of an input layer, $n-2$ hidden
layers, and an output layer.
We use $s_i$ to denote the \emph{dimension} of layer $i$, which is the number of
neurons in that layer. We use $v_{i,j}$ to refer to the $j$-th neuron in the
$i$-th layer.
Each hidden layer is associated with a weight matrix $W_i$ and a bias
vector $b_i$. The FFNN input vector is denoted as $v_1$, and the output
vector of each hidden layer $1 < i < n$ is $v_i = f\left( W_i v_{i-1} + b_i
\right)$, where $f$ is some element-wise activation function (such as
$\text{ReLU}\xspace{}{}(x) = \max{}(0,x)$). The output layer is evaluated similarly, but
without an activation function: $v_n = W_{n-1}v_{n-1}+b_n$.  Given an input
vector $v_1$, the network is evaluated by sequentially calculating $v_i$ for
$i=2,3,\ldots,n$, and returning $v_n$ as the network's output.

\begin{wrapfigure}[8]{r}{4.5cm}
  \vspace{-1cm}
  \begin{center}
    \scalebox{0.9}{
      \input{fig_fullyconnect}
    }
    \caption{A simple feed-forward neural network.}
    \label{fig:fullyConnectNetwork}
  \end{center}
\end{wrapfigure}

A simple example appears in Fig.~\ref{fig:fullyConnectNetwork}. This
FFNN has a single input neuron $v_{1,1}$, a single
output neuron $v_{3,1}$, and two hidden neurons $v_{2,1}$ and
$v_{2,2}$. All bias values are assumed to be
$0$, and we use the common $\text{ReLU}\xspace{}{}(x) = \max(0,x)$ function as our activation function.
When the input neuron is assigned
$v_{1,1}=4$, the weighted sum and activation functions
yield $v_{2,1}=\text{ReLU}\xspace{}{}(4)=4$ and $v_{2,2}=\text{ReLU}\xspace{}{}(-4)=0$. Finally, we obtain
the output $v_{3,1} = 4$.

\mysubsubsection{FFNN Verification.}
In FFNN verification we seek inputs that satisfy certain constraints,
such that their corresponding outputs also satisfy certain
constraints. Looking again at the network from
Fig.~\ref{fig:fullyConnectNetwork}, we might wish to know whether
$v_{1,1}\leq 5$ always entails $v_{3,1}<20$. Negating the output
property, we can use a verification engine to check whether it is
possible that $v_{1,1}\leq 5$ and $v_{3,1}\geq 20$. If this query is
unsatisfiable (\texttt{UNSAT}{}), then the original property holds; otherwise,
if the query is satisfiable (\texttt{SAT}{}), then the verification engine
will provide us with a counter-example (e.g.,
$v_{1,1}=-10, v_{3,1}=20$ in our case).

Formally, we define an FFNN verification query as a triple
$\langle P,N,Q\rangle$, where $N$ is an FFNN, $P$ is a predicate over
the input variables $x$, and $Q$ is a predicate over the output
variables $y$. Solving this query entails deciding whether there
exists a specific input assignment $x_0$ such that
$P(x_0)\wedge Q(N(x_0))$ holds (where $N(x_0)$ is the output of $N$ for the
input $x_0$). It has been shown that even for simple FFNNs and for predicates
$P$ and $Q$ that are conjunctions of linear constraints, the
verification problem is NP-complete~\cite{ReluPlex}: in the
worst-case, solving it requires a number of operations that is
exponential in the number of neurons in $N$.

\subsection{Recurrent Neural Networks}

Recurrent Neural Networks (RNNs) are similar to FFNNs, but have an
additional construct called a \emph{memory unit}. Memory units allow a hidden
neuron to \emph{store} its assigned value for a specific evaluation
of the network, and have that value become part of the neuron's
weighted sum computation in the \emph{next} evaluation. Thus, when
evaluating the RNN in time step $t+1$, e.g. when the RNN reads the
$t+1$'th word in a sentence, the results of the $t$ previous evaluations can
affect the current result.

A simple RNN appears in Fig.~\ref{fig:rnn_1d}. There, node $\tilde{v}_{2,1}$
represents node $v_{2,1}$'s memory unit (we draw memory units as squares, and
mark them using the tilde sign). When computing the weighted sum for node
$v_{2,1}$, the value of $\tilde{v}_{2,1}$ is also added to the sum, according to
its listed weight ($1$, in this case). We then update $\tilde{v}_{2,1}$ for the
next round, using the vanilla RNN update rule: $\tilde{v}_{2,1} :=
v_{2,1}$. Memory units are initialized to $0$ for the first evaluation, at time
step $t=1$.

\begin{figure}[htp]
  \begin{minipage}{.42\textwidth}
    \begin{center}
      \begin{tabular}{cc|ccccc}
        \toprule
        Time Step &&&
        $v_{1,1}$ &
        $v_{2,1}$ &
        $\tilde{v}_{2,1}$ &
        $v_{3,1}$
        \\
        \midrule
        1 &&& 0.5 & 0.5 & 0 & 0.5 \\
        2 &&& 1.5 & 2 & 0.5 & 2 \\
        3 &&& -1 & 1 & 2 & 1 \\
        4 &&& -3 & 0 & 1 & 0 \\
        \bottomrule
      \end{tabular}
    \end{center}
  \end{minipage}
  \begin{minipage}{.42\textwidth}
    \begin{center}
      \begin{tikzpicture}[shorten >=1pt,->,draw=black!50, node distance=2.5cm,font=\footnotesize]
        \def2.5cm{2.5cm}
        \node[input neuron] (I-1) at (0,-1) {$v_{1,1}$};
        \path[] node[shadow neuron] (H-1-s)  at (0.5*2.5cm,0.5) {$\tilde{v}_{2,1}$};
        \path[] node[hidden neuron] (H-1)  at (2.5cm,-1) {$v_{2,1}$};
        \node[output neuron] at (2*2.5cm, -1) (O-1) {$v_{3,1}$};

        \draw[nnedge] (I-1) -- node[above] {$1$} (H-1);
        \draw[nnedge] (H-1-s) edge[bend left, black] node[above] {$\ 1$} (H-1);
        \draw[nnedge] (H-1) edge[bend left, dotted, black] node[] {} (H-1-s);
        \draw[nnedge] (H-1) -- node[above] {$1$} (O-1);

      \end{tikzpicture}
    \end{center}
  \end{minipage}
  \caption{ An illustration of a toy RNN with the ReLU activation
    function. Each row of the table represents a single time step,
    and depicts the value of each neuron for that step. Using a $t$
    superscript to represent time step $t$, we observe that
    $v^t_{2,1}$ is computed as
    $\max{}(0, \tilde{v}^{t}_{2,1} + v^t_{1,1})$, according to the ReLU
    function. }
  \label{fig:rnn_1d}
\end{figure}

The FFNN definitions are extended to RNNs as follows. We use the $t$
superscript to indicate the timestamp of the RNN's evaluation: e.g.,
$v_{3,2}^4$ indicates the value that node $v_{3,2}$ is assigned in the
$4$'th evaluation of the RNN.  We associate each hidden layer of the
RNN with a square matrix $H_i$ of dimension $s_i$, which represents
the weights on edges from memory units to neurons.  Observe that each
memory unit in layer $i$ can contribute to the weighted sums of all
neurons in layer $i$, and not just to the neuron whose values it
stores.  For time step $t>0$, the evaluation of each hidden layer
$1<i<n$ is now computed by
$v^{t}_i = f\left(W_i v^{t}_{i-1} + H_i \tilde{v}^{t}_i + b_i\right)$,
and the output values are given by $v^t_n = W_nv^t_{n-1} + H_nv^{t-1}_n + b_n$.
By convention, we initialize memory units to $0$ (i.e. for every
memory unit $\tilde{v}$, $\tilde{v}^1 = 0$).  For simplicity, we
assume that each hidden neuron in the network has a memory unit. This
definition captures also ``regular'' neurons, by setting the
appropriate entries of $H$ to 0.

While we focus here on vanilla RNNs, our technique could be extended
to, e.g., LSTMs or GRUs; we leave
this for future work.

\mysubsubsection{RNN Verification.}
 We define an RNN verification query as a
tuple $\langle P, N, Q, T_{\max}\rangle$, where $P$ is an input property, $Q$ is
an output property, $N$ is an RNN, and $T_{\max}\in \mathbb{N}$ is a bound on
the time interval for which the property should hold. $P$ and $Q$ include linear
constraints over the network's inputs and outputs, and may
also use the notion of time.

As a \setlabel{running example}{par:rnn_example},
consider the network from Fig.~\ref{fig:rnn_1d}, denoted by $N$, the
input predicate
$P = \bigwedge_{t=1}^5(-3\leq v^t_{1,1}\leq 3)$, the
output predicate
$Q = \bigvee_{t=1}^5(v_{3,1}^t \geq 16)$, and the time bound $T_{\max}=5$. This query searches for an
evaluation of $N$ with $5$ time steps, in which all input values are
in the range $[-3,3]$, and such that at some time step the output value is at least 16.
By the weights of $N$, it can be proved that $v^t_{3,1}$ is
at most the sum of the ReLUs of inputs so far, $v^t_{3,1}\leq
\sum_{i=1}^t\text{ReLU}\xspace{}{}(v_{1,1}^i)\leq 3t$; and so $v_{3,1}^t\leq
15$ for all $1\leq t \leq 5$, and the query is \texttt{UNSAT}{}.

\subsection{Inductive Invariants}
\label{sec:inductive_invariant}
Inductive invariants~\cite{PaImShKaSa16} are a well-established way to reason
about software with loops. Formally, let $\langle Q, q_0, T\rangle$ be
a transition system, where $Q$ is the set of states, $q_0\in Q$ is an
initial state, and $T\subseteq Q\times Q$ is a transition relation.
An invariant $I$ is a logical formula defined over the states of $Q$,
with two properties:
\begin{inparaenum}[(i)]
\item $I$ holds for the initial state, i.e. $I(q_0)$ holds; and
\item $I$ is closed under $T$, i.e. $(I(q) \wedge
  \langle q,q' \rangle\in T) \Rightarrow I(q')$.
  \end{inparaenum}
  If it can be proved (in a given proof system) that formula $I$ is an
  invariant, we say that $I$ is an inductive invariant.

  Invariants are particularly useful when attempting to verify that a
  given transition system satisfies a \emph{safety property}. There,
  we are given a set of bad states $B$, and seek to prove that none of
  these states is reachable. We can do so by showing that
  $\{q\in Q \ |\ I(q)\}\cap B=\emptyset$.  Unfortunately,
  automatically discovering invariants for which the above holds is
  typically an undecidable problem~\cite{PaImShKaSa16}. Thus, a common
  approach is to restrict the search space --- i.e., to only search
  for invariants with a certain syntactic form.

\section{Reducing RNN Verification to FFNN Verification}
\label{sec:method}

\subsection{Unrolling}

To date, the only available general approach for verifying
RNNs~\cite{AkKeLoPi19} is to transform the RNN in question into a
\emph{completely equivalent}, feed-forward network, using
\emph{unrolling}. An example appears in Fig.~\ref{fig:unroll}. The
idea is to leverage $T_{\max}$, which is an upper bound on the number of times
that the RNN will be evaluated. The RNN is duplicated $T_{\max}$ times, once
for each time step in question, and its memory units are
removed. Finally, the nodes in the $i$'th copy are used to fill the
role of memory units for the $i+1$'th copy of the network.

While unrolling gives a sound reduction from RNN verification to FFNN
verification, it unfortunately tends to produce very large networks.
When verifying a property that involves $t$ time steps, an RNN network
with $n$ memory units will be transformed into an FFNN with
$(t-1)\cdot n$ new nodes. Because the FFNN verification problem
becomes exponentially more difficult as the network size
increases~\cite{ReluPlex}, this renders the problem infeasible for
large values of $t$. As scalability is a major limitation of existing
FFNN verification technology, unrolling can currently only be applied
to small networks that are evaluated for a small number of time steps.

\begin{figure}[htp]
    \begin{center}
        \scalebox{0.8}{ \input{fig_unrolling} }
        \caption{ Unrolling the network from Fig.~\ref{fig:rnn_1d}, for $T_{\max}=5$
            time steps. The edges in red fill the role of the
            memory units of the original RNN. The number of neurons in
            the unrolled network is $5$ times the number of neurons in
            the original. }
    \label{fig:unroll}
    \end{center}
\end{figure}

\subsection{Circumventing Unrolling}
\label{sec:overApproximation}

We propose a novel alternative to unrolling, which can reduce RNN
verification to FFNN verification without the blowup in network
size. The idea is to transform a verification query
$\varphi = \langle P, N, Q, T_{\max}\rangle$ over an RNN $N$ into a
different verification query
$\hat{\varphi} = \langle \hat{P}, \hat{N}, \hat{Q}\rangle$ over an
FFNN $\hat{N}$.  $\hat{\varphi}$ is not equivalent to $\varphi$, but
rather \emph{over-approximates} it: it is constructed in a way that
guarantees that if $\hat{\varphi}$ in \texttt{UNSAT}{}, then $\varphi$ is also
\texttt{UNSAT}{}. As is often the case, if $\hat{\varphi}$ is \texttt{SAT}{}, either
the original property truly does not hold for $N$, or the
over-approximation is too coarse and needs to be refined; we discuss
this case later.

A key point in our approach is that $\hat{\varphi}$ is created
in a way that captures the notion of time in the FFNN setting, and
without increasing the network size. This is done by incorporating
into $\hat{P}$ an \emph{invariant} that puts bounds on the memory
units as a function of the time step $t$. This invariant does not
precisely compute the values of the memory units --- instead, it
bounds each of them in an interval. This inaccuracy is what makes
$\hat{\varphi}$ an over-approximation of $\varphi$. More specifically,
the construction is performed as follows:
\begin{enumerate}
  \item $\hat{N}$ is constructed from $N$ by adding a new input
    neuron, $t$, to represent time. In line with standard FFNN
    definitions, $t$ is treated as a
    real number.
  \item For every node $v$ with memory unit $\tilde{v}$, in $\hat{N}$
    we replace $\tilde{v}$ with a regular neuron, $v^m$, which is
    placed in the input layer.  Neuron $v^m$ will be connected to the
    network's original neurons with the original weights, just as
    $\tilde{v}$ was.\footnote{Note that we slightly abuse the
      definitions from Sec.~\ref{sec:background}, by allowing an input
      neuron to be connected to neurons in layers other than its
      preceding layer.}
  \item We set $\hat{P}=P\wedge (1\leq t\leq T_{\max})\wedge I$, where
    $I$ is a formula that bounds the values of each new $v^m$ node as a function of
    the time step $t$. The constraints in $I$ constitute
    the invariant over the memory units' values.
    \item The output property is unchanged: $\hat{Q}=Q$.
\end{enumerate}

We name $\hat{\varphi}$ and $\hat{N}$ constructed in this way the
\emph{snapshot query} and the \emph{snapshot network}, respectively,
and denote  $\hat{\varphi} = \mathcal{S}{}(\varphi)$ and $\hat{N}=\mathcal{S}{}(N)$.
The intuition behind this construction is that query $\hat{\varphi}$
encodes a snapshot (an assignment of $t$) in which all constraints
are satisfied. At this point in time, the $v^m$ nodes
represent the values stored in the memory units (whose assignments
are bounded by the invariant $I$); and the input and output nodes
represent the network's inputs and outputs at time $t$. Clearly, a
satisfying assignment for $\hat{\varphi}$ does not necessarily
indicate a counter-example for $\varphi$; e.g., because the values
assigned to $v^m$ might be impossible to obtain at time $t$ in the
original network. However, if $\hat{\varphi}$ is \texttt{UNSAT}{} then so is
$\varphi$, because there does not exist a point in time in which the
query might be satisfied. Note that the construction only increases the network size
by $1$ (the $v^m$ neurons replace the memory units, and we add a
single neuron $t$).

\mysubsubsection{Time-Agnostic Properties.}
In the aforementioned construction of $\hat{\varphi}$, the original
properties $P$ and $Q$ appear, either fully or as a conjunct, in the
new properties $\hat{P}$ and $\hat{Q}$. It is not immediately clear that this is
possible, as $P$ and $Q$ might also involve time. For example,
if $P$ is the formula $v_{1,2}^7\geq 10$, it cannot be
directly incorporated into $\hat{P}$, because $\hat{N}$ has no notion
of time step $7$.

For simplicity, we assume that $P$ and $Q$ are \emph{time-agnostic},
i.e. are given in the following form:
$P = \bigwedge_{t=1}^{T_{\max}}\psi_1$ and
$Q=\bigvee_{t=1}^{T_{\max}}\psi_2$, where $\psi_1$ and $\psi_2$
contain linear constraints over the inputs and outputs of $N$,
respectively, at time stamp $t$.  This formulation can express queries
in which the inputs are always in a certain interval, and a bound
violation of the output nodes is sought. Our running example from
Fig.~\ref{fig:rnn_1d} has this structure. When the properties are
given in this form, we set $\hat{P} = \psi_1$ and $\hat{Q} =\psi_2$,
with the $t$ superscripts omitted for all neurons.  This assumption
can be relaxed significantly; see Sec.~\ref{sec:relaxTimeAgnostic} of
the appendix

\begin{wrapfigure}[9]{r}{4.5cm} \vspace{-1.2cm}
    \begin{center}
    \scalebox{0.8}{
        \input{fig_rnn_encoding}
    }
        \caption{
          The feed-forward snapshot network $\hat{N}$ for the RNN from
            Fig.~\ref{fig:rnn_1d}.
        }
    \label{fig:encoding}
    \end{center}
\end{wrapfigure}

\mysubsubsection{Example.}
We demonstrate our approach on the running
example from Fig.~\ref{fig:rnn_1d}. Recall that
$P = \bigwedge_{t=1}^5(-3\leq v^t_{1,1}\leq 3)$,
and
$Q = \bigvee_{t=1}^5(v_{3,1}^t \geq 16)$.
First, we build the snapshot network $\hat{N}$ (Fig.~\ref{fig:encoding})
by replacing the memory unit $\tilde{v}_{2,1}$ with a regular
neuron, $v^m_{2,1}$, which is connected to node $v_{2,1}$
with weight 1 (the same weight previously found on the edge from
$\tilde{v}_{2,1}$ to $v_{2,1}$), and adding neuron $t$
to represent time. Next, we set $\hat{P}$ to be the conjunction of
\begin{inparaenum}[(i)]
\item $P$, with its internal conjunction and $t$ superscripts omitted;
\item the time constraint $1\leq t\leq 5$; and
  \item
the
invariant that bounds the values of $v^m_{2,1}$ as a function of
time: $v^m_{2,1}\leq 3(t-1)$.
\end{inparaenum}
Our new verification query is thus:
\[
  \langle
  \underbrace{
  v_{1,1} \in \left[-3,3\right]
  \wedge
  t \in \left[1,5\right]
  \wedge
  (v^m_{2,1}\leq 3(t-1))}_{\hat{P}},
  \hat{N},
  \underbrace{v_{3,1}\geq 16}_{\hat{Q}}
  \rangle
\]
This query is, of course, \texttt{UNSAT}{}, indicating that the original query is
also \texttt{UNSAT}{}. Note that the new node $t$ is added solely for the
purpose of including it in constraints that appear in $\hat{P}$.

The requirement that $I$ be an invariant over the memory units of $N$
 ensures that our approach is sound. Specifically,
it guarantees
that $I$ allows any assignment for $v^m$ that the
original memory unit $\tilde{v}$ might be assigned.
This is formulated in the following lemma
(whose
proof, by induction, is omitted):
\begin{lemma}
  Let $\varphi = \langle P, N, Q, T_{\max}\rangle$ be an RNN verification
  query, and let
  $\hat{\varphi} = \langle \hat{P}, \hat{N}, \hat{Q}\rangle$ be the
  snapshot query $\hat{\varphi}=\mathcal{S}{}(\varphi)$.  Specifically,
  let $\hat{P} = P \wedge (1\leq t \leq T_{\max})\wedge I$, where $I$ is an
  invariant that bounds the values of each $v^m$.  If $\hat{\varphi}$
  is \texttt{UNSAT}{}, then $\varphi$ is also \texttt{UNSAT}{}.
\end{lemma}

\subsection{Constructing $\hat{\varphi}:$ Verifying the Invariant}
\label{sec:verifyInvariant}
A key assumption in our reduction from RNN to FFNN verification was
that we were supplied some invariant $I$, which bounds the values of
the $v^m$ neurons as a function of the time $t$. In this section we
make our method more robust, by including a step that verifies that
the supplied formula $I$ is indeed an invariant. This step, too, is
performed by creating an FFNN verification query, which can then be
dispatched using the back-end FFNN verification engine.  (We treat $I$
simultaneously as a formula over the nodes of $\mathcal{S}{}(N)$ and
those of $N$; the translation is performed
by renaming every occurrence of $v^m$
to $\tilde{v}^t$, or vice versa.)

First, we adjust the definitions of an inductive invariant
(Sec.~\ref{sec:inductive_invariant}) to the RNN setting.
The state space $Q$ is comprised of states
$ q = \langle \mathcal{A}, t\rangle $, where $\mathcal{A}$ is the
current assignment to the nodes of $N$ (including the assignments of
the memory units), and $t\in\mathbb{N}$ represents time
step. For another state $q'=\langle \mathcal{A}',t'\rangle$, the
transition relation $T(q,q')$ holds if and only if:
\begin{inparaenum}[(i)]
\item $t'=t+1$;  i.e., the time step has advanced by one;
\item for each neuron $v$ and its memory unit $\tilde{v}$
    it holds that $\mathcal{A}'[\tilde{v}] = \mathcal{A}[v]$; i.e.,
    the vanilla RNN update rule holds; and
\item the assignment $\mathcal{A}'$ of all of the network's neurons
  constitutes a proper evaluation of the RNN according to
  Sec.~\ref{sec:background}; i.e., all weighted sums and activation
  functions are computed properly.
\end{inparaenum}
A state $q_0$ is initial if $t=1$, $\tilde{v} = 0$ for every memory unit,
and the assignment of the network's neurons
constitutes a proper evaluation of the RNN.

Next, let $I$ be a formula over the memory units of $N$, and suppose we
wish to verify that $I$ is an invariant.
Proving that $I$ is in invariant amounts to proving that
$I(q_0)$ holds for any initial state $q_0$, and that for every two
states $q,q'\in Q$, $I(q) \wedge T(q,q')
\rightarrow I(q')$.
Checking whether $I(q_0)$ holds is trivial.
The second check is more tricky; here, the key point is that because
$q$ and $q'$ are consecutive states, the memory units of $q'$ are
simply the neurons of $q$. Thus, we can prove that $I$ holds for $q'$ by looking at
 the snapshot network, assuming that $I$ holds initially, and proving that
$I[v^m\mapsto v, t\mapsto t+1]$, i.e. the invariant with each memory unit
$v^m$ renamed to its corresponding neuron $v$ and the time step
advanced by $1$, also holds. The resulting verification query, which
we term $\varphi_I$,
 can be verified using the underlying FFNN verification back-end.

We illustrate this process using the running example from Fig.~\ref{fig:rnn_1d}.
Let $I=v^m_{2,1}\leq 3(t-1)$.  $I$ holds at every initial state $q_0$; this is
true because at time $t=1$, $v^m_{2,1} = 0 \leq 3\cdot 0$. Next, we
assume that $I$ holds for state $q=\langle \mathcal{A}, t\rangle$ and
prove that it holds for $q=\langle \mathcal{A}', t + 1\rangle$.
 First, we create the snapshot FFNN $\hat{N}$, shown in
 Fig.~\ref{fig:encoding}. We then extend the original input property
 $P = \bigwedge_{t=1}^5(-3\leq v^t_{1,1}\leq 3)$ into a property
 $P'$ that also captures our assumption that the invariant holds at
 time $t$:
$
   P' = (-3\leq v_{1,1}\leq 3) \wedge (v^m_{2,1}\leq 3(t-1)).
$
 Finally, we prepare an output property $Q'$ that asserts that the
 invariant does not hold for $v_{2,1}$ at time $t+1$, by renaming
 $v_{2,1}^m$ to $v_{2,1}$ and incrementing $t$:
 $
   Q' = \neg( v_{2,1} \leq 3(t+1-1)).
$
When the FFNN verification engine answers
that $\varphi_I=\langle P', \mathcal{S}{}(N), Q'\rangle$ is \texttt{UNSAT}{}, we conclude that $I$ is indeed an
invariant. In cases where the query turns out to be \texttt{SAT}{}, $I$ is not
an invariant, and needs to be refined.

Given a formula $I$, the steps described so far allow us to reduce RNN verification to FFNN
verification, in a completely sound and automated way. Next we discuss how to
automate the generation of $I$, as well.

\section{Invariant Inference}
\label{sec:invariant_generation}

\subsection{Single Memory Units}
\label{sec:single_dim}

In general, automatic invariant inference
is undecidable~\cite{PaImShKaSa16}; thus, we employ here a
heuristic approach, that uses \emph{linear templates}.
We first describe the approach on a simple case, in which the network has
a single hidden node $v$ with a memory unit, and then relax this limitation.
Note that the running example depicted in
Fig.~\ref{fig:rnn_1d} fits this case. Here, inferring an invariant according to a
linear template means finding values
$\alpha_l$ and $\alpha_u$, such that
$
\alpha_l \cdot (t-1) \le \tilde{v}^t \le \alpha_u \cdot (t-1).
$
The value of $\tilde{v}^t$ is thus bounded from below and from above
as a function of time. In our template we use $(t-1)$, and not $t$, in
order to account for the fact that $\tilde{v}^t$ contains the value
that node $v$ was assigned at time $t-1$.  For simplicity, we focus
only on finding the upper bound; the lower bound case is symmetrical.
We have already seen such an upper bound for our running example,
which was sufficiently strong for proving the desired property:
$\tilde{v}^t_{2,1}\leq 3(t-1)$.

Once candidate $\alpha$'s are proposed, verifying that the
invariant holds is performed using the techniques outlined in
Sec.~\ref{sec:method}. There are two places where the process might
fail:
\begin{inparaenum}[(i)]
\item the proposed invariant cannot be proved ($\varphi_I$ is \texttt{SAT}{}), because a
  counter-example exists. This means that our invariant is \emph{too
    strong}, i.e. the bound is too tight. In this case we can weaken
  the invariant by increasing $\alpha_u$; or
\item the proposed invariant holds, but the FFNN verification problem
  that it leads to, $\hat{\varphi}$, is \texttt{SAT}{}. In this case, the invariant is
  \emph{too weak}: it does not
  imply the desired output property. We can
  strengthen the invariant by decreasing $\alpha_u$.
\end{inparaenum}

This search problem leads us to binary search strategy,
described in Alg.~\ref{alg:verification_1d}.  The search stops,
i.e. an optimal invariant is found, when $ub-lb\leq \epsilon$ for a
small constant $\epsilon$. The algorithm
fails if the optimal linear invariant is found, but is insufficient
for proving the property in question; this can happen if $\varphi$ is
indeed \texttt{SAT}{}, or if a more sophisticated invariant is required.
\begin{algorithm}
\caption{Automatic Single Memory Unit Verification($P,N, Q, T_{\max}$) }
\begin{algorithmic}[1]
  \State $lb \leftarrow -M$, $ub \leftarrow M$ \Comment{M is a large constant}
  \While {$ub - lb \ge \epsilon$}
      \State $\alpha_{u} \leftarrow \frac{ub+lb}{2},\quad I \leftarrow v_{2,1}^m \le \alpha_u \cdot (t-1)$
      \If {$\varphi_I$ is \texttt{UNSAT}{}}
          \State Construct $\hat{\varphi}$ using invariant $I$
          \If {$\hat{\varphi}$ is \texttt{UNSAT}{}}
          \State \Return True
          \EndIf
          \State $ub \leftarrow \alpha_{u}$  \Comment{Invariant too weak}
          \label{step:stronger_invariant}
       \Else
          \State $lb \leftarrow
          \alpha_{u}$ \Comment{Invariant too strong} \label{step:weaker_invariant}
       \EndIf
  \EndWhile
  \State \Return False
\end{algorithmic}
\label{alg:verification_1d}
\end{algorithm}

\mysubsubsection{Discussion: Linear Templates.}
Automated invariant inference has been studied extensively in program
analysis (see Sec.~\ref{sec:relatedWork}). In
particular, elaborate templates have been proposed, which are more
expressive than the linear template that we use. The approach we
presented in Sec.~\ref{sec:method} is general, and is compatible with
many of these templates. Our main motivation for focusing on linear
templates is that most FFNN verification tools readily support linear
constraints, and can thus verify the $\varphi_I$ queries that
originate from linear invariants.  As we demonstrate in
Sec.~\ref{sec:evaluation}, despite their limited expressiveness,
linear invariants are already sufficient for solving many verification
queries.  Extending the technique to work with more expressive
invariants is part of our ongoing work.

\mysubsubsection{Multiple Memory Units in Separate Layers.}
Our approach can be extended to RNNs with multiple memory units,
each in a separate layer, in an iterative
fashion: an invariant is proved separately for each layer, by using
the already-proved invariants of the previous layers. As before, we
begin by constructing the snapshot network in which all memory units
are replaced by regular neurons.  Next, we work layer by layer and
generate invariants that over-approximate each memory unit, by
leveraging the invariants established for memory units in the previous
layers.  Eventually, all memory units are over-approximated using
invariants, and we can attempt to prove the desired property by
solving the snapshot query. An example and the general algorithm for this case
appears in Sec.~\ref{sec:app_multiple_layers} of the appendix

\subsection{Layers with Multiple Memory Units}
\label{sec:multidim_verification}

\begin{wrapfigure}[14]{r}{4.5cm}
  \vspace{-1.2cm}
    \begin{center}
    \scalebox{0.8}{ \input{fig_2d_rnn.tex} }
    \caption{
      An RNN where both memory units
      affect both neurons of the hidden layer:
        $v^t_{2,1} = \text{ReLU}\xspace{}{}(\tilde{v}^t_{2,1}  + \tilde{v}^t_{2,2}
        - v_{1,1}^t)$;
        and
        $v^t_{2,2} = \text{ReLU}\xspace{}{}(-\tilde{v}^t_{2,1}  + \tilde{v}^t_{2,2}
        +2  v_{1,1}^t)$.
    }
    \label{fig:rnn_2d}
    \end{center}
\end{wrapfigure}

We now extend our approach to support the most general case: an RNN
with layers that contain multiple memory units. We again apply
an iterative, layer-by-layer approach.  The main difficulty is
in inferring invariants for a layer that has multiple memory units, as
in Fig.~\ref{fig:rnn_2d}:  while each memory
unit belongs to a single neuron, it affects the assignments of all
other neurons in that layer.  We propose to handle this case using
separate linear invariants for upper- and lower-bounding each of the
memory units.  However, while the invariants have the same linear form
as in the single memory unit case, \emph{proving} them requires taking
the other invariants of the same layer into account.  Consider the
example in Fig.~\ref{fig:rnn_2d}, and suppose we have
$\alpha_l^1,\alpha_u^1$ and $\alpha_l^2,\alpha_u^2$ for which we wish
to verify that
\begin{equation}
    \alpha_l^1\cdot (t-1) \leq \tilde{v}_{2,1}^t \leq \alpha_u^1\cdot (t-1) \qquad\qquad
    \alpha_l^2\cdot (t-1) \leq  \tilde{v}_{2,2}^t \leq \alpha_u^2\cdot (t-1)
  \label{eq:multidim_bounds}
\end{equation}
In order to prove these bounds we need to dispatch an FFNN verification query
that assumes Eq.~\ref{eq:multidim_bounds} holds and uses it to
prove the inductive step:
\begin{equation}
    \tilde{v}_{2,1}^{t+1} = v_{2,1}^t = \text{ReLU}\xspace{}{}(- \tilde{v}^t_{1,1} +  \tilde{v}_{2,1}^t + \tilde{v}_{2,2}^t)
    \leq \alpha_u^1 \cdot (t+1-1)
    \label{eq:multidim_step}
\end{equation}
Similar steps must be performed for $\tilde{v}_{2,1}^{t+1}$'s lower bound, and
also for
$\tilde{v}_{2,2}^{t+1}$'s lower and upper bounds. The key point is that because
Eq.~\ref{eq:multidim_step} involves $\tilde{v}_{2,1}^t$ and $\tilde{v}_{2,2}^t$,
multiple $\alpha$ terms from
Eq.~\ref{eq:multidim_bounds} may need to be used in proving it. This
interdependency means that later changes to some $\alpha$ value
might invalidate previously acceptable assignments for other $\alpha$
values. This adds a layer of complexity that did not exist in the
cases that we had considered previously.

For example, consider the network in Figure~\ref{fig:rnn_2d}, with
$P = \bigwedge_{t=1}^3 -3 \leq v_{1,1}^t \leq 3$,
and
$Q = \bigvee^3_{t=1} v_{3,1}^{t} \ge 100$.
Our goal is to find values
for  $\alpha_l^1,\alpha_u^1$ and $\alpha_l^2,\alpha_u^2$ that will
satisfy Eq.~\ref{eq:multidim_bounds}. Let us consider
$\alpha_l^1 =0, \alpha_u^1 = 8, \alpha_l^2 = 0$ and $\alpha_u^2 =
 0$. Using these values, the induction hypothesis
 (Eq.~\ref{eq:multidim_bounds}) and the bounds for $v_{1,1}$,
 we can indeed prove the upper bound for
 $\tilde{v}_{2,1}^{t+1}$:
 \[
     \tilde{v}_{2,1}^{t+1} = v_{2,1}^t = \text{ReLU}\xspace{}{}(- \tilde{v}^t_{1,1} +  \tilde{v}_{2,1}^t + \tilde{v}_{2,2}^t)
   \leq \text{ReLU}\xspace{}{}(3 + 8(t-1) +0) \leq 8t
 \]

 Unfortunately, the bounds $0\leq
 \tilde{v}_{2,2}^t\leq 0$ are inadequate, because $\tilde{v}_{2,2}^t$ can
 take on positive values. We are thus required to adjust the $\alpha$
 values, for example by increasing $\alpha_u^2$ to $2$. However, this
 change invalidates the upper bound for $\tilde{v}_{2,1}^{t+1}$,
 i.e. $\tilde{v}_{2,1}^{t+1}\leq 8t$, as that bound relied on the upper bound for
 $\tilde{v}_{2,2}^t$; Specifically, knowing only that $1\leq t \leq 3$, $-3\leq v_{1,1}^t\leq
 3$, $0\leq \tilde{v}_{2,1}^t\leq 8(t-1)$ and $0\leq \tilde{v}_{2,2}^t\leq 2(t-1)$, it is
 impossible to show that $\tilde{v}_{2,1}^{t+1} = v_{2,1}^t  \leq 8t$.

The example above demonstrates the intricate dependencies between the
$\alpha$ values, and the complexity that these dependencies add to the
search process. Unlike in the single memory unit case, it is not immediately clear
how to find an initial invariant that simultaneously holds for all
memory units, or how to strengthen this invariant (e.g., which
$\alpha$ constant to try and improve).

\mysubsubsection{Finding an Initial Invariant.}
We propose to encode the
problem of finding initial $\alpha$ values as a \emph{mixed integer
  linear program} (MILP). The linear and
piecewise-linear constraints that the
$\alpha$ values must satisfy (e.g., Eq.~\ref{eq:multidim_step})
can be precisely encoded in MILP
using standard big-M encoding~\cite{ReluPlex}.
There are two main advantages
to using MILP here:
\begin{inparaenum}[(i)]
\item an MILP solver
  is guaranteed to return a valid invariant, or soundly report that no such
  invariant exists; and
\item MILP instances include a \emph{cost function} to be
  minimized, which can be used to optimize the invariant. For example,
  by setting the cost function to be $ \sum\alpha_u - \sum\alpha_l, $
  the MILP solver will typically generate tight upper and lower bounds.
\end{inparaenum}

The main disadvantage to using MILP is that, in order to ensure that
the invariants hold for all time steps $1\leq t\leq T_{\max}{}$, we must
encode all of these steps in the MILP query. For example, going back
to Eq.~\ref{eq:multidim_step}, in order to guarantee that
$v_{2,1}^{t+1} = \text{ReLU}\xspace{}{}(- v^t_{1,1} +  v_{2,1}^t + v_{2,2}^t) \leq \alpha_u^1 \cdot t$,
we would need to encode within our MILP instance the fact that
$
  \bigwedge_{t=1}^{T_{\max}}\left( \text{ReLU}\xspace{}{}(- v^t_{1,1} +  v_{2,1}^t + v_{2,2}^t) \leq \alpha_u^1 \cdot t \right)
$.
This might render the MILP instance difficult to solve for large
values of $T_{\max}{}$.
However, we stress that this approach is quite
different from, and significantly easier than, unrolling the RNN. The
main reason is that these MILP instances are each generated for a single
layer (as opposed to the entire network in unrolling), which renders
them much simpler. Indeed, in our experiments
(Sec.~\ref{sec:evaluation}), solving these MILP
instances was never the bottleneck.
Still, should this become a problem, we propose to encode
only a subset of the values of $t\in\{1,\ldots,T_{\max}{}\}$, making the
problem easier to solve; and should the $\alpha$ assignment fail to
produce an invariant (this will be discovered when $\varphi_I$ is
verified), additional constraints could be added to guide the MILP
solver towards a correct solution. We also describe an alternative
approach, which does not require the use of an MILP solver, in
Sec.~\ref{sec:invariantsNoMilp} of the appendix

\mysubsubsection{Strengthening the Invariant.}
If we are unable to prove that $\hat{\varphi}$ is
\texttt{UNSAT}{} for a given $I$, then the invariant needs to be strengthened. We propose to achieve this by
invoking the MILP solver again, this time adding new linear
constraints for each $\alpha$, that will force the selection of tighter bounds. For example,
if the current invariant is $\alpha_l=3, \alpha_u=7$, we
add constraints specifying that $\alpha_l\geq 3+\epsilon$ and
$\alpha_u\leq 7-\epsilon$ for some small positive $\epsilon$ ---
leading to stronger invariants.

\section{Evaluation}
\label{sec:evaluation}

Our  proof-of-concept implementation of the approach,
called \emph{RnnVerify}, reads an RNN in TensorFlow format. The input
and output properties, $P$ and $Q$, and also $T_{\max}{}$, are supplied in a simple
proprietary format, and the tool then automatically:
\begin{inparaenum}[(i)]
  \item creates the FFNN snapshot network;
  \item infers a candidate invariant using the MILP heuristics from Sec.~\ref{sec:invariant_generation};
  \item formally verifies that $I$ is an invariant; and
  \item uses $I$ to show that $\hat{\varphi}$, and hence $\varphi$,
    are \texttt{UNSAT}{}.
  \end{inparaenum}
If $\hat{\varphi}$ is \texttt{SAT}{}, our module refines $I$ and repeats the
process for a predefined number of steps.

For our evaluation, we focused on neural networks for \emph{speaker
recognition} --- a task for which RNNs are commonly used, because
audio signals tend to have temporal properties and varying lengths. We
applied our verification technique to prove \emph{adversarial
  robustness} properties of these networks, as we describe next.

\mysubsubsection{Adversarial Robustness.}
\label{sec:adversarial_robustness}
It has been shown that alarmingly many neural networks are susceptible to
\emph{adversarial inputs}~\cite{SzZaSuBrErGoFe13}. These inputs are generated by slightly
perturbing correctly-classified inputs, in a way that causes the
misclassification of the perturbed inputs.
Formally, given a network $N$ that classifies inputs into labels $l_1,\ldots,l_k$, an input $x_0$, and a
target label $l \neq N(x_0)$, an adversarial input is an input
$x$ such that $N(x) = l$ and
$\lVert x-x_0 \rVert\leq\delta$; i.e., input $x$ is very
close to $x_0$, but is misclassified as label $l$.

\emph{Adversarial robustness} is a measure of how difficult it is to
find an adversarial example --- and specifically, what is the smallest
$\delta$ for which such an example
exists. Verification can be used to find adversarial inputs or rule
out their existence for a given $\delta$, and consequently can find
the smallest $\delta$ for which an adversarial input
exists~\cite{CaKaBaDi17}.

\mysubsubsection{Speaker Recognition.} A speaker recognition system
receives a voice sample and needs to identify the speaker from a set
of candidates. RNNs are often applied in implementing such
systems~\cite{WaWaPaLo18}, rendering them vulnerable to adversarial
inputs~\cite{KrAdCiKe18}. Because such vulnerabilities in these
systems pose a security concern, it is important to
verify that their underlying RNNs afford high adversarial robustness.

\mysubsubsection{Benchmarks.}
\sloppy
We trained $6$ speaker recognition RNNs, based
on the VCTK dataset~\cite{vctk}. Our networks are of modest, varying
sizes of approximately 220 neurons: they
each contain an input layer of dimension $40$, one or two hidden layers with
$d\in\left\{2,4,8\right\}$ memory units, followed by $5$ fully connected,
memoryless layers with $32$ nodes each, and an output
layer with $20$ nodes. The output nodes represent
the possible speakers between which the RNNs were trained to
distinguish. In addition, in order to enable a comparison to the state
of the art~\cite{AkKeLoPi19}, we trained another, smaller network, which
consists of a single hidden layer. This was
required to accommodate technical constraints in the implementation
of~\cite{AkKeLoPi19}. All networks use ReLUs as their activation functions.

Next, we selected $25$ random, fixed input points
$X = \{x_1,\ldots,x_{25}\}$, that do not change over time; i.e. $x_i\in
\mathbb{R}^{40}$ and $x_i^1=x_i^2=\ldots$ for each $x_i\in X$. Then,
for each RNN $N$ and input $x_i\in X$, and for each value $2
\leq T_{\max} \leq 20$, we computed the ground-truth
label $l = N(x_i)$, which is the label that received the highest score
at time step $T_{\max}{}$. We also computed the label that received the
second-highest score, $l_{sh}$, at time step $T_{\max}{}$.
Then, for every combination of $N$,
$x_i\in X$, and value of $T_{\max}{}$, we created the query
$
  \langle
  \bigwedge_{t=1}^{T_{\max}} (\lVert x'^t - x_i^t \rVert_{L_\infty} \leq 0.01),
  N,
  l_{sh}\geq l
  \rangle
$.
The allowed perturbation, at most $0.01$ in $L_\infty$ norm, was
selected arbitrarily. The query is only \texttt{SAT}{} if there exists an input $x'$ that is at distance at most
$0.01$ from $x$, but for which label $l_{sh}$ is assigned a higher score
than $l$ at time step $T_{\max}{}$. This formulation resulted in a
total of $2850$ benchmark queries over our 6 networks.

\begin{wrapfigure}[13]{r}{4.9cm}
   \vspace{-1.2cm}
    \begin{center}
            \scalebox{.30}{
                \includegraphics[width=1.3\textwidth]{figures/rns_ours_rnn2_fc0_avg.pdf}
            }
    \end{center}
    \caption{ Average running time (in seconds) of RnnVerify and
        RNSVerify, as a function of $T_{\max}{}$. }
  \label{fig:prev_work_comperssion}
\end{wrapfigure}

\mysubsubsection{Results.}
We began by comparing our technique to the state-of-the-art,
unrolling-based RNSVerify tool~\cite{AkKeLoPi19}, using the small
network we had trained.  Each dot in
Fig.~\ref{fig:prev_work_comperssion} represents a tool's average run
time on the 25 input points, for a specific $T_{\max}{}$.  Both methods
returned \texttt{UNSAT}{} on all queries; however, the runtimes clearly
demonstrate that our approach is far less sensitive to large $T_{\max}{}$
values.  In a separate experiment, our tool was able to solve a
verification query on the same network with $T_{\max}{}= 180$ in 2.5
seconds, whereas RNSVerify timed out after 24 hours.

Next, we used RnnVerify on all $2850$ benchmark queries on the 6
larger networks. The results appear in
Sec.~\ref{sec:resultTable} of the appendix
and are summarized as follows:
\begin{inparaenum}[(i)]
\item RnnVerify terminated on all benchmarks, with a median runtime
  of 5.39 seconds and an average runtime
  of $48.67$ seconds. The maximal solving time
  was 5701 seconds;
    \item $85\%$ of RnnVerify's runtime was spent within the
      underlying FFNN verification engine, solving $\varphi_I$
      queries. This indicates that as the underlying FFNN verification
      technology improves, our approach will become significantly more scalable;
    \item for $1919$ ($67\%$) of the
        benchmarks, RnnVerify proved that the RNN was robust around the tested point. For
        the remaining $931$ benchmarks, the results are inconclusive: we do not
        know whether the network is vulnerable, or whether more
        sophisticated invariants are needed to prove
        robustness. This demonstrates that for a majority of tested benchmarks, the linear
        template proved useful; and
    \item RnnVerify could generally prove fewer instances with larger values of
      $T_{\max}$. This is because the linear bounds afforded by our
      invariants become more
      loose as $t$ increases, whereas the neuron's values typically do
      not increase significantly over time. This highlights the need
      for more expressive invariants.
\end{inparaenum}

\section{Related Work}
\label{sec:relatedWork}

Due to the discovery of undesirable behaviors in many DNNs, multiple
approaches have been proposed for verifying them. These include the
use of SMT solving~\cite{HuKwWaWu17,ReluPlex,Marabou,KuKaGoJuBaKo18},
LP and MILP solving~\cite{Eh17,TjXiTe19}, symbolic interval
propagation~\cite{WaPeWhYaJa18}, abstract
interpretation~\cite{ElGoKa20,GeMiDrTsChVe18}, and many others
(e.g.,~\cite{BuTuToKoMu18,GoFeMaBaKa20,GoKaPaBa18,KaBaKaSc19,LoMa17,NaKaRySaWa17}).
Our technique focuses on RNN verification, but uses an FFNN
verification engine as a back-end. Consequently, it could be
integrated with many of the aforementioned tools, and will benefit
from any improvement in scalability of FFNN verification technology.

Whereas FFNN verification has received a great deal of attention, only
little research has been carried out on RNN verification. Akintunde et
al.~\cite{AkKeLoPi19} were the first to propose such a technique,
based on the notion of unrolling the network into an equivalent FFNN.
Ko et al.~\cite{KoLuWeDaWoLi19} take a different approach, which aims
at quantifying the robustness of an RNN to adversarial inputs ---
which can be regarded as an RNN verification technique tailored for a
particular kind of properties.  The scalability of both approaches is
highly sensitive to the number of time steps, $T_{\max}{}$, specified by
the property at hand.  In this regard, the main advantage of our
approach is that it is far less sensitive to the number of time steps
being considered.  This affords great
potential for scalability, especially for long sequences of inputs. A
drawback of our approach is that it requires invariant inference,
which is known to be challenging.

In a very recent paper, Zhang et al.~\cite{ZhShGuGuLeNa20} propose a
verification scheme aimed at RNNs that perform cognitive tasks. This
scheme includes computing polytope invariants for the neuron layers of
an RNN, using abstract interpretation and fixed-point analysis. We
consider this as additional evidence of the usefulness of invariant
generation in the context of RNN verification.

Automated invariant inference is a key problem in program
analysis. A few
notable methods for doing so include abstract-interpretation
 (e.g.,~\cite{ShDiDiAi11}); counterexample-guided
approaches (e.g.,~\cite{NgAnRuHi17}); and learning-based approaches
(e.g.,~\cite{SiDaRaNaSo18}).  It will be interesting to apply these
techniques within the context of our framework, in order to more
quickly and effectively discover useful invariants.

\section{Conclusion}
\label{sec:conclusion}
Neural network verification is
becoming increasingly important to industry, regulators, and society as
a whole. Research to date has focused primarily on
FFNNs. We propose a novel approach for
the verification of recurrent neural networks --- a kind of
neural networks that is particularly useful for context-dependent
tasks, such as NLP. The cornerstone of our approach is the reduction of
RNN verification to FFNN verification through the use of inductive
invariants. Using a proof-of-concept implementation, we demonstrated
that our approach can tackle many benchmarks orders-of-magnitude
more efficiently than the state of the art. These experiments indicate
the great potential that our approach holds.
In the future, we plan to experiment with more expressive invariants,
and also to apply
\emph{compositional verification} techniques in order to break the RNN into
multiple, smaller networks, for which invariants can more easily be inferred.

\mysubsubsection{Acknowledgements.}
This work was partially supported by the Semiconductor
Research Corporation, the Binational Science Foundation (2017662), the
Israel Science Foundation (683/18), and the National Science
Foundation (1814369).

\bibliographystyle{abbrv}


\section{Introduction}

	Quantum optics and the related fields of quantum computation are at their heart concerned with the interactions between atoms and light -
	light as in coherent modes of electromagnetic radiation and atoms as in well controlled, engineered quantum few-level systems~\cite{QuantumOpticsBook}.
	Typically this interaction is described in the so-called Jaynes-Cummings model~\cite{JaynesCummings, Blais:PRA:2004},
	which is based on an approximation of the more fundamental Rabi model~\cite{RabiModel},
	describing the interaction between the light and dipole allowed transitions in the atom.
	The differences between Rabi and Jaynes-Cummings model are thought to be small in the usual experimental situations,
	and to see noticeable effects one usually needs to consider the ultra-strong coupling regime~\cite{FornDiaz:NP:2016, Kockum:NR:2019},
	where the coupling strength between atoms and light becomes comparable to their characteristic energy scales.
	In this paper we show that already for much smaller coupling strength, qualitative and quantitative differences between the two models can be observed.

	On the way towards further improving the degree of control over quantum hardware, we continuously need to improve our understanding of the quantum systems and their coupled dynamics.
	Of special importance for quantum computation is the so-called dispersive regime of the atom-light interaction~\cite{Blais:PRA:2004},
	where the atomic transitions are detuned from the mode energies of the light field by more than the strength of their coupling.
	It is in this regime that the successful early quantum computing prototypes based on
	superconducting artificial atoms and microwave resonators are operated~\cite{Chow:NC:2014, Barends:N:2016, Roushan:S:2017, Kandala:N:2019}.
	It allows the resonator mode on one hand to isolate the sensitive qubits from most of the electromagnetic environment
	while at the same time acting as an access port for qubit manipulation and state readout~\cite{QuantumEngineer}.
	Similar advantages are also envisioned for coupling quantum dot spin qubits to microwave resonators~\cite{Petersson:N:2012, vanWoerkom:PRX:2018, Landig:NC:2019}.
	When modelling the system dynamics in the dispersive regime, one typically employs analytic approximations for the coupling-induced changes to Hamiltonian parameters
	as well as for dissipative processes arising due to the atom-light hybridisation~\cite{Blais:PRA:2004, Boissonneault:PRA:2008, Boissonneault:PRA:2009}.
	These, however, are usually based on the approximate Jaynes-Cummings interaction instead of the more fundamental Rabi model.

	Here, we show analytic expressions for Hamiltonian corrections and dominant dissipative dynamical contributions arising in the dispersive regime of the Rabi model directly,
	without making the rotating wave-approximation underlying the Jaynes-Cummings interaction.
	Our treatment is based on a Keldysh diagrammatic perturbation approach~\cite{Mueller:PRA:2016},
	and delivers well-behaved and simple analytic expressions for all relevant parameters without requiring additional approximation.
	These results are relevant for more accurate analytical modelling of any quantum hardware in the dispersive regime, like superconducting and spin qubits.
	The dissipative corrections to the dynamics we derive here are additionally important for a better understanding of qubit readout, when the resonators may be strongly driven.
	In this case, they lead to photon number dependent dissipative corrections to the qubit dynamics.

\section{Multi-level dissipative Rabi model \label{sec:Model}}

	We focus our treatment on a system of a multi-level atom coupled to a single, quantized resonator mode.
	This model accurately describes the typical situation for superconducting transmon qubits coupled to resonators in the circuit QED architecture.
	Results for the special case of a two-level atom, more relevant to e.g. quantum-dot spin or charge qubits are detailed in Appendix~\ref{app:TwoLevel}.

	We write the total system Hamiltonian as $\H = \H_{0} + \H_{\text{int}} + \H_{\text{env}}$, with the unperturbed Hamiltonian
	\begin{align}
		\H_{0} = \omega_{r} a\hc a + \sum_{k=0}^{N-1} \omega_{k} \sigma_{k,k} \,.
		\label{eq:H0}
	\end{align}
	Here, we use the notation $\sigma_{k,l} = \ket k \bra l$ with $\ket k$ an eigenstate of the $N$-level system with eigenenergy $\omega_{k}$.
	$a$ is the bosonic annihilation operator of the resonator mode at frequency $\omega_{r}$.
	The interaction between multi-level qubit and resonator is written in the Rabi model as
	\begin{align}
		\H_{\text{int, Rabi}} = \sum_{k} g_{k} \l( \sigma_{k,k+1} + \sigma_{k+1,k} \r) \l( a\hc + a \r) \,,
	\end{align}
	assuming purely transversal coupling between the qubit and resonator, as is natural for transmon qubits.
	Alternatively we could make a rotating wave approximation in the coupling, leading to the Jaynes-Cummings model interaction
	\begin{align}
		\H_{\text{int, JC}} = \sum_{k} g_{k} \l( \sigma_{k,k+1} a\hc + \sigma_{k+1,k} a \r) \,,
	\end{align}
	which discards fast rotating terms.

	The system is additionally coupled to three independent baths via $H_{\text{env}} = H_{\text{sys-env}} + H_{\text{env}, 0}$.
	The system-bath interactions are described by
	\begin{align}
		\H_{\text{sys-env}} =& \sum_{k} \beta_{k} \l( \sigma_{k,k+1} + \sigma_{k+1,k} \r)  \op X + \sum_{k} \delta\omega_{k} \sigma_{k,k} \op Z \nn\\
			&+ \l( a\hc + a \r) \op R \,.
	\end{align}
	Here the first term induces transitions in the multi-level system, at lowest order leading to energy dissipation and excitation.
	For weakly anharmonic qubits like the transmon, one usually finds the coupling strengths $\beta_{k} \sim \sqrt{k+1}$, but we do not restrict our analysis to this special case.
	The second term describes fluctuations of the qubits energy levels, leading primarily to qubit dephasing.
	The $\delta\omega_{k}$ characterise the sensitivity of the qubit level energy $\omega_{k}$ to small fluctuations in the external parameter $\op Z$.
	The final term then is to lowest order responsible for decay and excitation of resonator photons.

	We are assuming the bath operators $\op X, \op Z$, and $\op R$ to be hermitian operators of bosonic environments which are in thermal equilibrium at temperature $T$.
	The Hamiltonian $H_{\text{env},0}$ describes the internal dynamics of the baths, which we do not state here explicitly.
	More details on how we treat the bath operators can be found in Appendix~\ref{app:Bath}.

	{At this point it is instructive to emphasize the differences between the present model and our earlier work, Ref.~\cite{Mueller:PRA:2016}, which focused on a two-level double-quantum dot coupled to a microwave resonator and a phononic environment.
	In this work, the focus is instead on the multi-level nature of the qubit and the presence of multiple independent environments coupled to both the qubit and the resonator, leading to correlated dissipative processes like Purcell decay.}

\section{Perturbative treatment in the dispersive limit \label{sec:Results}}

	We use the technique developed in Ref.~\onlinecite{Mueller:PRA:2016} to derive effective dissipative rates and coherent Hamiltonian corrections
	in the dispersive limit where $g\ll \abs{\Delta_{0}} = \abs{\omega_{1,0} - \omega_{r}}$.
	This technique is based on a perturbative expansion of the density matrix time-evolution on the Keldysh contour.
	The individual terms in this expansion can then be expressed as Keldysh diagrams, in the same spirit as Feynman diagrams for quantum state evolution,
	and the resulting master equation can be written in Lindblad form.
	Here we do a simultaneous perturbation theory in both the system interaction $H_{\text{int}}$ as well as the bath interaction $H_{\text{sys-env}}$,
	assuming both interactions to be weak compared to the internal system dynamics.
	The Keldysh expansion is well behaved also when considering the full Rabi interaction, and does not rely on the rotating wave approximation of the Jaynes-Cummings model.
	Then, at second order in the perturbation theory, we obtain the usual incoherent contributions to the dynamics, i.e. qubit dissipation and dephasing as well as resonator dissipation,
	due to their coupling to their individual environments.
	Additionally, from the perturbative expansion including the atom-resonator interaction term $\H_{\text{int}}$,
	we find corrections to the unperturbed Hamiltonian $H_{0}$ at second order, which we identify with the dispersive shifts~\cite{Blais:PRA:2004, Stace:PRL:2013}.
	One of the major advantages of the Keldysh approach is that it provides a clear recipe for going to higher orders in perturbation theory.
	At fourth order this theory predicts, amongst others,
	correlated dissipative processes that arise due to the hybridisation of the qubit and resonator states and their individual coupling to environments, which are at the focus of this paper.
	Details on the technique and derivation of the master equation can be found in our earlier work~\cite{Mueller:PRA:2016}.

	We write the master equation resulting from the Keldysh diagrammatic expansion up to fourth order as
	\begin{align}
		\dot \rho = -\ii \comm{\H_{0} + H_{2}}{\rho(t)} + \mathcal L_{2} \rho(t) + \mathcal L_{4} \rho(t) \,.
		\label{eq:ME}
	\end{align}
	Here, $\H_{2}$ is a dispersive Hamiltonian correction
	and $\L_{2}\rho$ summarises the incoherent dynamics at the same order.
	Finally $\L_{4}\rho$ contains all incoherent contributions at fourth order perturbation theory, which are the main focus of this work.
	In the following we will provide the analytic expressions for all terms in Eq.~\eqref{eq:ME} and will
	contrast the results when performing the perturbation theory either with the full Rabi model or the approximate Jaynes-Cummings interaction.

	\subsection{Second order dissipative terms}

	The Keldysh expansion at second order in the system-bath interaction $\H_{\text{sys-env}}$ reproduces the well-known incoherent terms in the master equation, which we reproduce here for clarity.
	For a multi-level qubit and resonator, these are
	\begin{align}
		\L_{2} \rho(t) = \sum_{k}& \gamma_{\downarrow_{k}} \diss{\sigma_{k,k+1}}\rho(t) + \gamma_{\uparrow_{k}} \diss{\sigma_{k+1,k}}\rho(t) \nn\\
			&+ \gamma_{\varphi_{k}}\diss{\sigma_{k,k}}\rho(t) \nn\\
			&+ \kappa_{-}\diss{a}\rho(t) + \kappa_{+}\diss{a\hc}\rho(t) \label{eq:Diss2}
	\end{align}
	with the rates
	\begin{align}
		\gamma_{\downarrow_{k}} &= \beta_{k}^{2} C_{\op X}(\omega_{k+1,k})  \quad\,,\quad \gamma_{\uparrow_{k}} = \beta_{k}^{2} C_{\op X}(-\omega_{k+1,k}) \,,\nn\\
		\gamma_{\varphi_{k}} &= \delta\omega_{k}^{2}  C_{\op Z}(0) \,,\nn\\
		\kappa_{-} &= C_{\op R}(\omega_{r}) \quad\,,\quad \kappa_{+} = C_{\op R}(-\omega_{r}) \,.
	\end{align}
	Here the first line in Eq.~\eqref{eq:Diss2} describes qubit decay and excitation, the second line its pure dephasing of the qubit
	and the final two terms incoherent photon loss and excitation from the resonator.
	We used the usual dissipator notation, $\diss{\op o}\rho = \op o \rho \op o\hc -\frac12\l( \op o\hc \op o \rho + \rho \op o \hc \op o \r)$.
	The spectral functions of the environmental operators we defined through $C_{\op o} (\omega) = \frac12 \int dt\: \ee^{\ii \omega (t-t')} \mean{\op o(t) \op o(t')}$.
	They describe the ability of the environment to exchange photons at energy $\omega$ with the system. More details in Appendix~\ref{app:Bath}.

	\subsection{Second order Hamiltonian corrections - dispersive shifts}

	\begin{figure}[htbp]
		\begin{center}
			\includegraphics[width=.95\columnwidth]{DispersiveShift}
			\includegraphics[width=.95\columnwidth]{DispersiveShiftError}
			\caption{\textbf{(a)} Dispersive Hamiltonian corrections to the one resonator photon energy, $-\tilde\chi_{0}$ for the Rabi model (solid blue)
				and $-\chi_{0}$ in the Jaynes-Cummings approximation (dashed orange), as function of detuning between resonator and lowest qubit transition,
				$\Delta_{0} = \omega_{1,0} - \omega_{r}$.
				Red circles are results from numerical exact diagonalisation of the Hamiltonian.
				\textbf{(b)} Error of the dispersive shift as a fraction of the exact diagonalisation result.
				Parameters in this and all following plots: $\omega_{r}/2\pi = 5$~GHz, $g_{0}/2\pi = 100$~MHz.

				}
			\label{fig:DispersiveShift}
		\end{center}
	\end{figure}
	Additionally, our technique produces corrections to the Hamiltonian, due to the perturbative expansion in the system coupling operator $\H_{\text{int}}$.
	When taking the Rabi-type coupling $\H_{\text{int,Rabi}}$ as the perturbative interaction, we find these Hamiltonian correction at second order as
	\begin{align}
		\H_{2, \text{Rabi}}
			=& \sum_{k} \l( \tilde\chi_{k-1} - \tilde\chi_{k} \r) a\hc a \sigma_{k,k} + \l( \chi_{k-1}  - \xi_{k} \r) \sigma_{k,k}\,,
	\end{align}
	with the generalized dispersive shift
	\begin{align}
		\tilde\chi_{k} = \frac{2 g_{k}^{2}\:\omega_{k+1,k}}{(\omega_{k+1,k}^{2}-\omega_{r}^{2})}
		\label{eq:Rabi}
	\end{align}
	and where we defined the qubit level splittings $\omega_{k+1, k} = \omega_{k+1} - \omega_{k}$, and $g_{k}=0\,, \forall k<0$.
	Here we also introduced the usual multi-level Jaynes-Cummings dispersive shifts $\chi_{k}$~\cite{Blais:PRA:2004} as well as the Bloch-Siegert shifts $\xi_{k}$~\cite{FornDiaz:PRL:2010} as
	\begin{align}
		\chi_{k} &= \frac{g_{k}^{2}}{(\omega_{k+1,k} - \omega_{r})} \,, \nn\\
		\xi_{k} &= \frac{g_{k}^{2}}{(\omega_{k+1,k} + \omega_{r})}\,.
	\end{align}
	Note that $\tilde\chi_{k} = \chi_{k} + \xi_{k}$.
	For the special case of a two-level atom, this result has previously been derived using different theoretical techniques~\cite{Zueco:PRA:2009, Zhu:NJP:2013}, see also Appendix~\ref{app:TwoLevel}.
	If we perform the perturbation expansion with the qubit-resonator interaction term in the Jaynes-Cummings approximation, $\H_{\text{int,JC}}$, we instead find
	\begin{align}
		\H_{2,JC} = \sum_{k} \l( \chi_{k-1} - \chi_{k} \r) a\hc a \sigma_{k,k} + \chi_{k-1} \sigma_{k,k} \,,
	\end{align}
	as is known in the literature~\cite{Boissonneault:PRA:2008, Slichter:PRL:2012}.
	Fig.~\ref{fig:DispersiveShift} shows a comparison of the Rabi and Jaynes-Cummings dispersive corrections to the one photon energy{, i.e. the energy required to add one photon to the resonator while the qubit rests in its groundstate.
	These are given for the Rabi and Jaynes-Cummings model by $\tilde\chi_{0}$ and $\chi_{0}$, respectively.
	We show them }together with results from exact numerical diagonalisation of the Hamiltonian{ for the same parameters}, truncated to {include the ten lowest states for both multi-level qubit and resonator, for details see Appendix~\ref{app:MoreResults}}.
	The major qualitative difference is the asymmetry in the magnitude of the shift for positive and negative detuning in the result for the Rabi interaction~\cite{Zueco:PRA:2009, Zhu:NJP:2013},
	compared to the symmetric response of the Jaynes-Cummings result.
	As a result, apart from a small region around small positive detuning, the error in the Rabi dispersive corrections is significantly smaller than for the Jaynes-Cummings result,
	and Eq.~\eqref{eq:Rabi} converges to the exact results for large detuning.
	For further comparison, including studying the behavior when fitting to experimental data and the implications for predictions of system dynamics,
	see Appendix~\ref{app:MoreResults}.

	\subsection{Fourth order dissipative terms}

	At fourth order, a large number of dissipators contribute to the master equation.
	Here we focus only on a subset of all incoherent contributions, and write the fourth-order dissipative contributions to the master equation as
	\begin{align}
		\mathcal L_{4}\rho = \mathcal L_\text{Purcell} \rho + \mathcal L_{\updownarrow,\pm} \rho + \mathcal L_{\varphi,\pm} \rho \,.
	\end{align}
	These three terms correspond to previously known corrections to the dissipative dynamics of a qubit and resonator in the dispersive regime~\cite{Mueller:PRA:2016, Blais:PRA:2004, Boissonneault:PRA:2008}.
	They arise from hybridisation of qubit and resonator states and the coupling of the resulting hybrid states to the qubit and resonator environments.
	In the Keldysh perturbation theory they appear at fourth order, where two interaction vertices originate from the qubit-resonator interaction $\H_{\text{int}}$
	and the other two from the interactions with the baths $\H_{\text{sys-env}}$.
	In a previous work~\cite{Mueller:PRA:2016}, this subset of incoherent contributions has been shown to be dominating the steady-state properties in the dispersive parameter regime.

	\subsubsection{Purcell process}

	The Purcell process describes decay and excitation of the qubit due to its effective coupling to the resonator environment.
	We find its contribution to the master equation as
	\begin{align}
		\mathcal L_\text{Purcell} \rho
			= \sum_k \gamma_{\text P,\downarrow}^{(k)} \mathcal D\left[ \sigma_{k,k+1} \right] \rho + \gamma_{\text P,\uparrow}^{(k)} \mathcal D\left[ \sigma_{k+1,k} \right] \rho \,,
	\end{align}
	with the Purcell decay and excitation rates
	\begin{align}
		\gamma_{\text P,\downarrow}^{(k)} &= p_{k} \: C_{\op R} \left(\omega_{k+1,k}\right) \,, \quad
		\gamma_{\text P,\uparrow}^{(k)} = p_{k} \: C_{\op R} \left(- \omega_{k+1,k}\right) \,,
	\end{align}
	where we defined dimensionless prefactors $p_{k}$. For the Rabi model, these are
	\begin{align}
		p_{k,\text{Rabi}} = \frac{8 g_{k}^2 \:\omega_r^2}{(\omega_r^2 - \omega_{k+1,k}^2)^2} \,,
		\label{eq:PurcellPreRabi}
	\end{align}
	while for the Jaynes-Cummings interaction we find the canonical result
	\begin{align}
		p_{k,\text{JC}} = \frac{2g_{k}^2 }{(\omega_r - \omega_{k+1,k})^2} \,.
		\label{eq:PurcellPreJC}
	\end{align}
	Fig.~\ref{fig:Purcell} shows a comparison of the prefactors for the Rabi and Jaynes-Cummings model.
	Similar to the dispersive shift, the inclusion of the fast rotating terms in the Rabi interaction leads to a notable asymmetry in the rates with respect to zero detuning.
	For large negative detuning, $\omega_{1,0} < \omega_{r}$, Purcell is suppressed strongly compared to the Jaynes-Cummings result
	while for large positive detuning, $\omega_{1,0} > \omega_{r}$ it is similarly enhanced.
	Note that the Purcell rates are proportional to the resonator environmental correlation function, $C_{{\op R}}(\omega)$, probed at the qubit transition frequencies.
	\begin{figure}[htbp]
		\begin{center}
			\includegraphics[width=.95\columnwidth]{Purcell}
			\caption{Comparison of the Purcell rate prefactor $p_{0}$, Eqs.~\eqref{eq:PurcellPreRabi},~\eqref{eq:PurcellPreJC},
				as function of detuning $\Delta_{0}$,
				when taking the Rabi (solid blue) or Jaynes-Cummings interaction (dashed orange).
				Note the asymmetry with respect to zero detuning for the Rabi result.

				}
			\label{fig:Purcell}
		\end{center}
	\end{figure}

	\subsubsection{Dressed dephasing}

	The so-called dressed dephasing dissipative corrections have previously been derived
	in the context of the usual dispersive transformation of the Jaynes-Cummings model~\cite{Boissonneault:PRA:2008, Slichter:PRL:2012}.
	They describe correlated decay and excitation of qubit and resonator due to coupling to the longitudinal bath of the qubit.
	In the usual second order perturbation theory this bath only leads to qubit dephasing proportional to its low frequency response.
	Here, due to the resonator-qubit hybridisation, its high frequency components contribute additionally to incoherent conversion of qubit and resonator photons.
	Using the Keldysh diagrammatic perturbation technique, we reproduce the previously known results, and find additional contributions that are unique to the Rabi model.
	The total dressed dephasing contribution to the master equation is written as
	\begin{align}
		\mathcal L_{\updownarrow,\pm} \rho
			= \sum_k& \gamma_{\downarrow,+}^{(k)} \mathcal D \left[ \sigma_{k,k+1} a^\dagger \right] \rho + \gamma_{\uparrow,-}^{(k)} \mathcal D \left[ \sigma_{k+1,k} a \right] \rho \nn \\
			+& \gamma_{\downarrow,-}^{(k)} \mathcal D \left[ \sigma_{k,k+1} a \right] \rho + \gamma_{\uparrow,+}^{(k)} \mathcal D \left[ \sigma_{k+1,k} a^\dagger \right] \rho \label{eq:DD}\,,
	\end{align}
	with the expressions for the rates
	\begin{align}
		\gamma_{\downarrow,+}^{(k)} &= d_{k} C_{\op Z} \left( \omega_{k+1,k} - \omega_r \right) \,, \quad
		\gamma_{\uparrow,-}^{(k)} = d_{k} C_{\op Z} \left( \omega_r - \omega_{k+1,k} \right) \,,\nn\\
		\gamma_{\downarrow,-}^{(k)} &= c_{k}  C_{\op Z} \left( \omega_r + \omega_{k+1,k} \right) \,, \quad
		\gamma_{\uparrow,+}^{(k)} = c_{k} C_{\op Z} \left( - \omega_{k+1,k} -\omega_r \right) \,,
	\end{align}
	and the dimensionless prefactors for the Rabi model
	\begin{align}
		d_{k,\text{Rabi}} &= \frac{2 g_{k}^2 \:(\delta\omega_{k} - \delta\omega_{k+1})^2}{(\omega_r - \omega_{k+1,k})^2} \,,\nn\\
		c_{k,\text{Rabi}} &= \frac{2 g_{k}^2 \: (\delta\omega_{k} - \delta\omega_{k+1})^2}{(\omega_r + \omega_{k+1,k})^2}\,,\label{eq:DressedPreRabi}
	\end{align}
	and for the Jaynes-Cummings approximation
	\begin{align}
		d_{k,\text{JC}} = d_{k, \text{Rabi}} \,, \quad c_{k,\text{JC}} = 0 \,.\label{eq:DressedPreJC}
	\end{align}
	The first two processes in Eq.~\eqref{eq:DD} correspond to environmentally assisted conversion of photons between the qubit and the resonator,
	and are equal for both the Rabi and the Jaynes-Cummings model.
	Exclusive to the Rabi model is the second line in Eq.~\eqref{eq:DD}, corresponding to simultaneous creation or annihilation of a qubit and resonator photon.
	Fig.~\ref{fig:DressedDephasing} shows a comparison of the relative strength of these processes.
	Note that the rates are proportional to the spectral function of the qubit's longitudinal bath, $C_{{\op Z}}(\omega)$, probed at the sum or difference of qubit and resonator frequencies,
	$\omega_{k+1,k}\pm\omega_{r}$.
	\begin{figure}[htbp]
		\begin{center}
			\includegraphics[width=.95\columnwidth]{DressedDephasing}
			\caption{Comparison of the dressed dephasing rate prefactors $d_{0}$ and $c_{0}$, Eqs.~\eqref{eq:DressedPreRabi}, ~\eqref{eq:DressedPreJC}
				when taking the Rabi (solid blue) or Jaynes-Cummings interaction (dashed orange).
				The upper curves show $d_{0}$, which is the same for Rabi and Jaynes-Cummings model,
				while the lower curve shows $c_{0}$, which is exclusive to the Rabi interaction case.
				}
			\label{fig:DressedDephasing}
		\end{center}
	\end{figure}

	\subsubsection{Photon assisted dephasing}

	The final class of process we include at fourth order is typically not considered in the literature, although its contribution to qubit linewidth is likely comparable to Purcell decay.
	It corresponds to creation or annihilation of a resonator photon together with a simultaneous dephasing process acting on the qubit.
	This has previously been discussed in the context of lasing in double quantum dots~\cite{Mueller:PRA:2016}, where the description of resonator gain and loss was the focus of investigation.
	We write its master equation contribution as
	\begin{align}
		\mathcal L_{\varphi,\pm}\rho
			= \sum_k \gamma_{\varphi,-}^{(k)} \mathcal D\left[ \sigma_{k,k} a \right] \rho + \gamma_{\varphi,+}^{(k)} \mathcal D\left[ \sigma_{k,k} a^\dagger \right] \rho \,,
		\label{eq:DA}
	\end{align}
	with the rates
	\begin{align}
		\gamma_{\varphi,-}^{(k)} &= a_{k} C_{\op X} \left( \omega_r \right) \,,\quad
		\gamma_{\varphi,+}^{(k)} = a_{k} C_{\op X} \left( -\omega_r \right)
	\end{align}
	and the dimensionless prefactor for the Rabi and Jaynes-Cummings model

	\begin{align}
		a_{k,\text{Rabi}} =& \frac{8g_k^{2} \beta_k^{2} \omega_{k+1,k}^{2}}{(\omega_r^{2} - \omega_{k+1,k}^{2})^2}
			+ \frac{8g_{k-1}^{2} \beta_{k-1}^{2} \omega_{k,k-1}^{2}}{(\omega_r^{2} - \omega_{k,k-1}^{2})^2} \nn\\
			&-\frac{16 g_{k} g_{k-1} \beta_{k} \beta_{k-1} \omega_{k+1,k}\omega_{k,k-1}}{(\omega_r^{2} - \omega_{k,k-1}^{2})  (\omega_r^{2} - \omega_{k+1,k}^{2})}
				\label{eq:DephasingAssistedPreRabi} \,,\\

		a_{k,\text{JC}} =& \frac{2 g_k^{2} \beta_k^{2}}{(\omega_r - \omega_{k+1,k})^2} + \frac{2 g_{k-1}^{2} \beta_{k-1}^{2}}{(\omega_r - \omega_{k,k-1})^2} \nn\\
			&- \frac{4 g_{k} g_{k-1} \beta_{k} \beta_{k-1}}{(\omega_r - \omega_{k,k-1}) (\omega_r - \omega_{k+1,k})}
				\label{eq:DephasingAssistedPreJC} \,.

	\end{align}

	Fig.~\ref{fig:DephasingAssisted} shows a comparison of the rate prefactors for the Rabi and Jaynes-Cummings interaction.
	As previously, the inclusion of the Rabi interaction terms leads to a pronounced asymmetry in the rates with respect to zero detuning between qubit and resonator,
	not seen in the Jaynes-Cummings model.
	This dissipative process is proportional to the qubit's transversal bath spectral function, $C_{{\op X}}(\omega)$, probed at the resonator frequency $\omega_{r}$.
	\begin{figure}[htbp]
		\begin{center}
			\includegraphics[width=.95\columnwidth]{DephasingAssisted}
			\caption{Comparison of the photon assisted dephasing rate prefactors $a_{0}$, Eqs.~\eqref{eq:DephasingAssistedPreRabi},~\eqref{eq:DephasingAssistedPreJC}
				when taking the Rabi (solid blue) or Jaynes-Cummings interaction (dashed orange).
				The Rabi interaction again leads to a notable asymmetry with respect to zero detuning, in contrast to the Jaynes-Cummings result.}
			\label{fig:DephasingAssisted}
		\end{center}
	\end{figure}

	\subsubsection{Relevance to the readout problem}

	Current prototype implementations of quantum processors all suffer from comparatively poor read-out fidelities.
	This is at least partly due to the so far imperfect theoretical understanding of the relatively high-powered readout employed in these architectures.
	As an example, Purcell decay of the qubit scales with readout photon number $n$ in the cavity as $\sim 1/n$~\cite{Sete:PRA:2014, Slichter:NJP:2016},
	while experimentally it has been shown that the qubit lifetime decreases with increased readout power~\cite{Minev:N:2019}, implying that other processes are dominant in this situation.
	%
	A way out may be offered by recent development of drive induced dissipative processes,
	which typically arise due to correlated decay processes, like the ones we also calculate here~\cite{Boissonneault:PRA:2009, Boissonneault:PRA:2008, Petrescu:PRB:2020}.
	In the following we give a short discussion of what the implications of our result are in the strong driving case.

	To describe the effect of driving the resonator, we start by applying a displacement transformation to the master equation
	\footnote{
	In the strong driving case, the displacement transformation should actually be applied first, before other perturbative expansions are performed.

	This would change some of the frequency dependence in the dissipators without changing their qualitative behaviour.
	For the purpose of simplicity we do not consider this additional complication here.

	},
	$D(\alpha) = \exp\{\alpha a\hc - \alpha\cc a\}$, which transforms resonator operators as
	\begin{align}
		D\hc a D  = \tilde a + \alpha
		\label{eq:Displace}
	\end{align}
	with the coherent state amplitude $\alpha$ and the new resonator annihilation operator in the displaced frame $\tilde a$.
	In this approach, one choses the displacement amplitude $\alpha$ such that the effective resonator variable in the displaced frame, $\tilde a$, now describes an undriven resonator.
	This is achieved by choosing a dynamical value of
	$\alpha$ which effectively cancels out the drive terms in the dynamical equations.
	$\alpha$ then describes the semi-classical dynamics of the photon number in the driven resonator, $n = \abss\alpha$,
	while the residual photonic quantum fluctuations are still described by the dynamics of $\tilde a$~\cite{Mueller:PRA:2016}.
	Th displacement transformation, \eqn{eq:Displace}, acts on correlated dissipators in a peculiar way.
	E.g. one of the dressed dephasing dissipators in Eq.~\eqref{eq:DD} transforms as
	\begin{align}
		\mathcal D\left[ D^\dagger \sigma_{k,k+1} a^\dagger D \right] = \mathcal D\left[ \sigma_{k,k+1} \tilde a^\dagger \right] + |\alpha|^2 \mathcal D \left[ \sigma_{k,k+1} \right] + \ldots
		\label{eq:Drive}
	\end{align}
	where the additional terms omitted here will {not contribute to the qubit's dynamics, i.e. will }cancel once a trace over resonator degrees of freedom is performed.
	From the second term in Eq.~\eqref{eq:Drive} we see that {in the driven frame now appears
	a qubit relaxation channel whose decay rate is proportional to the resonator photon number $n = \abss\alpha$.
	A similar expression holds for all the dressed dephasing terms,
	which will contribute qubit decay and excitation rates proportional to the photon number. {In the strongly driven case, and reduced to the qubit dynamics, \eqn{eq:DD} then changes to
	\begin{align}
		\mathcal L_{\updownarrow,\pm} \rho \rightarrow \sum_{k} \gamma_{\downarrow}^{(k)} \diss{\sigma_{k, k+1}}\rho + \gamma_{\uparrow}^{(k)} \diss{\sigma_{k+1, k}}\rho
	\end{align}
	with the photon number-dependent rates $\gamma_{\downarrow}^{(k)} = n ( \gamma_{\downarrow,+}^{(k)} +  \gamma_{\downarrow,-}^{(k)})$ and $\gamma_{\uparrow}^{(k)} = n (\gamma_{\uparrow,+}^{(k)} +  \gamma_{\uparrow,-}^{(k)})$.
	Similar corrections have previously been derived in the Jaynes-Cummings approximation~\cite{Boissonneault:PRA:2009}.}
	{Additionally, here we predict a novel photon number dependent contribution to the qubit dephasing rate, from the photon assisted dephasing process, \eqn{eq:DA}, which transforms as
	\begin{align}
		\mathcal L_{\varphi,\pm}\rho \rightarrow \sum_{k} \gamma_{\varphi}^{(k)} \diss{\sigma_{k,k}}\rho
	\end{align}
	with $\gamma_{\varphi}^{(k)} = n (\gamma_{\varphi,+}^{(k)} + \gamma_{\varphi,-}^{(k)} )$.}
	For superconducting {transmon} qubits, where the longitudinal bath spectral function is thought to decay as $C_{\op Z}(\omega) \sim 1/\omega$,
	the major contribution to qubit linewidth here will likely be through {the second process of} photon assisted dephasing.
	%
	A proper comparison to experiments is unfortunately outside the scope of this work at the current time,
	as experimental investigations are still in the early stages.
	Additionally, the frequency dependence of the spectral functions of the dissipative baths of both qubit and resonator play a nontrivial role
	and are currently relatively poorly understood.

\section{Conclusion and Outlook}

	The Jaynes-Cummings model in the dispersive regime is of major importance for todays quantum computing prototypes based on superconducting qubits.
	At its heart it is based on the rotating wave approximation of the underlying Rabi model, and all expression derived from it are subject to the limitations of this approximation.

	A better analytic understanding of the dispersive parameter regime is fundamental for further improving prototype quantum processors based on superconducting qubits,
	and will similarly affect the upcoming efforts on large-scale spin qubit devices.

	The analytic equations developed here are based on the Rabi model directly, and allow a more accurate description of quantum systems in the dispersive regime from measured quantities,
	and thus improved predictions for their behaviour.
	Further, going to higher orders perturbation is straightforward using the Keldysh diagrammatic technique employed here.
	This may be used in the future to further improve the expressions for the dispersive shifts or to investigate higher order dissipative processes.

	\acknowledgments{I want to thank T.~M.~Stace for help with the early stages of the project, much useful feedback and making me chase up those pesky minus signs,
	A.~Blais and A.~DiPaolo for suggesting the project in the first place, A.~Petrescu for making me aware of the measurement problem and
	A.~Blais, J.~H.~Cole, J.~Delaforce, A.~Fedorov, and S.~Filipp for general discussions and feedback on the manuscript.
	This work was supported by the Australian Research Council Centre of Excellence for Engineered Quantum Systems (EQuS, CE110001013 and CE170100009)
	and the Swiss National Science Fund through NCCR QSIT.}