Exact Inference for Quantum Circuits: A Testing Oracle for Quantum Software Stacks

Quantum software stacks (QSSs), which provide quantum circuit transformers and simulators, enable circuit transformations and the execution of circuits on classical computers. Despite their importance, they have not been effectively tested yet, leaving the correctness in question. The main obstacle to testing is the absence of a testing oracle, which checks the semantics-preservation of circuit transformations and the correctness of simulation results. While previous studies have employed differential and metamorphic testing to circumvent the necessity for an oracle, they have detected very few non-crash bugs. In this work, we address this gap by introducing QASMInfer, an exact inference system for quantum circuits, which computes the probability distribution of possible circuit outcomes. By supporting circuits written in OpenQASM, the de facto standard quantum assembly language used by most QSSs, QASMInfer acts as a unified testing oracle for multiple QSSs. Our design of QASMInfer achieves three key goals: (1) support for dynamic circuits, an important class of quantum circuits, (2) efficiency, and (3) reliability. For efficiency, we introduce two optimizations and an efficient matrix representation. For reliability, we prove physical consistency, ensuring that QASMInfer’s inference results adhere to the physical principles of quantum computing. To simplify the proof, we introduce OpenQASMCore, a core language for OpenQASM, and perform exact inference for OpenQASM by desugaring it to OpenQASMCore. Our implementation and proof are fully mechanized in the Coq proof assistant. Testing six real-world QSSs using QASMInfer revealed 31 bugs, including 20 non-crash bugs, demonstrating QASMInfer’s effectiveness as a testing oracle.