Skalierbare Verifikation Digitaler Quanten Simulationen

• Antragsteller: Professor Dr. Benedikt Fauseweh; Professor Dr.-Ing. Ben Hermann; Professor Dr. Falk Howar
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen ; Theoretische Physik der kondensierten Materie
• Förderung: Förderung seit 2025
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 563135278

Die Quanteninformatik hat das Potenzial, Wissenschaft und Technologie grundlegend zu. Eine ihrer vielversprechenden Anwendungen ist die digitale Quantensimulation (DQS), die es ermöglicht, Quantenphänomene auf digitalen Quantencomputern zu modellieren. Mit der steigenden Anzahl von Qubits, der Tiefe und der Komplexität moderner Quantenschaltkreise wird die Analyse ihrer Eigenschaften jedoch zunehmend herausfordernd. Verifikationstechniken stehen vor dem Problem der Skalierbarkeit, das durch das exponentielle Wachstum des Zustandsraums, komplexe Qubit-Interaktionen und die Tiefe moderner Schaltkreise entsteht. Dieses Projekt zielt darauf ab, ein skalierbares, automatisiertes und kompositionales Framework für die Verifikation digitaler Quantensimulationen zu entwickeln. Mithilfe von Techniken aus der formalen Verifikation, Programmanalyse und domänenspezifischen Optimierungen sollen drei zentrale Herausforderungen adressiert werden: (1) die Encoding-Explosion globaler Gate-Effekte, die die Skalierbarkeit bei großen Qubit-Zahlen einschränkt; (2) die Automatisierung der Identifikation von Zwischen-Eigenschaften, die eine Dekomposition der Verifikationsaufgaben bei komplexen Gate-Strukturen ermöglicht; und (3) die zeitliche Dekomposition der Verifikation, um tiefe Schaltkreise mit vielen Iterationen handhabbar zu machen. Das Forschungsprojekt ist in vier Arbeitspakete gegliedert: (1) Anwendungsfälle und Benchmarks: Identifikation repräsentativer Quantenschaltkreise und Eigenschaften zur Evaluierung des Verifikationsframeworks. (2) Verifikationstechniken: Entwicklung neuer Methoden, darunter Assume-Guarantee-Reasoning, Schwächste-Vorbedingungs-Transformationen und Property-Directed Reachability, um große und komplexe Quantenschaltkreise zu verifizieren. (3) Automatisierung und Dekomposition: Design und Implementierung automatisierter Werkzeuge zur Entdeckung lokaler Eigenschaften, basierend auf Datenfluss- und statischer Analyse. (4) Integration und Demonstration: Kombination aller Komponenten in ein einheitliches Framework und Nachweis der Skalierbarkeit durch umfassende Evaluierung an Benchmarks aus der digitalen Quantensimulation. Das Feld der digitalen Quantensimulation wird von diesem Framework auf verschiedene Weise profitieren. Die Verifikation der Symmetrieerhaltung ist entscheidend für die Simulation von Quantenphysik und Quantenchemie. Der Einsatz skalierbarer Methoden ermöglicht, fundierte Entscheidungen über symmetrieerhaltende und symmetriebrechende Schaltkreise zu treffen. Darüber hinaus ist die Verifikation von Quantenschaltkreisen äußerst hilfreich bei der Programmierung von NISQ-Quantenhardware. Am Ende des Projekts soll ein robustes, skalierbares Verifikations-Framework in Form eines prototypischen Tools vorliegen. Dieses wird an realen Anwendungsfällen validiert und empirisch getestet.

• DFG-Verfahren: Schwerpunktprogramme
• Teilprojekt zu: SPP 2514: Quantum Software, Algorithmen und Systeme - Konzepte, Methoden und Werkzeuge für den Quanten-Softwarestack