Search papers, labs, and topics across Lattice.
This paper addresses the gap in quantum programming research by incorporating noise-aware semantics that reflect the realities of executing programs on actual quantum hardware. By developing a noise-aware quantum Hoare logic, the authors enable bounded verification and automatic synthesis of quantum programs tailored to specific hardware error models. The key result reveals that the synthesis tool can identify optimal subroutines for various noise models, highlighting the necessity of classical probabilistic branching for achieving optimality in quantum programming.
Quantum programs can be optimized for real-world noise, revealing that classical probabilistic branching is essential for achieving optimal performance.
While most research on quantum programming considers an idealized, noise-free semantics for quantum programs, we reason about quantum programs that are executed on real, noisy hardware. We consider the error models published by quantum hardware vendors to give a hardware-dependent semantics to quantum programs. This work presents a comprehensive study of noise-aware quantum programming, ranging from logical foundations to automated verification and synthesis. We develop a noise-aware quantum Hoare logic, and use it to derive algorithmic methods for the bounded verification of quantum programs on specific hardware, and for the automatic synthesis of noise-optimal loop-free quantum programs. In this way, we synthesize hardware-dependent subroutines that commonly occur in quantum algorithms, such as parity checks, quantum state preparation, and quantum state discrimination. We evaluate our method on the hardware specifications provided by the IBM Qiskit toolkit. Besides finding different optimal subroutines for different noise models, our synthesis tool also shows that classical probabilistic branching is needed for optimality in quantum programming.
