\section{Neural Networks}
\label{sec:neural-networks}

A neural network is a computational model inspired by biological neural networks. It consists of
connected nodes called neuron, introduced in its early form by Rosenblatt et al.~\cite{rosenblatt1958perceptron}.
\textit{Multi-Layer Perceptrons} is an architecture composed of sequential layers, trained using
backpropagation as popularized by Rumelhart et al.~\cite{rumelhart1986learning}.

\subsection{Neuron}
A neuron, illustrated in \textbf{\Cref{fig:single-neuron}}, receives a vector of inputs $x = (x_1, x_2, \dots, x_n)$, scales each input by a corresponding weight $w_i$,
adds a scalar bias $b$, and passes the resulting sum through a non-linear activation function $h$.
The output $y$ is defined as:
\begin{equation}
    y = h\left( \sum_{i=1}^{n} w_i x_i + b \right)
\end{equation}

\begin{figure}[H]
    \centering
    \begin{tikzpicture}[
        neuron/.style={circle, draw, minimum size=1.2cm, fill=black!5},
        input/.style={circle, draw, minimum size=0.6cm, fill=black!5},
        >=stealth,
        node distance=2cm
    ]
        % Inputs
        \node[input] (x1) at (0, 1.5) {$x_1$};
        \node[input] (x2) at (0, 0.5) {$x_2$};
        \node[coordinate] (dots) at (0, -0.3) {};
        \node[input] (xn) at (0, -1) {$x_n$};
        
        \node at (0, -0.2) {$\vdots$};
        
        % Neuron body (Sum and Activation)
        \node[neuron] (sum) at (4, 0.25) {$\sum$};
        \node[neuron] (act) at (6.5, 0.25) {$h$};
        
        % Weights labels on connections
        \draw[->] (x1) -- (sum) node[pos=0.4, above] {$w_1$};
        \draw[->] (x2) -- (sum) node[pos=0.4, above] {$w_2$};
        \draw[->] (xn) -- (sum) node[pos=0.4, below] {$w_n$};
        
        % Bias
        \node[input] (b) at (4, 2.2) {$b$};
        \draw[->] (b) -- (sum);
        
        % Connection sum -> act
        \draw[->] (sum) -- (act) node[above, midway] {$z$};
        
        % Output
        \node (y) at (9, 0.25) {$y$};
        \draw[->] (act) -- (y);
        
    \end{tikzpicture}
    \caption{Mathematical model of an artificial neuron.}
    \label{fig:single-neuron}
\end{figure}

\subsection{Multi-Layer Perceptron}
A \textit{Multi-Layer Perceptron} (MLP), illustrated in \textbf{\Cref{fig:mlp}}, is a type of neural network organized
in fully connected layers of neurons: an input layer, one or more hidden layers and an output layer.
An MLP is \textit{feedforward}, meaning that the flow of information is strictly propagated from the input to
the outputs.
\begin{figure}[H]
    \centering
    \begin{tikzpicture}[
        node/.style={circle, draw, minimum size=0.8cm, fill=black!5},
        >=stealth
    ]
        % Input Layer
        \foreach \i in {1,...,3} {
            \node[node] (I-\i) at (0, \i*1.2 - 2.4) {$x_{\i}$};
        }
        
        % Hidden Layer
        \foreach \i in {1,...,4} {
            \node[node] (H-\i) at (3.5, \i*1.2 - 3) {$h_{\i}$};
        }
        
        % Output Layer
        \foreach \i in {1,...,2} {
            \node[node] (O-\i) at (7, \i*1.2 - 1.8) {$y_{\i}$};
        }
        
        % Connect input layer to hidden layer
        \foreach \i in {1,...,3} {
            \foreach \j in {1,...,4} {
                \draw[->, thin, gray] (I-\i) -- (H-\j);
            }
        }
        
        % Connect hidden layer to output layer
        \foreach \i in {1,...,4} {
            \foreach \j in {1,...,2} {
                \draw[->, thin, gray] (H-\i) -- (O-\j);
            }
        }
        
        % Labels
        \node[above] at (0, 1.8) {Input Layer};
        \node[above] at (3.5, 2.4) {Hidden Layer};
        \node[above] at (7, 1.2) {Output Layer};
        
    \end{tikzpicture}
    \caption{Architecture of a Multi-Layer Perceptron (MLP) with one hidden layer.}
    \label{fig:mlp}
\end{figure}

One of the most common activation function is the ReLU, defined as:
\begin{equation}
    \text{ReLU}(z) = \max(0, z)
\end{equation}

\subsection{Neural Network Verification}
The verification problem of a neural network $F: \mathbb{R}^n \to \mathbb{R}^m$ with input constraint
$\mathcal{X} \subset \mathbb{R}^n$ and property $\mathcal{Y} \subset \mathbb{R}^m$ is defined as:
\begin{equation}
    \forall x \in \mathbb{R}^n, \quad x \in \mathcal{X} \implies F(x) \in \mathcal{Y}
\end{equation}
This can be interpreted as a satisfiability problem. We assert that there exists a counterexample $x$
that satisfies the constraint but violates the property:
\begin{equation}
    x \in \mathcal{X} \land F(x) \notin \mathcal{Y}
\end{equation}
If the SMT solver finds this formula to be unsatisfiable (UNSAT), the property holds. Instead, if it
finds it to be satisfiable (SAT), the solver provides a counterexample $x$.