Abschlussarbeit

Die Korrektheit von Marabou, einem Verifikationsprogramm von Eigenschaften Neuronaler Netze, wird untersucht. Neben einer kurzen Einführung in die Theorie Neuronaler Netze und ihrer Prädikatenlogischen Formalisierung, wird eine ausführliche Darstellung der Grundlagen dieser Formalisierung sowie der Spezifizierung der zu verifizierenden Eigenschaften gegeben, was auf die Introduktion von Marabou als Satisfiablity-Modulo-Theory-(SMT)-basierten Programm führt. Es wird der Reluplexalgorithmus vorgestellt, auf dem das Verfikationsverfahren basiert. Dass die Korrektheit dieses Algorithmus, durch die Verwendung von Fließkommazahlen anstelle der Reellen Zahlen gefährdet ist, findet sich exemplifiziert. Die Falsifikation Marabous wird auf der Grundlage eines neuartigen auf Hilbertmatrizen basierenden Verfahrens durchgeführt. Der von Jia und Rinard in [JR20] vorgestellte Exploit eines vollständigen Verifizierers Neuronaler Netze wird mit Bezug auf Marabou reproduziert.