Cutoff Theorems for the Equivalence of Parameterized Quantum Circuits

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.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.

arXiv:2506.20985Jun 26, 20250 citations

Equivalence Checking of Parameterized Quantum Circuits

Tom Peham, Lukas Burgholzer, Robert Wille

Variational quantum algorithms have been introduced as a promising class of quantum-classical hybrid algorithms that can already be used with the noisy quantum computing hardware available today by employing parameterized quantum circuits. Considering the non-trivial nature of quantum circuit compilation and the subtleties of quantum computing, it is essential to verify that these parameterized circuits have been compiled correctly. Established equivalence checking procedures that handle parameter-free circuits already exist. However, no methodology capable of handling circuits with parameters has been proposed yet. This work fills this gap by showing that verifying the equivalence of parameterized circuits can be achieved in a purely symbolic fashion using an equivalence checking approach based on the ZX-calculus. At the same time, proofs of inequality can be efficiently obtained with conventional methods by taking advantage of the degrees of freedom inherent to parameterized circuits. We implemented the corresponding methods and proved that the resulting methodology is complete. Experimental evaluations (using the entire parametric ansatz circuit library provided by Qiskit as benchmarks) demonstrate the efficacy of the proposed approach.Variational quantum algorithms have been introduced as a promising class of quantum-classical hybrid algorithms that can already be used with the noisy quantum computing hardware available today by employing parameterized quantum circuits. Considering the non-trivial nature of quantum circuit compilation and the subtleties of quantum computing, it is essential to verify that these parameterized circuits have been compiled correctly. Established equivalence checking procedures that handle parameter-free circuits already exist. However, no methodology capable of handling circuits with parameters has been proposed yet. This work fills this gap by showing that verifying the equivalence of parameterized circuits can be achieved in a purely symbolic fashion using an equivalence checking approach based on the ZX-calculus. At the same time, proofs of inequality can be efficiently obtained with conventional methods by taking advantage of the degrees of freedom inherent to parameterized circuits. We implemented the corresponding methods and proved that the resulting methodology is complete. Experimental evaluations (using the entire parametric ansatz circuit library provided by Qiskit as benchmarks) demonstrate the efficacy of the proposed approach.

arXiv:2210.12166Asia and South Pacific Design Automation Conference (ASP-DAC)Jan 16, 202327 citations

Equivalence Checking of Parameterised Quantum Circuits

Xin Hong, Wei‐Jia Huang, Wei‐Chen Chien +4 more

Parameterised quantum circuits (PQCs) hold great promise for demonstrating quantum advantages in practical applications of quantum computation. Examples of successful applications include the variational quantum eigensolver, the quantum approximate optimisation algorithm, and quantum machine learning. However, before executing PQCs on real quantum devices, they undergo compilation and optimisation procedures. Given the inherent error-proneness of these processes, it becomes crucial to verify the equivalence between the original PQC and its compiled or optimised version. Unfortunately, most existing quantum circuit verifiers cannot directly handle parameterised quantum circuits; instead, they require parameter substitution to perform verification. In this paper, we address the critical challenge of equivalence checking for PQCs. We propose a novel compact representation for PQCs based on tensor decision diagrams. Leveraging this representation, we present an algorithm for verifying PQC equivalence without the need for instantiation. Our approach ensures both effectiveness and efficiency, as confirmed by experimental evaluations. The decision-diagram representations offer a powerful tool for analysing and verifying parameterised quantum circuits, bridging the gap between theoretical models and practical implementations.Parameterised quantum circuits (PQCs) hold great promise for demonstrating quantum advantages in practical applications of quantum computation. Examples of successful applications include the variational quantum eigensolver, the quantum approximate optimisation algorithm, and quantum machine learning. However, before executing PQCs on real quantum devices, they undergo compilation and optimisation procedures. Given the inherent error-proneness of these processes, it becomes crucial to verify the equivalence between the original PQC and its compiled or optimised version. Unfortunately, most existing quantum circuit verifiers cannot directly handle parameterised quantum circuits; instead, they require parameter substitution to perform verification. In this paper, we address the critical challenge of equivalence checking for PQCs. We propose a novel compact representation for PQCs based on tensor decision diagrams. Leveraging this representation, we present an algorithm for verifying PQC equivalence without the need for instantiation. Our approach ensures both effectiveness and efficiency, as confirmed by experimental evaluations. The decision-diagram representations offer a powerful tool for analysing and verifying parameterised quantum circuits, bridging the gap between theoretical models and practical implementations.

arXiv:2404.18456Apr 29, 20241 citation

Optimizing Parameterized Quantum Circuits with Free-Axis Selection

Hiroshi C Watanabe, Rudy Raymond, Yu‐ya Ohnishi +2 more

Parameterized quantum circuits (PQCs), which are essential for variational quantum algorithms, have conventionally been optimized by parameterized rotational angles of single-qubit gates around predetermined set of axes. We propose a new method to optimize a PQC by continuous parameterization of both the angles and the axes of its single-qubit rotations. The method is based on the observation that when rotational angles are fixed, optimal axes of rotations can be computed by solving a system of linear equations whose coefficients can be determined from the PQC with small computational overhead. The method can be further simplified to select axes freely from continuous parameters with rotational angles fixed to π. We show the simplified free-axis selection method has better expressibility against other structural optimization methods when measured with Kullback-Leibler (KL) divergence. We also demonstrate PQCs with free-axis selection are more effective to search the ground states of Heisenberg models and molecular Hamiltoni- ans. Because free-axis selection allows designing PQCs without specifying their single-qubit rotational axes, it may significantly improve the handiness of PQCs.Parameterized quantum circuits (PQCs), which are essential for variational quantum algorithms, have conventionally been optimized by parameterized rotational angles of single-qubit gates around predetermined set of axes. We propose a new method to optimize a PQC by continuous parameterization of both the angles and the axes of its single-qubit rotations. The method is based on the observation that when rotational angles are fixed, optimal axes of rotations can be computed by solving a system of linear equations whose coefficients can be determined from the PQC with small computational overhead. The method can be further simplified to select axes freely from continuous parameters with rotational angles fixed to π. We show the simplified free-axis selection method has better expressibility against other structural optimization methods when measured with Kullback-Leibler (KL) divergence. We also demonstrate PQCs with free-axis selection are more effective to search the ground states of Heisenberg models and molecular Hamiltoni- ans. Because free-axis selection allows designing PQCs without specifying their single-qubit rotational axes, it may significantly improve the handiness of PQCs.

arXiv:2104.14875IEEE International Conference on Quantum Computing and Engineering (QCE)Oct 1, 202114 citations

Optimizing Parameterized Quantum Circuits With Free-Axis Single-Qubit Gates

Hiroshi C Watanabe, Rudy Raymond, Yu‐ya Ohnishi +2 more

Variational quantum algorithms, which utilize Parametrized Quantum Circuits (PQCs), are promising tools to achieve quantum advantage for optimization problems on near-term quantum devices. Their PQCs have been conventionally constructed from parametrized rotational angles of single-qubit gates around predetermined set of axes, and two-qubit entangling gates, such as CNOT gates. We propose a method to construct a PQC by continuous parametrization of both the angles and the axes of its single-qubit rotation gates. The method is based on the observation that when rotational angles are fixed, optimal axes of rotations can be computed by solving a system of linear equations whose coefficients can be determined from the PQC with small computational overhead. The method can be further simplified to select axes freely from continuous parameters with rotational angles fixed to $\pi$ . We show the simplified free-axis selection method has better expressibility against other structural optimization methods when measured with Kullback-Leibler (KL) divergence. We also demonstrate PQCs with free-axis selection are more effective to search the ground states of Hamiltonians for condensed matter physics, quantum chemistry and combinatorial optimization. Because free-axis selection allows designing PQCs without specifying their single-qubit rotational axes, it may significantly improve the handiness of PQCs.Variational quantum algorithms, which utilize Parametrized Quantum Circuits (PQCs), are promising tools to achieve quantum advantage for optimization problems on near-term quantum devices. Their PQCs have been conventionally constructed from parametrized rotational angles of single-qubit gates around predetermined set of axes, and two-qubit entangling gates, such as CNOT gates. We propose a method to construct a PQC by continuous parametrization of both the angles and the axes of its single-qubit rotation gates. The method is based on the observation that when rotational angles are fixed, optimal axes of rotations can be computed by solving a system of linear equations whose coefficients can be determined from the PQC with small computational overhead. The method can be further simplified to select axes freely from continuous parameters with rotational angles fixed to$\pi$. We show the simplified free-axis selection method has better expressibility against other structural optimization methods when measured with Kullback-Leibler (KL) divergence. We also demonstrate PQCs with free-axis selection are more effective to search the ground states of Hamiltonians for condensed matter physics, quantum chemistry and combinatorial optimization. Because free-axis selection allows designing PQCs without specifying their single-qubit rotational axes, it may significantly improve the handiness of PQCs.

IEEE Transactions on Quantum EngineeringJan 1, 202314 citations

Parameterized Verification of Quantum Circuits (Technical Report)

Parosh Aziz Abdulla, Yu‐Fang Chen, Michal Hečko +4 more

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

arXiv:2511.19897Nov 25, 20250 citations

\pi

. We show the simplified free-axis selection method has better expressibility against other structural optimization methods when measured with Kullback-Leibler (KL) divergence. We also demonstrate PQCs with free-axis selection are more effective to search the ground states of Hamiltonians for condensed matter physics, quantum chemistry and combinatorial optimization. Because free-axis selection allows designing PQCs without specifying their single-qubit rotational axes, it may significantly improve the handiness of PQCs.