Formal verification of optical quantum flip gate

Abstract

Quantum computers are promising to efficiently solve hard computational problems, especially NP problems. In this paper, we propose to tackle the formal verification of quantum circuits using theorem proving. In particular, we focus on the verification of quantum computing based on coherent light, which is typically light produced by laser sources. We formally verify the behavior of the quantum flip gate in HOL Light: we prove that it can flip a zero-quantum-bit to a one-quantum-bit and vice versa. To this aim, we model two optical devices: the beam splitter and the phase conjugating mirror and prove relevant properties about them. Then by cascading the two elements and utilizing these properties, the complete model of the flip gate is formally verified. This requires the formalization of some fundamental mathematics like exponentiation of linear transformations. © 2014 Springer International Publishing.