Verified Pauli-Product Measurement Compilation for Fault-Tolerant Quantum Computation

Quantencomputer versprechen, Probleme zu lösen, die selbst für die leistungsstärksten Supercomputer derzeit unmöglich sind, von der Entschlüsselung komplexer Codes bis hin zur Simulation neuer Materialien. Diese Maschinen sind jedoch unglaublich fragil. Die kleinste Störung durch Hitze oder Vibration kann dazu führen, dass ihre Berechnungen zusammenbrechen. Um zu überleben, bauen Wissenschaftler fehlertolerante Quantencomputer, die spezielle Fehlerkorrektur-Codes verwenden, um Informationen zu schützen. Anstatt Daten auf einem einzelnen, empfindlichen Teilchen zu speichern, verteilen diese Systeme die Informationen über viele Teilchen und prüfen sowie korrigieren ständig Fehler. Die Herausforderung liegt in der Übersetzung: Wie nimmt man einen High-Level-Algorithmus und wandelt ihn in die spezifischen, Low-Level-Operationen um, die diese fehlerkorrigierten Maschinen tatsächlich ausführen können?

Die Standardmethode für viele dieser zukünftigen Maschinen beinhaltet eine Technik namens Lattice Surgery (Gitterchirurgie). Stellen Sie sich ein großes Stück Stoff vor, das den Speicher des Computers repräsentiert. Um eine Berechnung durchzuführen, betätigt man nicht einfach einen Schalter; man näht Stücke dieses Stoffes zusammen und zieht sie in präzisen Mustern auseinander. Diese Nähte sind keine physischen Fäden, sondern gemeinsame Messungen von Gruppen von Teilchen. Der Computer misst, wie diese Gruppen zueinander stehen, zeichnet das Ergebnis als einfaches Bit an Daten auf und nutzt diese Daten dann, um zu entscheiden, was als Nächstes zu tun ist. Dieser Prozess, bekannt als Pauli-Produkt-Messung, ist die fundamentale Sprache dieser zukünftigen Maschinen. Das Problem ist, dass die Softwarewerkzeuge, die zur Übersetzung von von Menschen entworfenen Algorithmen in diese Sprache verwendet werden, bisher unverifiziert waren. Wenn ein Compiler während der Übersetzung einen Fehler macht, könnte die gesamte Berechnung fehlschlagen, und da der Prozess so komplex ist, ist es schwierig zu wissen, wo der Fehler aufgetreten ist.

Ein Forscherteam der University of California, Los Angeles, hat diese Lücke geschlossen, indem es ein System entwickelt hat, das mathematisch beweist, dass die Übersetzung korrekt ist. Sie entwickelten eine neue Sprache speziell für diese messbasierten Programme und bauten einen Compiler, der Standard-Quantenschaltkreise in diese Sprache übersetzt. Entscheidend ist, dass sie nicht nur Code geschrieben, sondern ein Formal Verification Tool namens Lean verwendet haben, um einen strengen mathematischen Beweis zu konstruksieren, dass ihr Compiler das Verhalten des ursprünglichen Algorithmus bewahrt. Das bedeutet, dass für jeden Schritt, den der Compiler unternimmt, ein Zertifikat existiert, das garantiert, dass die Ausgabe exakt das ist, was die Eingabe produzieren sollte, bis hin zu den spezifischen Wahrscheinlichkeiten der Ergebnisse.

Die Forscher konzentrierten sich auf zwei Hauptaufgaben: Lowering (Abstieg) und Optimierung. Lowering ist der Prozess, einen Standard-Quantengatter, wie etwa eine Rotation oder ein Logikgatter, zu nehmen und ihn in die Sequenz von Messungen und Korrekturen zu zerlegen, die für die Lattice-Surgery-Hardware erforderlich ist. Die Optimierung beinhaltet das Umordnen dieser Messungen, um den Prozess schneller und effizender zu machen. In ihrer Arbeit bewiesen sie, dass ihr Compiler in der Lage ist, einen Schaltkreis zu nehmen, ihn in Messanweisungen zu übersetzen und dann Regeln anzuwenden, um diese Anweisungen zu verschmelzen und umzuordnen, ohne das Endergebnis zu verändern. Sie verifizierten, dass ihr Compiler korrekt mit „Magic States“ umgeht – speziellen Ressourcen, die erforderlich sind, um bestimmte Arten von Berechnungen durchzuführen – und dass er private Messergebnisse vor der Außenwelt verbirgt, während öffentliche Ergebnisse zugänglich bleiben.

Als sie ihr System an einer Suite von fünfunddreißig kleinen Quantenschaltkreisen testeten, waren die Ergebnisse konkret und messbar. Der verifizierte Compiler übersetzte jeden gültigen Input erfolgreich und lieferte ein Zertifikat, das bestätigte, dass die Übersetzung korrekt war. In Bezug auf die Leistung reduzierten die verifizierten Optimierungstechniken die Anzahl der benötigten logischen Messrunden zur Ausführung dieser Schaltkreise um einen Median von 17,9 Prozent. Für einige spezifische Schaltkreise war die Reduktion sogar höher und erreichte fast 29 Prozent. Diese Reduktion ist signifikant, da in diesen fehlertoleranten Systemen jede Messrunde Zeit beansprucht und Ressourcen verbraucht; das Kürzen der Anzahl der Runden übersetzt sich direkt in einen schnelleren und effizienteren Computer.

Das Team demonstrierte auch, wie man mit approximativen Berechnungen umgeht, die notwendig sind, wenn eine perfekte mathematische Rotation nicht exakt aufgebaut werden kann. Sie entwickelten eine Methode, um den durch diese Approximationen eingeführten Fehler zu begrenzen, wodurch sichergestellt wird, dass das Endergebnis innerhalb eines benutzerdefinierten Limits bleibt. Sie zeigten, dass ihr System die beste mögliche Version eines Schaltkreises aus einer Liste von Kandidaten auswählen kann, wobei es diejenige wählt, die das Fehlerrat begrenzt und gleichzeitig die wenigsten Ressourcen verbraucht. Dieser Auswahlprozess wurde ebenfalls verifiziert, was bedeutet, dass der Computer nicht versehentlich einen Schaltkreis wählen kann, der zu ungenau oder zu langsam ist.

Diese Arbeit stellt einen Wandel dar: weg vom Hoffen, dass ein Compiler funktioniert, hin zum Wissen, dass er funktioniert. Durch den Aufbau eines maschinengeprüften Beweises für die gesamte Compilation-Pipeline haben die Forscher eine große Quelle der Unsicherheit auf dem Weg zur groß angelegten Quantenberechnung beseitigt. Sie haben gezeigt, dass es möglich ist, einen komplexen Algorithmus zu nehmen, ihn in die spezifische Sprache der fehlerkorrigierten Hardware zu übersetzen und ihn für die Geschwindigkeit zu optimieren, während man gleichzeitig eine mathematische Garantie aufrechterhält, dass die Logik intakt bleibt. Das System verarbeitete erfolgreich Schaltkreise mit bis zu 433 Qubits und bewies damit, dass diese Ebene der Verifizierung auch auf substanzielle Probleme skalierbar ist. Während die physische Hardware zum Ausführen dieser Schaltkreise noch in der Entwicklung ist, stellt dieses Software-Fundament sicher, dass die Anweisungen, die an sie gesendet werden, vertrauenswürdig sind, sobald die Maschinen eintreffen.