Verifikation von Anomaliedetektoren

• Antragsteller: Professor Dr. Daniel Neider
• Fachliche Zuordnung: Theoretische Informatik ; Softwaretechnik und Programmiersprachen ; Technische Thermodynamik
• Förderung: Förderung seit 2022
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 459419731

Anomaliedetektoren müssen sicher und zuverlässig arbeiten. Dies gilt insbesondere, wenn sie in sicherheitskritischen Anwendungsbereichen wie den chemischen Anlagen dieser Forschungsgruppe eingesetzt werden. Hier können nicht erkannte Anomalien schnell eine Gefahr für die Umwelt und menschliches Leben bedeuten. Umgekehrt führen Fehlalarme zu unnötigen Abschaltungen und den damit einhergehenden wissenschaftlichen und finanziellen Einbußen. Das grundlegende Ziel dieses Projekts ist daher die Entwicklung leistungsfähiger Verifikationsverfahren, welche die Sicherheit und Zuverlässigkeit der in den Projekten A1 und A4 generierten künstlichen neuronalen Netzen zur Anomaliedetektion bzw. Datengenerierung formal beweisen können.Trotz intensiver Bemühungen in den letzten Jahren steckt die Verifikation neuronaler Netze noch immer in den Kinderschuhen. Speziell für die Verifikation der für diese Forschungsgruppe relevanten neuronalen Netzwerke, welche unüberwacht aus multimodalen Zeitreihen gelernt werden, existieren bis heute nur wenige, stark eingeschränkte Methoden. Das beantragte Projekt wird wesentlich dazu beitragen, diese Lücke zu schließen und die Entwicklung und Implementierung von Verifikationsverfahren für neuronale Netzwerke bedeutend voranzutreiben. Insgesamt werden wir in drei Schritten vorgehen.Im ersten Schritt werden wir Korrektheitseigenschaften identifizieren, welche neuronale Netzwerke (in dieser Forschungsgruppe und darüber hinaus) erfüllen müssen, um sicher und verlässlich zu arbeiten. Dazu werden wir eng mit den Projekten A1, A4, B1 und B2 zusammenarbeiten.Im zweiten Schritt werden wir die zuvor identifizierten Korrektheitseigenschaften formalisieren. Dazu werden wir eine "Neural Temporal Logic (NTL)" genannte und speziell auf neuronale Netzwerke für multimodale Zeitreihen zugeschnittene Logik entwickeln. Bei dieser Logik wird es dabei erstmals möglich sein, auch "informelle" Eigenschaften wie "wenn das Gas in der Leitung kondensiert, muss ein Alarm muss ausgelöst werden" auszudrücken (und zu verifizieren).Im dritten Schritt werden wir schließlich effiziente Verfahren zur Verifikation von neuronalen Netzen bzgl. in NTL ausgedrückten Korrektheitseigenschaften entwickeln. Dabei werden wir sowohl qualitative Verifikationsverfahren (die "ja" oder "nein" antworten) als auch quantitative Verifikationsverfahren (die eine Wahrscheinlichkeit berechnen) berücksichtigen. In beiden Fällen werden wir zwei orthogonale Typen von Algorithmen entwickeln: solche, die direkt auf den neuronalen Netzen arbeiten, und solche, die Abstraktionen berechnen. Da wir im Allgemeinen nicht davon ausgehen können, dass jedes unserer neuronalen Netze alle Korrektheitseigenschaften erfüllen wird, werden wir auch effektive Reparaturverfahren entwerfen, die Fehler anhand von Informationen aus fehlgeschlagenen Verifikationsversuchen korrigieren können. Dabei werden wir unsere Algorithmen auf den neuronalen Netzen der Projekte A1 und A4 empirisch evaluieren.

• DFG-Verfahren: Forschungsgruppen
• Teilprojekt zu: FOR 5359: KI-FOR: Deep Learning auf dünnbesetzten, chemischen Prozessdaten