QEDIA: verifica dei programmi quantistici in Lean

Abstract degli autori

I programmi quantistici pratici alternano computazione quantistica e classica: i dati classici determinano le operazioni quantistiche eseguite, mentre gli esiti delle misurazioni determinano la computazione classica che segue. La verifica formale di questi programmi in un assistente di dimostrazione richiede di formalizzare una logica di programma che gestisca coerentemente questa interazione a ogni livello: dalla matematica della meccanica quantistica alla sintassi e alla semantica dei programmi, fino alle specifiche e alle regole di dimostrazione. Queste formalizzazioni, insieme alle dimostrazioni sui programmi che vi si basano, richiedono in genere un notevole lavoro manuale. Presentiamo QEDIA, un framework per verificare in Lean 4 programmi quantistici con variabili classiche. Alla sua base c’è una libreria aperta che formalizza la logica di Hoare quantistica QHL+ a tutti questi livelli e dimostra la solidità della logica sia per la correttezza parziale sia per quella totale. Costruiamo la libreria e le dimostrazioni dei programmi, sotto supervisione umana, utilizzando un agente dimostratore basato su un LLM, il cui nucleo di uso generale estendiamo per la verifica dei programmi quantistici. Presentiamo QEDIA con programmi verificati che includono la trasformata quantistica di Fourier, la stima di fase, circuiti a ripetizione fino al successo e la simulazione hamiltoniana.