background

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$.