background

5 files changed, 248 insertions, 24 deletions

diff --git a/chapters/02-background.tex b/chapters/02-background.tex
index c2d92b9..ca6160e 100644
--- a/chapters/02-background.tex
+++ b/chapters/02-background.tex
@@ -1,7 +1,9 @@
 \chapter{Background}
 \label{ch:background}
 
-% This chapter covers the fundamental concepts and notions required to understand the work
+This chapter contains the background theory necessary to understand the rest of the thesis such as:
+neural networks (\textbf{\Cref{sec:neural-networks}}), interaction nets
+(\textbf{\Cref{sec:interaction-nets}}) and SMT solvers (\textbf{\Cref{sec:satisfiability-modulo-theories}}).
 
 \input{chapters/background/01-neural-networks}
 
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$.
diff --git a/chapters/background/02-interaction-nets.tex b/chapters/background/02-interaction-nets.tex
index 268e441..36a7a32 100644
--- a/chapters/background/02-interaction-nets.tex
+++ b/chapters/background/02-interaction-nets.tex
@@ -1,4 +1,75 @@
 \section{Interaction Nets}
 \label{sec:interaction-nets}
 
-% This section introduces Interaction Nets
+Interaction Nets, introduced by Yves Lafont et al.~\cite{lafont1990interactionnets}, are a
+graphical model of computation based on graph rewriting.
+
+\subsection{Basic Concepts}
+An interaction net is an undirected graph with labelled vertices, called \textit{agents}. Each agent
+is an instance of a \textit{symbol}, which has a principal port and a fixed number of auxiliary ports:
+\begin{figure}[H]
+	\centering
+	\begin{tikzpicture}
+		\inetcell[arity=2](A){\textit{Add}}[90]
+		\inetwirefree(A.pax 1) \inetwirefree(A.pax 2) \inetwirefree(A.pal)
+		\node[left] at (A.above pax 1) {$\mathit{z}$};
+		\node[left] at (A.above pax 2) {$\mathit{y}$};
+		\node[right] at (A.above pal) {$\mathit{x}$};
+	\end{tikzpicture}
+	\caption{Example of an agent \textit{Add} with two auxiliary ports.}
+	\label{fig:agent}
+\end{figure}
+
+Each port can be wired to at most one other port. When two different agents are wired to their respective principal ports they are called an \textit{active pair}:
+
+\begin{figure}[H]
+	\centering
+	\begin{tikzpicture}
+		\inetcell[arity=2](A){\textit{Add}}[90]
+		\inetcell[arity=1, right=of A.pal](S){\textit{S}}[-90]
+		\inetwire(A.pal)(S.pal)
+		\inetwirefree(A.pax 1) \inetwirefree(A.pax 2) \inetwirefree(S.pax)
+		\node[left] at (A.above pax 1) {$\mathit{z}$};
+		\node[left] at (A.above pax 2) {$\mathit{y}$};
+		\node[right] at (S.above pax) {$\mathit{x}$};
+	\end{tikzpicture}
+	\caption{Example of an active pair, where a $\mathit{Add}$ agent and an $\mathit{S}$ agent are connected via their principal ports.}
+	\label{fig:active-pair}
+\end{figure}
+
+\subsection{Interaction Rules}
+Computation in interaction nets proceeds by rewriting the net using local \emph{interaction rules}. A rule
+is defined only for an active pair and, for any pair of agent types, there is at most one
+interaction rule.
+
+\begin{figure}[H]
+	\centering
+	\interactionrule{
+		\inetcell[arity=2](A){\textit{Add}}[90]
+		\inetcell[arity=1, right=of A.pal](S){\textit{S}}[-90]
+		\inetwire(A.pal)(S.pal)
+		\inetwirefree(A.pax 1) \inetwirefree(A.pax 2) \inetwirefree(S.pax)
+		\node[left] at (A.above pax 1) {$\mathit{z}$};
+		\node[left] at (A.above pax 2) {$\mathit{y}$};
+		\node[right] at (S.above pax) {$\mathit{x}$};
+	}{
+		\inetcell[arity=2](A){\textit{Add}}[90]
+		\inetcell[arity=1, left=of A.pax 1](S){\textit{S}}[-90]
+		\inetwire(A.pax 1)(S.pax)
+		\inetwirefree(A.pal) \inetwirefree(A.pax 2) \inetwirefree(S.pal)
+		\node[right] at (A.above pal) {$\mathit{x}$};
+		\node[left] at (A.above pax 2) {$\mathit{y}$};
+		\node[left] at (S.above pal) {$\mathit{z}$};
+	}
+	\caption{Interaction rule for $\mathit{S}$ and $\mathit{Add}$ that emulates Peano addition rule.}
+	\label{fig:rule-concrete-zero}
+\end{figure}
+
+\subsection{Properties}
+Interaction nets possess the following properties:
+\begin{itemize}
+	\item \textbf{Locality}: only active pairs can be rewritten.
+	\item \textbf{Linearity}: each interaction rule can be applied in constant time.
+	\item \textbf{Strong Confluence}: given a net $\text{IN}$ that can reduce to $\text{IN}_1$ and $\text{IN}_2$ in one
+		step, then both $\text{IN}_1$ and $\text{IN}_2$ reduce to some net $\text{IN}'$ in one step.
+\end{itemize}
diff --git a/chapters/background/03-satisfiability-modulo-theories.tex b/chapters/background/03-satisfiability-modulo-theories.tex
index b2c1416..bd90559 100644
--- a/chapters/background/03-satisfiability-modulo-theories.tex
+++ b/chapters/background/03-satisfiability-modulo-theories.tex
@@ -1,4 +1,24 @@
 \section{Satisfiability Modulo Theories}
 \label{sec:satisfiability-modulo-theories}
 
-% This section introduces Satisfiability Modulo Theories
+Satisfiability Modulo Theories (SMT) is the problem of determining whether a mathematical formula is
+satisfiable within a certain formal theory in first-order logic. Barrett et al.~\cite{barrett2016smtlib}
+defined the SMT-LIB standard for input format and theory definitions.
+
+For the verification of neural networks, the formal theory is \textit{Linear Real Arithmetic}
+(LRA). LRA deals with formulas containing real variables, constants, addition, subtraction,
+multiplication by constants, and equality/inequality relations: 
+\begin{equation}
+    \phi ::= t_1 \sim t_2 \mid \phi_1 \lor \phi_2 \mid \phi_1 \land \phi_2 \mid \neg \phi_1
+\end{equation}
+where $t_1, t_2$ are linear terms of the form $c_1 x_1 + \dots + c_k x_k + c_0$ (with $c_i \in \mathbb{R}$ and $x_i$ being real
+variables), and $\sim \;\in \{=, \le, <, \ge, >\}$.
+
+To represent a ReLU activation $y = \max(0, x)$ in LRA, we must introduce a disjunction:
+\begin{equation}
+    (x > 0 \land y = x) \lor (x \le 0 \land y = 0)
+\end{equation}
+For a network with $N$ ReLU neurons, there are up to $2^N$ possible activation patterns. Solving the
+verification property requires the SMT solver, such as Z3 presented by Demura et al.~\cite{demoura2008z3},
+to implicitly explore this branching search space.
+
diff --git a/references.bib b/references.bib
index 194a8b4..303b83f 100644
--- a/references.bib
+++ b/references.bib
@@ -94,26 +94,36 @@
 }
 
 @article{rosenblatt1958perceptron,
-  added-at = {2017-07-19T15:29:59.000+0200},
-  author = {Rosenblatt, F.},
-  biburl = {https://www.bibsonomy.org/bibtex/214ee8da21c66cd4d00d7ab6eca2d96a9/andreashdez},
-  citeulike-article-id = {13697582},
-  citeulike-linkout-0 = {http://dx.doi.org/10.1037/h0042519},
-  doi = {10.1037/h0042519},
-  interhash = {dc0cef9dc06033a04f525efdcde7a660},
-  intrahash = {14ee8da21c66cd4d00d7ab6eca2d96a9},
-  issn = {0033-295X},
-  journal = {Psychological Review},
-  keywords = {imported},
-  number = 6,
-  pages = {386--408},
-  posted-at = {2016-05-02 20:23:36},
-  priority = {2},
-  timestamp = {2017-07-19T15:31:02.000+0200},
-  title = {{The perceptron: A probabilistic model for information storage and organization in the brain.}},
-  url = {http://dx.doi.org/10.1037/h0042519},
-  volume = 65,
-  year = 1958
+	added-at = {2017-07-19T15:29:59.000+0200},
+	author = {Rosenblatt, F.},
+	biburl = {https://www.bibsonomy.org/bibtex/214ee8da21c66cd4d00d7ab6eca2d96a9/andreashdez},
+	citeulike-article-id = {13697582},
+	citeulike-linkout-0 = {http://dx.doi.org/10.1037/h0042519},
+	doi = {10.1037/h0042519},
+	interhash = {dc0cef9dc06033a04f525efdcde7a660},
+	intrahash = {14ee8da21c66cd4d00d7ab6eca2d96a9},
+	issn = {0033-295X},
+	journal = {Psychological Review},
+	keywords = {imported},
+	number = 6,
+	pages = {386--408},
+	posted-at = {2016-05-02 20:23:36},
+	priority = {2},
+	timestamp = {2017-07-19T15:31:02.000+0200},
+	title = {{The perceptron: A probabilistic model for information storage and organization in the brain.}},
+	url = {http://dx.doi.org/10.1037/h0042519},
+	volume = 65,
+	year = 1958
+}
+@article{rumelhart1986learning,
+	title={Learning representations by back-propagating errors},
+	author={Rumelhart, David E and Hinton, Geoffrey E and Williams, Ronald J},
+	journal={Nature},
+	volume={323},
+	number={6088},
+	pages={533--536},
+	year={1986},
+	publisher={Nature Publishing Group}
 }
 
 @inproceedings{katz2017reluplex,