diff options
Diffstat (limited to 'chapters/background')
| -rw-r--r-- | chapters/background/01-neural-networks.tex | 123 | ||||
| -rw-r--r-- | chapters/background/02-interaction-nets.tex | 73 | ||||
| -rw-r--r-- | chapters/background/03-satisfiability-modulo-theories.tex | 22 |
3 files changed, 215 insertions, 3 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$. 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. + |