Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Springer eBooks

Equivalence Checking of Parameterized Quantum Circuits: Verifying the Compilation ofVariational Quantum Algorithms

Lukas Burgholzer, Robert Wille

Published Jan 1, 2026• 0 citations
Publisher
DOI
10.1007/978-3-032-06770-8_19

Related papers

Equivalence Checking of Quantum Protocols

Ebrahim Ardeshir-Larijani, Simon J. Gay, Rajagopal Nagarajan

Lecture notes in computer science•Jan 1, 2013•35 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.

arXiv:2210.12166•Asia and South Pacific Design Automation Conference (ASP-DAC)•Jan 16, 2023•27 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.

arXiv:2404.18456•Apr 29, 2024•1 citation

Model Checking for Verification of Quantum Circuits

Mingsheng Ying

arXiv:2104.11359•Lecture notes in computer science•Jan 1, 2021•15 citations

Equivalence checking of quantum finite-state machines

Qisheng Wang, Junyi Liu, Mingsheng Ying

arXiv:1901.02173•Journal of Computer and System Sciences•Sep 17, 2020•5 citations

Cutoff Theorems for the Equivalence of Parameterized Quantum Circuits

Ross, Neil J., Wesley, Scott

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.

•Jan 1, 2025•0 citations
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.
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.
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.