Nächster Artikel
Maschinelles Lernen
Formale Verifikation von neuronalen Netzen mit Quantencomputern
Neuronale Netze sind nicht robust. Die Entwicklung zuverlässiger Prädiktoren erfordert systematische Methoden, um sowohl ihre Qualität zu bewerten als auch Vertrauen in ihre Korrektheit zu gewinnen. Hier kann Quantencomputing helfen.
© iStock/elenaleonova
Neuronale Netze können bei einigen grundlegenden Anforderungen unzuverlässig sein, z. B. bei der Bildskalierung und Helligkeitsänderungen. Sie sind auch sehr unverlässlich für bereichsspezifische Bedingungen, wie z. B. die Platzierung von Aufklebern auf Verkehrsschildern. Um zuverlässig zu arbeiten, muss das Modell daher die Stichprobe unter verschiedenen Lichtverhältnissen, Kamerawinkeln usw., die in der Realität vorkommen, korrekt klassifizieren.
Dieses Problem ist nicht neu. Die formale Überprüfung neuronaler Netze hat in verschiedenen Bereichen wie dem Maschinellen Lernen, Künstlicher Intelligenz, formalen Methoden und Sicherheit großes Interesse geweckt. Um das Problem besser zu verstehen, betrachten wir eine Menge zulässiger Störungen, S, für jedes Bild x. Damit wird die Manipulationsfähigkeit des Störfaktors erfasst. Bei der Bildklassifizierung steht S für die Wahrnehmungsähnlichkeit zwischen Bildern. S kann beispielsweise als konvexe Form um x herum modelliert werden. So können wir die Umgebungsbedingungen formal spezifizieren und neuronale Netze systematisch gegen sie testen.
Neuronale Netze und ihre Zertifizierung
In diesem Zusammenhang stellt S die Menge der möglichen Bilder dar, die durch den Angriff hervorgerufen werden könnten. Sie wird auch als »adversial region« bezeichnet. Es ist wichtig anzumerken, dass es praktisch unmöglich ist, alle möglichen Bilder in dieser Region aufzulisten und das Netz einfach in jedem einzelnen Bild laufen zu lassen, um zu überprüfen, ob es richtig klassifiziert ist. Daher gibt es zwei Methoden, um die Robustheit von neuronalen Netzen zu überprüfen:
- Konvexe Approximation
- Genaue Verifikation
Der erste Ansatz besteht darin, die konvexe Form S um die Eingabe x zu berechnen und sie auf das gesamte Netz zu übertragen, um eine Ausgabeform zu erhalten. Die Robustheit der Methode zeigt sich dann, wenn alle konkreten Ausgaben innerhalb der Ausgabenform korrekt klassifiziert werden.
Ein anderer Ansatz besteht darin, die ReLU (Rectified Linear Unit) mit binären Variablen zu formulieren, die angeben, ob ein bestimmtes Element aktiv oder inaktiv ist. Diese Methode ermöglicht es uns, das Verifikationsproblem als gemischt-ganzzahliges Optimierungsprogramm (mixed-integer optimization program, MIP) darzustellen. Bei kleineren Netzen kann eine Eingangsform mit exakter Präzision durch MIP übertragen werden. Um größere Netze zu skalieren, verwenden klassische Ansätze in der Regel die erste Methode und approximieren die Form mithilfe verschiedener konvexer Relaxationen (z. B. Intervalle, Zonotopen und Polytopen). Die approximative Analyse ist zwar in der Regel schneller und skalierbarer als die exakte Analyse, aber sie ist nicht immer effektiv bei der Überprüfung der Robustheit. Umgekehrt ist die exakte Analyse in der Regel exponentiell zeitaufwändig und weniger skalierbar. Sie gewährleistet jedoch die Vollständigkeit des Ergebnisses.
Wo das Quantum Machine Learning ins Spiel kommt...
Die Entwicklung von Hardware und Software für Quantencomputing (QC) hat in den vergangenen Jahren erhebliche Fortschritte gemacht. Die praktischen Anwendungen der Quantencomputer sind jedoch nach wie vor ein aktives Forschungsgebiet, da die derzeitigen Quantencomputer zur Kategorie der Noisy Intermediate Scale Quantum (NISQ)-Geräte gehören. Diese Geräte zeichnen sich durch eine relativ geringe Anzahl von Qubits (etwa 100), Rauschen und eine begrenzte Konnektivität zwischen den Qubits aus. Daher ist es derzeit nicht möglich, große und komplexe Berechnungen ausschließlich auf einem Quanten-PC durchzuführen. Stattdessen sind die derzeitigen Algorithmen hybrider Natur und erfordern die Interaktion zwischen klassischen und Quantencomputern.
Die Möglichkeit, den exponentiell großen Raum der Qubits zu nutzen, hat zu einem erheblichen Interesse an der kombinatorischen Optimierung sowohl des gatebasierten QC als auch des Quantum Annealing geführt. So sind wir die ersten, die die kombinatorische Kraft des Quantencomputing nutzen, um die Robustheit neuronaler Netze mit einem hybriden Quanten- und klassischen Algorithmus für maschinelles Lernen zu überprüfen.
In unserer Veröffentlichung 2022 haben wir das Verifikationsproblem formalisiert, um es an die Fähigkeiten von Quantenoptimierungs-Algorithmen anzupassen. Das Problem ist in zwei Teile gegliedert: Der erste Teil ist so aufgeschlüsselt, dass er in den Rahmen der quadratischen uneingeschränkten binären Optimierung (QUBO) passt, die von aktuellen Quanten-Heuristiken wie dem Quantum Approximate Optimization Algorithm (QAOA) verwendet wird. Der zweite Teil wird auf ein lineares Programm heruntergebrochen, das mit klassischen Solvern berechnet wird. Der Ansatz wechselt zwischen klassischem KI-basierten Maschinellen Lernen und Quantensystemen. Das QUBO wird von einem Quantencomputer oder einem Quanten-Annealer gelöst, und die Parameter werden von einem Optimierer aktualisiert, der auf klassischer Hardware läuft. Da es sich um ein heuristisches Verfahren handelt, führen mehr Iterationen zu besseren Ergebnissen. In unserem Ansatz haben wir die Anzahl der Iterationen reduziert und die maximale Anzahl der benötigten Qubits begrenzt.
Zusammenfassend lässt sich sagen, dass die Herausforderungen, die die derzeitigen NISQ-Geräte und die heuristischen Quantenalgorithmen darstellen, gut erforscht sind. Der Schlüssel zur Erschließung des Quantenvorteils liegt in der Identifizierung geeigneter Anwendungen und praktischer Anwendungsfälle. Angesichts der kombinatorischen Natur der formalen Verifikation neuronaler Netze bietet diese Herausforderung eine bedeutende Gelegenheit, den Quantenvorteil zu demonstrieren.
Quellen:
Franco, Nicola, Tom Wollschläger, Nicholas Gao, Jeanette Miriam Lorenz, and Stephan Günnemann. 2022. “Quantum Robustness Verification: A Hybrid Quantum-Classical Neural Network Certification Algorithm.” arXiv preprint.
Goodfellow, Ian J, Jonathon Shlens and Christian Szegedy. 2014. “Explaining and Harnessing Adversarial Examples.” arXiv preprint arXiv:1412.6572.