Verification of Quantum Circuits
In the not-so-distant future, quantum computing will change the way we tackle certain problems. It promises to dramatically speed-up many chemical, financial, cryptographical, and machine-learning applications. However, in order to capitalize on those promises, complex design flows composed of steps such as synthesis, mapping, or optimizations need to be employed before being able to execute a conceptual quantum algorithm on an actual device. This results in many descriptions at various levels of abstraction which may significantly differ from each other. The complexity of the underlying design problems makes it ever more important to not only provide efficient solutions for the single steps, but also to verify that the originally intended functionality is preserved throughout all levels of abstraction. This motivates methods for equivalence checking of quantum circuits. However, most existing methods for this are inspired by equivalence checking in the classical realm and have merely been extended to support quantum circuits (i.e., circuits which do not only rely on 0’s and 1’s, but also employ superposition and entanglement).
On this page, we summarize our work on the verification of quantum circuits which takes the different paradigms of quantum computing not only as a burden, but as an opportunity. To this end, we first introduce the developed advanced equivalence checking methodology; afterwards, we describe its application to the verification of compilation results, which clearly demonstrates its effectiveness.
All proposed methods have been implemented into the quantum circuit equivalence checking tool QCEC as part of the open-source Munich Quantum Toolkit (MQT; formerly known as JKQ). QCEC is also designed to natively integrate with IBM Qiskit. Moreover, in order to allow interested researchers and designers to quickly get an understanding of how decision diagrams can be employed for the simulation and verification of quantum circuits, we additionally provide an installation-free web-tool visualizing decision diagrams for quantum computing. In case of questions/problems, don’t hesitate to contact us via quantum.cda@xcit.tum.de, or by creating an issue on GitHub.
- To the Advanced Equivalence Checking Methodology »
- To the Verification of Compilation Flow Results »
- To the Integration with IBM Qiskit »
- To the MQT DDVis Online Tool »
Advanced Equivalence Checking Methodology
The proposed methodology explicitly utilizes characteristics unique to quantum computing in order to overcome the shortcomings of existing approaches. By exploiting the reversibility of quantum circuits, complexity can be kept feasible in many cases. Moreover, in contrast to the classical realm, simulation proves very powerful in verifying quantum circuits. The resulting methodology allows to conduct equivalence checking drastically faster than ever before—in many cases just a single simulation run is sufficient.
Details of the methodology are summarized in the paper entitled “Advanced Equivalence Checking for Quantum Circuits” [pdf].
If you use this tool for your research, we will be thankful if you refer to it by citing the following publication:
@article{burgholzer2020advanced,
author = {Burgholzer, Lukas and Wille, Robert},
title = {Advanced Equivalence Checking for Quantum Circuits},
year = 2021,
journaltitle = {{IEEE} Trans. on {CAD} of Integrated Circuits and Systems}
}
Verification of Compilation Flow Results
We propose an efficient scheme for quantum circuit equivalence checking—specialized for verifying results of the IBM Qiskit quantum circuit compilation flow. To this end, we combine characteristics unique to quantum computing, e.g., its inherent reversibility, and certain knowledge about the compilation flow into a dedicated equivalence checking strategy. Experimental evaluations confirm that the proposed scheme allows to verify even large circuit instances with tens of thousands of operations within seconds or even less, whereas state-of-the-art techniques frequently time-out or require substantially more runtime.
Details of the verification scheme are summarized in the paper entitled “Verifying Results of the IBM Qiskit Quantum Circuit Compilation Flow” [pdf].
If you use this verification scheme for your research, we will be thankful if you refer to it by citing the following publication:
@inproceedings{burgholzer2020verifyingResultsIBM,
title = {Verifying results of the {{IBM Qiskit}} quantum circuit compilation flow},
booktitle = {International Conference on Quantum Computing and Engineering},
author = {Burgholzer, Lukas and Raymond, Rudy and Wille, Robert},
year = {2020}
}
Integration with IBM Qiskit
The MQT QCEC tool is designed to natively integrate with IBM Qiskit. After installing the tool using pip install mqt.qcec, verifying the results of IBM Qiskit’s quantum circuit compilation flow is as easy as running the following Python script:
from mqt import qcec
from qiskit import QuantumCircuit, transpile
# create your quantum circuit
qc = <...>
# append measurements to save output mapping of physical to logical (qu)bits
qc.measure_all()
# compile circuit to appropriate backend using some optimization level
qc_comp = transpile(qc, backend=<...>, optimization_level=<0 | 1 | 2 | 3>)
# initialize the equivalence checker
ecm = qcec.EquivalenceCheckingManager(qc, qc_comp)
# execute the check
ecm.run()
# obtain the result
print(ecm.equivalence())
MQT DDVis Online Tool
In an effort to make decision diagrams for quantum computing more accessible, we present MQT DDVis—an installation-free web-tool which visualizes quantum decision diagrams and allows to explore their behavior when used in design tasks such as simulation, synthesis, and verification.
MQT Bench Online Tool
To evaluate the correspondingly developed methods, we additionally provide the benchmark suite MQT Bench comprising more than 70,000 benchmark circuits ranging from 2 up to 130 qubits on four abstraction levels.
