The quantum circuit model is the most widely used theoretical model for quantum computing. Therefore, determining whether two quantum circuits whose internal structures cannot be seen have the same functionality will be a fundamental problem in future quantum industries, which however turns out to be QMA-hard. Here, based on a photonic system we experimentally implement the equivalence checking of two unknown quantum circuits with real unitary matrix representations, where quantum nonlocality plays a key role and allows us to measure an "average-case" distance between the two quantum circuits very efficiently. Particularly, we also experimentally apply such protocols to verify the correctness of quantum circuit optimizations, which is another crucial topic in future quantum industries. Our work constitutes a proof of concept for the equivalence checking of quantum circuits without relying on their detailed structures.
The quantum circuit model is the most widely used theoretical model for quantum computing. Therefore, determining whether two quantum circuits whose internal structures cannot be seen have the same functionality will be a fundamental problem in future quantum industries, which however turns out to be QMA-hard. Here, based on a photonic system we experimentally implement the equivalence checking of two unknown quantum circuits with real unitary matrix representations, where quantum nonlocality plays a key role and allows us to measure an "average-case" distance between the two quantum circuits very efficiently. Particularly, we also experimentally apply such protocols to verify the correctness of quantum circuit optimizations, which is another crucial topic in future quantum industries. Our work constitutes a proof of concept for the equivalence checking of quantum circuits without relying on their detailed structures.
Abstract Suppose two quantum circuit chips are located at different places, for which we do not have any prior knowledge, and cannot see the internal structures either. In such a situation, a realistic and fundamental problem is to find out whether they have the same functions or not with certainty. In this paper, we show that this problem can be solved completely from the viewpoint of quantum nonlocality. Specifically, we design an elegant protocol that examines underlying quantum nonlocality, where the strongest nonlocality can be observed if and only if two quantum circuits are equivalent to each other. We show that the protocol also works approximately, where the distance between two quantum circuits can be calculated accurately by observing quantum nonlocality in an analytical manner. Furthermore, it turns out that the computational cost of our protocol is independent of the size of compared quantum circuits. Lastly, we also discuss the possibility to generalize the protocol to multipartite cases, i.e., if we do equivalence checking for multiple quantum circuits, we try to solve the problem in one go.
Suppose two quantum circuit chips are located at different places, for which we do not have any prior knowledge, and cannot see the internal structures either. If we want to find out whether they have the same functions or not with certainty, what should we do? In this paper, we show that this realistic problem can be solved from the viewpoints of quantum nonlocality. Specifically, we design an elegant protocol that examines underlying quantum nonlocality. We prove that in the protocol the strongest nonlocality can be observed if and only if two quantum circuits are equivalent to each other. We show that the protocol also works approximately, where the distance between two quantum circuits can be lower and upper bounded analytically by observed quantum nonlocality. Furthermore, we also discuss the possibility to generalize the protocol to multipartite cases, i.e., if we do equivalence checking for multiple quantum circuits, we try to solve the problem in one go. Our work introduces a nontrivial application of quantum nonlocality in quantum engineering.
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 compilation, decomposition, mapping, or transpilation 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). In this work, we propose an advanced methodology that takes the different paradigms of quantum circuits not only as a burden but as an opportunity. In fact, the proposed methodology explicitly utilizes characteristics unique to quantum computing in order to overcome the shortcomings of existing approaches. We show that by exploiting the reversibility of quantum circuits, complexity can be kept feasible in many cases. Moreover, we show that, in contrast to the classical realm, simulation is very powerful in verifying quantum circuits. Experimental evaluations confirm that the resulting methodology allows one to conduct equivalence checking dramatically faster than ever before-in many cases just a single simulation run is sufficient. An implementation of the proposed equivalence checking flow is publicly available at https://iic.jku.at/eda/research/quantum_verification/.
Equivalence checking of hybrid quantum circuits is of primary importance, given that quantum circuit transformations are omnipresent along the quantum compiler chain. While some approaches exist for automating this task, most focus on the simple case of unitary circuits. At the same time, real quantum computing requires hybrid circuits equipped with measurement operators. Moreover, the few approaches targeting the hybrid case are limited to a restricted class of problems. We propose tackling the Quantum Hybrid Circuit Equivalence Checking problem through lifting unitary circuit verification using a transformation known as deferred measurement. We show that this approach alone significantly outperforms prior work, and that, with the addition of specific unitary-level techniques we call separation and projection, it can handle much larger classes of hybrid circuit equivalence problems. We have implemented and evaluated our method over standard circuit transformations such as teleportation, one-way measurement, or the IBM Qiskit compiler, demonstrating its promises. As a side finding, we have identified and reported several unexpected behaviours with the Qiskit compiler.
As state-of-the-art quantum computers are capable of running increasingly complex algorithms, the need for automated methods to design and test potential applications rises. Equivalence checking of quantum circuits is an important, yet hardly automated, task in the development of the quantum software stack. Recently, new methods have been proposed that tackle this problem from widely different perspectives. However, there is no established baseline on which to judge current and future progress in equivalence checking of quantum circuits. In order to close this gap, we conduct a detailed case study of two of the most promising equivalence checking methodologies---one based on decision diagrams and one based on the ZX-calculus---and compare their strengths and weaknesses.
As quantum computing advances, the complexity of quantum circuits is rapidly increasing, driving the need for robust methods to aid in their design. Equivalence checking plays a vital role in identifying errors that may arise during compilation and optimization of these circuits and is a critical step in quantum circuit verification. In this work, we introduce a method based on matrix product operators (MPOs) for determining the equivalence of quantum circuits. Our approach contracts tensorized quantum gates from two circuits into an intermediary MPO, exploiting their reversibility to determine their equivalence or nonequivalence. Our results show that this method offers significant scalability improvements over existing methods, with polynomial scaling in circuit width and depth for the practical use cases we explore. We expect that this work to set a standard for scalable equivalence checking of quantum circuits and will become a crucial tool for the validation of increasingly complex quantum systems.