Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Log inSign up
Challenges
Datasets
Workspaces
Papers
Discussions
Leaderboard
Blog
Job Board
Q3AS

© 2026 Aqora Quantum S.A.S.

TermsPrivacyLegal Notice

Black-box equivalence checking of quantum circuits by nonlocality

Weixiao Sun, Zhaohui Wei

Published May 6, 2021• 0 citations
OpenAlex

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. 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.

Related papers

Equivalence checking of quantum circuits by nonlocality

Weixiao Sun, Zhaohui Wei

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.

arXiv:2105.02634•npj Quantum Information•Nov 29, 2022•3 citations

Experimental Equivalence Checking of Quantum Circuits by Nonlocality

Hao Tang, Yu Guo, Weixiao Sun +7 more

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.

Physical Review Letters•Dec 23, 2024•1 citation

Partial Equivalence Checking of Quantum Circuits

Tian-Fu Chen, Jie-Hong Roland Jiang, Min-Hsiu Hsieh

Equivalence checking of quantum circuits is an essential element in quantum program compilation, in which a quantum program can be synthesized into different quantum circuits that may vary in the number of qubits, initialization requirements, and output states. Verifying the equivalences among the implementation variants requires proper generality. Although different notions of quantum circuit equivalence have been defined, prior methods cannot check observational equivalence between two quantum circuits whose qubits are partially initialized, which is referred to as partial equivalence. In this work, we prove a necessary and sufficient condition for two circuits to be partially equivalent. Based on the condition, we devise algorithms for checking quantum circuits whose partial equivalence cannot be verified by prior approaches. Experiment results confirm the generality and demonstrate the efficiency and effectiveness of our method. Our result may unleash the optimization power of quantum program compilation to take more aggressive steps.

arXiv:2208.07564•IEEE International Conference on Quantum Computing and Engineering (QCE)•Sep 1, 2022•17 citations

Equivalence checking paradigms in quantum circuit design

Tom Peham, Lukas Burgholzer, Robert Wille

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.

ACM/IEEE Design Automation Conference (DAC)•Jul 10, 2022•16 citations

Quantum Circuit Equivalence Checking: A Tractable Bridge From Unitary to Hybrid Circuits

Jérome Ricciardi, Sébastien Bardin, Christophe Chareton +1 more

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.

quant-pharXiv:2511.22523•Nov 28, 2025•1 citation

Towards Equivalence Checking of Classical Circuits Using Quantum Computing

Nils Quetschlich, Tobias V. Forster, Adrian Osterwind +2 more

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.

arXiv:2408.14539•IEEE International Conference on Quantum Computing and Engineering (QCE)•Sep 15, 2024•5 citations
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.
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.
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.
Equivalence checking of quantum circuits is an essential element in quantum program compilation, in which a quantum program can be synthesized into different quantum circuits that may vary in the number of qubits, initialization requirements, and output states. Verifying the equivalences among the implementation variants requires proper generality. Although different notions of quantum circuit equivalence have been defined, prior methods cannot check observational equivalence between two quantum circuits whose qubits are partially initialized, which is referred to as partial equivalence. In this work, we prove a necessary and sufficient condition for two circuits to be partially equivalent. Based on the condition, we devise algorithms for checking quantum circuits whose partial equivalence cannot be verified by prior approaches. Experiment results confirm the generality and demonstrate the efficiency and effectiveness of our method. Our result may unleash the optimization power of quantum program compilation to take more aggressive steps.
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.
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.
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.