000253715 001__ 253715
000253715 005__ 20260203173103.0
000253715 0247_ $$aG:(GEPRIS)286525601$$d286525601
000253715 035__ $$aG:(GEPRIS)286525601
000253715 040__ $$aGEPRIS$$chttp://gepris.its.kfa-juelich.de
000253715 150__ $$aFormale Verifikation von analoger AI-Hardware (FAI)$$y2016 - 2026
000253715 371__ $$aProfessor Dr.-Ing. Matthias Althoff
000253715 371__ $$aProfessor Dr.-Ing. Lars Hedrich
000253715 371__ $$aDr.-Ing. Markus Olbrich
000253715 450__ $$aDFG project G:(GEPRIS)286525601$$wd$$y2016 - 2026
000253715 5101_ $$0I:(DE-588b)2007744-0$$aDeutsche Forschungsgemeinschaft$$bDFG
000253715 680__ $$aKü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.
000253715 909CO $$ooai:juser.fz-juelich.de:920317$$pauthority$$pauthority:GRANT
000253715 909CO $$ooai:juser.fz-juelich.de:920317
000253715 980__ $$aG
000253715 980__ $$aAUTHORITY