diff options
Diffstat (limited to 'chapters/background/01-neural-networks.tex')
| -rw-r--r-- | chapters/background/01-neural-networks.tex | 123 |
1 files changed, 122 insertions, 1 deletions
diff --git a/chapters/background/01-neural-networks.tex b/chapters/background/01-neural-networks.tex index 75bd8c4..848f65a 100644 --- a/chapters/background/01-neural-networks.tex +++ b/chapters/background/01-neural-networks.tex @@ -1,4 +1,125 @@ \section{Neural Networks} \label{sec:neural-networks} -% This section introduces 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$. |