Stabilizer circuit verification

TL;DR

This paper introduces efficient classical algorithms for comprehensive verification of stabilizer circuits in quantum computing, enabling full characterization, equivalence checking, and logical action analysis, which enhances correctness assurance in quantum circuit design.

Contribution

The paper presents novel algorithms for complete stabilization circuit characterization, equivalence verification, and logical action analysis, advancing the tools for quantum circuit correctness verification.

Findings

Algorithms efficiently verify stabilizer circuit equivalence.

Methods characterize logical actions on encoded inputs.

Application to correctness proofs in quantum error correction.

Abstract

The ubiquity of stabilizer circuits in the design and operation of quantum computers makes techniques to verify their correctness essential. The simulation of stabilizer circuits, which aims to replicate their behavior using a classical computer, is known to be efficient and provides a means of testing correctness. However, simulation is limited in its ability to examine the exponentially large space of possible measurement outcomes. We propose a comprehensive set of efficient classical algorithms to fully characterize and exhaustively verify stabilizer circuits with Pauli unitaries conditioned on parities of measurements. We introduce, as a practical characterization, a general form for such circuits and provide an algorithm to find a general form of any stabilizer circuit. We then provide an algorithm for checking the equivalence of stabilizer circuits. When circuits are not equivalent our algorithm suggests modifications for reconciliation. Next, we provide an algorithm that characterizes the logical action of a (physical) stabilizer circuit on an encoded input. All of our algorithms provide relations of measurement outcomes among corresponding circuit representations. Finally, we provide an analytic description of the logical action induced by measuring a stabilizer group, with application in correctness proofs of code-deformation protocols including lattice surgery and code switching.