Maschinelles Lernen (ML) dringt zunehmend in sicherheitskritische Bereiche vor – das macht absolute Vertrauenswürdigkeit unverzichtbar. Um KI-Systeme in sicheren Bahnen zu halten und schwerwiegende Fehler zu verhindern, sind Methoden für kontrollierte Ergebnisse der Modelle entscheidend. Das rasch wachsende Quanten-Machine-Learning (QML) übernimmt diese Risiken nicht nur, sondern erweitert sowohl die Angriffsmethoden als auch die potenziellen Folgen von Fehlern. Genau das macht eine intensivere Forschung in diesem Bereich so dringlich, auch das Fraunhofer IKS ist mit dabei.
25. Juni 2026
© iStock/yekorzh
Im vorherigen Blogbeitrag haben wir heuristische Abwehrmaßnahmen gegen feindliche Angriffe im Quantum Machine Learning (QML) diskutiert. Diese Maßnahmen erweisen sich gegen eine Vielzahl bekannter Angriffe als zuverlässig; doch was passiert, wenn Angreifer klügere und fortschrittlichere Attacken gegen Modelle Künstlicher Intelligenz (KI) entwickeln? Gibt es also eine allgemeinere Methode, die Robustheit von Modellen nachzuweisen? Die formale Verifikation bietet eine präzise Alternative: Sie zielt darauf ab, einen Rahmen (Framework) bereitzustellen, um die Robustheit eines KI-Modells unter einem definierten Bedrohungsmodell zu überprüfen. Und entweder eine beweisbare Robustheitsgarantie zu liefern oder einen verifizierten Gegenbeweis anzutreten.
Wie bei vielen theoretischen, formalen Methoden ist der Entwurfsprozess jedoch anspruchsvoll, und der Ansatz kann bei einer einfachen Umsetzung enorm viel Rechenleistung erfordern. Dieser Beitrag fasst das Buchkapitel zusammen, das die Abteilung Quanten Computing am Fraunhofer-Institut für Kognitive Systeme IKS gemeinsam mit der Data Analytics and Machine Learning Group der TUM über formale Verifikationsmethoden der Quanten-KI sowie quanten-gestützte Verfahren zur Verifikation klassischer KI verfasst hat.
© Fraunhofer IKS
Welche formalen Verifikationsmethoden gibt es? Exakte Verfahren liefern enge Ober- und Untergrenzen und ermöglichen damit sowohl die Beurteilung der Robustheit (das Modell bleibt unter einem festgelegten Bedrohungsmodell sicher) als auch die Identifikation von Nicht-Robustheit (es existieren adversarial examples innerhalb dieses Bedrohungsmodells). Der Nachteil ist, dass diese Methoden oft sehr rechenintensiv sind, da sie in der Regel das Lösen von NP-schweren Optimierungsproblemen erfordern.
Ergänzt werden diese durch stochastische Methoden, die stattdessen probabilistische Garantien bieten. Sie zertifizieren, dass die gewünschten Eigenschaften mit hoher Wahrscheinlichkeit erfüllt sind, und tauschen so absolute Gewissheit gegen bessere Skalierbarkeit und Effizienz ein.
Eine neue Alternative ist der Einsatz von Quanten- oder quanten-klassischen Hybrid-Routinen, um rechenintensive formale Verifikationsmethoden zu beschleunigen – ein Thema, das später noch diskutiert wird. Parallel dazu arbeitet die aktuelle Forschung daran, approximative Schranken für eine breitere Palette von Modellfamilien zu verschärfen und gleichzeitig die Rechenkosten überschaubar zu halten.
Die formale Verifikation von Quanten-KI untersucht das gesamte Spektrum der verfügbaren Methoden, um die Robustheit und Korrektheit von Quantenmodellen zu zertifizieren. In diesem Bereich wurden bereits erhebliche Fortschritte erzielt, insbesondere durch das Fraunhofer IKS und die TUM als Teil des Bayerischen Kompetenzzentrums für Quanten Security and Data Science (BayQS), in dem die Teams an der QC-basierte Zertifizierung von Neuronalen Netzen arbeiten und maßgeblich zur Gestaltung grundlegender Ansätze beigetragen haben. Ein zentrales Thema ist dabei, Quantenrauschen nicht nur als Herausforderung, sondern als potenziellen Verbündeten zu betrachten: Quantensysteme sind von Natur aus verrauscht, und Forschende untersuchen derzeit, ob dieses kontrollierte Rauschen die Robustheit zertifizieren oder sogar verbessern kann.
Ein wichtiges Konzept, das diesen Methoden zugrunde liegt, ist die Differential Privacy (DP) – ein strenges mathematisches Framework, das quantifiziert, wie effektiv ein Algorithmus sensible Informationen in seinen Eingangsdaten verbirgt. Ein Hauptmerkmal von DP ist das Einbringen von Zufälligkeit, die im Quantenkontext durch das inhärente Hardware-Rauschen quasi „umsonst“ mitgeliefert wird. Obwohl Quantenrauschen typischerweise als Problem gesehen wird, zeigen neuere Arbeiten, dass es innerhalb eines DP-Frameworks gezielt genutzt werden kann, um beweisbare Robustheitsgarantien zu liefern. Diese und weitere Ansätze bieten ein fundiertes Fundament für die rigorose Verifikation von Quanten-KI-Anwendungen.
Diese Forschung wird vom Bayerischen Ministerium für Wirtschaft, Landesentwicklung und Energie mit Mitteln aus der Hightech Agenda Bayern gefördert.
Angesichts der mangelnden Praktikabilität der exakten Verifikation ist es von entscheidender Bedeutung, das Quantencomputing als Mittel zur Verringerung des Rechenaufwands zu erforschen. Beispielsweise können Formulierungen der gemischt-ganzzahligen linearen Programmierung (Mixed-Integer Linear Programming, MILP) für neuronale Netze mit stückweise linearen Aktivierungsfunktionen präzise, beweisbare Garantien liefern, sie sind jedoch NP-schwer und deshalb skalieren schlecht. Um dieses Problem anzugehen, nutzen Dekompositionsmethoden die Problemstruktur aus, um große MILPs in kleinere, handhabbarere Teilprobleme aufzuteilen. Die Teams des Fraunhofer IKS und der TUM im Rahmen von BayQC haben solche Ansätze ausführlich untersucht. Ihre Arbeit, kombiniert mit den Einschränkungen aktueller Quantenhardware, hat zu hybriden quanten-klassischen Dekompositionen geführt. Diese verbinden klassische Linear Programming Solver für die kontinuierlichen Variablen mit Quantenoptimierern (wie Quantum Approximate Optimization Algorithm, QAOA) für die binären Teilprobleme. Obwohl diese Methoden die klassischen Benchmarks noch nicht übertreffen, legen sie einen wichtigen Grundstein für eine skalierbare, quantenunterstützte Verifikation.
Mit Blick auf die Zukunft werden mit der Weiterentwicklung der Hardware in Richtung Fehlertoleranz andere Algorithmen wie die Grover-Suche und die Quanten-Amplitudenverstärkung (QAA) immer praktikabler. Diese Techniken bieten beweisbare Rechenbeschleunigungen, und Forschende weltweit (einschließlich des Teams am Fraunhofer IKS) arbeiten aktiv an praktischen Wegen, um sie so schnell wie möglich einzusetzen. Neben der Beschleunigung der exakten Verifikation sind sie auch vielversprechend für die Robustheitszertifizierung mittels Randomized Smoothing. Beim Randomized Smoothing wird ein Basis-Klassifikator in einen geglätteten Klassifikator mit einem zertifizierten Robustheitsradius umgewandelt – allerdings um den Preis einer hohen Anzahl von Monte-Carlo-Auswertungen. Quantenmethoden wie QAA können die Anzahl der erforderlichen Abfragen zur Schätzung der korrekten Klassifizierungswahrscheinlichkeit quadratisch reduzieren und den Zertifizierungsprozess dadurch erheblich beschleunigen.
Diese Forschung wird vom Bayerischen Ministerium für Wirtschaft, Landesentwicklung und Energie mit Mitteln aus der Hightech Agenda Bayern gefördert.
