From dbdd3ea807232b0be83d6a0eba9eb13011eb48e5 Mon Sep 17 00:00:00 2001 From: ericmarin Date: Sun, 21 Jun 2026 15:38:35 +0200 Subject: related work + conclusion --- chapters/background/01-neural-networks.tex | 2 +- chapters/background/03-satisfiability-modulo-theories.tex | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'chapters/background') diff --git a/chapters/background/01-neural-networks.tex b/chapters/background/01-neural-networks.tex index 848f65a..a1ecad2 100644 --- a/chapters/background/01-neural-networks.tex +++ b/chapters/background/01-neural-networks.tex @@ -2,7 +2,7 @@ \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 et al.~\cite{rosenblatt1958perceptron}. +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}. diff --git a/chapters/background/03-satisfiability-modulo-theories.tex b/chapters/background/03-satisfiability-modulo-theories.tex index bd90559..a55d54d 100644 --- a/chapters/background/03-satisfiability-modulo-theories.tex +++ b/chapters/background/03-satisfiability-modulo-theories.tex @@ -19,6 +19,6 @@ To represent a ReLU activation $y = \max(0, x)$ in LRA, we must introduce a disj (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}, +verification property requires the SMT solver, such as Z3 presented by De Moura et al.~\cite{demoura2008z3}, to implicitly explore this branching search space. -- cgit v1.2.3