Quantum computing promises to change the way we tackle certain problems in the future, however, developing applications for this new and upcoming technology has proven to be quite a challenge
Many tools and conveniences we take for granted today when developing classical circuits and systems (such as simulators, compilers, verification methods, debuggers, or high-level programming languages) are barely available to quantum developers. Due to this limited tool support and lack of automation methods for the design of quantum applications, developers need to conduct many of the tedious and error-prone design steps manually. It is estimated that developers for classical circuits and systems already spend roughly 75% of their time debugging. Without proper methods and tools, this is bound to get worse in quantum computing – motivating corresponding verification approaches.
The Subtlety of Bugs in Quantum Computing
In contrast to classical computing, where errors typically manifest themselves in the form of compiler errors or program crashes, bugs in quantum programs frequently are more subtle. A quantum program might have successfully run on a quantum computer, but the obtained results may be nowhere close to what the developer expected. Making matters worse, a recent study has shown that around 40% of all bugs encountered in developing quantum computing applications stem from the tools used for their development (e.g., for compilation and optimisation). This means that, when the code is not behaving as expected, there is a 4 out of 10 chance that this has nothing to do with the algorithm design itself or the programmer. Thus, days and days may be spent on debugging code without avail. It is crucial to provide quantum developers with automated methods to check that what is executed on the quantum computer still realizes the originally intended functionality.
Equivalence Checking of Quantum Circuits
Conceptually, checking the equivalence of two quantum circuits (e.g., the algorithmic description and the low-level implementation) is rather straightforward. The functionality of each gate g in a quantum circuit G is described by a (unitary) matrix U. Consequently, the functionality of a whole quantum circuit can be constructed by subsequently multiplying all individual gate matrices. Then, checking the equivalence of two circuits reduces to the comparison of the respectively obtained matrices. However, the size of the involved matrices grows exponentially concerning the number of qubits and, as a result, necessitates special data structures and methods for all but the most trivial cases.
Researchers at the Technical University of Munich, the Johannes Kepler University Linz, and the Software Competence Center Hagenberg are working on efficient techniques for this challenging problem. In their efforts, the computational paradigm of quantum computing and its technicalities are not seen as a burden, but rather as an opportunity. In classical computing, operations do not have to be reversible, i.e., it is not possible to compute the inputs to an operation from its outputs. For example, if the logical AND of a and b is 0, it is not possible to uniquely determine a and b. In contrast, every operation in quantum computing is inherently reversible.
This reversibility allows inverting a quantum circuit easily (by reversing the order of operations and inverting each operation). Combining the original circuit and the inverse of the other circuit allows reducing the question of whether two circuits are equivalent to the question of whether the combined circuit realises the identity function, i.e., the function where the output always equals the input. For many commonly used data structures, such as decision diagrams or tensor networks, the identity has a very compact representation. Thus, starting from this compact structure, an efficient way of checking whether both considered circuits are equivalent is to alternatingly apply gates from either circuit (G or G’–1) to stay as close as possible to the identity. If the identity results at the end of this procedure, the circuits in question are considered equivalent.
Moreover, in classical computing, the inevitable information loss introduced by many logic gates (such as observed for the AND gate above) frequently makes it hard to detect errors in classical circuits and systems. Thus, sophisticated schemes for constraint-based stimuli generation or fuzzing are necessary to adequately check the functionality of such systems. Again, quantum characteristics improve the situation considerably. Due to the reversibility, even small errors frequently impact the whole functionality of a quantum circuit. This makes probing quantum circuits with randomly chosen input states a feasible (and computationally less complex) alternative to checking the complete functionality as demonstrated above.
A First Step Towards Aiding Quantum Software Engineers
These complementary observations for checking the equivalence of quantum circuits form an advanced equivalence checking flow that is illustrated in Figure 1. The corresponding methods have been published and incorporated into open-source software available to all researchers and engineers in the field (see box above). The resulting tool natively integrates with IBM’s SDK Qiskit and can be used to verify that a high-level quantum circuit has been correctly compiled to a specific device using Qiskit. This provides users with the confidence that what is executed on the quantum computer is what was intended and that no error has been introduced through compilation.
Open-Source Software Tools
The tools described in this article are publicly available as open-source at https://github.com/cda-tum/qcec. Furthermore, a web-based graphical interface showcasing a lightweight visualisation of what is going on under the hood of the verification method can be accessed at https://www.cda.cit.tum.de/app/ddvis/. More details on the sketched concepts are provided at https://www.cda.cit.tum.de/research/quantum_verification/ and the papers linked there.
Please note: This is a commercial profile
