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

Quantumcomputers beloven problemen op te lossen die momenteel onmogelijk zijn voor zelfs de krachtigste supercomputers, van het kraken van complexe codes tot het simuleren van nieuwe materialen. Deze machines zijn echter ongelooflijk fragiel. De kleinste verstoring door warmte of trilling kan ervoor zorgen dat hun berekeningen instorten. Om te overleven, bouwen wetenschappers fouttolerante quantumcomputers, die speciale foutcorrigerende codes gebruiken om informatie te beschermen. In plaats van gegevens op te slaan op een enkel, delicaat deeltje, verspreiden deze systemen informatie over vele deeltjes, waarbij ze voortdurend controleren op fouten en deze herstellen. De uitdaging ligt in de vertaling: hoe neem je een algoritme op hoog niveau en zet je dat om in de specifieke, laag-niveau operaties die deze foutgecorrigeerde machines daadwerkelijk kunnen uitvoeren?

De standaardmethode voor veel van deze toekomstige machines maakt gebruik van een techniek genaamd lattice surgery (roosterchirurgie). Stel je een groot stuk stof voor dat het geheugen van de computer representeert. Om een berekening uit te voeren, zet je niet simpelweg een schakelaar om; je stikt stukken van deze stof aan elkaar en trekt ze in precieze patronen uit elkaar. Deze steken zijn geen fysieke draden, maar eerder gezamenlijke metingen van groepen deeltjes. De computer meet hoe deze groepen met elkaar samenhangen, legt het resultaat vast als een eenvoudige bit aan gegevens, en gebruikt die gegevens vervolgens om te beslissen wat de volgende stap is. Dit proces, bekend als Pauli-productmeting, is de fundamentele taal van deze toekomstige machines. Het probleem is dat de softwaretools die worden gebruikt om door mensen ontworije algoritmen naar deze taal te vertalen, nog niet geverifieerd zijn. Als een compiler een fout maakt tijdens de vertaling, kan de hele berekening mislukken, en omdat het proces zo complex is, is het moeilijk te weten waar de fout is opgetreden.

Een team onderzoekers aan de University of California, Los Angeles, heeft deze kloof gedicht door een systeem te creëren dat wiskundig bewijst dat de vertaling correct is. Ze ontwikkelden een nieuwe taal specifiek voor deze op metingen gebaseerde programma's en bouwden een compiler die standaard quantumcircuits naar deze taal vertaalt. Cruciaal is dat ze niet alleen code schreven; ze gebruikten een formeel verificatietool genaamd Lean om een rigoureus wiskundig bewijs te construeren dat hun compiler het gedrag van het oorspronkelijke algoritme behoudt. Dit betekent dat voor elke stap die de compiler neemt, er een certificaat is dat garandeert dat de output exact is wat de input had moeten produceren, tot aan de specifieke waarschijnlijkheden van de resultaten.

De onderzoekers concentreerden zich op twee hoofdtaken: lowering (verlagen) en optimalisatie. Lowering is het proces van het nemen van een standaard quantumgate, zoals een rotatie of een logische gate, en het afbreken ervan in de sequentie van metingen en correcties die vereist zijn door de lattice surgery-hardware. Optimalisatie houdt in dat de metingen worden herschikt om het proces sneller en efficiënter te maken. In hun werk hebben ze bewezen dat hun compiler een circuit kan nemen, het kan vertalen naar metingsinstructies, en vervolgens regels kan toepassen om die instructies te fuseren en te herordenen zonder de uiteindelijke uitkomst te veranderen. Ze hebben geverifieerd dat de compiler correct omgaat met "magic states", speciale hulpbronnen die nodig zijn om bepaalde soorten berekeningen uit te voeren, en dat het de private meetresultaten verborgen houdt voor de buitenwereld terwijl de publieke resultaten toegankelijk blijven.

Toen ze hun systeem testten op een reeks van vijfendertig kleine quantumcircuits, waren de resultaten concreet en meetbaar. De geverifieerde compiler vertaalde elke geldige input succesvol en produceerde een certificaat dat bevestigde dat de vertaling correct was. Wat betreft de prestaties, hebben de geverifieerde optimalisatietechnieken het aantal logische meetrondes dat nodig is om deze circuits uit te voeren, gemiddeld met 17,9 procent verminderd. Voor sommige specifieke circuits was de reductie zelfs hoger, bijna 29 procent. Deze reductie is significant omdat in deze fouttolerante systemen elke meetronde tijd kost en middelen verbruikt; het verminderen van het aantal rondes vertaalt zich direct naar een snellere en efficiëntere computer.

Het team demonstreerde ook hoe men om moet gaan met benaderende berekeningen, die noodzakelijk zijn wanneer een perfecte wiskundige rotatie niet exact gebouwd kan worden. Ze creëerden een methode om de fout te begrenzen die door deze benaderingen wordt geïntroduceerd, met de garantie dat het eindresultaat binnen een door de gebruiker gedefinieerde limiet blijft. Ze toonden aan dat hun systeem de beste mogelijke versie van een circuit uit een lijst met kandidaten kan selecteren, waarbij de versie wordt gekozen die aan de foutlimiet voldoet en tegelijkert in de minste middelen voorziet. Dit selectieproces werd ook geverifieerd, wat betekent dat de computer niet per ongeluk een circuit kan kiezen dat te onnauwkeurig of te traag is.

Dit werk vertegenwoordigt een verschuiving van hopen dat een compiler werkt naar weten dat hij werkt. Door een door een machine gecontroleerd bewijs te bouwen voor de gehele compilatiepijplijn, hebben de onderzoekers een grote bron van onzekerheid in de weg naar grootschalige quantumcomputing weggenomen. Ze hebben aangetoond dat het mogelijk is om een complex algoritme te nemen, te vertalen naar de specifieke taal van foutgecorrigeerde hardware, en dit te optimaliseren voor snelheid, terwijl er een wiskundige garantie wordt gehandhaafd dat de logica intact blijft. Het systeem verwerkte succesvol circuits met tot wel 433 qubits, wat bewijst dat dit niveau van verificatie kan schalen naar aanzienlijke problemen. Hoewel de fysieke hardware om deze circuits uit te voeren nog in ontwikkeling is, zorgt dit softwarematige fundament ervoor dat de instructies die naar hen worden gestuurd, betrouwbaar zijn wanneer de machines arriveren.