Parameterized Verification of Quantum Circuits (Technical Report)

TL;DR

The paper tackles automated, parameterized verification of quantum circuits by introducing synchronized weighted tree automata (SWTAs) to compactly represent infinite families of quantum states and weighted tree transducers (WTTs) to model gate semantics. It develops a composition framework to build transducers for complex and parameterized circuits, and provides decision procedures for functional equivalence and inclusion, enabling relational verification. The AutoQ-Para tool demonstrates practical effectiveness on diverse quantum programs (BV, arithmetic adders, QECC syndrome extraction, Grover iterations, and Hamiltonian simulation) with runtimes from milliseconds to seconds. This work advances scalable, fully automatic verification for size-parameterized quantum circuits, with formal guarantees grounded in automata theory and linear-algebraic reasoning.

Abstract

We present the first fully automatic framework for verifying relational properties of parameterized quantum programs, i.e., a program that, given an input size, generates a corresponding quantum circuit. We focus on verifying input-output correctness as well as equivalence. At the core of our approach is a new automata model, synchronized weighted tree automata (SWTAs), which compactly and precisely captures the infinite families of quantum states produced by parameterized programs. We introduce a class of transducers to model quantum gate semantics and develop composition algorithms for constructing transducers of parameterized circuits. Verification is reduced to functional inclusion or equivalence checking between SWTAs, for which we provide decision procedures. Our implementation demonstrates both the expressiveness and practical efficiency of the framework by verifying a diverse set of representative parameterized quantum programs with verification times ranging from milliseconds to seconds.

Figures (17)

• Figure 1: A quantum state involving three qubits. We provide the vector, Dirac, and tree-based representations. The tree spans all basis states, with the corresponding amplitudes shown as leaf labels. For instance, the left-most path represents $\ket{000}$ with amplitude ${{ \frac{1}{\sqrt{2}}}}$.
• Figure 2: A plain tree automaton that characterizes the set of all $3$-qubit basis states. In the figure, transitions are represened by hyperedges (represented by grey arcs) with dashed arrows going to the left-hand child and solid arrows going to the right-hand child.
• Figure 3: An LSTA. (a) A picture of the automaton. (b) The set of transitions. (c) The two trees accepted by the automaton.
• Figure 4: An LSTA recognizing the set of all basis states.
• Figure 5: (\ref{['fig:weight-swta']}) An SWTA recognizing the set of all quantum states with uniform superposition; $\ell$ is a leaf state. (\ref{['fig:weight-tree1']}) and (\ref{['fig:weight-tree2']}) show the trees with one qubit resp. two qubits in uniform superposition.

Theorems & Definitions (16)

• theorem 1
• theorem 2
• theorem 3
• theorem 4
• corollary 1
• theorem 5
• theorem 6
• theorem 7
• theorem 8
• theorem 9