Equivalence Checking of Parameterized Quantum Circuits: Verifying the Compilation of Variational Quantum Algorithms
arXiv:2210.12166 · doi:10.1145/3566097.3567932
Abstract
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. The implementation is open source and publicly available as part of the equivalence checking tool QCEC (https://github.com/cda-tum/qcec) which is part of the Munich Quantum Toolkit (MQT).
7 pages, 3 figures, 2 tables, 28th Asia and South Pacific Design Automation Conference (ASPDAC '23)
References in corpus (5)
- Quantum computational advantage using photons
- Provably efficient machine learning for quantum many-body problems
- Verifying Results of the IBM Qiskit Quantum Circuit Compilation Flow
- ReQWIRE: Reasoning about Reversible Quantum Circuits
- Efficient Construction of Functional Representations for Quantum Algorithms
Cited by in corpus (6)
- MQT Bench: Benchmarking Software and Design Automation Tools for Quantum Computing
- The MQT Handbook: A Summary of Design Automation Tools and Software for Quantum Computing
- On the need for effective tools for debugging quantum programs
- Optimizing ZX-Diagrams with Deep Reinforcement Learning
- Verifying Fault-Tolerance of Quantum Error Correction Codes
- Equivalence Checking of Quantum Circuits via Path-Sum and Weighted Model Counting