Record #253715 - GSI Repository

DFG project G:(GEPRIS)286525601

Formale Verifikation von analoger AI-Hardware (FAI)

Coordinator	Professor Dr.-Ing. Matthias Althoff ; Professor Dr.-Ing. Lars Hedrich ; Dr.-Ing. Markus Olbrich
Grant period	2016 - 2026
Funding body	Deutsche Forschungsgemeinschaft
	DFG
Identifier	G:(GEPRIS)286525601

Note: 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.

Recent Publications

There are no publications

Record created 2023-01-19, last modified 2026-02-03

Similar records

Add to personal basket
Export as Author List with IDs BibTeX (UTF-8), EndNote XML, EndNote Text, RIS, MARC, Print MARC, MARCXML, DC,
Request correction
Submit fulltext

GSI Homepage \| GSI Library \| English Deutsch \| guest :: login GSI Repository
Search	Submit	Personalize Your alerts Your baskets Your searches	Help