🤖 machine learning

Formally Verifying Analog Neural Networks Under Process Variations Using Polynomial Zonotopes

Dieser Beitrag stellt einen formalen Verifikationsansatz für analoge neuronale Netze unter Prozessvariationen vor, der Polynomzonotope und ein polynombasiertes Modell verwendet, wodurch die Verifikationszeit von Tagen auf Sekunden reduziert wird, während gleichzeitig 99 % der Variationsstichproben präzise eingeschlossen werden, ohne auf Monte-Carlo-Simulationen zurückzugreifen.

Ursprüngliche Autoren: Yasmine Abu-Haeyeh, Tobias Ladner, Matthias Althoff, Lars Hedrich

Veröffentlicht 2026-05-12

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Yasmine Abu-Haeyeh, Tobias Ladner, Matthias Althoff, Lars Hedrich

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Stellen Sie sich vor, Sie bauen ein ultraschnelles, energieeffizientes Gehirn mit winzigen elektronischen Schaltkreisen anstelle von Softwarecode. Dies ist die Versprechung analoger neuronaler Netzwerke. Im Gegensatz zu den digitalen Computern in Ihrem Telefon, die strenge „Ein/Aus"-Schalter (0 und 1) verwenden, nutzen diese analogen Schaltkreise glatte, fließende elektrische Ströme, um zu imitieren, wie echte Neuronen funktionieren. Sie sind unglaublich schnell und verbrauchen sehr wenig Batterieleistung, was sie perfekt für tragbare Geräte und Sensoren macht.

Allerdings gibt es einen Haken. Da dies physische Schaltkreise sind, die aus Sand (Silizium) gefertigt werden, sind sie extrem empfindlich gegenüber dem Herstellungsprozess. Denken Sie daran wie an das Backen eines Kuchens: Selbst wenn Sie das Rezept perfekt befolgen, können winzige Schwankungen in der Ofentemperatur, der Luftfeuchtigkeit oder der exakten Größe Ihres Messlöffels das Ergebnis verändern. Bei der Chipfertigung bedeuten diese „Schwankungen", dass kein einziger Transistor exakt identisch mit einem anderen ist. Der eine könnte etwas breiter sein, der andere etwas dicker.

Für einen digitalen Computer macht ein winziger Unterschied nichts aus; eine 1 bleibt eine 1. Aber für ein analoges Gehirn kann ein winziger Unterschied dazu führen, dass das gesamte System eine falsche Vermutung anstellt.

Das Problem: Die „Monte-Carlo"-Falle

Um sicherzustellen, dass diese analogen Gehirne trotz dieser Fertigungsfehler korrekt funktionieren, verwenden Ingenieure normalerweise eine Methode namens Monte-Carlo-Simulation.

Stellen Sie sich vor, Sie wollen wissen, ob eine neue Brücke einem Sturm standhält. Der traditionelle Weg besteht darin, ein Modell zu bauen und dann einen Sturm 1.000 Mal mit leicht unterschiedlichen Windgeschwindigkeiten und Regenintensitäten zu simulieren. Sie tun dies immer wieder, um zu sehen, ob die Brücke jemals einstürzt.

Die Behauptung des Papiers: Dies für analoge neuronale Netzwerke zu tun, ist wie der Versuch, einen Sturm 1.000 Mal für jede einzelne Schicht eines komplexen Gehirns zu simulieren. Es dauert Tage Rechenzeit. Für eine einfache Bilderkennungsaufgabe (wie das Erkennen handschriftlicher Zahlen) benötigten die Forscher laut dem Papier fast 29.000 Sekunden (etwa 8 Stunden), nur um diese Simulationen auf einem Standardcomputer durchzuführen.

Die Lösung: Das „Polynomiale Zonotop"

Die Autoren dieses Papiers schlagen einen klügeren Weg vor. Anstatt den Sturm 1.000 Mal zu simulieren, erstellen sie eine mathematische Karte, die alle möglichen Stürme gleichzeitig abdeckt.

So haben sie es getan, aufgeteilt in einfache Schritte:

1. Die „Haupttäter" finden
Zuerst betrachteten sie den Schaltkreis und stellten fest, dass es zwar Dutzende von Variablen gibt, die schiefgehen könnten (wie die Dicke des Drahts oder die Spannung), aber nur zwei spezifische Variablen tatsächlich die meisten Probleme verursachten. Es ist, als würde man erkennen, dass bei einem Auto nur der Reifendruck und die Motortemperatur für die Sicherheit wirklich wichtig sind; die Farbe der Sitze spielt keine Rolle. Sie konzentrierten ihre Aufmerksamkeit auf diese beiden „dominanten" Faktoren.

2. Eine „Form" für die Fehler erstellen
Anstatt einzelne Punkte zu prüfen, verwendeten sie eine mathematische Form namens Polynomiales Zonotop.

Die Analogie: Stellen Sie sich vor, Sie versuchen, eine Herde Vögel zu fangen, die in einem chaotischen, unvorhersehbaren Muster fliegen.
- Der alte Weg (Monte Carlo): Sie versuchen, jeden Vogel einzeln zu fangen. Es dauert ewig, und Sie könnten einige verpassen.
- Der neue Weg (Polynomiale Zonotope): Sie spannen ein riesiges, flexibles, transparentes Netz über die gesamte Herde. Dieses Netz ist perfekt geformt, um die Bewegung der Vögel einzuhüllen und berücksichtigt, wie der Wind (die Fertigungsschwankungen) sie vorantreibt.
- Dieses „Netz" ist das Polynomiale Zonotop. Es ist eine spezielle Art von Form, die sich biegen und drehen kann, um die komplexen, gekrümmten Pfade anzupassen, die die Fehler nehmen, was einfachere Formen (wie gerade Kisten) nicht können.

3. Der „Verifikations"-Test
Sobald sie dieses Netz haben, müssen sie den Schaltkreis nicht Tausende von Malen simulieren. Sie prüfen einfach: „Bleibt das Netz innerhalb der 'Sicherheitszone'?"

Wenn das Netz (das alle möglichen Ergebnisse darstellt) die „unsichere Zone" (wo das Gehirn einen Fehler macht) niemals berührt, dann ist der Schaltkreis garantiert sicher, egal wie die Fertigung variierte.

Die Ergebnisse: Von Tagen zu Sekunden

Das Papier testete diese Methode an drei verschiedenen Aufgaben:

Brustkrebs-Erkennung: Unterscheidung zwischen gutartigen und bösartigen Tumoren.
Iris-Klassifizierung: Identifizierung verschiedener Blumentypen.
MNIST: Erkennung handschriftlicher Ziffern (0–9).

Das Ergebnis:

Geschwindigkeit: Die alte Methode dauerte Stunden oder sogar Tage. Die neue Methode dauerte Sekunden.
- Für die handschriftlichen Ziffern (MNIST) dauerte der alte Weg etwa 8 Stunden. Der neue Weg benötigte 1,77 Sekunden.
Genauigkeit: Die neue Methode war unglaublich präzise. Sie fang erfolgreich 99 % aller möglichen Schwankungen ein. Mit anderen Worten: Wenn Sie 100 dieser Chips bauen würden, garantierte das mathematische Netz, dass 99 davon korrekt funktionieren würden.

Warum dies wichtig ist (laut dem Papier)

Die Autoren betonen, dass es hier nicht nur um Geschwindigkeit geht, sondern um Durchführbarkeit.

Skalierbarkeit: Da die Methode so schnell ist, können Ingenieure nun größere, komplexere analoge Gehirne entwerfen, ohne wochenlang auf die Verifikation warten zu müssen.
Robustheit: Es ermöglicht den Designern genau zu sehen, wie viel Schwankung ein Chip aushalten kann, bevor er versagt. Zum Beispiel stellten sie fest, dass Chips mit kleinen Schwankungen (1 oder 2 Standardabweichungen) immer noch gut funktionierten, während Chips mit riesigen Schwankungen (3 Standardabweichungen) anfingen zu versagen. Dies hilft den Designern zu wissen, wo sie die Grenze ziehen müssen.

Zusammenfassung

Kurz gesagt, stellt das Papier ein neues „mathematisches Netz" (Polynomiale Zonotope) vor, das Ingenieuren ermöglicht, die Sicherheit analoger neuronaler Netzwerke in Sekunden statt in Tagen zu verifizieren. Indem sie sich auf die wichtigsten Fertigungsfehler konzentrieren und diese in eine flexible mathematische Form hüllen, bewiesen sie, dass diese energieeffizienten Schaltkreise vertrauenswürdig korrekt funktionieren können, selbst wenn sie mit unvollkommenen Materialien gebaut werden.

Technische Zusammenfassung: Formale Verifikation analoger neuronaler Netze unter Prozessvariationen mittels polynomialer Zonotopen

Problemstellung

Analoge neuronale Netze (ANNs) bieten im Vergleich zu digitalen Gegenstücken erhebliche Vorteile bei Stromverbrauch, Verarbeitungsgeschwindigkeit und Chipfläche, was sie für energiebeschränkte Anwendungen des Internets der Dinge (IoT) ideal macht. Als physikalische Schaltungen sind ANNs jedoch stark anfällig für Fertigungsprozessvariationen (z. B. Gatebreite, Schwellenspannung, Oxiddicke). Diese Variationen führen zu Abweichungen vom nominalen Modell und können die Sicherheit und Genauigkeit des Netzes gefährden.

Traditionelle Verifikationsmethoden stützen sich auf zeitaufwändige Monte-Carlo-Simulationen, um die Schaltungsfunktionalität unter diesen Variationen zu validieren. Für komplexe Netze, wie etwa Faltende Neuronale Netze (CNNs), können diese Simulationen Tage in Anspruch nehmen und stellen einen Engpass im Designzyklus dar. Darüber hinaus versagen bestehende Modellierungsansätze oft darin, das vollständige Systemverhalten zu erfassen oder fehlen an Skalierbarkeit über verschiedene Netzarchitekturen hinweg.

Methodik

Die Autoren schlagen einen Rahmenwerk zur formalen Verifikation vor, das Monte-Carlo-Simulationen durch eine mengenbasierte Erreichbarkeitsanalyse unter Verwendung von polynomialen Zonotopen ersetzt. Die Methodik besteht aus drei Hauptstufen:

1. Sensitivitätsanalyse und Parameterreduktion

Die Autoren analysierten eine 130-nm-CMOS-analoge Neuronenschaltung unter Verwendung des PSP-Transistormodells. Durch eine Sensitivitätsanalyse von über 50 Prozessparametern identifizierten sie, dass nur zwei dominante Parameter ( $\phi_1$ und $\phi_2$ ), die das Oberflächenpotential von NMOS-Transistoren beeinflussen, die Schaltungsleistung signifikant beeinträchtigen. Andere Parameter erwiesen sich als vernachlässigbar oder wurden durch die Schaltungstopologie (z. B. Stromspiegel) kompensiert.

2. Polynomiale parametrische Modellierung

Anstatt die vollständige Schaltungsphysik für jede Variation zu simulieren, leiteten die Autoren ein Polynommodell ab, um das Verhalten des Neurons zu abstrahieren.

Gewichtsmodellierung: Die Gewichte ( $\tilde{W}_k$ ) werden als Polynome dritter Ordnung der dominanten Parameter $\phi_1$ und $\phi_2$ modelliert.
Bias und Rauschen: Bias-Terme werden als vernachlässigbar behandelt, während die verbleibenden geringfügigen Variationen durch ein einziges drittes Rauschsymbol ( $d_3$ ) erfasst werden.
Formulierung: Das Netzwerkverhalten wird als Funktion dieser Parameter ausgedrückt, wodurch die Gewichte als Mengen statt als feste Werte dargestellt werden können. Spezifisch werden die Gewichte wie folgt modelliert:
$\tilde{W}_k = \sum_{i=0}^{3} \sum_{j=0}^{3} A_{k,i,j} \phi_1^i \phi_2^j + d_3$
wobei die Koeffizienten durch polynomiale Regression auf Monte-Carlo-Daten für jedes quantisierte Gewicht bestimmt werden.

3. Erreichbarkeitsanalyse mit polynomialen Zonotopen

Der Verifikationsprozess propagiert Eingabemengen durch das Netzwerk unter Verwendung von polynomialen Zonotopen, einer Mengendarstellung, die Abhängigkeiten zwischen Variablen handhaben kann.

Mengenpropagation: Die Eingabemenge wird schichtweise propagiert. Lineare Schichten beinhalten eine Matrixmultiplikation mit den polynomialen Gewichtsmengen.
Handhabung von Nichtlinearitäten: ReLU-Aktivierungsfunktionen werden mittels Standardtechniken für mengenbasierte Berechnungen eingeschlossen.
Verifikation: Die finale Ausgabemenge wird eingeschlossen. Wenn diese Einschließung nicht mit der Menge der „unsicheren" Ausgaben (z. B. falsche Klassifizierungsgrenzen) schneidet, wird das Netzwerk für den angegebenen Variationsbereich (z. B. $\pm 3\sigma$ ) formal als sicher verifiziert.

Hauptbeiträge

Optimiertes Polynommodell: Ein parametrisches Modell, das die Leistung analoger Neuronen unter Prozessvariationen präzise abstrahiert, indem es nur zwei dominante Parameter und ein Rauschterm verwendet, wodurch die Komplexität reduziert wird, während die Genauigkeit erhalten bleibt.
Systemweite formale Verifikation: Die Anwendung der Erreichbarkeitsanalyse mit polynomialen Zonotopen zur Verifikation von schaltungsebenenmodellen unter Prozessvariationen, wodurch der Bedarf an exhaustiven Monte-Carlo-Simulationen entfällt.
Skalierbarkeit: Der Ansatz wurde als skalierbar über verschiedene Architekturen hinweg nachgewiesen, einschließlich vollverbundener und faltender neuronaler Netze (CNNs).
Effizienz: Die Methode reduziert die Verifikationszeit drastisch, während sie einen hohen Prozentsatz der Variationsstichproben einschließt.

Experimentelle Ergebnisse

Der Ansatz wurde an drei Datensätzen evaluiert: Wisconsin Breast Cancer, Iris und MNIST (sowohl vollverbundene als auch CNN-Architekturen).

Verifikationszeit: Die vorgeschlagene Methode reduzierte die Verifikationszeit von Tagen auf Sekunden.
- MNIST CNN: Die Cadence-Monte-Carlo-Simulation benötigte ~29.592 Sekunden (ca. 8,2 Stunden); der vorgeschlagene Ansatz benötigte 3,37 Sekunden.
- Iris: Die Simulation benötigte ~865 Sekunden; der vorgeschlagene Ansatz benötigte 1,15 Sekunden.
Genauigkeit der Einschließung: Die Einschließung durch polynomialen Zonotopen erfasste erfolgreich etwa 99 % der Monte-Carlo-Variationsstichproben über alle Datensätze hinweg (im Bereich von 97,77 % bis 99,51 %).
Notwendigkeit des Modells: Eine Ablationsstudie, die polynomialen Zonotopen gegen Standardzonotopen (lineare Relaxationen) verglich, zeigte, dass lineare Modelle unzureichend waren. Standardzonotopen erzeugten Einschließungen, die Entscheidungsgrenzen kreuzten und somit die Sicherheitsverifikation scheiterten, wohingegen polynomialen Zonotopen enge Einschließungen lieferten, die die Spezifikationen erfolgreich verifizierten.

Bedeutung und Behauptungen

Die Autoren behaupten, dass ihre primäre Bedeutung darin liegt, die formale Verifikation analoger neuronaler Netze unter Prozessvariationen in einem rechnerisch machbaren Zeitrahmen zu ermöglichen. Durch den Wechsel von der statistischen Simulation (Monte Carlo) zur deterministischen mengenbasierten Analyse ermöglichen die Autoren:

Schnelle Designzyklen: Designer können die Robustheit analoger Schaltungen gegenüber Fertigungsvariationen schnell bewerten, ohne Tage an Simulationszeit abwarten zu müssen.
Sicherheitsgarantien: Die Methode bietet formale Garantien, dass das Netzwerk innerhalb eines angegebenen Variationsbereichs (z. B. 99 % der Stichproben) korrekt funktioniert, was für sicherheitskritische IoT-Anwendungen entscheidend ist.
Robustheitsbewertung: Der Ansatz ermöglicht die Quantifizierung, wie viele hergestellte Schaltungen fehlerhaft sein könnten (z. B. Identifizierung, dass Schaltungen, die über $2\sigma$ abweichen, an Genauigkeit verlieren könnten), und leitet den Bedarf an robusteren Schaltungsdesigns.

Die Autoren stellen fest, dass die aktuellen Modelle zwar relativ klein sind, dies jedoch eine Einschränkung der physikalischen Robustheit analoger Schaltungen und nicht der Verifikationsmethode selbst darstellt. Sie schließen daraus, dass dieser Ansatz den Designzyklus für größere, robustere analoge Inferenzschaltungen erheblich beschleunigen kann.