Cutoff Theorems for the Equivalence of Parameterized Quantum Circuits

Ross, Neil J.; Wesley, Scott

doi:10.4230/LIPIcs.MFCS.2025.85

Cutoff Theorems for the Equivalence of Parameterized Quantum Circuits

Neil J. Ross

Dalhousie University, Halifax, Canada Scott Wesley

Dalhousie University, Halifax, Canada

Abstract

Many promising quantum algorithms in economics, medical science, and material science rely on circuits that are parameterized by a large number of angles. To ensure that these algorithms are efficient, these parameterized circuits must be heavily optimized. However, most quantum circuit optimizers are not verified, so this procedure is known to be error-prone. For this reason, there is growing interest in the design of equivalence checking algorithms for parameterized quantum circuits. In this paper, we define a generalized class of parameterized circuits with arbitrary rotations and show that this problem is decidable for cyclotomic gate sets. We propose a cutoff-based procedure which reduces the problem of verifying the equivalence of parameterized quantum circuits to the problem of verifying the equivalence of finitely many parameter-free quantum circuits. Because the number of parameter-free circuits grows exponentially with the number of parameters, we also propose a probabilistic variant of the algorithm for cases when the number of parameters is intractably large. We show that our techniques extend to equivalence modulo global phase, and describe an efficient angle sampling procedure for cyclotomic gate sets.

Keywords and phrases:

Quantum Circuits, Parameterized Equivalence Checking

Copyright and License:

2012 ACM Subject Classification:

Hardware

\rightarrow

Quantum computation ; Hardware

\rightarrow

Equivalence checking

Related Version:

Full Version: https://arxiv.org/abs/2506.20985 [39]

Acknowledgements:

We thank Mingkuan Xu for his feedback on the paper and our initial experiments, Linh Dinh for sharing their insights on the number-theoretic aspects of this paper, and Mingsheng Ying for his feedback on an early draft of the paper.

DOI:

10.4230/LIPIcs.MFCS.2025.85

Event:

50th International Symposium on Mathematical Foundations of Computer Science (MFCS 2025)

Editors:

Paweł Gawrychowski, Filip Mazowiecki, and Michał Skrzypczak

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

In quantum mechanics, unitary operators describe how the probability distributions of quantum systems evolve over time. In quantum computing, primitive operators (known as quantum gates) are composed in sequence and parallel, to create quantum circuits which prepare quantum systems with desirable probability distributions. By sampling from these distributions, answers can be obtained to many high-value problems, such as those from economics [19], medical science [40, 14], and material science [29]. In these algorithms, an initial guess is made for the correct probability distribution, and then each sample is used to further refine the distribution. To make this search tractable, the probability distributions are sampled from a family of parameterized quantum circuits, known as ansatz circuits.

In practice, the structure of the ansatz circuit is static, so that the parameters only vary the operators which appear within the circuits. The parameterized operators within ansatz circuits can be understood geometrically as rotations by arbitrary angles. As a result, the gate sets used to construct ansatz circuits are necessarily infinite. In contrast, the gate sets implemented by real quantum computers are finite, due to limitations related to error-correction [15]. This means that for each parameter refinement, the ansatz circuit must be recompiled and optimized again. However, the compilation and optimization of quantum circuits are known to be highly error-prone [50, 20], so it is desirable to verify both the equivalence of the optimized circuit to the original circuit, and more generally, the correctness of each optimization. In both cases, it is necessary to reason equationally about parameterized relations between quantum circuits.

The problem of parameterized equivalence-checking has been well-studied in the context of distributed system. Given a set of parameters $P$ and two programs parameterized by $P$ , say $C_{1}$ and $C_{2}$ , the parameterized-equivalence checking problem asks whether $C_{1}(\theta)=C_{2}(\theta),\forall\theta\in P$ . When $P$ is finite, this problem can be solved by simply testing the elements of $P$ . When $P$ is infinite, one approach to this problem is to find a cutoff $n$ for which checking the equivalence of $C_{1}$ and $C_{2}$ for $n$ distinct elements of $P$ implies the equivalence of $C_{1}$ and $C_{2}$ for all elements of $P$ [16]. Formally, one tries to find an $n\in\mathbb{N}$ such that for all $D\subseteq P$ , if $|D|\geq n$ , then $\forall\theta\in D\cdot C_{1}(\theta)=C_{2}(\theta)$ implies $\forall\theta\in P\cdot C_{1}(\theta)=C_{2}(\theta)$ . Typically, the choice of $n$ (and sometimes even $D$ ) will depend on both $C_{1}$ and $C_{2}$ , and therefore this technique requires domain-specific insights (see, e.g., [22, 25, 27, 2, 34, 45]). When $n$ becomes intractably large, probabilistic techniques have also been employed [13].

Cutoff-based techniques have yet to see wide application in the domain of parameterized quantum circuit equivalence-checking. In 2020, Miller-Bakewell developed a framework which adapts cutoff-based techniques to quantum circuits [32], though these techniques have yet to be applied in practice. The key insight of this work was to note that parameterized quantum circuits are analytic for realistic gate sets, and (up to a change of variable) can often be expressed as matrices over complex Laurent polynomials. The positive and negative degrees of these Laurent polynomials can be over-approximated in an inductive manner, and correspond to a cutoff for parameterized verification. The main challenge in applying the Miller-Bakewell framework is to identify an appropriate change-of-variables such that all parameterized matrices become matrices over complex Laurent polynomials. Once this change-of-variable has been identified, further steps may be taken, such as deriving a closed-form equation for the cutoff. In Miller-Bakewell’s paper, the framework was applied to ZX-, ZW-, and ZH-diagrams, though closed-form bounds were not derived.

In this paper, we propose a cutoff-based technique for quantum circuits with arbitrary rotations with linear arguments. This technique can be understood as an instantiation of the Miller-Bakewell framework, insofar as each parameterized circuit is realized as a matrix over complex Laurent polynomials. However, the circuits considered in this paper correspond to ZXW-diagrams (i.e., with matrix exponentiation) [42], which are not addressed in Miller-Bakewell’s original work. We derive closed-form equations for these cutoffs, which depend only on the coefficients of the parameters in the circuits. Furthermore, we provide an alternative proof for the correctness of the Miller-Bakewell framework, which depends on the distribution of zeros of Laurent polynomials as opposed to polynomial interpolation. This change in perspective motivates a probabilistic variant of the Miller-Bakewell framework, which is applicable for circuits with intractably large cutoffs.

In Sec. 3, we provide the syntax and semantics for our circuit language. In Sec. 4, we illustrate our technique on a simple real-world example. In Sec. 5, we prove a cutoff theorem, and propose a probabilistic variant. In Sec. 6, we identify and solve several challenges faced when implementing this technique. All appendices can be found in the full paper [39].

2 Background

We write $\mathbb{N}$ for the set of natural numbers (including zero), $\mathbb{Z}$ for the set of integers, $\mathbb{Q}$ for the set of rational numbers, $\mathbb{R}$ for the set of real numbers, and $\mathbb{C}$ for the set of complex numbers. If $z\in\mathbb{C}$ , then $\overline{z}$ denotes the complex conjugate of $z$ . If $n\in\mathbb{N}$ , then $[n]$ denotes the set $\{j\in\mathbb{N}:1\leq j\leq n\}$ so that $[0]=\varnothing$ . If $a\in\mathbb{R}$ , then $a^{+}=\max(0,a)$ and $a^{-}=\min(0,a)$ .

2.1 Linear Algebra

We assume familiarity with the basics of linear algebra. Otherwise, we refer the reader to an introductory text, such as [7]. Let $M$ be a complex matrix. We let $M_{j,k}$ denote the entry of $M$ in the $j$ -th row and the $k$ -th column. We recall the following definitions. The conjugate of $M$ is the matrix $\overline{M}$ such that $\overline{M}_{j,k}=\overline{M_{j,k}}$ . The transpose of $M$ is the matrix $M^{T}$ such that $(M^{T})_{j,k}=M_{k,j}$ . The adjoint of $M$ is the matrix $\overline{M}^{T}$ , and is denoted $M^{\dagger}$ . A matrix $H$ is called Hermitian if $H=H^{\dagger}$ . A matrix $U$ is called unitary if $U$ is invertible and $U^{-1}=U^{\dagger}$ .

2.2 Algebraic Numbers and Computation

We assume the reader is familiar with field theory, as found in standard abstract algebra textbooks, such as [17]. Let $\mathbb{F}$ be a subfield of $\mathbb{K}$ . An element $\alpha\in\mathbb{K}$ is algebraic over $\mathbb{F}$ if there exists a polynomial $p\in\mathbb{F}[x]$ such that $p(\alpha)=0$ . We write $\mathbb{F}(\alpha)$ to denote the smallest subfield of $\mathbb{K}$ containing both $\mathbb{F}$ and $\alpha$ . If $\deg(p)=n$ , then it can be shown that the elements of $\mathbb{F}(\alpha)$ form a finite-dimensional $\mathbb{F}$ -vector space with basis vectors $\{1,\alpha,\alpha^{2},\ldots,\alpha^{n-1}\}$ . Furthermore, this vector space forms an $\mathbb{F}$ -algebra under the multiplication of $\mathbb{F}(\alpha)$ . In the case where $\mathbb{F}=\mathbb{Q}$ and $\mathbb{K}=\mathbb{C}$ , we say that $\alpha$ is an algebraic number. The field of all algebraic numbers is denoted $\mathbb{Q}^{\mathrm{Alg}}$ . Algebraic numbers are ideal from a computational perspective, since elements from $n$ -dimensional $\mathbb{Q}$ -vector spaces can be represented exactly using only $2n$ integers (i.e., the numerators and denominators). This is in contrast to floating-point arithemtic, which is inherently inexact.

A special class of algebraic numbers are the cyclotomic numbers. These are solutions to polynomial equations of the form $x^{n}-1=0$ . In other words, each cyclotomic number is a root of unity. We let $\zeta_{n}$ denote the primitive $n$ -th root of unity, which can be defined analytically as $\zeta_{n}=e^{i2\pi/n}$ . For example, $\zeta_{2}=-1$ and $\zeta_{4}=i$ . The smallest subfield of $\mathbb{C}$ containing $\mathbb{Q}$ and all cyclotomic numbers is referred to as the universal cyclotomic field. Many algorithms exist to work efficiently with elements of the universal cyclotomic field, such as [10] and [11]. It is well-known that many quantum gate sets can be defined exactly using only finite-dimensional sub-fields of the universal cyclotomic field, such as the Clifford+ $T$ gate set [18] and its generalizations [4]. For this reason, recent work in the verification of quantum programs has advocated for the use of cyclotomic numbers as an exact representation [6].

(a) The roots of unity in

\mathbb{Q}(\zeta_{8})

.

(b)

\mathbb{Q}(\zeta_{6})=\mathbb{Q}(\zeta_{3})

since

\zeta_{6}=-(\zeta_{3})^{2}

.

Figure 1: Geometry of the cyclotomic numbers. The basis vectors of

\mathbb{Q}[\zeta_{n}]

form the vertices of a regular

n

-gon on the complex unit circle, with one vertex at

(1,0)

.

In this paper, we also utilize analytic properties of cyclotomic numbers. It follows from Euler’s formula that $e^{i\theta}=\cos(\theta)+i\sin(\theta)$ . We can then think of each cyclotomic number as a point of the complex unit circle (see Figure 1(a)). It follows geometrically that $\mathbb{Q}(\zeta_{n})=\mathbb{Q}(\zeta_{2n})$ whenever $n$ is odd (see Figure 1(b)). Moreover, it can be shown by simple algebraic manipulations that the following equations hold.

\displaystyle\cos(\theta)

\displaystyle=\frac{e^{i\theta}+e^{-i\theta}}{2}

\displaystyle\sin(\theta)

\displaystyle=\frac{e^{i\theta}-e^{-i\theta}}{2i}

If $\theta$ is a rational multiple of $\pi$ , say $(q/r)2\pi$ , this means that both $\cos(\theta)$ and $\sin(\theta)$ are elements of $\mathbb{Q}(i,\zeta_{r})$ . However, identifying roots of unity can be challenging, since not all elements of norm $1$ in the universal cyclotomic field are roots of unity. A well-known example is $(3+4i)/5$ , which has norm $1$ but is not a root of unity.

2.3 Multivariate Laurent Polynomials

Let $R$ be a ring. Then $R[x_{1},\ldots,x_{k}]$ denotes the ring of multivariate polynomials with coefficients in $R$ and indeterminates $x_{1}$ through $x_{k}$ . An arbitrary element $f\in R[x_{1},\ldots,x_{k}]$ is of the form $f(x_{1},\ldots,x_{k})=\sum_{t\in T}(a_{t}\prod_{j=1}^{k}{x_{j}}^{t_{j}})$ for some finite $T\subseteq\mathbb{N}^{k}\setminus\{0\}^{k}$ with a non-zero sequence $\{a_{t}\}_{t\in T}$ over $R$ . We write $\deg_{x_{j}}(f)$ for the degree of $f$ in variable $x_{j}$ and $\deg(f)$ for the total degree of $f$ , where $\deg_{x_{j}}(f)=\max\{t_{j}:t\in T\}$ and $\deg(f)=\max\{\sum_{j=1}^{k}t_{j}:t\in T\}$ . When $R$ is an integral domain, the following hold for all $f,g\in R[x_{1},\ldots,x_{k}]$ and $j\in[k]$ .

	$\displaystyle\deg_{x_{j}}(fg)$	$\displaystyle=\deg_{x_{j}}(f)+\deg_{x_{j}}(g)$	$\displaystyle\deg(fg)$	$\displaystyle=\deg(f)+\deg(g)$
	$\displaystyle\deg_{x_{j}}(f+g)$	$\displaystyle\leq\max\{\deg_{x_{j}}(f),\deg_{x_{j}}(g)\}$	$\displaystyle\deg(f+g)$	$\displaystyle\leq\max\{\deg(f),\deg(g)\}$

It is well known that when $k=1$ and $R$ is an integral domain, either $f=0$ or $f$ has at most $\deg(f)$ zeros. A consequence is that for any $S\subseteq R$ , if $f\neq 0$ and $|S|>\deg_{x_{1}}(f)$ , then there exists an $s\in S$ such $f(s)\neq 0$ . Moreover, if $s$ is sampled uniformly from $S$ , then $\Pr(f(x)=0)\leq\deg(f)/|S|$ . The latter two remarks generalize to multivariate polynomials. Further generalization to Laurent polynomials are possible, by clearing the denominators.

Theorem 2.1 (Combinatorial Nullstellensatz [3]).

Let $\mathbb{F}$ be a field and $f$ a polynomial in $\mathbb{F}[x_{1},x_{2},\ldots,x_{k}]$ with total degree $d_{1}+d_{2}+\cdots+d_{k}$ such that the coefficient of $\prod_{j=1}^{k}x_{j}^{d_{j}}$ is nonzero in $f$ . If $S_{1},S_{2},\ldots,S_{k}$ are subsets of $\mathbb{F}$ with $|S_{j}|>d_{j}$ for each $j$ , then there exists $x\in S_{1}\times S_{2}\times\cdots\times S_{k}$ such that $f(x)\neq 0$ .

Theorem 2.2 (DeMillo–Lipton–Schwartz–Zippel Lemma [13, 51, 41]).

Let $R$ be an integral domain and $f\in R[x_{1},x_{2},\ldots,x_{k}]$ a polynomial with total degree $d$ . For each finite subset $S$ of $R$ , if $s_{1},s_{2},\ldots,s_{k}$ are sampled at random, both independently and uniformly from $S$ , then $\Pr(f(s_{1},s_{2},\ldots,s_{k})=0)\leq d/|S|$ .

We can further generalize multivariate polynomials to multivariate Laurent polynomials, denoted $R[x_{1},x_{1}^{-1},\ldots,x_{k},x_{k}^{-1}]$ . In this setting, $T\subseteq\mathbb{Z}^{k}$ , so that powers may be positive or negative. For example, $f(x_{1},x_{2})=x_{1}x_{2}-x_{1}^{-3}+5$ is a Laurent polynomial from $\mathbb{Z}[x_{1},x_{1}^{-1},x_{2},x_{2}^{-1}]$ . Since the exponents in a Laurent polynomial may be both positive and negative, each Laurent polynomial has both positive and negative degrees. We write $\deg_{x_{j}}^{+}(f)$ for the positive degree of $f$ in variable $x_{j}$ and $\deg_{x_{j}}^{-}$ for the negative degree of $f$ in variable $x_{j}$ , where $\deg_{x_{j}}^{+}(f)=\max\{t_{j}^{+}:t\in T\}$ and $\deg_{x_{j}}^{-}(f)=\max\{-t_{j}^{-}:t\in T\}$ . Similarly, the total positive degree of $f$ is $\deg^{+}(f)=\max\{\sum_{j=1}^{k}t_{j}^{+}:t\in T\}$ .

3 A Syntax and Semantics for Parameterized Circuits

This section begins by reviewing quantum states, quantum operators, and their composition, as in [35, Ch. 4]. This background material is then used to give syntax and parameterized semantics for quantum circuits with arbitrary gates, and rotations around arbitrary axes.

3.1 Quantum States

The primitive unit of information in quantum computing is the qubit. As in classical computing, a qubit can be in the states zero and one, denoted $\left|0\right\rangle$ and $\left|1\right\rangle$ . However, a qubit may also be in a superposition of the states $\left|0\right\rangle$ and $\left|1\right\rangle$ . Formally, this means that the state of a qubit $\left|\psi\right\rangle$ can be described as $\alpha\left|0\right\rangle+\beta\left|1\right\rangle$ for any $\alpha\in\mathbb{C}$ and $\beta\in\mathbb{C}$ satisfying $|\alpha|^{2}+|\beta|^{2}=1$ . To simplify calculations, we think of $\left|0\right\rangle$ and $\left|1\right\rangle$ as the standard basis vectors for $\mathbb{C}^{2}$ to obtain the following vector equation: $\left|\psi\right\rangle=\alpha\left|0\right\rangle+\beta\left|1\right\rangle=% \alpha\bigl{[}\begin{smallmatrix}1\\ 0\end{smallmatrix}\bigr{]}+\beta\bigl{[}\begin{smallmatrix}0\\ 1\end{smallmatrix}\bigr{]}=\bigl{[}\begin{smallmatrix}\alpha\\ \beta\end{smallmatrix}\bigr{]}$ .

Of course, the quantum algorithms described in the introduction of this paper require more than a single qubit of information. Given an $n$ -qubit quantum system, there are clearly $2^{n}$ possible basis states. For example, when $n=2$ , these are $\left|00\right\rangle$ , $\left|01\right\rangle$ , $\left|10\right\rangle$ , and $\left|11\right\rangle$ . As before, an $n$ -qubit quantum system may also be in an arbitrary superposition of these basis states with the modulus-squared of the coefficients summing to $1$ . For example, an arbitrary $2$ -qubit quantum system has state $\left|\psi\right\rangle=\alpha\left|00\right\rangle+\beta\left|01\right\rangle% +\gamma\left|10\right\rangle+\rho\left|11\right\rangle$ for any $\alpha,\beta,\gamma,\rho\in\mathbb{C}$ satisfying $|\alpha|^{2}+|\beta|^{2}+|\gamma|^{2}+|\rho|^{2}=1$ . This means that the states of an $n$ -qubit quantum system correspond to the unit vectors in $\mathbb{C}^{2^{n}}$ .

3.2 Quantum Operations

A quantum program evolves the state of a quantum system, after which all qubits are measured. Given a quantum state $\left|\psi\right\rangle=\sum_{j=1}^{2^{n}}\alpha_{j}\left|j\right\rangle$ , the probability of observing state $\left|j\right\rangle$ is $|\alpha_{j}|^{2}$ . Then the paradigm of quantum computing is to construct an $n$ -qubit quantum system whose probability distribution assigns high probability to the correct output.

The evolution of a quantum system is described by a linear transformation of its state space. Since the laws of physics are reversible, then this transformation must be invertible. Moreover, the inverse of this transformation should be its conjugate transpose. This means that operations on $n$ -qubit systems correspond to unitary matrices. Given an $n$ -qubit state $\left|\psi\right\rangle$ and an $(2^{n})\times(2^{n})$ dimensional matrix $M$ , the state obtained by applying $M$ to $\left|\psi\right\rangle$ is $M\left|\psi\right\rangle$ . For example, the following four matrices are unitary operations on a qubit.

\displaystyle I

\displaystyle=\begin{bmatrix}1&0\\ 0&1\end{bmatrix}

\displaystyle X

\displaystyle=\begin{bmatrix}0&1\\ 1&0\end{bmatrix}

\displaystyle Z

\displaystyle=\begin{bmatrix}1&0\\ 0&-1\end{bmatrix}

\displaystyle Y

\displaystyle=\begin{bmatrix}0&-i\\ i&0\end{bmatrix}

The matrix $I$ corresponds to a no-op and the matrix $X$ corresponds to a not gate. The matrix $Z$ can be understood as adjusting the coefficient of $\left|1\right\rangle$ by a factor of $(-1)$ . This has no classical analogue. The gate $Y$ is equal to $(-iZ)X$ , and therefore, corresponds to a not gate followed by some non-classical operation.

An important construct in classical computing is the if-then statement. This can be generalized to quantum computing as follows. Let $M$ be a unitary transformation on an $n$ -qubit quantum system. Then there exists a unitary transformation $I_{2^{n}}\oplus M$ on an $(n+1)$ -qubit quantum system, such that $I_{2^{n}}\oplus M$ applies $M$ to the last $n$ qubits of a basis state if and only if the first qubit of the basis is in state $\left|1\right\rangle$ . Formally, $I_{2^{n}}$ is the $(2^{n})\times(2^{n})$ identity matrix, and $I_{2^{n}}\oplus M$ is the direct sum of $I_{2^{n}}$ with $M$ . In terms of matrices, $I_{2^{n}}\oplus M$ is simply the block diagonal matrix with blocks $I_{2^{n}}$ and $M$ , as shown below.

\displaystyle I_{2^{n}}\oplus M

\displaystyle=\begin{bmatrix}I_{2^{n}}&0\\ 0&M\end{bmatrix}

\displaystyle I_{2}\oplus X

\displaystyle=\begin{bmatrix}I_{2}&0\\ 0&X\end{bmatrix}=\begin{bmatrix}1&0&0&0\\ 0&1&0&0\\ 0&0&0&1\\ 0&0&1&0\end{bmatrix}

The matrix for $I_{2}\oplus X$ , known as a cnot gate, is given above. This generalizes the classical conditional statement: if the first bit is in state $\left|1\right\rangle$ , then apply a not gate to the second bit.

So far, all of the operations discussed are parameter-free. However, quantum algorithms also make use of rotation gates, which are parameterized by an angle of rotation. As the name suggests, a rotation gate is defined by its axis-of-rotation. Formally, each axis $M$ is a Hermitian unitary matrix. Then one can define, as a generalization of Euler’s formula, the rotation $R_{M}(\theta)$ as follows.

R_{M}(\theta)=e^{-iM\theta/2}=\sum_{n=0}^{\infty}\frac{(-iM\theta/2)^{n}}{n!}=% \cos(-\theta/2)I+i\sin(-\theta/2)M

This definition can be extended to $k$ parameters by taking any transformation $f:\mathbb{R}^{k}\to\mathbb{R}$ . For example, given $f(\theta_{1},\theta_{2})=\theta_{1}+\theta_{2}$ , we can define a two parameter rotation $R_{M}(f)$ where $R_{M}(f)(\theta_{1},\theta_{2})=R_{M}(f(\theta_{1},\theta_{2}))=R_{M}(\theta_{% 1}+\theta_{2})$ . In this work, we consider the family $\mathcal{F}$ of $k$ -variable rational-linear functions with affine translations by rational multiples of $\pi$ . That is, the set $\mathcal{F}$ is defined to be $\{f(\theta)=a_{1}\theta_{1}+a_{2}\theta_{2}+\cdots+a_{k}\theta_{k}+q\pi\mid a_% {1},a_{2},\ldots,a_{k},q\in\mathbb{Q}\}$ .

The most common rotations in quantum circuits are the $I$ -, $X$ -, $Y$ -, and $Z$ -rotations. However, there are many single qubit rotations not of this form. For example, given any coefficients $\alpha,\beta,\gamma\in\mathbb{R}$ , if $\alpha^{2}+\beta^{2}+\gamma^{2}=1$ , the matrix $\alpha X+\beta Y+\gamma Z$ is also a Hermitian unitary matrix. Note that the matrix $R_{I}(-2\theta)$ is typically referred to as a global phase gate, rather than an $I$ -rotation.

Example 3.1 (Real Amplitude Ansatz Circuit).

In quantum machine learning, convolutional layers are often implemented using the real amplitude ansatz circuit [1, 5, 31, 26, 48]. This circuit is composed from one or more layers of $Z$ -rotations, each followed by a layer of controlled-not gates. Since $Z$ -rotations do not commute with the targets of controlled-not gates, then these layers can interact in non-trivial ways. The choice of parameter to each $Z$ -rotation is treated as a weight in the quantum machine learning model.

3.3 Composing Quantum Operations

Just like classical operations, quantum operations can also be composed in sequence and in parallel. Of the two, sequential composition is the simplest to describe. Assume that both $M$ and $N$ are operations on an $n$ -qubit quantum system. If $N$ is applied to an $n$ -qubit system $\left|\psi\right\rangle$ , then the state $N\left|\psi\right\rangle$ is obtained. If $M$ is then applied to this intermediate state, then the state $M(N\left|\psi\right\rangle)$ is obtained. This is equivalent to applying $M N$ to $\left|\psi\right\rangle$ . In other words, the sequential composition of quantum operations corresponds to matrix multiplication.

Now let $M$ denote a quantum operation on an $m$ -qubit quantum system and $N$ denote a quantum operation on an $n$ -qubit quantum system. Intuitively, the parallel composition of $M$ and $N$ should act on the first $m$ -qubits by $M$ , and the last $n$ -qubits by $N$ . However, this composition must also respect superposition, through a property known an bilinearity. To compute this new operation, the Kronecker tensor product is required, which is denoted $\otimes$ and defined as follows for matrices of any dimension.

\begin{bmatrix}c_{1,1}&c_{1,2}&\cdots&c_{1,n}\\ c_{2,1}&c_{2,2}&\cdots&c_{2,n}\\ \vdots&\vdots&\ddots&\vdots\\ c_{m,1}&c_{m,2}&\cdots&c_{m,n}\end{bmatrix}\otimes M=\begin{bmatrix}c_{1,1}M&c% _{1,2}M&\cdots&c_{1,n}M\\ c_{2,1}M&c_{2,2}M&\cdots&c_{2,n}M\\ \vdots&\vdots&\ddots&\vdots\\ c_{m,1}M&c_{m,2}M&\cdots&c_{m,n}M\end{bmatrix}

It follows that $(M\otimes N)(\left|\psi\right\rangle\otimes\left|\varphi\right\rangle)=(M\left% |\phi\right\rangle)\otimes(N\left|\varphi\right\rangle)$ as desired.

3.4 Quantum Circuits

Quantum circuits are constructed from primitive gates, under sequential and parallel composition. In this section, we first define what we take to be primitive gates, and then define what it means to be a circuit over this gate set. The distinction between syntax and semantics is emphasized. In both cases, we introduce inductive principles which will be used later in this paper. Formally, these circuits correspond to diagrams in a certain PROP category [8], with semantics given functorially [28], though this is only used to prove the inductive principles used throughout the paper, and to establish that our semantics and circuit transformations are well-defined (see the full paper for more details).

In what follows, $C(-)$ is a function symbol used to denote conditional control. A gate set is a collection of basic gates, closed under conditional control. A basic gate is a complex matrix (e.g. unitary operations, state preparation, post-selection) or parameterized rotation. Formally, we take some set $\mathcal{G}$ of complex matrices and some set $\mathcal{H}$ of Hermitian unitary matrices. The associated gate set, denoted $\Sigma(\mathcal{G},\mathcal{H})$ is defined inductively as follows.

$\blacksquare$

If $G\in\mathcal{G}$ , then $G\in\Sigma(\mathcal{G},\mathcal{H})$ .
$\blacksquare$

If $M\in\mathcal{H}$ , then $R_{M}(f)\in\Sigma(\mathcal{G},\mathcal{H})$ for each parameterization $f\in\mathcal{F}$ .
$\blacksquare$

If $G\in\Sigma(\mathcal{G},\mathcal{H})$ and $G$ is unitary, then $C(G)\in\Sigma(\mathcal{G},\mathcal{H})$ .

We let $\textsf{in}(-)$ and $\textsf{out}(-)$ denote the input and output arities of these gates, which are defined as follows.

$\blacksquare$

If $G\in\mathcal{G}$ is $(2^{n})\times(2^{m})$ , then $\textsf{in}(G)=n$ and $\textsf{out}(G)=m$ .
$\blacksquare$

If $M\in\mathcal{H}$ is $(2^{n})\times(2^{n})$ and $f\in\mathcal{F}$ , then $\textsf{in}(R_{M}(f))=\textsf{out}(R_{M}(f))=n$ .
$\blacksquare$

If $G\in\Sigma(\mathcal{G},\mathcal{H})$ , then $\textsf{in}(C(G))=\textsf{in}(G)+1$ and $\textsf{out}(C(G))=\textsf{out}(G)+1$ .

We let $[\![-]\!]$ denote the parameterized semantics of each gate, which are defined as expected.

$\blacksquare$

If $G\in\mathcal{G}$ , then $[\![G]\!](\theta)=G$ .
$\blacksquare$

If $M\in\mathcal{H}$ and $f\in\mathcal{F}$ , then $[\![R_{M}(f)]\!](\theta)=\cos(-f(\theta)/2)I+i\sin(-f(\theta)/2)M$ .
$\blacksquare$

If $G\in\Sigma(\mathcal{G},\mathcal{H})$ with $G$ an $(2^{n})\times(2^{n})$ unitary, then $[\![C(G)]\!](\theta)=I_{2^{n}}\oplus[\![G]\!](\theta)$ .

Since this gate set is defined inductively, then to prove that every gate satisfies a predicate $P$ , it suffices to use well-founded induction (see the full paper).

Proposition 3.2.

Assume that a predicate $P$ on $\Sigma(\mathcal{G},\mathcal{H})$ satisfies the following.

$\blacksquare$

Base Case (1). $\forall G\in\mathcal{G},P(G)$ .
$\blacksquare$

Base Case (2). $\forall M\in\mathcal{H},\forall f\in\mathcal{F},P(R_{M}(f))$ .
$\blacksquare$

Control Induction. $\forall G\in\Sigma(\mathcal{G},\mathcal{H})$ , $G$ unitary and $P(G)$ implies $P(C(G))$ .

Then $P(G)$ holds for each $G\in\Sigma(\mathcal{G},\mathcal{H})$ .

(a)

G\in\mathcal{G}

.

(b)

C(G)

.

(c)

R_{H}(f)

.

(d)

C_{1}//C_{2}

.

(e)

C_{2}\circ C_{1}

.

Figure 2: The graphical language for circuits in

\textsf{Circ}(\mathcal{G},\mathcal{H})

.

Circuits are then constructed from the elements of $\Sigma(\mathcal{G},\mathcal{H})$ through sequential and parallel composition. We let $(\circ)$ denote sequential composition and $(//)$ denote parallel composition, to distinguish between syntactic compositions and their semantic counterparts. Of course, sequential composition requires that the outputs of the first sub-circuit matches the inputs of the second sub-circuit. To handle this, we extend $\textsf{in}(-)$ and $\textsf{out}(-)$ as follows.

$\blacksquare$

$\textsf{in}(C_{1}//C_{2})=\textsf{in}(C_{1})+\textsf{in}(C_{2})$ and $\textsf{out}(C_{1}//C_{2})=\textsf{out}(C_{1})+\textsf{out}(C_{2})$ .
$\blacksquare$

$\textsf{in}(C_{2}\circ C_{1})=\textsf{in}(C_{1})$ and $\textsf{out}(C_{2}\circ C_{1})=\textsf{out}(C_{2})$ .

Then $\textsf{Circ}(\mathcal{G},\mathcal{H})$ , the family of circuits over the gate set $\Sigma(\mathcal{G},\mathcal{H})$ , is defined inductively as follows where $\epsilon$ denotes the empty wire with $\textsf{in}(\epsilon)=\textsf{out}(\epsilon)=1$ .

$\blacksquare$

If $C\in\Sigma(\mathcal{G},\mathcal{H})$ , then $C\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ .
$\blacksquare$

If $C_{1},C_{2}\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ , then $C_{1}//C_{2}\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ .
$\blacksquare$

If $C_{1},C_{2}\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ and $\textsf{in}(C_{2})=\textsf{out}(C_{1})$ , then $C_{2}\circ C_{1}\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ .

A graphical language for $\textsf{Circ}(\mathcal{G},\mathcal{H})$ is given in Figure 2. The semantic map $[\![-]\!]$ extends to these circuits as expected: $[\![C_{2}//C_{1}]\!](\theta)=[\![C_{2}]\!](\theta)\otimes[\![C_{1}]\!](\theta)$ , $[\![C_{2}\circ C_{1}]\!](\theta)=([\![C_{2}]\!](\theta))([\![C_{1}]\!](\theta))$ , and $[\![\epsilon]\!]=I_{2}$ . As with quantum gates, an inductive principle also holds for quantum circuits.

Proposition 3.3.

Assume that a predicate $P$ on $\textsf{Circ}(\mathcal{G},\mathcal{H})$ satisfies the following.

$\blacksquare$

Base Case (1). $P(\epsilon)$ .
$\blacksquare$

Base Case (2). $\forall G\in\Sigma(\mathcal{G},\mathcal{H}),P(G)$ .
$\blacksquare$

Parallel Induction. If $C_{1},C_{2}\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ such that $P(C_{1})$ and $P(C_{2})$ , then $P(C_{1}//C_{2})$ .
$\blacksquare$

Sequential Induction. If $C_{1},C_{2}\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ such that $\textsf{in}(C_{2})=\textsf{out}(C_{1})$ with $P(C_{1})$ and $P(C_{2})$ , then $P(C_{2}\circ C_{1})$ .

Then $P(C)$ holds for each $C\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ .

4 A Motivating Example: Circuit Compilation

\displaystyle\begin{matrix}{\includegraphics{dagpub-standalone-combined-2025-0% 7-07-07-46-16-page-6.pdf2svg.svg}}\end{matrix}

\displaystyle=\begin{matrix}{\includegraphics{dagpub-standalone-combined-2025-% 07-07-07-46-16-page-7.pdf2svg.svg}}\end{matrix}

Figure 3: A parameterized equality used to compile controlled rotations.

We now discuss the verification of a concrete circuit equation. The example is simple but illustrative of the techniques we will develop in the next section. Consider the equation in Figure 3. A naive approach to establishing this equation is to evaluate the right-hand side to obtain the following operator.

(I\oplus X)(I\otimes R_{Z}(-\theta))(I\oplus X)(I\otimes R_{Z}(\theta))=\begin% {bmatrix}R_{Z}(-\theta)R_{Z}(\theta)&0\\ 0&XR_{Z}(-\theta)XR_{Z}\left(\theta\right)\end{bmatrix}

Then, by further simplification, we obtain the following equations.
$\displaystyle R_{Z}(-\theta)R_{Z}(\theta)$ $\displaystyle=\begin{bmatrix}e^{-i\theta/2}e^{i\theta/2}&0\\ 0&e^{i\theta/2}e^{-i\theta/2}\end{bmatrix}$ $\displaystyle XR_{Z}(-\theta)XR_{Z}(\theta)$ $\displaystyle=\begin{bmatrix}e^{-i\theta/2}e^{-i\theta/2}&0\\ 0&e^{i\theta/2}e^{i\theta/2}\end{bmatrix}$
Using the identities $e^{a}e^{b}=e^{a+b}$ and $e^{0}=1$ , it then follows that $XR_{Z}(-\theta)XR_{Z}(\theta)=R_{Z}(2\theta)$ and $R_{Z}(-\theta)R_{Z}(\theta)=I$ . Consequently,

(I\oplus X)(I\otimes R_{Z}(-\theta))(I\oplus X)(I\otimes R_{Z}(\theta))=\begin% {bmatrix}I&0\\ 0&R_{Z}(2\theta)\end{bmatrix}=(I\oplus R_{Z}(2\theta)).

This establishes the equation in Figure 3 for all choices of $\theta$ . However, this proof depends on the parameterized equations $e^{a+b}=e^{a}e^{b}$ and $e^{0}=1$ . In general, it is challenging to find a complete set of parameterized relations for a parameterized gate set [33]. Moreover, given an arbitrary set of complete relations, the problem of deciding if two expressions are equivalent is known to be undecidable [36]. For these reasons, we adopt a different approach.

A perhaps surprising result is that all parameterized circuit equalities can be established by checking only a finite number of rotation angles. In other words, if the equality in Figure 3 did not hold, then a counterexample could be found by checking only a fixed number of instances. To do this, we first convert the equality into a family of polynomials, such that the equality holds if and only if all of the polynomials are identically zero. We then find an integer $n$ such that each of the polynomials has degree at most $n$ . Since non-zero polynomials of degree $n$ have at most $n$ roots, then either the polynomial is zero and will evaluate to zero on $n+1$ angles, or the polynomial is non-zero and at least one of the $n+1$ angles yields a non-zero result.

To obtain the desired polynomials, we apply the change-of-variable $e^{-i\theta/2}\mapsto z$ . Under this change of variable, the following equalities hold.

	$\displaystyle R_{Z}(-\theta)R_{Z}(\theta)$	$\displaystyle=\begin{bmatrix}z^{-1}z&0\\ 0&zz^{-1}\end{bmatrix}=\begin{bmatrix}1&0\\ 0&1\end{bmatrix}=z^{-2}\begin{bmatrix}z^{2}&0\\ 0&z^{2}\end{bmatrix}$
	$\displaystyle XR_{Z}(-\theta)XR_{Z}(\theta)$	$\displaystyle=\begin{bmatrix}z^{-1}z^{-1}&0\\ 0&zz\end{bmatrix}=\begin{bmatrix}z^{-2}&0\\ 0&z^{2}\end{bmatrix}=z^{-2}\begin{bmatrix}1&0\\ 0&z^{4}\end{bmatrix}$

Continuing in this fashion, we can find that each matrix entry on the left-hand side or the right-hand side of Figure 3 has degree at most four. Then the difference between the left-hand side and the right-hand side also has degree at most four. Note that the $z^{-2}$ terms correspond to a removable singularity at $z=0$ , which does not fall on the complex unit circle, and can be safely ignored. Since degree four polynomials have at most four roots, then it suffices to check the equality in Figure 3 using only $5$ angles from $[0,4\pi)$ . For example, consider the five angles $\theta_{j}=j\pi/2$ for $0\leq j\leq 4$ . It is easily verified that $(I\oplus R_{Z}(2\theta_{j}))=(I\oplus X)(I\otimes R_{Z}(-\theta_{j}))(I\oplus X% )(I\otimes R_{Z}(\theta_{j}))$ for all $0\leq j\leq 4$ . Then $f(\theta)=(I\oplus R_{Z}(2\theta))-(I\oplus X)(I\otimes R_{Z}(-\theta))(I% \oplus X)(I\otimes R_{Z}(\theta))$ has at least five roots. Since each entry of $f(\theta)$ has degree at most four, then $f$ is identically zero and Figure 3 must hold. Note that the angles were sampled from $[0,4\pi)$ since $e^{-i\theta_{j}/2}$ has period $4\pi$ .

While this example was admittedly simplistic, we will see in the next section, that the technique generalizes to all parameterized circuits. In particular, just as in this example, we will see that computing the polynomials is inconsequential. Instead, it will suffice to find an efficient procedure which provides a reason bound on each degree.

5 Equivalence Checking Techniques

In this section, we consider parameterized quantum circuits where all coefficients are from $\mathbb{Z}$ , rather than $\mathbb{Q}$ . We denote these circuits $\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ . It is first shown that up to a change of variable, these circuits admit semantics as matrices over the ring of Laurent polynomials $\mathbb{C}[z_{1},z_{1}^{-1},\ldots,z_{k},z_{k}^{-1}]$ . This is then combined with Thm. 2.1 to establish a cutoff-based equivalence checking theorem for these circuits. Using Thm. 2.2, a probabilistic variant is also obtained. In Sec. 6, we show how these results generalize back to parameterized circuits with rational coefficients.

5.1 Polynomial Semantics

This section shows that, up to a change of variable, each circuit $\textsf{Circ}(\mathcal{G},\mathcal{H})$ has semantics given by a matrix with entries corresponding to complex Laurent polynomials. Moreover, these polynomials are shown to have degrees bounded by certain sums of the coefficients which appear in the circuit. It follows that the techniques used in Sec. 4 can be generalized to all integral circuits in $\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ .

As a first step, a new semantic interpretation $[\![-]\!]_{\textsf{Poly}}$ is provided for $\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ , which interprets each circuit in $\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ as a polynomial over $\mathbb{C}[z_{1},z_{1}^{-1},\ldots,z_{k},z_{k}^{-1}]$ . Since parameters only appear in trigonometric terms, then a first step is to give Laurent polynomials which abstract the trigonometric terms. Let $\alpha\in\mathbb{Z}^{k}$ , $q\in\mathbb{Q}$ , and $f(\theta)=\alpha_{1}\theta_{1}+\cdots\alpha_{k}\theta_{k}+q$ .
$\displaystyle\cos\left(-\frac{f(\theta)}{2}\right)$ $\displaystyle=\frac{e^{i(-f(\theta)/2)}+e^{-i(-f(\theta)/2)}}{2}=\frac{e^{-iq/% 2}}{2}\prod_{j=1}^{k}\left(e^{-i\theta_{j}/2}\right)^{a_{j}}+\frac{e^{iq/2}}{2% }\prod_{j=1}^{k}\left(e^{i\theta_{j}/2}\right)^{a_{j}}$ $\displaystyle\sin\left(-\frac{f(\theta)}{2}\right)$ $\displaystyle=\frac{e^{i(-f(\theta)/2)}-e^{-i(-f(\theta)/2)}}{2i}=\frac{e^{-iq% /2}}{2i}\prod_{j=1}^{k}\left(e^{-i\theta_{j}/2}\right)^{a_{j}}-\frac{e^{iq/2}}% {2i}\prod_{j=1}^{k}\left(e^{i\theta_{j}/2}\right)^{a_{j}}$
By substituting $z_{j}=e^{-i\theta_{j}/2}$ for each $j\in[k]$ and letting $c=e^{-iq/2}$ , the following Laurent polynomials are obtained.

\displaystyle\textsf{CPoly}(f)

\displaystyle=\frac{c}{2}\prod_{j=1}^{k}z_{j}^{\alpha_{j}}+\frac{1}{2c}\prod_{% j=1}^{k}z_{j}^{-\alpha_{j}}

\displaystyle\textsf{SPoly}(f)

\displaystyle=\frac{-ic}{2}\prod_{j=1}^{k}z_{j}^{\alpha_{j}}+\frac{i}{2c}\prod% _{j=1}^{k}z_{j}^{-\alpha_{j}}

Then the following equations hold by construction.
$\displaystyle\textsf{CPoly}(f)\left(e^{-i\theta_{1}/2},\ldots,e^{-i\theta_{k}/% 2}\right)$ $\displaystyle=\frac{e^{-iq/2}}{2}\prod_{j=1}^{k}\left(e^{-i\theta_{j}/2}\right% )^{a_{j}}+\frac{e^{iq/2}}{2}\prod_{j=1}^{k}\left(e^{i\theta_{j}/2}\right)^{a_{% j}}=\cos\left(-\frac{f(\theta)}{2}\right)$ $\displaystyle\textsf{SPoly}(f)\left(e^{-i\theta_{1}/2},\ldots,e^{-i\theta_{k}/% 2}\right)$ $\displaystyle=\frac{e^{-iq/2}}{2i}\prod_{j=1}^{k}\left(e^{-i\theta_{j}/2}% \right)^{a_{j}}-\frac{e^{iq/2}}{2i}\prod_{j=1}^{k}\left(e^{i\theta_{j}/2}% \right)^{a_{j}}=\sin\left(-\frac{f(\theta)}{2}\right)$
Given these polynomials, $[\![-]\!]_{\textsf{Poly}}$ is defined inductively on the gates as follows.

$\blacksquare$

If $G\in\mathcal{G}$ , then $[\![G]\!]_{\textsf{Poly}}=G$ .
$\blacksquare$

If $M\in\mathcal{H}$ and $f\in\mathcal{F}$ , then $[\![R_{M}(f)]\!]_{\textsf{Poly}}=\textsf{CPoly}(f)I+i\,\textsf{SPoly}(f)M$ .
$\blacksquare$

If $G\in\Sigma(\mathcal{G},\mathcal{H})$ with $G$ an $(2^{n})\times(2^{n})$ unitary, then $[\![C(G)]\!]_{\textsf{Poly}}=I_{2^{n}}\oplus[\![G]\!]_{\textsf{Poly}}$ .

The semantics extend as expected to sequential and parallel composition. This makes precise the change of variable used in Sec. 4.

Definition 5.1 (Polynomial Abstraction).

A polynomial abstraction is a function $[\![-]\!]_{*}$ from $\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ to collection of matrices over $\mathbb{C}[z_{1},z_{1}^{-1},\ldots,z_{k},z_{k}^{-1}]$ such that $[\![C]\!](\theta_{1},\ldots,\theta_{k})=[\![C]\!]_{*}\left(e^{-i\theta_{1}/2},% \ldots,e^{-i\theta_{k}/2}\right)$ for all $C\in\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ .

Theorem 5.2.

$[\![-]\!]_{\textsf{Poly}}$ is a polynomial abstraction.

Example 5.3 (Polynomial Semantics).

The calculations from Sec. 4 can be revisited from the perspective of polynomial semantics. Of course, the circuit in Figure 3 is somewhat uninteresting, since the circuit has only one parameter. Instead, we will consider a new circuit with two parameters $\rho_{1}$ and $\rho_{2}$ obtained through the substitution $\theta=f(\rho_{1},\rho_{2})$ where $f(\rho_{1},\rho_{2})=\rho_{1}-2\rho_{2}$ . The sine and cosine polynomials for $f$ are as follows.

\displaystyle\textsf{CPoly}(f)

\displaystyle=\frac{1}{2}z_{1}z_{2}^{-2}+\frac{1}{2}z_{1}^{-1}z_{2}^{2}

\displaystyle\textsf{SPoly}(f)

\displaystyle=\frac{-i}{2}z_{1}z_{2}^{-2}+\frac{i}{2}z_{1}^{-1}z_{2}^{2}

Then $\textsf{CPoly}(f)+i\;\textsf{SPoly}(f)=z_{1}z_{2}^{-2}$ and $\textsf{CPoly}(f)-i\;\textsf{SPoly}(f)=z_{1}^{-1}z_{2}^{2}$ . Let $C_{1}$ denote the right-hand side of the equation in Figure 3. To compute $[\![C_{1}]\!]_{\textsf{Poly}}$ , we start by evaluating each gate. Clearly $[\![C(X)]\!]_{\textsf{Poly}}=I_{2}\oplus X$ . Moreover,

	$\displaystyle[\![\epsilon//R_{Z}(f)]\!]_{\textsf{Poly}}=I_{2}\otimes[\![R_{Z}(% f)]\!]_{\textsf{Poly}}$	$\displaystyle=I_{2}\otimes\begin{bmatrix}z_{1}z_{2}^{-2}&0\\ 0&z_{1}^{-1}z_{2}^{2}\end{bmatrix},$
	$\displaystyle[\![\epsilon//R_{Z}(-f)]\!]_{\textsf{Poly}}=I_{2}\otimes[\![R_{Z}% (-f)]\!]_{\textsf{Poly}}$	$\displaystyle=I_{2}\otimes\begin{bmatrix}z_{1}^{-1}z_{2}^{2}&0\\ 0&z_{1}z_{2}^{-2}\end{bmatrix}.$

It follows by calculations similar to those in Sec. 4 that,

[\![C_{1}]\!]_{\textsf{Poly}}=[\![C(X)]\!]_{\textsf{Poly}}[\![\epsilon//R_{Z}(% -f)]\!]_{\textsf{Poly}}[\![C(X)]\!]_{\textsf{Poly}}[\![\epsilon//R_{Z}(f)]\!]_% {\textsf{Poly}}=I_{2}\oplus\begin{bmatrix}z_{1}^{-2}z_{2}^{4}&0\\ 0&z_{1}^{2}z_{2}^{-4}\end{bmatrix}.

Then $[\![C_{1}]\!]_{\textsf{Poly}}(e^{-i\rho_{1}/2},e^{-i\rho_{2}/2})=I\oplus R_{Z}% (2f(\rho_{1},\rho_{2}))=[\![C_{1}]\!](\rho_{1},\rho_{2})$ as expected. $\lrcorner$

To check that $[\![C_{1}]\!]=[\![C_{2}]\!]$ , it suffices to check symbolically that $[\![C_{1}]\!]_{\textsf{Poly}}=[\![C_{2}]\!]_{\textsf{Poly}}$ . However, it is often too computationally expensive to compute the polynomials explicitly. Instead, one could first upper-bound the degree of each polynomial, and then combine these degree bounds with the theorems of Sec. 2.3. It is not hard to see that for each component of $[\![R_{H}(f)]\!]_{\textsf{Poly}}$ , its degrees are all bounded by the coefficients of $f$ . This property extends to all circuits in $\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ by studying their coefficient sequences. Intuitively, the coefficient sequence of a circuit $C$ is a sequence $A(C)$ over $\mathbb{Q}^{k}$ such that $A(C)_{j}$ is the list of coefficients for the $j$ -th rotation in $C$ . More formally, let $(\mathbb{Q}^{k})^{*}$ denote the set of all finite sequences over $\mathbb{Q}^{k}$ and $(\cdot)$ denote sequence concatenation. Then $A(-)$ is defined inductively as follows.

$\blacksquare$

If $G\in\mathcal{G}$ , then $A(G)=\epsilon$ .
$\blacksquare$

If $M\in\mathcal{H}$ and $f(\theta)=a_{1}\theta_{1}+\cdots+a_{k}\theta_{k}+q$ , then $A(R_{M}(f))=((a_{1},\ldots,a_{k}))$ .
$\blacksquare$

If $G\in\Sigma(\mathcal{G},\mathcal{H})$ , then $A(C(G))=A(G)$ .
$\blacksquare$

If $C_{1},C_{2}\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ , then $A(C_{1}//C_{2})=A(C_{1})\cdot A(C_{2})$ .
$\blacksquare$

If $C_{1},C_{2}\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ and $\textsf{in}(C_{2})=\textsf{out}(C_{1})$ , then $A(C_{2}\circ C_{1})=A(C_{2})\cdot A(C_{1})$ .

Then $\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ is precisely the set of circuits in $\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ such that $A(C)\in(\mathbb{Z}^{k})^{*}$ . We define $\Sigma_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ analogously. The following definition generalizes the coefficient bound of the degree of a gate to a coefficient bound on the degree of all circuits.

Definition 5.4 (Coefficient Bounded Semantics).

Let $[\![-]\!]_{*}$ be a polynomial abstraction. A circuit $C\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ with $\textsf{in}(C)=n$ and $\textsf{out}(C)=m$ is coefficient bounded with respect to $[\![-]\!]_{*}$ , denoted $\textsf{Bnd}_{*}(C)$ , if for each $s\in[2^{n}]$ and $t\in[2^{m}]$ with $f=([\![C]\!]_{*})_{s,t}$ ,

$\blacksquare$

(B1). $\deg^{+}_{z_{j}}(f)\leq\sum_{a\in A(C)}|a_{j}|$ for each $j\in[k]$ ,
$\blacksquare$

(B2). $\deg^{-}_{z_{j}}(f)\leq\sum_{a\in A(C)}|a_{j}|$ for each $j\in[k]$ ,
$\blacksquare$

(B3). $\deg^{+}(f)\leq\sum_{a\in A(C)}\kappa(a)$ where $\kappa(a)=\max\{\sum_{j=1}^{k}a_{j}^{+},\sum_{j=1}^{k}-a_{j}^{-}\}$ .

Example 5.5 (Coefficient Bounded Semantics).

Recall $C_{1}$ from Ex. 5.3. It will be shown that $\textsf{Bnd}_{\textsf{Poly}}(C_{1})$ holds. First, the coefficient sequence of $C_{1}$ must be computed. As illustrated in the previous example, $C_{1}$ contains only the rotations: $R_{1}=C(R_{Z}(-\rho_{1}+2\rho_{2}))$ and $R_{2}=C(R_{Z}(\rho_{1}-2\rho_{2}))$ . The coefficient sequences of these rotations are $\beta=(-1,2)$ and $\gamma=(1,-2)$ respectively. Then $A(C_{2})=A(R_{1})\cdot A(R_{2})=(\beta)\cdot(\gamma)=(\beta,\gamma)$ . Moreover, $\kappa(\beta)=\max\{0+2,1+0\}=2$ and $\kappa(\gamma)=\max\{1+0,0+2\}=2$ . By inspecting the matrices in Ex. 5.3, it is clear that the following bounds hold for all $j\in[2]$ and $s,t\in[4]$ .

	$\displaystyle\deg_{z_{j}}^{+}(([\![R_{1}]\!]_{\textsf{Poly}})_{s,t})$	$\displaystyle\leq\|\beta_{j}\|$	$\displaystyle\deg_{z_{j}}^{-}(([\![R_{1}]\!]_{\textsf{Poly}})_{s,t})$	$\displaystyle\leq\|\beta_{j}\|$	$\displaystyle\deg^{+}(([\![R_{1}]\!]_{\textsf{Poly}})_{s,t})$	$\displaystyle\leq\kappa(\beta)$
	$\displaystyle\deg_{z_{j}}^{+}(([\![R_{2}]\!]_{\textsf{Poly}})_{s,t})$	$\displaystyle\leq\|\gamma_{j}\|$	$\displaystyle\deg_{z_{j}}^{-}(([\![R_{2}]\!]_{\textsf{Poly}})_{s,t})$	$\displaystyle\leq\|\gamma_{j}\|$	$\displaystyle\deg^{+}(([\![R_{2}]\!]_{\textsf{Poly}})_{s,t})$	$\displaystyle\leq\kappa(\gamma)$

The $\kappa$ terms can be thought of as adding together the maximum positive degrees of the two terms in each sine or cosine polynomial It turns out that these bounds compose additively under the composition of matrices, motivating properties (B1) through to (B3). In this example $\sum_{\alpha\in A(C_{1})}|\alpha_{1}|=|-1|+|1|=2$ , $\sum_{\alpha\in A(C_{1})}|\alpha_{2}|=|2|+|-2|=4$ , and $\sum_{\alpha\in A(C_{1})}\kappa(\alpha)=2+2=4$ By inspecting the final matrix in Ex. 5.3, it is clear that the following bounds hold for all $s,t\in[4]$ where $f=([\![C_{1}]\!]_{\textsf{Poly}})_{s,t}$ .

\displaystyle\deg_{z_{1}}^{+}(f)

\displaystyle\leq 2

\displaystyle\deg_{z_{1}}^{-}(f)

\displaystyle\leq 2

\displaystyle\deg_{z_{2}}^{+}(f)

\displaystyle\leq 4

\displaystyle\deg_{z_{2}}^{-}(f)

\displaystyle\leq 4

\displaystyle\deg^{+}(f)

\displaystyle\leq 4

Then $C_{1}$ satisfies (B1) through to (B3). Therefore, $\textsf{Bnd}_{\textsf{Poly}}(C_{1})$ holds $\lrcorner$

This rationale given in Ex. 5.5 extends to all circuits in $\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ . Since primitive gates map to constant matrices, then they trivially satisfy $\textsf{Bnd}_{\textsf{Poly}}(-)$ . By construction of $\textsf{CPoly}(f)$ and $\textsf{SPoly}(f)$ , then rotation matrices also satisfy $\textsf{Bnd}_{\textsf{Poly}}(-)$ . It is then easy to show, using Prop. 3.2, that every gate in $\Sigma_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ satisfies $\textsf{Bnd}_{\textsf{Poly}}(-)$ . With a slightly more careful analysis, it can then be shown that this invariant is closed under sequential and parallel composition. Intuitively, both matrix multiplication and the Kronecker tensor product yields sums of products of polynomials, in which each term can be shown to satisfy the degree bounds. Then by Prop. 3.3, every circuit in $\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ also satisfies $\textsf{Bnd}_{\textsf{Poly}}(-)$ . Given these coefficient bounded semantics, the singularity factoring techniques of Sec. 4 can then be applied to obtain Cor. 5.7. All proof details can be found in the full paper.

Theorem 5.6.

If $C\in\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ , then $\textsf{Bnd}_{\textsf{Poly}}(C)$ .

Corollary 5.7.

If $C_{1}\in\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ and $C_{2}\in\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ with $\textsf{in}(C_{1})=\textsf{in}(C_{2})=n$ and $\textsf{out}(C_{1})=\textsf{out}(C_{2})=m$ , then for each pair of indices $s\in[2^{n}]$ and $t\in[2^{m}]$ , there exists a polynomial $f\in\mathbb{C}[x_{1},\ldots,x_{k}]$ such that,

$\blacksquare$

(D1). $\deg_{x_{j}}(f)\leq 2\lambda_{j}$ for each $j\in[k]$ ,
$\blacksquare$

(D2). $\deg(f)\leq\max\{\sum_{a\in A(C)}\kappa(a):C\in\{C_{1},C_{2}\}\}+\sum_{j=1}^{k% }\lambda_{j}$ ,
$\blacksquare$

(D3). $\left([\![C_{1}]\!]-[\![C_{2}]\!]\right)_{s,t}(\theta)=0$ if and only if $f(e^{-i\theta_{1}/2},\ldots,e^{-i\theta_{k}/2})=0$ ,

where $\lambda_{j}=\max\{\sum_{a\in A(C)}|a_{j}|:C\in\{C_{1},C_{2}\}\}$ for each $j\in[k]$ .

An interesting observation is that the bounds obtained through Thm. 5.6 were tight in Ex. 5.5. A natural question is whether these bounds are always tight, with respect to the granularity of the abstraction. We answer this question in the positive, by showing that for each coefficient sequence $\alpha$ , there exists a circuit $C$ with $A(C)=\alpha$ such that the corresponding bound is tight. Of course, it is not possible to reconstruct a circuit from its coefficient sequence, so some information must be lost. To this end, we exhibit a family of circuits in Ex. 5.9, each of degree zero, for which arbitrarily large bounds can be obtained. In this example, relations exist between the rotations that depend on the axes-of-rotation and the parameter-free gates in the circuit, both of which are not captured by the coefficient sequence. In particular, both examples rely on the relations $(R_{X}(\beta))(R_{X}(\gamma))=R_{X}(\beta+\gamma)$ and $Z(R_{X}(\beta))=(R_{X}(-\beta))Z$ .

(a) The circuit for

\alpha=((1,2),(0,-1))

.

(b)

(R_{X}(n\theta))\circ Z\circ(R_{X}(n\theta))

.

Figure 4: Circuits used in Ex. 5.8 and Ex. 5.9 to illustrate the precision of

\textsf{Bnd}(-)

.

Example 5.8 (Necessary Bounds).

Let $\alpha$ be any sequence over $\mathbb{Z}^{k}$ with $|\alpha|=n$ . For each $j\in[n]$ , define a linear function $f_{j}(\theta)=(\alpha_{j})_{1}\theta_{1}+\cdots+(\alpha_{j})_{k}\theta_{k}$ and a rotation gate $G_{j}=R_{X}(f_{j})$ . Now consider the circuit $C=G_{1}//\cdots//G_{n}$ (see Figure 4(a)). It follows that $A(C)=\alpha$ . Moreover, $([\![C]\!](\theta))_{0,0}=\prod_{j=1}^{n}\cos(f_{j}(\theta)/2)$ . With regard to the polynomial semantics, $[\![C]\!]_{\textsf{Poly}}=2^{-n}\prod_{a\in\alpha}(\prod_{j=1}^{k}z_{k}^{a_{j}% }-\prod_{j=1}^{k}z_{k}^{-a_{j}})$ . Clearly $\deg_{x_{j}}^{+}(([\![C]\!]_{\textsf{Poly}})_{0,0})=\sum_{a\in\alpha}|a_{j}|$ and $\deg_{x_{j}}^{-}(g)=\sum_{a\in\alpha}|a_{j}|$ for each $j\in[k]$ . Then $\textsf{Bnd}_{\textsf{Poly}}(C)$ is tight. Since $\alpha$ was arbitrary, then every coefficient sequence is realizable with tight bounds. $\lrcorner$

Example 5.9 (Impact of Circuit Relations).

Fix $k=1$ as the number of parameters and let $n\in\mathbb{N}$ . Consider the circuit $C=R_{X}(n\theta)\circ Z\circ R_{X}(n\theta)$ , as illustrated in Figure 4(b). It follows that $[\![C]\!](\theta)=(R_{X}(n\theta))Z(R_{X}(n\theta))=(R_{X}(n\theta))(R_{X}(-n% \theta))Z=R_{X}(0)Z=Z$ . Since $[\![C]\!](\theta)$ is constant, its associated polynomials have degree zero. However, $\textsf{Bnd}_{\textsf{Poly}}(C)$ yields an upper bound of $\sum_{a\in A(C)}|a_{1}|=|n|+|n|=2n$ , which exceeds the true degree by $2n$ . Since $n$ was arbitrary, this error can be made arbitrarily large. $\lrcorner$

5.2 A Cutoff Theorem for Parameterized Equivalence

This section shows that parameterized equivalence checking reduces to parameter-free equivalence checking for quantum circuits (Thm. 5.10). The proof proceeds as follows. First, Cor. 5.7 is used to characterize a family of polynomials which are identically zero if and only if the two circuits are equal. Using Thm. 2.1, a finite set of points $S\subseteq\mathbb{Q}^{k}$ can be constructed to determine if these polynomials are identically zero. The points in $S$ are in bijection with a set of points on the complex unit circle under the transformation $x\mapsto e^{-ix/2}$ . It follows that each polynomial is identically zero if and only if $[\![C_{1}]\!](s)=[\![C_{2}]\!](s)$ for all points $s\in S$ . Note that the polynomials are never explicitly constructed. All proof details are in the full paper.

Theorem 5.10.

Let $C_{1}\in\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ and $C_{2}\in\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ with $\textsf{in}(C_{1})=\textsf{in}(C_{2})$ and $\textsf{out}(C_{1})=\textsf{out}(C_{2})$ . If $S_{1},S_{2},\ldots,S_{k}\subseteq[0,4\pi)$ such that $|S_{j}|>2\lambda_{j}$ for each $j\in[k]$ , then $[\![C_{1}]\!](\theta)=[\![C_{2}]\!](\theta)$ for all $\theta\in\mathbb{R}^{k}$ if and only if $[\![C_{1}]\!](v)=[\![C_{2}]\!](v)$ for all $v\in S_{1}\times S_{2}\times\cdots\times S_{k}$ .

Corollary 5.11.

If $\mathcal{G}$ and $\mathcal{H}$ consist of matrices over the universal cyclotomic field, then the parameterized equivalence checking problem is decidable for $\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ .

As $k$ grows large, the utility of Thm. 5.10 decreases. For example, if each $\lambda_{j}$ is $b$ , then $|S_{1}\times\cdots\times S_{k}|=(2b+1)^{k}$ . That is, the number of instances grows exponentially with $k$ . However, this exponential growth can be overcome by a probabilistic algorithm. Fix a finite subset $S$ of $[0,4\pi)^{k}$ and assume that $s$ is chosen at random from $S$ . If $[\![C_{1}]\!](s)=[\![C_{2}]\!](s)$ , then conclude that $[\![C_{1}]\!]=[\![C_{2}]\!]$ , otherwise conclude that $[\![C_{2}]\!]\neq[\![C_{2}]\!]$ . Clearly, this algorithm has no false negatives, since $[\![C_{1}]\!](s)\neq[\![C_{2}]\!](s)$ implies $[\![C_{2}]\!]\neq[\![C_{2}]\!]$ . A more interesting question is the false positive rate. Note that a false positive occurs when $[\![C_{1}]\!](s)=[\![C_{2}]\!](s)$ but $[\![C_{1}]\!]\neq[\![C_{2}]\!]$ . It is shown in the following theorem that the probability of a false positive decreases with order $O(1/|S|)$ , as an application of Thm. 2.2.

Theorem 5.12.

Let $C_{1}\in\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ and $C_{2}\in\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ with $\textsf{in}(C_{1})=\textsf{in}(C_{2})$ , $\textsf{out}(C_{1})=\textsf{out}(C_{2})$ , and $[\![C_{1}]\!]\neq[\![C_{2}]\!]$ . For each finite subset $S\subseteq[0,4\pi)$ , if $s_{1},\ldots,s_{k}$ are sampled at random both independently and uniformly from $S$ , then

\Pr\left([\![C_{1}]\!](s_{1},\ldots,s_{k})=[\![C_{2}]\!](s_{1},\ldots,s_{k})% \right)\leq d/|S|

where $d=\max\{\sum_{\alpha\in A(C)}\kappa(\alpha):C\in\{C_{1},C_{2}\}\}+\sum_{j=1}^{% k}\lambda_{j}$ .

6 Extending to Rational Coefficients and Global Phase

The methods presented in Sec. 5 face several limitations. In particular, both Thm. 5.10 and Thm. 5.12 assume that the circuits are integral, and do not allow for equivalence up to global phase. In this section, we show how to extend the techniques of Sec. 5 to handle rational circuits and global phase. We also expand Thm. 5.12 into an algorithm, and consider the problem of angle sampling given a gate set over the universal cyclotomic field.

6.1 Verifying Circuits with Rational Coefficients

Most parameterized quantum circuits have fractional coefficients. For example, the equality in Figure 3 is typically stated with a parameter $\theta$ on the left-hand side and the parameters $\pm\theta/2$ on the right-hand side. The circuits in Figure 3 are related to these fractional circuits by the substitution $f(\theta)=\theta/2$ . Conceptually, $f:\mathbb{R}^{k}\to\mathbb{R}^{k}$ reparameterizes the circuit, by inducing a bijection between the parameter space of the rational circuits and the parameter space of the integral circuits. This generalizes to all examples (see the full paper for proofs).

Lemma 6.1.

Let $C_{1},C_{2}\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ . If $f:\mathbb{R}^{k}\to\mathbb{R}^{k}$ is a bijective function, then $[\![C_{1}]\!]=[\![C_{2}]\!]$ if and only if $[\![C_{1}]\!]\circ f=[\![C_{2}]\!]\circ f$ .

The goal of this section is to construct a syntactic transformation which eliminates all rational coefficients, which preserving the semantic interpretation via a bijective reparameterization. A syntactic reparameterization is a map $F:\textsf{Circ}(\mathcal{G},\mathcal{H})\to\textsf{Circ}(\mathcal{G},\mathcal{% H})$ with a bijective function $f:\mathbb{R}^{k}\to\mathbb{R}^{k}$ such that $[\![F(C)]\!]=[\![C]\!]\circ f$ . The simplest syntactic reparameterization is a linear rescaling of the parameters in the circuit by a non-zero rational vector. For each vector $v\in(\mathbb{Q}\setminus\{0\})^{k}$ , define the map $F_{v}:\textsf{Circ}(\mathcal{G},\mathcal{H})\to\textsf{Circ}(\mathcal{G},% \mathcal{H})$ as follows.

$\blacksquare$

If $G\in\mathcal{G}$ , then $F_{v}(G)=G$ .
$\blacksquare$

If $M\in\mathcal{H}$ and $f(\theta)=a_{1}\theta_{1}+a_{2}\theta_{2}+\cdots+a_{k}\theta_{k}+q$ , then $F_{v}(R_{M}(f))=R_{M}(g)$ where $g(\theta)=(v_{1}a_{1})\theta_{1}+(v_{2}a_{2})\theta_{2}+\cdots+(v_{k}a_{k})% \theta_{k}+q$ .
$\blacksquare$

If $G\in\Sigma(\mathcal{G},\mathcal{H})$ , then $F_{v}(C(G))=C(F_{v}(G))$ .
$\blacksquare$

If $C_{1},C_{2}\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ , then $F_{v}(C_{1}//C_{2})=F_{v}(C_{1})//F_{v}(C_{2})$ .
$\blacksquare$

If $C_{1},C_{2}\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ , then $F_{v}(C_{2}\circ C_{1})=F_{v}(C_{2})\circ F_{v}(C_{1})$ .

Theorem 6.2.

For each $v\in(\mathbb{Q}\setminus\{0\})^{k}$ , $f:\mathbb{R}^{k}\to\mathbb{R}^{k}$ defined by $f(\theta)=(v_{1}\theta_{1},v_{2}\theta_{2},\ldots,v_{k}\theta_{k})$ is bijective and $F_{v}$ is syntactic reparameterization with respect to $f$ .

Now assume that $C_{1}$ and $C_{2}$ are circuits in $\textsf{Circ}(\mathcal{G},\mathcal{H})$ . For the correct choice of $v$ , both $F_{v}(C_{1})$ and $F_{v}(C_{2})$ are elements of $\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ . Intuitively, each $v_{j}$ must be chosen such that it clears the denominators of all coefficients tied to $\theta_{k}$ in both $C_{1}$ and $C_{2}$ . Formally, let $\operatorname{denom}(q)$ denote the denominator of $q\in\mathbb{Q}$ and $\operatorname{lcm}\{x_{1},x_{2},\ldots,x_{n}\}$ denote the least common multiple of $x_{1},x_{2},\ldots,x_{n}\in\mathbb{Z}$ . Then for each $j\in[k]$ , $X_{j}=\{\operatorname{denom}(\alpha_{j}):\alpha\in A(C_{1})\cdot A(C_{2})\}$ is the set of all denominators of coefficients tied to $\theta_{k}$ in both $C_{1}$ and $C_{2}$ . Then $v_{j}=\operatorname{lcm}(X_{j})$ for each $j\in[k]$ . Let $\textsf{circLcm}(C_{1},C_{2})$ denote this vector.

Theorem 6.3.

If $C_{1},C_{2}\in\textsf{Circ}(\mathcal{G},\mathcal{H})$ and $v=\textsf{circLcm}(C_{1},C_{2})$ , then $F_{v}(C_{1})\in\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ and $F_{v}(C_{2})\in\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ . Moreover, $[\![C_{1}]\!]=[\![C_{2}]\!]$ if and only if $[\![F_{v}(C_{1})]\!]=[\![F_{v}(C_{2})]\!]$ .

Corollary 6.4.

If $\mathcal{G}$ and $\mathcal{H}$ consist of matrices over the universal cyclotomic field, then the parameterized equivalence checking problem is decidable for $\textsf{Circ}(\mathcal{G},\mathcal{H})$ .

6.2 Verifying Circuits Modulo Global Phase

In Sec. 5 the circuits $C_{1}$ and $C_{2}$ where defined to be equivalence when $[\![C_{1}]\!](\theta)=[\![C_{2}]\!](\theta)$ for all $\theta\in\mathbb{R}^{k}$ . For many applications, this notion of equivalence is far too strict. This is because $C_{1}$ and $C_{2}$ will prepare the same probability distribution provided there exists some function $p:\mathbb{R}^{k}\to\mathbb{R}$ such that $[\![C_{1}]\!](\theta)=e^{ip(\theta)}[\![C_{2}]\!](\theta)$ for all $\theta\in\mathbb{R}^{k}$ . When such a function exists, we say that $C_{1}$ and $C_{2}$ are equivalent modulo global phase. Of course, verifying the existence of an arbitrary $p$ is infeasible. Prior work has assumed $p$ to be affine linear [21, 38, 47]. That is, $p(\theta)=\alpha_{1}\theta_{1}+\cdots\alpha_{k}\theta_{k}+\beta$ . We further assume that $\alpha_{1}$ through to $\alpha_{k}$ are rational. In this section we show how to verify the equivalence of $C_{1}$ and $C_{2}$ modulo affine rational linear global phase, under the following assumptions.

1.

All matrices in $\mathcal{H}$ are defined over the universal cyclotomic field.
2.

All matrices in $\mathcal{G}$ are injective and defined over the universal cyclotomic field.

In practice, the second assumption restricts $\mathcal{G}$ to unitary operations and state preparation.

Since the universal cyclotomic field is closed under addition and multiplication, then every global phase will be cyclotomic when evaluated at rational multiples of $\pi$ . In general, $\alpha$ need not be rational, since there exists cyclotomic numbers of norm $1$ which are not roots of unity. However, the periodicity of $[\![C_{1}]\!]$ an $[\![C_{2}]\!]$ ensure that $\alpha\in\mathbb{Q}^{k}$ . Using properties of cyclotomic numbers, such as the fact that $\mathbb{Q}(\zeta_{2n})=\mathbb{Q}(\zeta_{n})$ for odd $n$ , it is then possible to solve for $\alpha$ (if it exists). In the full paper, an algorithm $\textsf{FindPhase}(C_{1},C_{2})$ is described to compute these coefficients. The injectivity of $\mathcal{G}$ ensures that all coefficients can be isolated (this condition is sufficient but not necessary). In the case where $C_{1}$ and $C_{2}$ are not equivalent up to global phase, then arbitrary coefficients are returned. Otherwise, the function $\textsf{FindPhase}(C_{1},C_{2})$ returns a tuple $(z,f)$ such that $z=e^{i\beta}$ and $f(\theta)=(-2\alpha_{1})\theta_{1}+\cdots+(-2\alpha_{k})\theta_{k}$ . Then the global phase can be offset by introducing a unitary gate $z I$ and a global phase gate $R_{I}(f)$ . Then equivalence modulo global phase reduces to exact equivalence as follows.

Theorem 6.5.

Assume $\mathcal{G}$ and $\mathcal{H}$ consist of matrices over the universal cyclotomic field, with all gates in $\mathcal{G}$ injective. If $C_{1},C_{2}\in\textsf{Circ}_{\mathbb{Z}}(\mathcal{G},\mathcal{H})$ and $(z,f)=\textsf{FindPhase}(C_{1},C_{2})$ , then $C_{1}$ is equivalent to $C_{2}$ modulo affine rational linear global phase if and only if the equation $[\![C_{1}]\!]=[\![zI\circ R_{I}(f)\circ C_{2}]\!]$ holds.

Corollary 6.6.

If $\mathcal{G}$ and $\mathcal{H}$ satisfy assumptions (1–2), then the parameterized equivalence checking problem is decidable modulo affine rational linear global phase for $\textsf{Circ}(\mathcal{G},\mathcal{H})$ .

6.3 A Probabilistic Equivalence Checking Procedure

Imagine applying Thm. 5.12 to a pair of quantum circuits $C_{1}$ and $C_{2}$ . In practice, an end-user would have some desired upper bound $p\in(0,1]$ on the false positive rate. A simply way to bound the false positive rate is to require that $d/|S|\leq p$ , meaning that $d/p\leq|S|$ . Since $d/p$ is positive and $|S|$ is a natural number, then the minimum value of $|S|$ which satisfies this inequality is $N=\lceil d/p\rceil$ . Using this optimal solution, the following algorithm is obtained.

1.

Compute $d=\max\{\sum_{\alpha\in A(C)}\kappa(\alpha):C\in\{C_{1},C_{2}\}\}+\sum_{j=1}^{% k}\lambda_{j}$ .
2.

Select a set $S\subseteq[0,4\pi)$ such that $|S|=\lceil d/p\rceil$ .
3.

Sample $s_{1},\ldots,s_{k}$ at random both independently and uniformly from $S$ .
4.

Determine if $[\![C_{1}]\!](s_{1},\ldots,s_{k})=[\![C_{2}]\!](s_{1},\ldots,s_{k})$ .

The most crucial step of this algorithm is the second step. First, the choice of $S$ must ensure that the values of $\sin(-)$ and $\cos(-)$ are exact. As outlined in Sec. 2.2, the simplest way to do this is to sample $S$ from $[0,4\pi)\cap\mathbb{Q}\pi$ for with for which $\sin(-)$ and $\cos(-)$ must evaluate to cyclotomic numbers. This method is particularly effective when $\mathcal{G}$ and $\mathcal{H}$ consists purely of matrices over the universal cyclotomic field, in which case all computation can be carried out over the universal cyclotomic field.

Now, consider the elements of $\sin(S)$ and $\cos(S)$ . For each $(j/n)\pi$ in $S$ , the elements $\sin(j/n)$ and $\cos(j/n)$ will be elements of $\mathbb{Q}[\zeta_{n}]$ . Likewise, if $\ell$ is the least common denominator of all fractions in $S$ , then $S\subseteq\mathbb{Q}[\zeta_{\ell}]$ . In the worst case, $\mathbb{Q}[\zeta_{\ell}]$ will be an $\ell$ -dimensional vector space. This means that the cost of addition will grow at least linearly with $\ell$ , and the cost of multiplication will grow at least quadratically with $\ell$ .

Theorem 6.7.

If $k\in\mathbb{N}$ , $S\subseteq[0,k)\cap\mathbb{Q}$ and $b=|S|$ , then $\operatorname{lcm}\{\operatorname{denom}(s):s\in S\}\geq\lceil b/k\rceil$ .

Let $M$ be the smallest multiple of $4$ which is greater than or equal to $N$ . It follows from Thm. 6.7 that $S=\{0,(1/M)4\pi,(2/M)4\pi,\ldots,((M-1)/M)4\pi\}$ minimizes $\ell$ . This set is also easy to compute, and is therefore taken to be the definition of $S$ .

7 Related Work

In the introduction, we discussed the cutoff-based techniques [32], which subsumes prior work such as [23]. In this section, we compare to other approaches.

Circuit Rewriting.

It was highlighted in Ex. 5.9 that circuit rewriting intersects with parameterized equivalence checking. In [38], an incomplete equational theory is given for a family of parameterized circuits, which is shown to be effective for equivalence checking. In [44], a complete set of relations are derived, under the assumption that each parameter appears exactly once in the circuit. Relations which hold for abstract gate sets, such as $\Sigma(\mathcal{G},\mathcal{H})$ , have yet to be explored.

Symbolic Techniques.

In [47], symbolic techniques are used to determine parameterized equivalence. Particularly, trigonometric relations, together with the Pythagorean relation $\cos(\theta)^{2}+\sin(\theta)^{2}=1$ , are used to reduce equivalence checking to a family of equations over the theory of non-linear real arithmetic. This is then solved using the Z3 [12] solver as a black box. However, the decision problem for non-linear real arithmetic is known to be double-exponential in the number of variables [24, 9], whereas our approach is exponential in the number of variables.

Probabilistic Techniques.

In [46], Thm. 2.2 was used to determine the equivalence of parameterized quantum circuits. However, our technique yields Laurent polynomials rather than ordinary polynomials, which we do not compute explicitly. In [38], Peham et al. show that if $v$ is sampled uniformly at random from $[0,4\pi)^{k}$ , then $\Pr([\![C_{1}]\!](v)=[\![C_{2}]\!](v))=0$ given $[\![C_{1}]\!]\neq[\![C_{2}]\!]$ . However, sampling $v$ from a uniform continuous distribution is impossible on a digital computer, which can only represent a countable and non-enumerable subset of real numbers [43]. In Peham et al., floating-point is used, and presumably, the error is assumed to be uniform as well. In our work, all computation is exact, and therefore, such assumptions do not apply. Since there does not exist a uniform distribution for countable sets, we instead sample uniformly from a finite subset of $[0,4\pi)$ , in which case Thm. 2.2 applies, rather than the analytic results of Peham et al.

8 Conclusion and Future Work

In this paper, we considered the problem of parameterized equivalence checking for quantum circuits. We show that the parameterized problem can be reduced to finitely many instances of the parameter-free problem, regardless of the gate set or axes of rotation. Consequently, the problem is decidable in the case of gate sets defined over the universal cyclotomic field. Moreover, we show that when the number of instances becomes intractable large, there exists a probabilistic variation of the algorithm where the probability of being incorrect can be made arbitrarily small. We have outlined how the techniques can be implemented in practice, taking into account rational coefficients, global phase, and angle sampling.

In future work, we would like to explore how these decision procedures can be implemented efficiently using circuit rewriting and sparse matrix representations. In particular, we would like to explore angle sampling and circuit evaluation using ZX-diagrams [37], tensor decision-diagrams [49], and model-counting [30], which have all proven effective in parameter-free equivalence checking. We would also like to explore how rewriting-based techniques and symmetry reductions might help to tighten the cutoffs obtained from $\textsf{Bnd}(-)$ . For example, the bound obtained in Ex. 5.9 could be reduced to zero by viewing each relation as a rewriting rule, and then searching for a derivation which reduces the bound.

References

[1] Amira Abbas, David Sutter, Christa Zoufal, Aurelien Lucchi, Alessio Figalli, and Stefan Woerner. The power of quantum neural networks. Nature Computational Science, 1(6):403–409, 2021. doi:10.1038/s43588-021-00084-1.
[2] Parosh Aziz Abdulla, Frédéric Haziza, and Lukás Holík. All for the price of few. In VMCAI, volume 7737 of LNCS, pages 476–495. Springer, 2013. doi:10.1007/978-3-642-35873-9_28.
[3] Noga Alon. Combinatorial Nullstellensatz. Combinatorics, Probability and Computing, 8(1–2):7–29, 1999. doi:10.1017/S0963548398003411.
[4] Matthew Amy, Andrew N. Glaudell, Shaun Kelso, William Maxwell, Samuel S. Mendelson, and Neil J. Ross. Exact synthesis of multiqubit Clifford-cyclotomic circuits. In RC, volume 14680 of LNCS, pages 238–245. Springer, 2024. doi:10.1007/978-3-031-62076-8_15.
[5] Davis Arthur and Prasanna Date. A hybrid quantum-classical neural network architecture for binary classification, 2022. arXiv:2201.01820.
[6] Martin Avanzini, Georg Moser, Romain Péchoux, and Simon Perdrix. On the hardness of analyzing quantum programs quantitatively. In Programming Languages and Systems, volume 14577 of LNCS, pages 31–58. Springer, 2024. doi:10.1007/978-3-031-57267-8_2.
[7] Sheldon Axler. Linear Algebra Done Right. Springer, 3rd edition, 2014. doi:10.1007/978-3-031-41026-0.
[8] John C. Baez, Brandon Coya, and Franciscus Rebro. Props in network theory. Theory and Applications of Categories, 33(25):727–783, 2010.
[9] Nikolaj Bjørne, Leonardo de Moura, Lev Nachmanson, and Christoph M. Wintersteiger. Programming Z3, volume 11430 of LNPSE, pages 148–201. Springer, 2019. doi:10.1007/978-3-030-17601-3_4.
[10] Wieb Bosma. Canonical bases for cyclotomic fields. Applicable Algebra in Engineering, Communication and Computing, 1:125–134, 1990. doi:10.1007/BF01810296.
[11] Thomas Breuer. Integral bases for subfields of cyclotomic fields. Applicable Algebra in Engineering, Communication and Computing, 8:279–289, 1997. doi:10.1007/s002000050065.
[12] Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008. doi:10.1007/978-3-540-78800-3_24.
[13] Richard A. Demillo and Richard J. Lipton. A probabilistic remark on algebraic program testing. Info. Proc. Letters, 7(4):193–195, 1978. doi:10.1016/0020-0190(78)90067-4.
[14] Qi-Ming Ding, Yi-Ming Huang, and Xiao Yuan. Molecular docking via quantum approximate optimization algorithm. Phys. Rev. Appl., 21:034036, 2024. doi:10.1103/PhysRevApplied.21.034036.
[15] Bryan Eastin and Emanuel Knill. Restrictions on transversal encoded quantum gate sets. Phys. Rev. Let., 102(11):110502, 2009. doi:10.1103/physrevlett.102.110502.
[16] E. Allen Emerson and Kedar S. Namjoshi. On reasoning about rings. Int. J. Found. Comput. Sci., 14(4):527–550, 2003. doi:10.1142/S0129054103001881.
[17] Richard M. Foote and David S. Dummit. Abstract Algebra. Wiley, 3rd edition, 2003.
[18] Brett Giles and Peter Selinger. Exact synthesis of multiqubit Clifford+ $T$ circuits. Phys. Rev. A, 87:032332, 2013. doi:10.1103/PhysRevA.87.032332.
[19] Dylan Herman, Cody Googin, Xiaoyuan Liu, Yue Sun, Alexey Galda, Ilya Safro, Marco Pistoia, and Yuri Alexeev. Quantum computing for finance. Nature Rev. Phys., 5(8):450–465, 2023. doi:10.1038/s42254-023-00603-1.
[20] Kesha Hietala, Robert Rand, Liyi Li, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. A verified optimizer for quantum circuits. ACM Trans. Program. Lang. Syst., 45(3), 2023. doi:10.1145/3604630.
[21] Xin Hong, Wei-Jia Huang, Wei-Chen Chien, Yuan Feng, Min-Hsiu Hsieh, Sanjiang Li, and Mingsheng Ying. Equivalence checking of parameterised quantum circuits, 2024. arXiv:2404.18456.
[22] C. Norris Ip and David L. Dill. Better verification through symmetry. In CHDL, volume A-32 of IFIP Transactions, pages 97–111. North-Holland, 1993. doi:10.5555/648251.752211.
[23] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. Diagrammatic reasoning beyond clifford+t quantum mechanics. In LICS. ACM, 2018. doi:10.1145/3209108.3209139.
[24] Dejan Jovanović and Leonardo de Moura. Solving non-linear arithmetic. In AR, volume 7364 of LNAI, pages 339–354. Springer, 2012. doi:10.1007/978-3-642-31365-3_27.
[25] Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Dynamic cutoff detection in parameterized concurrent programs. In CAV, volume 6174 of LNCS, pages 645–659. Springer, 2010. doi:10.1007/978-3-642-14295-6_55.
[26] Shu Kanno, Hajime Nakamura, Takao Kobayashi, Shigeki Gocho, Miho Hatanaka, Naoki Yamamoto, and Qi Gao. Quantum computing quantum Monte Carlo with hybrid tensor network for electronic structure calculations. npj Quantum Information, 10(1), 2024. doi:10.1038/s41534-024-00851-8.
[27] Ayrat Khalimov, Swen Jacobs, and Roderick Bloem. Towards efficient parameterized synthesis. In VMCAI, volume 7737 of LNCS, pages 108–127. Springer, 2013. doi:10.1007/978-3-642-35873-9_9.
[28] F. William Lawvere. Functorial semantics of algebraic theories. Proc. Natl. Acad. Sci. U.S.A., 50(5):869–872, 1963. doi:10.1073/pnas.50.5.869.
[29] He Ma, Govoni Marco, and Giulia Galli. Quantum simulations of materials on near-term quantum computers. npj Computational Materials, 6:85, 2020. doi:10.1038/s41524-020-00353-z.
[30] Jingyi Mei, Marcello Bonsangue, and Alfons Laarman. Simulating quantum circuits by model counting. In CAV, volume 14683 of LNCS, pages 555–578. Springer, 2024. doi:10.1007/978-3-031-65633-0_25.
[31] Dekel Meirom and Steven H. Frankel. PANSATZ: pulse-based ansatz for variational quantum algorithms. Frontiers in Quantum Science and Technology, 2, 2023. doi:10.3389/frqst.2023.1273581.
[32] Hector Miller-Bakewell. Finite verification of infinite families of diagram equations. EPTCS, 318:27–52, 2020. doi:10.4204/eptcs.318.3.
[33] Hector Miller-Bakewell. Graphical Calculi and their Conjecture Synthesis. PhD thesis, University of Oxford, 2020.
[34] Kedar S. Namjoshi and Richard J. Trefler. Parameterized compositional model checking. In TACAS, volume 9636 of LNCS, pages 589–606. Springer, 2016. doi:10.1007/978-3-662-49674-9_39.
[35] Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, 2011.
[36] Pyotr Novikov. On the algorithmic unsolvability of the word problem in group theory. Trudy Matematicheskogo Instituta imeni V.A. Steklova, 44:3–143, 1955.
[37] Tom Peham, Lukas Burgholzer, and Robert Wille. Equivalence checking of quantum circuits with the ZX-calculus. IEEE Journal on Emerging and Selected Topics in Circuits and Systems, 12(3):662–675, 2022. doi:10.1109/jetcas.2022.3202204.
[38] Tom Peham, Lukas Burgholzer, and Robert Wille. Equivalence checking of parameterized quantum circuits: Verifying the compilation of variational quantum algorithms. In ASPDAC, pages 702–708. ACM, 2023. doi:10.1145/3566097.3567932.
[39] Neil J. Ross and Scott Wesley. Cutoff theorems for the equivalence of parameterized quantum circuits (extended), 2025. arXiv:2506.20985.
[40] Raffaele Santagati, Alan Aspuru-Guzik, Ryan Babbush, Matthias Degroote, Leticia González, Elica Kyoseva, Nikolaj Moll, Markus Oppel, Robert M. Parrish, Nicholas C. Rubin, Michael Streif, Christofer S. Tautermann, Horst Weiss, Nathan Wiebe, and Clemens Utschig-Utschig. Drug design on quantum computers. Nature Phys., 20:549–557, 2024. doi:10.1038/s41567-024-02411-5.
[41] J. T. Schwartz. Fast probabilistic algorithms for verification of polynomial identities. J. ACM, 27(4):701–717, October 1980. doi:10.1145/322217.322225.
[42] Razin A. Shaikh, Quanlong Wang, and Richie Yeung. How to sum and exponentiate Hamiltonians in ZXW calculus. EPTCS, 394:236–261, 2023. doi:10.4204/eptcs.394.14.
[43] A. M. Turing. On computable numbers, with an application to the entscheidungsproblem. Proc. of the London Math. Soc., s2-42(1):230–265, 1937. doi:10.1112/plms/s2-42.1.230.
[44] John van de Wetering, Richie Yeung, Tuomas Laakkonen, and Aleks Kissinger. Optimal compilation of parametrised quantum circuits, 2024. doi:10.48550/arXiv.2401.12877.
[45] Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel. Verifying Solidity smart contracts via communication abstraction in SmartACE. In VMCAI, pages 425–449. Springer, 2022. doi:10.1007/978-3-030-94583-1_21.
[46] Amanda Xu, Abtin Molavi, Lauren Pick, Swamit Tannu, and Aws Albarghouthi. Synthesizing quantum-circuit optimizers. Proc. ACM Program. Lang., 7(PLDI), 2023. doi:10.1145/3591254.
[47] Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar, and Zhihao Jia. Quartz: superoptimization of quantum circuits. In PLDI, pages 625–640. ACM, 2022. doi:10.1145/3519939.3523433.
[48] Daniel Yoffe, Noga Entin, Amir Natan, and Adi Makmal. A qubit-efficient variational selected configuration-interaction method. Quantum Science and Technology, 10(1):015020, 2024. doi:10.1088/2058-9565/ad7d32.
[49] Qirui Zhang, Mehdi Saligane, Hun-Seok Kim, David Blaauw, Georgios Tzimpragos, and Dennis Sylvester. Quantum circuit simulation with fast tensor decision diagram. In ISQED, pages 1–8. IEEE, 2024. doi:10.1109/isqed60706.2024.10528748.
[50] Pengzhan Zhao, Zhongtao Miao, Shuhan Lan, and Jianjun Zhao. Bugs4Q: A benchmark of existing bugs to enable controlled testing and debugging studies for quantum programs. J. of Systems and Software, 205:111805, 2023. doi:10.1016/j.jss.2023.111805.
[51] Richard Zippel. Probabilistic algorithms for sparse polynomials. In EUROSAM, volume 72 of LNCS, pages 216–226. Springer, 1979. doi:10.1007/3-540-09519-5_73.

[bib.bib1] [1] Amira Abbas, David Sutter, Christa Zoufal, Aurelien Lucchi, Alessio Figalli, and Stefan Woerner. The power of quantum neural networks. Nature Computational Science, 1(6):403–409, 2021. doi:10.1038/s43588-021-00084-1.

[bib.bib2] [2] Parosh Aziz Abdulla, Frédéric Haziza, and Lukás Holík. All for the price of few. In VMCAI, volume 7737 of LNCS, pages 476–495. Springer, 2013. doi:10.1007/978-3-642-35873-9_28.

[bib.bib3] [3] Noga Alon. Combinatorial Nullstellensatz. Combinatorics, Probability and Computing, 8(1–2):7–29, 1999. doi:10.1017/S0963548398003411.

[bib.bib4] [4] Matthew Amy, Andrew N. Glaudell, Shaun Kelso, William Maxwell, Samuel S. Mendelson, and Neil J. Ross. Exact synthesis of multiqubit Clifford-cyclotomic circuits. In RC, volume 14680 of LNCS, pages 238–245. Springer, 2024. doi:10.1007/978-3-031-62076-8_15.

[bib.bib5] [5] Davis Arthur and Prasanna Date. A hybrid quantum-classical neural network architecture for binary classification, 2022. arXiv:2201.01820.

[bib.bib6] [6] Martin Avanzini, Georg Moser, Romain Péchoux, and Simon Perdrix. On the hardness of analyzing quantum programs quantitatively. In Programming Languages and Systems, volume 14577 of LNCS, pages 31–58. Springer, 2024. doi:10.1007/978-3-031-57267-8_2.

[bib.bib7] [7] Sheldon Axler. Linear Algebra Done Right. Springer, 3rd edition, 2014. doi:10.1007/978-3-031-41026-0.

[bib.bib8] [8] John C. Baez, Brandon Coya, and Franciscus Rebro. Props in network theory. Theory and Applications of Categories, 33(25):727–783, 2010.

[bib.bib9] [9] Nikolaj Bjørne, Leonardo de Moura, Lev Nachmanson, and Christoph M. Wintersteiger. Programming Z3, volume 11430 of LNPSE, pages 148–201. Springer, 2019. doi:10.1007/978-3-030-17601-3_4.

[bib.bib10] [10] Wieb Bosma. Canonical bases for cyclotomic fields. Applicable Algebra in Engineering, Communication and Computing, 1:125–134, 1990. doi:10.1007/BF01810296.

[bib.bib11] [11] Thomas Breuer. Integral bases for subfields of cyclotomic fields. Applicable Algebra in Engineering, Communication and Computing, 8:279–289, 1997. doi:10.1007/s002000050065.

[bib.bib12] [12] Leonardo de Moura and Nikolaj Bjørner. Z3: An efficient SMT solver. In TACAS, volume 4963 of LNCS, pages 337–340. Springer, 2008. doi:10.1007/978-3-540-78800-3_24.

[bib.bib13] [13] Richard A. Demillo and Richard J. Lipton. A probabilistic remark on algebraic program testing. Info. Proc. Letters, 7(4):193–195, 1978. doi:10.1016/0020-0190(78)90067-4.

[bib.bib14] [14] Qi-Ming Ding, Yi-Ming Huang, and Xiao Yuan. Molecular docking via quantum approximate optimization algorithm. Phys. Rev. Appl., 21:034036, 2024. doi:10.1103/PhysRevApplied.21.034036.

[bib.bib15] [15] Bryan Eastin and Emanuel Knill. Restrictions on transversal encoded quantum gate sets. Phys. Rev. Let., 102(11):110502, 2009. doi:10.1103/physrevlett.102.110502.

[bib.bib16] [16] E. Allen Emerson and Kedar S. Namjoshi. On reasoning about rings. Int. J. Found. Comput. Sci., 14(4):527–550, 2003. doi:10.1142/S0129054103001881.

[bib.bib17] [17] Richard M. Foote and David S. Dummit. Abstract Algebra. Wiley, 3rd edition, 2003.

[bib.bib18] [18] Brett Giles and Peter Selinger. Exact synthesis of multiqubit Clifford+ $T$ circuits. Phys. Rev. A, 87:032332, 2013. doi:10.1103/PhysRevA.87.032332.

[bib.bib19] [19] Dylan Herman, Cody Googin, Xiaoyuan Liu, Yue Sun, Alexey Galda, Ilya Safro, Marco Pistoia, and Yuri Alexeev. Quantum computing for finance. Nature Rev. Phys., 5(8):450–465, 2023. doi:10.1038/s42254-023-00603-1.

[bib.bib20] [20] Kesha Hietala, Robert Rand, Liyi Li, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. A verified optimizer for quantum circuits. ACM Trans. Program. Lang. Syst., 45(3), 2023. doi:10.1145/3604630.

[bib.bib21] [21] Xin Hong, Wei-Jia Huang, Wei-Chen Chien, Yuan Feng, Min-Hsiu Hsieh, Sanjiang Li, and Mingsheng Ying. Equivalence checking of parameterised quantum circuits, 2024. arXiv:2404.18456.

[bib.bib22] [22] C. Norris Ip and David L. Dill. Better verification through symmetry. In CHDL, volume A-32 of IFIP Transactions, pages 97–111. North-Holland, 1993. doi:10.5555/648251.752211.

[bib.bib23] [23] Emmanuel Jeandel, Simon Perdrix, and Renaud Vilmart. Diagrammatic reasoning beyond clifford+t quantum mechanics. In LICS. ACM, 2018. doi:10.1145/3209108.3209139.

[bib.bib24] [24] Dejan Jovanović and Leonardo de Moura. Solving non-linear arithmetic. In AR, volume 7364 of LNAI, pages 339–354. Springer, 2012. doi:10.1007/978-3-642-31365-3_27.

[bib.bib25] [25] Alexander Kaiser, Daniel Kroening, and Thomas Wahl. Dynamic cutoff detection in parameterized concurrent programs. In CAV, volume 6174 of LNCS, pages 645–659. Springer, 2010. doi:10.1007/978-3-642-14295-6_55.

[bib.bib26] [26] Shu Kanno, Hajime Nakamura, Takao Kobayashi, Shigeki Gocho, Miho Hatanaka, Naoki Yamamoto, and Qi Gao. Quantum computing quantum Monte Carlo with hybrid tensor network for electronic structure calculations. npj Quantum Information, 10(1), 2024. doi:10.1038/s41534-024-00851-8.

[bib.bib27] [27] Ayrat Khalimov, Swen Jacobs, and Roderick Bloem. Towards efficient parameterized synthesis. In VMCAI, volume 7737 of LNCS, pages 108–127. Springer, 2013. doi:10.1007/978-3-642-35873-9_9.

[bib.bib28] [28] F. William Lawvere. Functorial semantics of algebraic theories. Proc. Natl. Acad. Sci. U.S.A., 50(5):869–872, 1963. doi:10.1073/pnas.50.5.869.

[bib.bib29] [29] He Ma, Govoni Marco, and Giulia Galli. Quantum simulations of materials on near-term quantum computers. npj Computational Materials, 6:85, 2020. doi:10.1038/s41524-020-00353-z.

[bib.bib30] [30] Jingyi Mei, Marcello Bonsangue, and Alfons Laarman. Simulating quantum circuits by model counting. In CAV, volume 14683 of LNCS, pages 555–578. Springer, 2024. doi:10.1007/978-3-031-65633-0_25.

[bib.bib31] [31] Dekel Meirom and Steven H. Frankel. PANSATZ: pulse-based ansatz for variational quantum algorithms. Frontiers in Quantum Science and Technology, 2, 2023. doi:10.3389/frqst.2023.1273581.

[bib.bib32] [32] Hector Miller-Bakewell. Finite verification of infinite families of diagram equations. EPTCS, 318:27–52, 2020. doi:10.4204/eptcs.318.3.

[bib.bib33] [33] Hector Miller-Bakewell. Graphical Calculi and their Conjecture Synthesis. PhD thesis, University of Oxford, 2020.

[bib.bib34] [34] Kedar S. Namjoshi and Richard J. Trefler. Parameterized compositional model checking. In TACAS, volume 9636 of LNCS, pages 589–606. Springer, 2016. doi:10.1007/978-3-662-49674-9_39.

[bib.bib35] [35] Michael A. Nielsen and Isaac L. Chuang. Quantum Computation and Quantum Information. Cambridge University Press, 2011.

[bib.bib36] [36] Pyotr Novikov. On the algorithmic unsolvability of the word problem in group theory. Trudy Matematicheskogo Instituta imeni V.A. Steklova, 44:3–143, 1955.

[bib.bib37] [37] Tom Peham, Lukas Burgholzer, and Robert Wille. Equivalence checking of quantum circuits with the ZX-calculus. IEEE Journal on Emerging and Selected Topics in Circuits and Systems, 12(3):662–675, 2022. doi:10.1109/jetcas.2022.3202204.

[bib.bib38] [38] Tom Peham, Lukas Burgholzer, and Robert Wille. Equivalence checking of parameterized quantum circuits: Verifying the compilation of variational quantum algorithms. In ASPDAC, pages 702–708. ACM, 2023. doi:10.1145/3566097.3567932.

[bib.bib39] [39] Neil J. Ross and Scott Wesley. Cutoff theorems for the equivalence of parameterized quantum circuits (extended), 2025. arXiv:2506.20985.

[bib.bib40] [40] Raffaele Santagati, Alan Aspuru-Guzik, Ryan Babbush, Matthias Degroote, Leticia González, Elica Kyoseva, Nikolaj Moll, Markus Oppel, Robert M. Parrish, Nicholas C. Rubin, Michael Streif, Christofer S. Tautermann, Horst Weiss, Nathan Wiebe, and Clemens Utschig-Utschig. Drug design on quantum computers. Nature Phys., 20:549–557, 2024. doi:10.1038/s41567-024-02411-5.

[bib.bib41] [41] J. T. Schwartz. Fast probabilistic algorithms for verification of polynomial identities. J. ACM, 27(4):701–717, October 1980. doi:10.1145/322217.322225.

[bib.bib42] [42] Razin A. Shaikh, Quanlong Wang, and Richie Yeung. How to sum and exponentiate Hamiltonians in ZXW calculus. EPTCS, 394:236–261, 2023. doi:10.4204/eptcs.394.14.

[bib.bib43] [43] A. M. Turing. On computable numbers, with an application to the entscheidungsproblem. Proc. of the London Math. Soc., s2-42(1):230–265, 1937. doi:10.1112/plms/s2-42.1.230.

[bib.bib44] [44] John van de Wetering, Richie Yeung, Tuomas Laakkonen, and Aleks Kissinger. Optimal compilation of parametrised quantum circuits, 2024. doi:10.48550/arXiv.2401.12877.

[bib.bib45] [45] Scott Wesley, Maria Christakis, Jorge A. Navas, Richard Trefler, Valentin Wüstholz, and Arie Gurfinkel. Verifying Solidity smart contracts via communication abstraction in SmartACE. In VMCAI, pages 425–449. Springer, 2022. doi:10.1007/978-3-030-94583-1_21.

[bib.bib46] [46] Amanda Xu, Abtin Molavi, Lauren Pick, Swamit Tannu, and Aws Albarghouthi. Synthesizing quantum-circuit optimizers. Proc. ACM Program. Lang., 7(PLDI), 2023. doi:10.1145/3591254.

[bib.bib47] [47] Mingkuan Xu, Zikun Li, Oded Padon, Sina Lin, Jessica Pointing, Auguste Hirth, Henry Ma, Jens Palsberg, Alex Aiken, Umut A. Acar, and Zhihao Jia. Quartz: superoptimization of quantum circuits. In PLDI, pages 625–640. ACM, 2022. doi:10.1145/3519939.3523433.

[bib.bib48] [48] Daniel Yoffe, Noga Entin, Amir Natan, and Adi Makmal. A qubit-efficient variational selected configuration-interaction method. Quantum Science and Technology, 10(1):015020, 2024. doi:10.1088/2058-9565/ad7d32.

[bib.bib49] [49] Qirui Zhang, Mehdi Saligane, Hun-Seok Kim, David Blaauw, Georgios Tzimpragos, and Dennis Sylvester. Quantum circuit simulation with fast tensor decision diagram. In ISQED, pages 1–8. IEEE, 2024. doi:10.1109/isqed60706.2024.10528748.

[bib.bib50] [50] Pengzhan Zhao, Zhongtao Miao, Shuhan Lan, and Jianjun Zhao. Bugs4Q: A benchmark of existing bugs to enable controlled testing and debugging studies for quantum programs. J. of Systems and Software, 205:111805, 2023. doi:10.1016/j.jss.2023.111805.

[bib.bib51] [51] Richard Zippel. Probabilistic algorithms for sparse polynomials. In EUROSAM, volume 72 of LNCS, pages 216–226. Springer, 1979. doi:10.1007/3-540-09519-5_73.