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.
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.
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/.
In the era of noisy intermediate-scale quantum devices, the number of controllable hardware qubits is insufficient to implement quantum error correction.As an alternative, quantum error mitigation (QEM) can suppress errors in measurement results via repeated experiments and postprocessing of data.Typical techniques for error mitigation, e.g., the quasiprobability decomposition method, ignore correlated errors between different gates.Here, we introduce a QEM method based on the matrix product operator (MPO) representation of a quantum circuit that can characterize the noise channel with polynomial complexity.Our technique is demonstrated on a depth = 20 fully parallel quantum circuit of up to N q = 20 qubits undergoing local and global noise.The circuit error is reduced by a several-times factor with only a small bond dimension D = 1 for the noise channel.The MPO representation increases the accuracy of modeling noise without consuming more experimental resources, which improves the QEM performance and broadens its scope of application.Our method is hopeful of being applied to circuits in higher dimensions with more qubits and deeper depth.
Parameterised quantum circuits (PQCs) hold great promise for demonstrating quantum advantages in practical applications of quantum computation. Examples of successful applications include the variational quantum eigensolver, the quantum approximate optimisation algorithm, and quantum machine learning. However, before executing PQCs on real quantum devices, they undergo compilation and optimisation procedures. Given the inherent error-proneness of these processes, it becomes crucial to verify the equivalence between the original PQC and its compiled or optimised version. Unfortunately, most existing quantum circuit verifiers cannot directly handle parameterised quantum circuits; instead, they require parameter substitution to perform verification. In this paper, we address the critical challenge of equivalence checking for PQCs. We propose a novel compact representation for PQCs based on tensor decision diagrams. Leveraging this representation, we present an algorithm for verifying PQC equivalence without the need for instantiation. Our approach ensures both effectiveness and efficiency, as confirmed by experimental evaluations. The decision-diagram representations offer a powerful tool for analysing and verifying parameterised quantum circuits, bridging the gap between theoretical models and practical implementations.
Quantum computing is gaining considerable momentum through the recent progress in physical realizations of quantum computers. This led to rather sophisticated design flows in which the originally specified quantum functionality is compiled through different abstractions. This increasingly raises the question whether the respectively resulting quantum circuits indeed realize the originally intended function. Accordingly, efficient methods for equivalence checking are gaining importance. However, existing solutions still suffer from significant shortcomings such as their exponential worst case performance and an increased effort to obtain counterexamples in case of non-equivalence. In this work, we propose an improved DD-based equivalence checking approach which addresses these shortcomings. To this end, we utilize decision diagrams and exploit the fact that quantum operations are inherently reversible - allowing for dedicated strategies that keep the overhead moderate in many cases. Experimental results confirm that the proposed strategies lead to substantial speed-ups - allowing to perform equivalence checking of quantum circuits factors or even magnitudes faster than the state of the art.
Quantum computing is arguably one of the most revolutionary and disruptive technologies of this century. Due to the ever-increasing number of potential applications as well as the continuing rise in complexity, the development, simulation, optimization, and physical realization of quantum circuits is of utmost importance for designing novel algorithms. We show how matrix product states (MPSs) and matrix product operators (MPOs) can be used to express certain quantum states, quantum gates, and entire quantum circuits as low-rank tensors. This enables the analysis and simulation of complex quantum circuits on classical computers and to gain insight into the underlying structure of the system. We present different examples to demonstrate the advantages of MPO formulations and show that they are more efficient than conventional techniques if the bond dimensions of the wave function representation can be kept small throughout the simulation.
Quantum circuit transpilation facilitates the decomposition of complex operations into simpler hardware-compatible gates. This results in significant changes to the input circuit, and consequently, it becomes imperative to verify the correctness of the transpilation process. Quantum circuit equivalence checking is used to verify the operational equivalence of large quantum circuits to ensure the correctness of computation. Although small quantum circuits can be simulated easily on a classical computer without transpilation, this approach is unscalable for larger, more complex quantum circuits. Furthermore, a scalable quantum equivalence checking algorithm exhibiting subpar performance when applied to larger quantum circuits lacks reliability. Therefore, an equivalence-checking algorithm with scalability and acceptable performance is necessary to verify large quantum circuits. In this paper, we propose QuaSi, a simulation-based verification methodology designed to generate distinct test cases to achieve a scalable and reliable quantum circuit equivalence-checking. Our proposed approach surpasses existing state-of-the-art simulation-based methodologies by boosting the success rate of verification, in addition to reducing the verification latency. When evaluating using large benchmarks with up to 130 qubits, QuaSi furnished significantly improved performance compared to existing approaches in all types of scenarios. Furthermore, we proposed an algorithm to locate the erroneous gates to facilitate debugging the transpilation process.