1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
|
\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~\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$.
|
