
\subsubsection{Acknowledgments}
The authors would like to thank Dr.\ Kiran Karra and Mr.\ Chace Ashcraft for
discussions on this topic and constructive comments on the approach. 

\subsection{Adversarial Input Generation}
The ``small'' MNIST classifier architecture is shown below
\begin{equation*}
    \label{eq:mnist_neural_net1}
    [\text{image}]
    \overset{784}{\rightarrow}
    \fbox{\strut PCA}
    \overset{30}{\rightarrow}
    \underbrace{\left[
    [x]
    \overset{30}{\rightarrow}
    \fbox{\strut Linear}
    \overset{10}{\rightarrow}
    \fbox{\strut ReLU}
    \overset{10}{\rightarrow}
    \fbox{\strut Linear}
    \overset{10}{\rightarrow}
    \fbox{\strut ReLU}
    \overset{10}{\rightarrow}
    [y]
    \right]}_{y=f(x;\theta)}
\end{equation*}
For the first experiment, the top-30 principal component network was probed to
see if there exist adversarial inputs to make the network misclassify specific
images.
The image representations with reduced dimensionality are treated as inputs
to~$f$,
a four-layer \textsc{PyTorch}{} \verb|Sequential| model composed of alternating
\verb|Linear| and \verb|ReLU| modules trained with stochastic gradient descent.
The components of the output vector are used to decide the digit
class according to~\eqref{eq:class-equality}.
This small network achieves 72.0\% accuracy on the validation data.

\begin{figure}[htbp]
    \vspace{-10pt}
    \centering
    \includegraphics[width=.9\textwidth]{figs/one_perturbed_to_seven.png}
    \caption{The network correctly classifies the original MNIST image (left) 
             as~\text{`}\texttt{1}\text{'}{} by observing the top-30 PCA components (middle).
             The input-perturbed image is misclassified as~\text{`}\texttt{7}\text{'}{} (right).}
    \label{fig:one_to_seven}
    \vspace{-15pt}
\end{figure}


We use \textsc{Lantern}{} to encode the small network as Z3 constraints.
Then we find a reduced-dimensionality representation of an image of a~\text{`}\texttt{1}\text{'}{}
that the network can correctly classify, and force that image to misclassify
as~\text{`}\texttt{7}\text{'}{}.
Figure~\ref{fig:one_to_seven} shows the original image, the image after PCA compression, 
and finally the misclassified version with an adversarial perturbation 
having magnitude $\|\Delta x\|_\infty = 0.4$.

\subsection{Adversarial Network Modification}
In this experiment, our goal was to modify the network biases such that several
\text{`}\texttt{1}\text{'}{} instances would be misclassified as~\text{`}\texttt{7}\text{'}{}, while the other classes
continued to be accurately classified. To test scalability and network
quantization, we used a slightly larger, top-100 component PCA compressed data
set with a similar neural network architecture:
\begin{equation*}
    \label{eq:mnist_neural_net2}
    [\text{image}]
    \overset{784}{\rightarrow}
    \fbox{\strut PCA}
    \overset{100}{\rightarrow}
    \underbrace{\left[
    [x]
    \overset{100}{\rightarrow}
    \overset{\begin{gathered}+\ensuremath{\Delta\theta_{\mathrm{bias}}} \\ \downarrow \end{gathered}}{\fbox{\strut Linear}}
    \overset{33}{\rightarrow}
    \fbox{\strut ReLU}
    \overset{33}{\rightarrow}
    \overset{\begin{gathered}+\ensuremath{\Delta\theta_{\mathrm{bias}}} \\ \downarrow \end{gathered}}{\fbox{\strut Linear}}
    \overset{10}{\rightarrow}
    \fbox{\strut ReLU}
    \overset{10}{\rightarrow}
    [y]
    \right]}_{y=f(x; \theta + \Delta\theta)}
\end{equation*}
Prior to any bias modifications, this medium-sized network had a 93.0\% overall
classification accuracy. Table~\ref{tab:class_accuracies} breaks down the
accuracy by each digit.

We encoded the linear layers with constraints of the form
\begin{equation}
    \quad y^{(k)} = W^{(k)} x^{(k)} + b^{(k)} + \ensuremath{\Delta\theta_{\mathrm{bias}}}^{(k)}
    \label{eq:bias_constraint}
\end{equation}
where $W^{(k)}$ and $b^{(k)}$ are the (fixed) network weights and biases for
the layer, $x^{(k)}$ and $y^{(k)}$ are the (variable) inputs and outputs of
each layer, and $\ensuremath{\Delta\theta_{\mathrm{bias}}}^{(k)}$ are (variable) bias perturbations.


To construct $D^\text{keep}$ and $D^\text{change}$, we chose one set of digits
\text{`}\texttt{0}\text{'}{} through \text{`}\texttt{9}\text{'}{}, which the original network classified correctly, and
added them to $D^\text{keep}$. This resulted in $|D^\text{keep}| = 10$
constraints of type~\eqref{eq:mod-a}.
We also found a specific~\text{`}\texttt{1}\text{'}{} image and set its classification target to~\text{`}\texttt{7}\text{'}{}. 
This resulted in $|D^\text{change}|=1$ constraint of type~\eqref{eq:mod-b}.
Additionally, we added constraints $\|\ensuremath{\Delta\theta_{\mathrm{bias}}}{}\|_\infty \leq 0.25$
to bound maximum parameter perturbations.


\subsubsection{Guarantees with inherited performance}
The results of our experiment are summarized in
Table~\ref{tab:class_accuracies}, which shows the digit classification
performance of the modified network. The accuracy shown for the modified
network (second column) is an average of two different $D^\text{keep}$ and
$D^\text{change}$ sets. These results indicate a considerable decrease in
accuracy when classifying \text{`}\texttt{1}\text{'}{}s, due to the forced prescription in
$D^\text{change}$, along with moderately smaller accuracy differences in the
other classes.  Note that for the modified network, the eleven examples in
$D^\text{keep}$ and $D^\text{change}$ are guaranteed to be at their prescribed,
forced values.

\begin{table}[htb!]

	\centering
    \caption{Classification accuracy of each digit with the original network 
    weights and biases, modified biases, and modified biases using a quantized model.}
    \label{tab:class_accuracies}
    \begin{tabular}{cccc}
    \toprule
	Digit & \multicolumn{3}{c}{Accuracy (\%)}\\
	\midrule
	{}  & Original & Modified & Quantized\\
	\text{`}\texttt{1}\text{'}{}     & 97.6  & 73.9  & 68.9\\ 
	\text{`}\texttt{2}\text{'}{}     & 92.4  & 89.6  & 91.1\\
	\text{`}\texttt{3}\text{'}{}   & 91.1  & 89.3  & 78.4\\
	\text{`}\texttt{4}\text{'}{}    & 94.0  & 84.2  & 86.1\\
	\text{`}\texttt{5}\text{'}{}    & 86.8  & 77.6  & 91.4\\
	\text{`}\texttt{6}\text{'}{}     & 95.1  & 90.5  & 93.3\\
	\text{`}\texttt{7}\text{'}{}   & 91.6  & 95.0  & 93.4\\
	\text{`}\texttt{8}\text{'}{}   & 91.1  & 85.9  & 74.8\\
	\text{`}\texttt{9}\text{'}{}    & 91.8  & 92.5  & 89.2\\
	\text{`}\texttt{0}\text{'}{}    & 97.9  & 96.7  & 98.6\\
	\midrule
	Overall & 93.0 & 87.4 & 89.2\\
    \bottomrule
    \end{tabular}
    \vspace{-5pt}
\end{table} 
It takes four hours for Z3 to find a satisfying assignment to \ensuremath{\Delta\theta_{\mathrm{bias}}}{} in
the top-100 network using linear rational arithmetic.\footnote{Tested on an
Intel(R) Core(TM) i9-8950HK CPU @ 2.90GHz on a 64-bit Windows operating system
with 32.0 GB installed RAM.}
After quantizing the network parameters to 10 bits with \verb|round_model()|,
run times went down to $30$ minutes per floating point arithmetic decision call
($8\times$ speedup).
Performance of the quantized model is shown in the last column of 
Table~\ref{tab:class_accuracies}.
The per-class accuracy for the quantized model is an average of three
different $D^\text{keep}$ and $D^\text{change}$ sets.

A visualization of how much the network biases changed is shown in
Figure~\ref{fig:histograms}.
\begin{figure}[htb!]
    \vspace{-10pt}
    \centering
    \subfigure[original biases]{
        \label{fig:histograms-a}
        \includegraphics[width=.34\textwidth]{figs/original_bias_histogram.pdf}
    }\hspace{-17pt}
    \subfigure[\ensuremath{\Delta\theta_{\mathrm{bias}}}{} values]{
        \label{fig:histograms-b}
        \includegraphics[width=.34\textwidth]{figs/delta_bias_histogram.pdf}
    }\hspace{-17pt}
    \subfigure[fine-tuned biases]{
        \label{fig:histograms-c}
        \includegraphics[width=.34\textwidth]{figs/modified_bias_histogram.pdf}
    }
    \caption{Histograms of \subref{fig:histograms-a} original network biases, 
    \subref{fig:histograms-b} solutions for the bias perturbations for adversarial 
    network modification, and \subref{fig:histograms-c} final modified biases.}
    \label{fig:histograms}
    \vspace{-10pt}
\end{figure}
Because the size distributions of the original and perturbed biases are so
similar, Figure~\ref{fig:histograms} suggests that detection of this type of
network tampering may be difficult. Thus, an across-the-board small change in
network biases guaranteed the eleven specific examples to be classified in a
user-prescribed way.



\subsubsection{Prior work}
\vspace{-1ex}
\paragraph{Prior work}
The rise in effective optimization techniques for producing adversarial
examples has led to an explosion of interest in how to fool neural networks
with inputs that are slight modifications of correctly classified examples.
Much effort has been devoted to finding such adversarial examples in various
neural networks~\cite{GoodfellowSS14,yuan2019adversarial}.
This has inspired researchers to use SMT to verify or construct neural networks
lacking such adversarial examples~\cite{Bohrer:2019,carlini2017provably,Cheng:2017}.

Like \textsc{Reluplex}{} and related approaches that use SMT to find adversarial
examples or guarantee their
absence~\cite{Katz2017ReluplexAE,Papusha:2018b,Bunel:2017,Ehlers:2017,Huang:2017,Dutta:2019},
we restrict our
attention to neural networks with piecewise affine activation layers. These
include, for example, rectifier linear unit (ReLU) and HardTanh, but
not sigmoid or softmax layers.
However, instead of searching for perturbations
on \emph{inputs}, we search for perturbations on the network \emph{biases},
thereby globally and tractably parameterizing all possible neural networks of a
certain class. 

Although we use MNIST as a running example, our patching approach inherits the
adverse scaling of SMT with neural network size, likely precluding adoption to
vision tasks in the near term. Our philosophy is therefore not just to retrain with
a modified training set as in~\cite{Gu:2017}, but rather to globally and
reliably optimize over the space of all neural networks that satisfy a set of
constraints.  This allows application in broader frameworks for design and
verification of high reliability systems with formal guarantees on end-to-end
behavior~\cite[\S{}2]{Papusha:2018b}.


As part of this paper, we review methods (\S\ref{sec:smt}) for translating a
neural network into SMT constraints, and follow with detail on using the
encoded network to generate adversarial inputs (\S\ref{sec:method}), as well as
adjusting the network parameters to implant guaranteed input-output pairs.
We demonstrate this approach (\S\ref{sec:experiments}) by implanting behavior
in a small example network for digit classification.  We conclude
(\S\ref{sec:conclusion}) with a discussion of the potential for this method to
scale to larger networks, as well as future work. 
\vspace{-2ex}

\subsection{Adversarial Input Generation}
\label{sec:adversarial-input}

Consider a trained network $f$, which \emph{correctly} classifies an input 
$x^0$ as $y^0$, so that specifically $y^0 = f(x^0; \theta)$ for the given input-output 
pair $(x^0, y^0)$. We would like the network to instead output a specified $y^1$ 
for a perturbed input $x^0 + \Delta x$, where $y^0 \neq y^1$ and the perturbation 
magnitude $\|\Delta x\|$ is small.


In this setting, finding a minimal adversarial input amounts to solving the
(nonconvex) optimization problem
\begin{equation}
    \label{eq:adv-input-opt}
	\begin{array}{ll}
	  \mbox{minimize} & \|\Delta x\|\\
	  \mbox{subject to} & f(x^0 + \Delta x; \theta) = y^1
	\end{array}
\end{equation}
over the variable $\Delta x\in\mathbf{R}^n$. This will give a smallest perturbation 
$\Delta x$ on the input that is enough to get the network to misclassify $x^0$ as 
$y^1$. We target the $\ell_\infty$ norm $\|\cdot\|$, 
because it can be represented with piecewise affine (`$\max$') functions, 
although many other norms are possible. 
The parameters of the network $\theta$ remain constant throughout the 
adversarial input generation process. 

\subsubsection{Optimal perturbation}
The objective in~\eqref{eq:adv-input-opt} can be minimized with bisection by 
posing a sequence of queries to the SMT solver. Specifically, define the formula
\[
	F(\alpha) = \exists \Delta x \in\mathbf{R}^m . \  (y^1 = f(x^0 + \Delta x; \theta)) \wedge (\|\Delta x\| \leq \alpha).
\]

If, for a given value of $\alpha \in [\alpha_-, \alpha_+]$ 
(where $F(\alpha_+)$ is \texttt{sat}{} and $F(\alpha_-)$ is \texttt{unsat}), 
the formula $F(\alpha)$ is \texttt{sat}, then we know that at the optimum $\|\Delta x^\star\| \leq \alpha$; 
we should therefore decrease the upper bound to $\alpha_+ := \alpha$, and 
determine the satisfiability of $F((\alpha_+ + \alpha_-)/2)$, say. 
Otherwise if $F(\alpha)$ is \texttt{unsat}, then a valid input perturbation 
must have norm no less than $\alpha$; therefore, to make the network misclassify 
$x^0$ as $y^1$ we should increase the lower bound to $\alpha_- := \alpha$, 
and try again. This way, a minimal value of $\|\Delta x\|$ can be determined
within an error $\epsilon$ in $O(\log_2(1/\epsilon))$ bisection steps.

\subsubsection{Class membership}
Encoding the constraint $y^1 = f(x^0 + \Delta x; \theta)$ in~\eqref{eq:adv-input-opt} 
deserves special attention in the case of classifiers, because class membership 
must be encoded with set membership ({\it e.g.}, lying on the correct side of a decision surface).
For example, for $m=10$ (MNIST digit classification problem), 
we identify the output indices with the classes 
\text{`}\texttt{1}\text{'}{}, \text{`}\texttt{2}\text{'}{}, \ldots, \text{`}\texttt{9}\text{'}{}, \text{`}\texttt{0}\text{'}{}.
For example, the network output
\[
	f(x^0; \theta) = \begin{bmatrix}
	  0.01\\
	  0.95\\
	  \ldots\\
	  0.02
	\end{bmatrix}
\]
is interpreted as \text{`}\texttt{2}\text{'}{}, because the second component has maximal value
(softmax layers are disallowed in linear SMT theories).
A class equality constraint like $y = \text{`}\texttt{7}\text{'}{}$ is in reality a requirement
on the seventh component of $y$ to be maximal, 
\begin{equation}
	\label{eq:class-equality}
	(y_7 > y_1) \wedge
	\cdots \wedge
	(y_7 > y_6) \wedge
	(y_7 > y_8) \wedge
	\cdots \wedge
	(y_7 > y_{10}).
\end{equation}
A class membership constraint is thus a conjunction of affine constraints.

\subsubsection{Forcing correctness}
The same adversarial input generation technique can be used if the correctness
senses of $y^0$ and $y^1$ are switched: when the network \emph{incorrectly}
classifies $x^0$ as $y^0$, then solving the optimization
problem~\eqref{eq:adv-input-opt} is akin to finding a minimum-size
perturbation on the input that will \emph{force} the output to the desired
correct value $y^1$. In this case, the network outputs a correct value with a
small input perturbation, even if it originally failed to do so.

\subsection{Adversarial Network Modification}
\label{sec:adversarial-nnmod}

The idea of forcing output values introduced in the previous section can 
similarly be used to \emph{patch} the network parameters 
to achieve desired
performance on specified input-output pairs. The key difference
lies in patching the biases only, meanwhile keeping the weights fixed.


\subsubsection{Bias patching}
Consider a supervised task with a training database of input-output pairs 
$D = \{(x,y)\} \subset \mathbf{R}^n \times \mathbf{R}^m$. We would like 
to keep the neural network output values the same on a finite set 
$D^\text{keep} \subset \mathbf{R}^n \times \mathbf{R}^m$, 
and force a change on a finite set 
$D^\text{change} \subset \mathbf{R}^n \times \mathbf{R}^m$ 
of values.
It is not necessary that $D^\text{keep}$ or $D^\text{change}$ 
be subsets of $D$, but we require that 
$D^\text{keep} \cap D^\text{change} = \emptyset$.
The procedure for patching the network biases consists of two conceptual steps:
\begin{enumerate}
  \item{} [Train] Classically train ({\it e.g.}, using stochastic gradient descent) 
  a ReLU network $f(x; \theta)$ on the database $D$, obtaining the parameter 
  vector $\theta = (\theta_\text{weight}, \theta_\text{bias})$ as a starting point.
  \item{} [Patch] Keeping the weight component $\theta_\text{weight}$ fixed, 
  modify the network from Step 1 by solving the optimization problem
  \begin{alignat}{3}
    &\mbox{minimize }   && \|\ensuremath{\Delta\theta}\| \quad && \nonumber \\
    &\mbox{subject to } && y = f(x; \theta + \ensuremath{\Delta\theta}), \quad && \text{for all } (x,y) \in D^\text{keep}, \label{eq:mod-a} \\
    & && y' = f(x'; \theta + \ensuremath{\Delta\theta}), \quad && \text{for all } (x', y') \in D^\text{change}, \label{eq:mod-b} \\
    & && \ensuremath{\Delta\theta_\mathrm{weight}} = 0. \label{eq:mod-c}
  \end{alignat}
  over the variables $\ensuremath{\Delta\theta} = (\ensuremath{\Delta\theta_\mathrm{weight}}, \ensuremath{\Delta\theta_{\mathrm{bias}}})$.
\end{enumerate}

Classical neural network training will not
(typically) result in a parameter vector $\theta$ that correctly assigns 
all points in $D$. However, the SMT patching procedure will force the values in 
$D^\text{keep}$ and $D^\text{change}$, or otherwise return a proof
that a network modification of the prescribed type is impossible.

\subsubsection{Linear arithmetic}
The biases can can be patched because they enter affinely into the neural network 
constraints~\eqref{eq:nn-encoding} (whereas the weights enter multiplicatively).
As a result, bias perturbation variables can be added at each 
$\alpha_k$ network layer while still using a decision procedure based on 
linear arithmetic, {\it cf.}~\eqref{eq:aff-encoding},
\begin{equation}
	\label{eq:aff-encoding-perturb}
		v = \alpha_k(u) 
		\Longleftrightarrow 
		v = W^{(k)} u + b^{(k)} + \ensuremath{\Delta\theta_{\mathrm{bias}}}^{(k)}.
\end{equation}
Staying within a linear decision theory helps performance, 
although we expect weight modification with nonlinear theories 
(and multiplicative terms) to be practical in small networks~\cite{Gao:2012}.

A key scaling challenge lies in keeping the fewest number of constraints
in~\eqref{eq:mod-a} and~\eqref{eq:mod-b}, since there are as many instances of
the fully encoded neural network in the optimization problem as there are
examples in $D^\text{keep}\cup D^\text{change}$. To help this potential
difficulty, it is desirable to keep $|D^\text{keep}|$ and $|D^\text{change}|$
small.



\section{Introduction}
\label{sec:intro}
\input{nnmod-intro}


\section{Neural Network as Constraints}
\label{sec:smt}
\input{nnmod-smt}

\section{Method for Planting Examples}
\label{sec:method}
\input{nnmod-method}

\section{Experiments}
\label{sec:experiments}
\input{nnmod-experiments}

\section{Conclusion and Future Work}
\label{sec:conclusion}
\input{nnmod-conclusion}


\nocite{Papusha:2018b}
\nocite{Paszke:2019}  

\nocite{Knuth:2015}   
\nocite{Kroening:2016}
\nocite{Gu:2017}      

\bibliographystyle{splncs04}

\subsection{Piecewise Affine Networks}
\label{sec:nn-encoding}
Consider a network $f:\mathbf{R}^n \to \mathbf{R}^m$, represented by a function
$y=f(x;\theta)$, with parameters $\theta$. The input $x$ and
output $y$ are $n$- and $m$-dimensional real vectors, respectively.
In a typical architecture, the neural network is designed as a sequential
composition of alternating affine functions and piecewise affine ({\it e.g.}, ReLU,
HardTanh) activations,
\begin{equation}
	\label{eq:neural-net}
	f = \beta_K \circ \alpha_K \circ \cdots \circ \beta_1 \circ \alpha_1.
\end{equation}

Each affine function $\alpha_k: \mathbf{R}^{n_k} \to \mathbf{R}^{m_k}$ is
parameterized by a dense $m_k$-by-$n_k$ real weight matrix
$W^{(k)}$ and an $m_k$-dimensional bias vector $b^{(k)}$,
\begin{align}
	\label{eq:aff-layer}
	[\text{Affine}]   & \quad \alpha_k(x; W^{(k)}, b^{(k)}) := W^{(k)} x + b^{(k)}.
\end{align}
Similarly, the activation functions $\beta_k : \mathbf{R}^{m_k} \to \mathbf{R}^{m_k}$
are piecewise affine. We consider componentwise ReLU and HardTanh activations,
although any piecewise affine activation can be likewise treated,
\begin{align}
	\label{eq:relu-layer}
	[\text{ReLU}]     & \quad {\beta_k(x)}_i := \max(x_i, 0), \quad i=1,\ldots,m_k, \\
	\label{eq:hardtanh-layer}
	[\text{HardTanh}] & \quad {\beta_k(x)}_i := \max(\min(x_i, 1), -1), \quad i=1,\ldots,m_k.
\end{align}

The input dimension of the network $f$ is $n = n_1$ in the first
layer, and the output dimension is $m = m_K$ in the last. The
signal dimension can only change in the affine layers ($m_k \neq n_k$ in
general), and remains the same through the activations ($m_k = n_{k+1}$).
For convenience, we split the network parameters into
weight and bias components $\theta = (\theta_\text{weight},
\theta_\text{bias})$,
\begin{align*}
	\theta_\text{weight} &= (W^{(1)},\ldots,W^{(K)}) 
		\in \mathbf{R}^{m_1\times n_1} \times \cdots \times \mathbf{R}^{m_K \times n_K}, \\
	\theta_\text{bias}   &= (b^{(1)},\ldots,b^{(K)}) 
		\in \mathbf{R}^{m_1} \times \cdots \times \mathbf{R}^{m_K}.
\end{align*}


\subsubsection{SMT encoding}
We encode the neural network by introducing intermediate variables
$x^{(1)},\ldots,x^{(K+1)}, y^{(1)},\ldots,y^{(K)}$ to hold the
results of the compositions in~\eqref{eq:neural-net}. Specifically, for an
input variable $x$ and output variable $y$, the input-output relation of the
neural network $y = f(x;\theta)$ is equivalent to
\begin{equation}
	\label{eq:nn-encoding}
	(x = x^{(1)})
	\wedge
	\left(\bigwedge_{k=1}^{K} x^{(k+1)} = \beta_k(y^{(k)}) \wedge y^{(k)} = \alpha_k(x^{(k)})\right)
	\wedge
	(y = x^{(K+1)}).
\end{equation}
The affine layers are encoded as-is following~\eqref{eq:aff-layer},
\begin{align}
	\label{eq:aff-encoding}
	[\text{Affine-Encoding}]   & \quad
		v = \alpha_k(u) 
		\Longleftrightarrow 
		v = W^{(k)} u + b^{(k)},
\end{align}
with variables $u, v$ and parameters $W^{(k)}, b^{(k)}$.

To encode the activation functions, note that equality constraints
involving `$\min$' and `$\max$' can be written as a logical combination
of affine atoms:
\begin{align}
	\eta = \min(\xi, a) &
	\Longleftrightarrow 
			[(\xi \geq a) \to (\eta = a)] \wedge 
			[(\xi < a) \to (\eta = \xi)],\\
	\eta = \max(\xi, b) &
	\Longleftrightarrow 
			[(\xi < b) \to (\eta = b)] \wedge 
			[(\xi \geq b) \to (\eta = \xi)].
\end{align}
Accordingly, the piecewise affine activation functions are logical conjunctions
over individual components,
\begin{align}
	[\text{ReLU-Encoding}]
		& \quad v = \beta_k(u)
		\Longleftrightarrow
		\bigwedge_{j=1}^{m_k}
			(v_j = \max(u_j, 0)),
		
		
		\label{eq:relu-encoding}
		\\
	[\text{HardTanh-Encoding}] 
		& \quad v = \beta_k(u)
		\Longleftrightarrow
		\bigwedge_{j=1}^{m_k}
			(v_j = \max(\min(u_j, 1), -1)).
		
		   
		\label{eq:hardtanh-encoding}
\end{align}
Put together, equations~\eqref{eq:aff-encoding}--\eqref{eq:hardtanh-encoding}
can be substituted successively into equation~\eqref{eq:nn-encoding}, resulting
in an encoding of the neural network~\eqref{eq:neural-net} into a single
formula consisting of conjunctions, disjunctions, and negations of affine
atoms. Thus, any neural network constraint of the form $y=f(x;\theta)$, with
variables $x$ and $y$, and parameters $\theta$, corresponds to a conjunction of
constraints of the form~\eqref{eq:nn-encoding}.

\subsection{Using Pretrained PyTorch modules}
\label{sec:pytorch}

To automate our experiments, we developed a Python package, \textsc{Lantern}{}
(``safer than a torch''), which converts common neural network modules
from the popular
\textsc{PyTorch}{} library~\cite{Paszke:2019} to variables and
constraints that can be further manipulated with an SMT solver such as
Z3~\cite{deMoura:2008}. We assume that the (trained) network is 
represented as a \verb|Sequential| module, a \textsc{PyTorch}{} container that
holds other modules and applies them in sequence. 
We further assume that the modules within a given
\verb|Sequential| instance are either \verb|Linear|, \verb|ReLU|, or \verb|Hardtanh|. 

For each module in a \verb|Sequential|, \textsc{Lantern}{} generates Z3 variables that
correspond to the inputs and outputs of that module, and encodes the behavior of
that module as affine constraints (see~\S\ref{sec:nn-encoding}).
In addition, it creates constraints that equate the output variables of each
module with the input variables of the next module in the sequence. This
process returns the input and output variables of the entire \verb|Sequential|,
as well as all the constraints that represent the internal modules.

The default settings of \textsc{PyTorch}{} result in models parameterized by 32-bit
floats, which can give computationally difficult SMT formulas.  When the floats
are losslessly cast to \verb|Real|-sorted variables, formulas involving
the neural network can be handled using Z3's linear real arithmetic solver.
However, in practice we found that arbitrary precision calculations often
dominated decision run times, meaning that computations involving even
moderately sized networks benefited from a translation to IEEE floating-point
arithmetic. Therefore, our software also supports quantizing networks into
floating-point representations.

The \verb|round_model()| function truncates the significand of the
floating-point parameters of a trained network to a desired number of
bits. This function provides an adjustable trade-off between the neural
network's performance and the difficulty of the corresponding SMT problem. 
A rounded model remains a valid \verb|Sequential| object, and can be run
just like the original at inference time, albeit with reduced accuracy. 
By quantizing the model itself, we preserve a one-to-one correspondence between
the SMT problem and the network, even though the rounded model is no longer
equivalent to the original.
