An Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits

1. Introduction

Quantum computing holds the potential to solve complex problems that classical computers struggle to address. Since its inception, quantum algorithms have showcased capabilities beyond classical limits, exemplified by Shor’s factoring algorithm and Grover’s search algorithm—both of which can solve important computational problems provably faster than classical methods.^16,20 For many years, the lack of hardware posed a barrier to implementing these algorithms, but recent advancements—including Google’s 2019 demonstration of a quantum computational advantage on a programmable superconducting processor—have marked significant milestones, though their results remain the subject of ongoing debate.³

As quantum computing moves toward practical applications, programming languages and systems for quantum computers are under active development to meet growing demands. Efficient algorithms have begun to emerge in fields such as optimization, machine learning (ML), and quantum chemistry, creating a pressing need for reliable verification methods to ensure circuit correctness in these applications.¹⁹ Verifying quantum circuits, however, presents unique challenges due to the exponential size of the computational space and the probabilistic nature of quantum operations. Traditional verification techniques are often unsuitable for quantum circuits, especially as they scale.

Currently, available automated analysis tools are limited in scalability, and many are inflexible in checking user-specified properties,^2,7,12 or imprecise and unable to catch bugs.²⁵ Scalable and flexible automated analysis tools for quantum circuits are indeed missing. In this paper, we introduce a novel approach to quantum circuit verification based on automata, a technique well-established in classical verification but largely unexplored in quantum contexts.⁵

In particular, we propose a new paradigm for analyzing and finding bugs in quantum circuits. In our approach, the problem is given by a Hoare triple {P}C{S}, where C is a quantum circuit and P and S are sets of quantum states. The verification question that we address is whether the set of output quantum states obtained by running C on all states from P is equal to (or included in) the set S.

We create a framework for analyzing the considered class of properties based on (finite) tree automata (TAs).¹³ Languages of TAs are sets of trees; in our case, we consider TAs whose languages contain perfect binary trees with the height being the number of qubits in the circuit. Each branch (a path from a root to a leaf) in such a tree corresponds to one computational basis state (for example, |0000⟩ or |0101⟩ for a four-qubit circuit), and the corresponding leaf represents the complex amplitude of the state (we use an algebraic encoding of complex numbers by tuples of integers to have a precise representation and avoid possible inaccuracies when dealing with floating-point numbers; this encoding is sufficient for a wide variety of quantum gates, including the Clifford+T universal set for quantum computing). Sets of such trees can be, in many cases, encoded compactly using TAs (for example, storing the output of Bernstein-Vazirani’s algorithm⁴ over n qubits requires a vector of 2n complex numbers), but can be encoded by a linear-sized TA. For each quantum gate, we construct a transformation that converts the input states TA to a TA representing the gate’s output states, in a similar way as classical program transformations are represented in.¹⁴

Testing equivalence and inclusion between the TA representing the set of outputs of a circuit and the postcondition S (from {P}C{S}) can then be done by standard TA language inclusion/equivalence testing algorithms.^13,18 If the test fails, the framework generates a witness for diagnosis.

One application of our framework is as a quick underapproximation of a quantum circuit non-equivalence test. Our approach can switch to a lightweight specification when equivalence checkers fail due to insufficient resources and still find bugs in the design. Quantum circuit (non-)equivalence testing is an essential part of the quantum computing toolkit. Its prominent use is in verifying results of circuit optimization, which is a necessary part of quantum circuit compilation to achieve the expected fidelity of quantum algorithms running on real-world quantum computers, which are heavily affected by noise and decoherence. Already in the world of classical programs, optimizer bugs are being found on a regular basis in compilers used daily by tens of thousands of programmers. In the world of quantum, optimization is much harder than in the classical setting, with many opportunities to introduce subtle and hard-to-discover bugs into the optimized circuits. It is therefore essential to be able to check that an output of an optimizer is functionally equivalent to its input.

Testing quantum circuit (non-)equivalence is, however, a challenging task (QMA-complete).¹⁷ Due to its complexity, approaches that can quickly establish circuit non-equivalence are highly desirable to be used, for example, as a preliminary check before a more heavyweight procedure (see Burgholzer and Wille⁷ or Chen et al.⁸) is used. One currently employed fast non-equivalence check is to use random stimuli generation.⁶ Finding subtle bugs by random testing is, however, challenging—with no guarantees due to the immense (in general uncountable) underlying state space.

Our approach can be used as follows: We start with a TA encoding the set of possible input states (created by the user or automatically) and run our analysis of the circuit over it, obtaining a TA A representing the set of all outputs. Then, we take the optimized circuit, run it over the same TA with inputs and obtain a TA A‘. Finally, we check whether L(A)=L(A‘). If the equality does not hold, we can conclude that the circuits are not functionally equivalent (if the equality holds, there can, however, still be some bug that does not manifest in the set of output states).

We implemented our technique in a prototype called AutoQ and evaluated it over a wide range of quantum circuits, including some prominent quantum algorithms, randomly generated circuits, reversible circuits from RevLib,²³ and benchmarks from the tool Feynman.² The results show that our approach is quite scalable. We did not find any tool with the same functionality with ours and hence pick the closest state-of-the art tools—a circuit simulator SliQSim²¹ and circuit equivalence checkers Feynman² (based on path-sum), Qcec⁷ (combining ZX-calculus, decision diagrams, and random stimuli generation), and SliQEC²²—as the baseline tools to compare with. In the first experiments, we evaluated AutoQ’s capability in verification against pre- and post-conditions. We managed to verify the functional correctness (with regard to one input state) of a circuit implementing Grover’s search algorithm with 40 qubits and 141,527 gates. We then evaluated AutoQ on circuits with injected bugs. The results confirm our claim—AutoQ was able to find injected bugs in various huge-scale circuits, including one with 320 qubits and 1,758 gates, which other tools failed to find.

In addition to the practical utility, our work also bridges the gap between quantum and classical verification, particularly automata-based approaches such as regular model checking.⁵ As far as we know, our approach to the verification of quantum circuits is the first one based on automata. The enabling techniques and concepts involved in this work are, for example, the use of TAs to represent sets of quantum states and express the pre- and post-conditions, the compactness of the TA structure enabling efficient gate operations, and our TA transformation algorithms enabling the execution of quantum gates over TAs. We believe the connection of automata theory with the quantum world we establish can start new fruitful collaborations between the two rich fields.

Overview.

We use a concrete example to demonstrate how to use our approach. Assume we want to design a circuit constructing the Bell state, that is, a 2-qubit circuit converting a basis state |00⟩ to a maximally entangled state 12(|00⟩+|11⟩). We first prepare TAs corresponding to the precondition (Figure 1a) and postcondition (Figure 1b). Both TAs use q as the root state and accept only one tree. One can see the correspondence between quantum states and TAs by traversing their structure. The precise definition will be given in Sections 2 and 3. Our approach will then use the transformers from Sections 4 to 6 to construct a TA A recognizing the quantum states after executing the EPR circuit (Figure 1c) from the precondition TA (Figure 1a). We will then use TA language inclusion/equivalence tool VATA¹⁸ to check A against the postcondition TA. If the circuit is buggy, our approach will return a witness quantum state that is reachable from the precondition but not allowed by the postcondition. From our experience of preparing benchmark examples, in many cases, this approach helps us finding bugs in incorrect designs.

2. Preliminaries

By default, we work with vectors and matrices over complex numbers C. In particular, we use Cm×n to denote the set of all m×n complex matrices. Given a k×ℓ matrix (axy), its transpose is the ℓ×k matrix (axy)T=(ayx) obtained by flipping (axy) over its diagonal. A 1×k matrix is called a row vector and a k×1 matrix is called a column vector. To save vertical space, we often write a column vector v using its row transpose vT. We use I to denote the identity matrix of any dimension (which should be clear from the context). The conjugate of a complex number a+bi is the complex number a–bi, and the conjugate transpose of a matrix A=(axy) is the matrix A†=(cyx) where cyx is the conjugate of ayx. For example:

The inverse of a matrix A is denoted as A–1. A square matrix A is unitary if A†=A–1. The Kronecker product of A=(axy)∈Ck×ℓ and B∈Cm×n is the km×ℓn matrix A⊗B=(axyB); For instance,

2.2 Tree automata.

Binary trees.

We use a ranked alphabet Σ with binary symbols f, g, … and constant symbols c1, c2, …. A binary tree is a ground term over Σ. For instance, T=f(f(c1,c2),g(f(c2,c3),c1)), shown below, represents a binary tree. The set of nodes of a binary tree T, denoted as NT, is defined inductively as a set of words over {0,1} such that for every constant symbol c, we define Nc={ϵ}, and for every binary symbol f, we define Nf(T0,T1)={ϵ}∪{a.w|a∈{0,1}∧w∈NTa}, where ϵ is the empty word and ‘.’ is concatenation. Each binary tree T is associated with a labeling function LT:{0,1}*→Σ, which maps a node in T to its label in Σ

Tree automata.

We focus on tree automata on binary trees and refer the interested reader to Comon¹³ for a general definition. A (nondeterministic finite) tree automaton (TA) is a tuple A=〈Q,Σ,Δ,R〉 where Q is a finite set of states, Σ is a ranked alphabet, R⊆Q is the set of root states, and Δ=Δint∪Δleaf is a set of tree transitions consisting of the set Δint of internal transitions of the form q→f(q0,q1) (for a binary symbol f) and the set Δleaf of leaf transitions of the form q→c() (for a constant symbol c), for q,q0,q1∈Q. We can conveniently describe TAs by providing only the set of root states R and the set of transitions Δ. The alphabet and states are implicitly defined as those that appear in Δ. For example, Δ={q→x1(q1,q0),q→x1(q0,q1),q0→0(),q1→1()} implies that Σ={x1,0,1} and Q={q,q0,q1}.

Run and language.

A run of A on a tree T is another tree ρ labeled with Q such that (i) T and ρ have the same set of nodes, that is, NT=Nρ; (ii) for all leaf nodes u∈NT, we have Lρ(u)→LT(u)()∈Δ; and (iii) for all non-leaf nodes v∈NT, we have the transitions Lρ(u)→LT(u)(Lρ(0.u),Lρ(1.u))∈Δ. The run ρ is accepting if Lρ(ϵ)∈R. The language L(A) of A is the set of trees accepted by A, that is, L(A)={T|there exists an accepting run ofAoverT}.

Example 1 (Accepted tree).

Assume a TAA3baswithqas its single root state and the following transitions:q→x1(q01,q11)q11→x2(q02,q12)q12→x3(q0,q1)q0→0()q→x1(q11,q01)q11→x2(q12,q02)q12→x3(q1,q0)q1→1()q01→x2(q02,q02)q02→x3(q0,q0)

Among others, A 3 bas accepts the above tree (Ex. 1 figure, left) with the run (Ex. 1 figure, right). Observe that all tree nodes satisfy the requirement of a valid run. For example, the node 111 corresponds to the transition q 0 → 0 ( ) , 01 to q 0 2 → x 3 ( q 0 , q 0 ) , and ϵ to q → x 1 ( q 1 1 , q 0 1 ) , and so on.

In A 3 bas , we use states named q 0 n to denote only subtrees with all zeros ( 0 ) in leaves that can be generated from here, and states named q 1 n to denote only subtrees with a single 1 in the leaves that can be generated from it. Intuitively, the TA accepts all trees of the height 3 with exactly one 1 leaf and all other leaves 0 (in our encoding of quantum states, this might correspond to saying that A 3 bas encodes an arbitrary computational basis state of a three-qubit system).

3. Encoding Sets of Quantum States with Tree Automata

Observe that we can use (perfect) binary trees to encode functions {0,1}n→Z5, for example, the function representation of quantum states. For instance, the tree given by the term

encodes the function T where T(000)=1 and T(i)=0 for all i∈{0,1}3{000}. Since TAs can concisely represent sets of binary trees, they can also encode sets of quantum states.

Formally a TA A recognizing a set of quantum states is a tuple 〈Q,Σ,Δ,R〉, whose alphabet Σ can be partitioned into two classes of symbols: binary symbols x1,…,xn and a finite set of leaf symbols Σc⊆Z5 representing all possible amplitudes of quantum states in terms of computational bases. By slightly abusing the notation, for a perfect binary tree T∈L(A), we also use T to denote the function {0,1}n→Z5 that maps a computational basis to the corresponding amplitude of T’s quantum state. The two meanings of T are used interchangeably throughout the paper.

4. Quantum Gates Encoding

With TAs used to concisely represent sets of quantum states, the next task is to capture the effects of applying quantum gates on this representation. When quantum states are represented as vectors, gates are represented as matrices and gate operations are matrix multiplications. When states are represented as binary trees, we need a new representation for quantum gates and their operations. Inspired by the work of Tsai et al.,²¹ we introduce symbolic update formulae, which describe how a gate transforms a tree representing a quantum state. Later, we will lift the tree update operation to a set of trees encoded in a TA.

We use the algebraic representation of quantum states from Equation 5 also for their symbolic handling. For instance, consider a system with qubits x1, x2 and its state

for c00,c01,c10,c11∈Z5, four complex numbers represented in the algebraic way. The result of applying the X gate (the quantum version of the NOT gate) on qubit x1 (cf. Figure 2a)—denoted as X1—is (c10,c11,c00,c01)T (cf. Equation 4). Intuitively, we observe that the effect of the gate is a permutation of the computational basis states that swaps the amplitudes of states where the x1’s value is 1 with states where the x1’s value is 0 (and the values of qubits other than x1 stay the same). Concretely, it swaps the amplitudes of the pairs (|00⟩, |10⟩) and (|01⟩, |11⟩) to obtain the quantum state

Instead of executing the quantum gate by performing a matrix-vector multiplication, we will capture its semantics symbolically by directly manipulating the tree function T:{0,1}n→Z5. For this, we will use the following operators on T, parameterized by a qubit xt (t for “target”):

In the previous, bt¯ denotes the complement of the bit bt (that is, 0¯=1 and 1¯=0). Intuitively, Pxt(T) and Pxt¯(T) fix the value of qubit xt to be 1 and 0 respectively (in the tree representation of the function, Pxt(T) corresponds to removing the 0-subtree of every xt node and substituting it with a copy of the 1-subtree of the node; vice versa for Pxt¯(T)). On the other hand, Rxt(T) returns a function that maps any computational basis state with xt=1 to the original value in T and the other basis states to 0 (or the other way around for Rxt¯(T)).

Equipped with the operators, we can now proceed to express the semantics of X1 symbolically. Let us first look at the first two summands on the right-hand side of Equation 8: T0=c10·|00⟩+c11·|01⟩. These summands can be obtained by manipulating the input function T in the following way:

When we view T as a tree, the operation Px1(T) essentially copies the right subtree of every x1-node to its left subtree, and Rx1¯(Px1(T)) makes all leaves in every right subtree of Px1(T)’s x1-node zero. This would give us

On the other hand, the last two summands in the right-hand side of Equation 8, that is, T1=c00·|10⟩+c01·|11⟩, could be obtained by manipulating T as follows:

The tree view of Rx1(Px1¯(T)) is symmetric to Rx1¯(Px1(T)), which would give us the following state:

Finally, by summing T0 and T1, we obtain Equation 8: T0+T1=c10·|00⟩+c11·|01⟩+c00·|10⟩+c01·|11⟩. That is, the semantics of the X gate could be expressed using the following symbolic formula:

Observe that the sum effectively swaps the left and right subtrees of each x1-node.

For multi-qubit gates, the update formulae get more complicated, since they involve more than one qubit. Consider, for example, the “controlled-NOT” gate CNOTtc (see Figure 2c for the graphical representation and Figure 2d for its semantics). The CNOTtc gate uses xt and xc as the target and control qubit respectively. Intuitively, it “flips” the target qubit’s value when the control qubit’s value is 1 and keeps the original value if it is 0. Similarly, as for the X1 gate, we can deduce a symbolic formula for the update done by a CNOTtc gate:

The sum consists of the following two summands:

• The summand Rxc¯(T) says that when the control qubit is 0, the values of all qubits stay the same.

• The summand Rxc(Rxt¯(Pxt(T))+Rxt(Pxt¯(T))) handles the case when xc is 1. In such a case, we apply the X gate on xt (observe that the inner term is the update formula of Xt in Equation 13).

One can obtain symbolic update formulae for other quantum gates in a similar way. In Table 1 we give the formulae for the gates supported by our framework.

For a gate G, we use the superscripts c and c‘ to denote that xc and xc‘ are the gate’s control qubits (if they exist) and the subscript t to denote that xt is the target bit (for example, Gtc,c‘). We note that the supported set of gates is much larger than is required to achieve (approximate) universal quantum computation (for which it suffices to have, for example, (i) Clifford gates (H, S, and CNOT) and T or (ii) Toffoli and H.

A note on expressivity.

The expressivity of our framework is affected by the following factors:

1. Algebraic complex number representation (a,b,c,d,k): This representation can arbitrarily closely approximate any complex number: when b=d=0, the quintuple (a,0,c,0,k) represents the number 12k(a+ic) Then any complex number can be approximated arbitrarily closely by picking suitable a, c, and k.

2. Supported quantum gates: We covered all standard quantum gates supported in modern quantum computers except parameterized rotation gate. From Solovay-Kitaev theorem,¹⁵ gates performing rotations by π2k can be approximated with an error rate ϵ with -many gates that we support.

3. Tree automata structure: We use non-deterministic transitions of tree automata to represent a set of trees compactly. Nevertheless, we can currently encode only a finite set of states. Hence, we cannot express, for example, all quantum states where the amplitudes of |10⟩ and |01⟩ are the same. In Chen et al.,¹⁰ we extend the work to allow using variables as leave symbols and this set becomes expressible.

In the next two sections, we discuss how to lift the tree update operation to a set of trees encoded in a TA. Our framework allows different instantiations. We will introduce two in this paper, namely the (i) permutation-based (Section 5) and (ii) composition-based (Section 6) approach. The former is simple, efficient, and works for all but the Ht, Rx(π2)t, and Ry(π2)t gates from 1 (those whose effect is a permutation of tree leaves, that is, for gates whose matrix contains only one non-zero element in each row, potentially with a constant scaling of amplitude), while the latter supports all gates in the table but is less efficient. The two approaches are compatible with each other, so one can, for example, choose to use the permutation-based approach by default and for unsupported gates fall back on the composition-based approach.

5. Permutation-Based Encoding of Quantum Gates

Let us first look at the simplest gate Xt(T)=Rxt(Pxt¯(T))+Rxt¯(Pxt(T)). Recall that in Section 4, we showed that the formula essentially swaps the left and right subtrees of each xt-labeled node. For a TA A, we can capture the effect of applying Xt to all states in L(A) by swapping the left and the right children of all xt-labeled transitions q→xt(q0,q1), that is, update them to q→xt(q1,q0). We use Xt(A) to denote the TA constructed following this procedure.

The update formulae of gates Zt, St, and Tt are all in the form a0·Rxt¯(T)+a1·Rxt(T) for a0,a1∈C. Intuitively, the formulae scale the left and right subtrees of T with scalars a0 and a1, respectively. The construction of the TA representing the result of the operation (given in Algorithm 1) can be done by (1) making one primed copy A1 of A (that is, a copy where every state q is renamed to q‘, with properly modified transitions and root states) whose leaf labels are multiplied with a1 (Lines 3–5); (2) multiplying all leaf labels of A with a0 (Lines 6–7); and (3) updating all xt-labeled transitions s→xt(p,q) to s→xt(p,q‘), that is, for the right child, jump to the primed version (Line 7). The case of Yt is similar, but we need both constant scaling (Lines 1–7) and swapping (Lines 10–12) (the left-hand side and right-hand side scalars being ω2 and –ω2, respectively).

The cases of multi-qubit gates CNOTtc, CZtc, and Toffolitc,c‘ can be handled when t is the lowest of the three qubits, that is, c<t∧c‘<t. We can assume w.l.o.g. that c<c‘. Output of these gates can be constructed recursively following Algorithm 2. Let us look at the corresponding update formulae:

We first construct the TA of the inner term, the shaded area, which are TAs for Xt, Zt, or CNOTtc‘. We call it the primed version here (cf. A1‘ at Line 4). We then update all xc-labeled transitions s→xc(p,q) to s→xc(p,q‘), that is, jump to the primed version in the right subtree.

6. Composition-Based Encoding of Quantum Gates

In the composition-based approach, we develop TA operations for all operations in the symbolic update formulae from Table 1—projection Pxk(T), restriction Rxk(T), multiplication, and binary operation ±—and then compose them to get the desired gate semantics. The update formulae in Table1 are always in the form of term1±term2. For example, for the Xt gate, term1=Rxt(Pxt¯(T)) and term2=Rxt¯(Pxt(T)). Our idea is to first construct TAs Aterm1 and Aterm2, recognizing quantum states of term1 and term2, and then combine them using binary operation ± to produce a TA recognizing the quantum states of term1±term2. The TAs Aterm1, Aterm2 would be constructed using TA versions of basic operations. We refer the reader to the original paper¹¹ for further details of the concrete TA constructions.

7. Experimental Evaluation

We implemented the proposed TA-based algorithm as a prototype tool named AutoQ in C++. We provide two settings: Hybrid, which uses the permutation-based approach (Section 5) to handle supported gates and switches to the composition-based approach for the other gates, and Composition, which handles all gates using the composition-based approach (Section 6). Further details are available in the original paper.¹¹ We evaluated AutoQ in two use cases.

8. Conclusion

We presented a foundational framework for automata-based verification of quantum circuits, demonstrating its effectiveness through empirical studies. We believe that applying automata to quantum verification establishes a valuable bridge between quantum and classical verification approaches, with the potential to adapt many classical verification techniques to quantum settings, for instance, by replacing constant tree leaf values with symbolic variables¹⁰ and tracking the symbolic values in a similar way as in symbolic execution. This allows the verification of properties such as whether the probability of finding a solution exceeds 90% or increases over time. We also extended the model’s applicability from quantum circuit to quantum program verification⁹ based on a classical deductive program verification approach.

Note that TAs allow representation of infinite languages, yet we only use them for finite ones, which might seem like the model is overly expressive. We, however, stick to TAs for the following two reasons: (i) there is an existing rich toolbox for TA manipulation and minimization, for example, Comon¹³ and Lengál¹⁸, and (ii) we want to have a robust formal model for extending our framework to parameterized verification, that is, proving that an n-qubit algorithm is correct for any n, which will require us to deal with infinite languages. In Abdulla¹, we introduced a specialized tree automata model tailored for quantum verification, achieving exponential speed-up over classical TAs and even allowing parameterized verification of some class of circuits.

There remain considerable opportunities for further advancements in this area, including but not limited to: (i) automated loop invariant synthesis procedures for quantum program verification and more fine-grained analyses such as probabilistic reachability; (ii) developing abstractions and refinement scheme suited to quantum verification; (iii) verification of quantum circuits simulating physical phenomena, for example, those implementing Hamiltonian simulation; and (iv) integrating automata with other quantum verification frameworks like Quantum Hoare Logic²⁴ and methods for equivalence checking to enable a more automated, systematic verification pipeline across diverse verification paradigms. These directions highlight the vast potential for refining and expanding automata-based quantum verification, promising a pathway to more robust, scalable, and versatile tools for analyzing complex quantum systems.

Acknowledgments

This material is based on a work supported by the Czech Ministry of Education, Youth and Sports project LL1908 of the ERC.CZ programme; the Czech Science Foundation project 23-07565S; the FIT BUT internal project FIT-S-23-8151; National Science and Technology Council, R.O.C., projects NSTC 111-2119-M-001-004, NSTC-112-2222-E-001-002-MY3, NSTC-113-2119-M-001-009, and NSTC-113-2222-E-027-007, ASOFR (Air Force Office of Scientific Research) project FA2386-23-1-4107, Foxconn research project 05T-1120327-1C, Academia Sinica Grand Challenge Seeding Project AS-GCS-113-M06, Academia Sinica Investigator Project Grant AS-IV-114-M07.