Test retromorfico dei pass dei compilatori quantistici

Abstract degli autori

I compilatori quantistici svolgono un ruolo fondamentale nel trasformare programmi quantistici di alto livello in circuiti ottimizzati e compatibili con l’hardware. Tuttavia, verificare la correttezza dei pass del compilatore rimane difficile, poiché determinare l’output atteso di circuiti quantistici grandi e fortemente entangled è intrattabile dal punto di vista computazionale. La difficoltà aumenta ulteriormente quando i pass del compilatore modificano strutture di circuiti già complesse, rendendo impraticabile la convalida manuale dei circuiti trasformati. In questo lavoro, conduciamo un’analisi sistematica dei test unitari per i pass dei compilatori quantistici in quattro framework di programmazione quantistica (PennyLane, Qiskit, Cirq e pytket). I nostri risultati indicano che la convalida si basa prevalentemente su asserzioni relative al contenuto e alle metriche dei programmi, e che i circuiti di test sono generalmente piccoli e poco profondi. Sulla base di queste osservazioni, introduciamo una metodologia per la convalida automatizzata dei pass dei compilatori quantistici, basata sul testing retromorfico e sui principi del test di Hadamard. La metodologia analizza un pass del compilatore, un circuito di test e il comportamento atteso del pass per verificare la preservazione semantica e le modifiche strutturali previste. Implementiamo i nostri metodi in un framework, RetroQ, e li applichiamo ai pass del compilatore in PennyLane e Qiskit. La valutazione sperimentale ha riprodotto diversi bug esistenti e ha inoltre individuato difetti non rilevati in precedenza, come una gestione errata dei parametri simbolici, una logica di commutazione scorretta, l’incapacità di riconoscere l’autoaggiuntezza dei gate e arresti anomali in fase di esecuzione. Questi risultati evidenziano la necessità di metodologie di test specifiche per i pass dei compilatori, al fine di migliorare l’affidabilità dello stack software quantistico in evoluzione.