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

I computer quantistici promettono di risolvere problemi che sono attualmente impossibili anche per i supercomputer più potenti, dalla decrittazione di codici complessi alla simulazione di nuovi materiali. Tuttavia, queste macchine sono incredibilmente fragili. La minima perturbazione causata dal calore o dalle vibrazioni può far collassare i loro calcoli. Per sopravvivere, gli scienziati stanno costruendo computer quantistici tolleranti ai guasti, che utilizzano speciali codici di correzione degli errori per proteggere l'informazione. Invece di memorizzare i dati su una singola particella delicata, questi sistemi distribuiscono l'informazione su molte particelle, controllando costantemente gli errori e correggendoli. La sfida risiede nella traduzione: come si prende un algoritmo di alto livello e lo si converte nelle specifiche operazioni di basso livello che queste macchine con correzione degli errori possono effettivamente eseguire?

Il metodo standard per molte di queste future macchine prevede una tecnica chiamata chirurgia del reticolo (lattice surgery). Immaginate un grande foglio di tessuto che rappresenta la memoria del computer. Per eseguire un calcolo, non basta premere un interruttore; bisogna cucire insieme pezzi di questo tessuto e separarli seguendo schemi precisi. Questi punti non sono fili fisici, ma piuttosto misurazioni congiunte di gruppi di particelle. Il computer misura come questi gruppi si relazionano tra loro, registra il risultato come un semplice bit di dati e poi usa quel dato per decidere cosa fare dopo. Questo processo, noto come misurazione del prodotto di Pauli, è il linguaggio fondamentale di queste future macchine. Il problema è che gli strumenti software utilizzati per tradurre gli algoritmi progettati dall'uomo in questo linguaggio non sono stati verificati. Se un compilatore commette un errore durante la traduzione, l'intero calcolo potrebbe fallire e, poiché il processo è così complesso, è difficile capire dove sia avvenuto l'errore.

Un team di ricercatori dell'Università della California, Los Angeles, ha affrontato questa lacuna creando un sistema che dimostra matematicamente che la traduzione è corretta. Hanno sviluppato un nuovo linguaggio specificamente per questi programmi basati sulla misurazione e costruito un compilatore che traduce i circuiti quantistici standard in questo linguaggio. Fondamentalmente, non si sono limitati a scrivere codice; hanno utilizzato uno strumento di verifica formale chiamato Lean per costruire una rigorosa prova matematica che il loro compilatore preservi il comportamento dell'algoritmo originale. Ciò significa che per ogni passaggio compiuto dal compilatore, esiste un certificato che garantisce che l'output sia esattamente ciò che l'input doveva produrre, fino alle specifiche probabilità dei risultati.

I ricercatori si sono concentrati su due compiti principali: il "lowering" (abbassamento del livello) e l'ottimizzazione. Il lowering è il processo di presa di un gate quantistico standard, come una rotazione o un gate logico, e della sua scomposizione nella sequenza di misurazioni e correzioni richieste dall'hardware della chirurgia del reticolo. L'ottimizzazione consiste nel riorganizzare queste misurazioni per rendere il processo più veloce ed efficiente. Nel loro lavoro, hanno dimostrato che il loro compilatore può prendere un circuito, tradurlo in istruzioni di misurazione e poi applicare regole per fondere e riordinare tali istruzioni senza cambiare il risultato finale. Hanno verificato che il compilatore gestisce correttamente gli "stati magici" (magic states), ovvero risorse speciali necessarie per eseguire certi tipi di calcoli, e che mantiene nascosti al mondo esterno i risultati delle misurazioni private, garantendo al contempo che i risultati pubblici rimangano accessibili.

Quando hanno testato il loro sistema su una suite di trentacinque piccoli circuiti quantistici, i risultati sono stati concreti e misurabili. Il compilatore verificato ha tradotto con successo ogni input valido, producendo un certificato che confermava la correttezza della traduzione. In termini di prestazioni, le tecniche di ottimizzazione verificate hanno ridotto il numero di round di misurazione logica necessari per eseguire questi circuiti di una mediana del 17,9 percento. Per alcuni circuiti specifici, la riduzione è stata ancora più alta, raggiungendo quasi il 29 percento. Questa riduzione è significativa perché in questi sistemi tolleranti ai guasti, ogni round di misurazione richiede tempo e consuma risorse; tagliare il numero di round si traduce direttamente in un computer più veloce ed efficiente.

Il team ha inoltre dimostrato come gestire i calcoli approssimativi, necessari quando non è possibile costruire esattamente una rotazione matematica perfetta. Hanno creato un metodo per delimitare l'errore introdotto da queste approssimazioni, assicurando che il risultato finale rimanga entro un limite definito dall'utente. Hanno dimostrato che il loro sistema può selezionare la migliore versione possibile di un circuito da una lista di candidati, scegliendo quello che soddisfa il limite di errore utilizzando al contempo le meno risorse possibili. Anche questo processo di selezione è stato verificato, il che significa che il computer non potrebbe accidentalmente scegliere un circuito troppo impreciso o troppo lento.

Questo lavoro rappresenta un passaggio dal sperare che un compilatore funzioni al sapere che funziona. Costruendo una prova verificata dalla macchina per l'intero processo di compilazione, i ricercatori hanno rimosso una grande fonte di incertezza nel percorso verso il calcolo quantistico su larga scala. Hanno dimostrato che è possibile prendere un algoritmo complesso, tradurlo nel linguaggio specifico dell'hardware con correzione degli errori e ottimizzarlo per la velocità, il tutto mantenendo una garanzia matematica che la logica rimanga intatta. Il sistema ha gestito con successo circuiti con fino a 433 qubit, provando che questo livello di verifica può scalare verso problemi sostanziali. Sebbene l'hardware fisico per eseguire questi circuiti sia ancora in fase di sviluppo, questa base software assicura che, quando le macchine arriveranno, le istruzioni inviate a esse saranno affidabili.