Verification of Quantum Circuits through Discrete-Time Barrier Certificates

TL;DR

This paper introduces a novel method for verifying quantum circuits by extending barrier certificates with Hermitian Sum of Squares optimization, leveraging dynamical systems verification techniques.

Contribution

It proposes k-inductive barrier certificates for quantum circuits and demonstrates their computation and application for property verification.

Findings

Successfully verified properties of various quantum circuits

Extended barrier certificates to complex variables for quantum systems

Demonstrated effectiveness of Hermitian Sum of Squares in quantum verification

Abstract

Current methods for verifying quantum computers are predominately based on interactive or automatic theorem provers. Considering that quantum computers are dynamical in nature, this paper employs and extends the concepts from the verification of dynamical systems to verify properties of quantum circuits. Our main contribution is to propose k-inductive barrier certificates over complex variables and show how to compute them using Hermitian Sum of Squares optimization. We apply this new technique to verify properties of different quantum circuits.