Formale Verifikation von analoger AI-Hardware (FAI)

• Antragsteller: Professor Dr.-Ing. Matthias Althoff; Professor Dr.-Ing. Lars Hedrich; Dr.-Ing. Markus Olbrich
• Fachliche Zuordnung: Elektronische Halbleiter, Bauelemente und Schaltungen, Integrierte Systeme, Sensorik, Theoretische Elektrotechnik
• Förderung: Förderung seit 2016
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 286525601

Künstliche neuronale Netze werden heute häufig in Hardware implementiert, um z.B. Energie zu sparen und/oder einfache bis komplexe Aufgaben in autonomen oder eingebetteten Systemen zu erledigen. Ein dringend zu lösender Nachteil solcher Implementierungen ist die schwere Verifizierbarkeit dieser Netze, da ihre Komplexität in der Regel die Anwendung vorhandener Verifikationstechniken unmöglich macht. Wenn KI jedoch nicht sicher gemacht werden kann, wird sie in der realen Welt trotz der enormen Investitionen nicht für sicherheitskritische Anwendungen verwendet werden können. Wir wollen daher völlig neue Ansätze für die formale Verifikation von analoger KI-Hardware - z.B. für energieeffiziente Implementierungen auf Transistorebene - entwickeln.Der Antrag umfasst folgende neue Forschungsziele. Es soll ein Framework zur formalen Verifikation speziell für analoge AI-Hardware erforscht werden, das eine sehr gute Skalierbarkeit für diesen Typus von neuronalen Netzen aufweist. Dies soll durch die Ausnutzung des Aufbaus analoger neuronaler Netze mit identischen Subsystemen und -gruppen in einem kompositionalen Verfahren erreicht werden. Zur weiteren Beschleunigung der formalen Verifikation werden spezifikationsorientierte Erreichbarkeitsalgorithmen entwickeln, die die Erreichbarkeitsanalyse durch Einbeziehung der Spezifikation mit dem Ziel des Beweises oder der Widerlegung steuert. Dies erhöht zusammen mit dem Einsatz von deutlich verbesserten Ordnungsreduktionsverfahren und einer verifikationsorientierten Synthese von Neuronen die Skalierbarkeit. Gerade der völlig neuartige vorgeschlagene Syntheseansatz in starker Kopplung mit den Verifizierungsalgorithmen schafft einfachere Schaltungen und damit verbunden einfachere Modelle, die es erlauben größere Netzwerke zu verifizieren.Das KI-fokussierte Framework soll in der Lage sein, beliebige Arten von Neuronen zu handhaben, die für eine breite Klasse von Anwendungen wie Fahrzeugsteuerung oder analoge Signalverarbeitung anwendbar sind. Als Unterstützung für den Entwickler solcher Systeme soll eine Berechnung von Gegenbeispielen zur direkten Falsifikation während des Entwurfsprozesses erforscht werden. Als Demonstratoren schlagen wir zwei Beispiele aus der Praxis vor: Ein medizinisches Beispiel mit einer analogen Implementierung von 2000 Neuronen für eine EKG-Klassifizierung und ein Beispiel aus dem Automobilbereich, das ein autonomes Fahrzeug mit Regelung auf Basis eines neuronalen Netzes realisiert.

• DFG-Verfahren: Sachbeihilfen