No Arabic abstract
We study the fundamental design automation problem of equivalence checking in the NISQ (Noisy Intermediate-Scale Quantum) computing realm where quantum noise is present inevitably. The notion of approximate equivalence of (possibly noisy) quantum circuits is defined based on the Jamiolkowski fidelity which measures the average distance between output states of two super-operators when the input is chosen at random. By employing tensor network contraction, we present two algorithms, aiming at different situations where the number of noises varies, for computing the fidelity between an ideal quantum circuit and its noisy implementation. The effectiveness of our algorithms is demonstrated by experimenting on benchmarks of real NISQ circuits. When compared with the state-of-the-art implementation incorporated in Qiskit, experimental results show that the proposed algorithms outperform in both efficiency and scalability.
Despite the rapid development of quantum computing these years, state-of-the-art quantum devices still contain only a very limited number of qubits. One possible way to execute more realistic algorithms in near-term quantum devices is to employ dynamic quantum circuits, in which measurements can happen during the circuit and their outcomes are used to control other parts of the circuit. This technique can help to significantly reduce the resources required to achieve a given accuracy of a quantum algorithm. However, since this type of quantum circuits are more flexible, their verification is much more challenging. In this paper, we give a formal definition of dynamic quantum circuits and then propose to characterise their functionality in terms of ensembles of linear operators. Based on this novel semantics, two dynamic quantum circuits are equivalent if they have the same functionality. We further propose and implement two decision diagram-based algorithms for checking the equivalence of dynamic quantum circuits. Experiments show that embedding classical logic into conventional quantum circuits does not incur significant time and space burden.
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 this talk, we will describe a framework for assertion-based verification (ABV) of quantum circuits by applying model checking techniques for quantum systems developed in our previous work, in which: (i) Noiseless and noisy quantum circuits are modelled as operator- and super-operator-valued transition systems, respectively, both of which can be further represented by tensor networks. (ii) Quantum assertions are specified by a temporal extension of Birkhoff-von Neumann quantum logic. Their semantics is defined based on the design decision: they will be used in verification of quantum circuits by simulation on classical computers or human reasoning rather than by quantum physics experiments (e.g. testing through measurements); (iii) Algorithms for reachability analysis and model checking of quantum circuits are developed based on contraction of tensor networks. We observe that many optimisation techniques for computing relational products used in BDD-based model checking algorithms can be generalised for contracting tensor networks of quantum circuits.
In 1998, Brassard, Hoyer, Mosca, and Tapp (BHMT) gave a quantum algorithm for approximate counting. Given a list of $N$ items, $K$ of them marked, their algorithm estimates $K$ to within relative error $varepsilon$ by making only $Oleft( frac{1}{varepsilon}sqrt{frac{N}{K}}right) $ queries. Although this speedup is of Grover type, the BHMT algorithm has the curious feature of relying on the Quantum Fourier Transform (QFT), more commonly associated with Shors algorithm. Is this necessary? This paper presents a simplified algorithm, which we prove achieves the same query complexity using Grover iterations only. We also generalize this to a QFT-free algorithm for amplitude estimation. Related approaches to approximate counting were sketched previously by Grover, Abrams and Williams, Suzuki et al., and Wie (the latter two as we were writing this paper), but in all cases without rigorous analysis.
The study of the impact of noise on quantum circuits is especially relevant to guide the progress of Noisy Intermediate-Scale Quantum (NISQ) computing. In this paper, we address the pulse-level simulation of noisy quantum circuits with the Quantum Toolbox in Python (QuTiP). We introduce new tools in qutip-qip, QuTiPs quantum information processing package. These tools simulate quantum circuits at the pulse level, fully leveraging QuTiPs quantum dynamics solvers and control optimization features. We show how quantum circuits can be compiled on simulated processors, with control pulses acting on a target Hamiltonian that describes the unitary evolution of the physical qubits. Various types of noise can be introduced based on the physical model, e.g., by simulating the Lindblad density-matrix dynamics or Monte Carlo quantum trajectories. In particular, we allow for the definition of environment-induced decoherence at the processor level and include noise simulation at the level of control pulses. As an example, we consider the compilation of the Deutsch-Jozsa algorithm on a superconducting-qubit-based and a spin-chain-based processor, also using control optimization algorithms. We also reproduce experimental results on cross-talk noise in an ion-based processor, and show how a Ramsey experiment can be modeled with Lindblad dynamics. Finally, we show how to integrate these features with other software frameworks.