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.
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.
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.
Quantum computers and quantum algorithms have made great strides in the last few years and promise improvements over classical computing for specific tasks. Although the current hardware is not yet ready to make real impacts at the time of writing, this will change over the coming years. To be ready for this, it is important to share knowledge of quantum computing in application domains where it is not yet represented. One such application is the verification of classical circuits, specifically, equivalence checking. Although this problem has been investigated over decades in an effort to overcome the verification gap, how it can potentially be solved using quantum computing has hardly been investigated yet. In this work, we address this question by considering a presumably straightforward approach: Using Grover's algorithm. However, we also show that, although this might be an obvious choice, there are several pitfalls to avoid in order to get meaningful results. This leads to the proposal of a working concept of a quantum computing methodology for equivalent checking providing the foundation for corresponding solutions in the (near) future.
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.
Among the post-CMOS technologies currently under investigation, quantum computing (QC) holds a special place. QC offers not only extremely small size and low power, but also exponential speed-ups for important simulation and optimization problems. It also poses new CAD problems that are similar to. but more challenging, than the related problems in classical (non-quantum) CAD. such as determining if two states or circuits are functionally equivalent. While differences in classical states are easy to detect, quantum states, which are represented by complex-valued vectors, exhibit subtle differences leading to several notions of equivalence. This provides flexibility in optimizing quantum circuits, but leads to difficult new equivalence-checking issues for simulation and synthesis. We identify several different equivalence-checking problems and present algorithms for practical benchmarks, including quantum communication and search circuits, which are shown to be very fast and robust for hundreds of qubits.