Moradkhani, Farzaneh (2024) Verification of Neural Networks Containing Non-Linear Activation Functions. PhD, Universität Oldenburg.

Preview

Volltext (3667Kb)

Abstract

Verifying the functionality of cyber-physical systems (CPS), including deep neural networks (DNNs), especially in safety-critical domains, presents a range of unresolved complexities. Despite their potential, prevalent computational structures lack scalable, automated verification mechanisms. The inherent size, non-linearity, and non-convexity of artificial neural networks (ANNs) make them particularly challenging for existing verification methods, such as mixed-integer linear programming (MILP) solvers and satisfiability modulo theories (SMT) solvers. This doctoral project undertakes a focused exploration of ANNs with nonlinear activation functions. A significant aspect of this research is the application of the SMT solver iSAT, which is uniquely adept at handling Boolean combinations of linear and nonlinear constraint formulas, even extending to transcendental functions. This capability makes iSAT suitable for verifying the safety properties of ANNs with nonlinear transfer functions.

["eprint_fieldname_title_plus" not defined]

Verifizierung neuronaler Netze mit nichtlinearen Aktivierungsfunktionen

["eprint_fieldname_abstract_plus" not defined]

Die Verifizierung der Funktionalität von cyber-physischen Systemen (CPS), einschließlich tiefer neuronaler Netze (DNNs), insbesondere in sicherheitskritischen Bereichen, stellt eine Reihe ungelöster Komplexitäten dar. Trotz ihres Potenzials fehlen den gängigen Rechenstrukturen skalierbare, automatisierte Verifikationsmechanismen. Die Größe, Nichtlinearität und Nichtkonvexität künstlicher neuronaler Netze (ANNs) machen sie besonders schwierig für bestehende Verifikationsmethoden wie Mixed-Integer-Linear-Programming (MILP)-Solver und Satisfiability Modulo Theories (SMT)-Solver. Dieses Promotionsprojekt widmet sich einer gezielten Erforschung von ANNs mit nichtlinearen Aktivierungsfunktionen. Ein wesentlicher Aspekt dieser Forschung ist die Anwendung des SMT-Solvers iSAT, der besonders geeignet ist, boolesche Kombinationen aus linearen und nichtlinearen Constraint-Formeln zu bearbeiten, einschließlich transzendenter Funktionen. Diese Fähigkeit macht iSAT geeignet, die Sicherheitseigenschaften von ANNs mit nichtlinearen Transferfunktionen zu verifizieren.

Item Type:	Thesis (PhD)
Uncontrolled Keywords:	Formal verification, Neural Networks, SMT solving, iSAT
Subjects:	Generalities, computers, information > Computer science, internet
Divisions:	School of Computing Science, Business Administration, Economics and Law > Department of Computing Science
Date Deposited:	30 Sep 2024 08:22
Last Modified:	30 Sep 2024 08:22
URI:	https://oops.uni-oldenburg.de/id/eprint/6925
URN:	urn:nbn:de:gbv:715-oops-70064
DOI:
Nutzungslizenz:

Actions (login required)

View Item