No Arabic abstract
We define syntax and semantics of quantum circuits, allowing measurement gates and classical channels. We define circuit-based quantum algorithms and prove that, semantically, any such algorithm is equivalent to a single measurement that depends only on the underlying quantum circuit. Finally, we use our formalization of quantum circuits to state precisely and prove the principle of deferred measurements.
We introduce various measures of forward classical communication for bipartite quantum channels. Since a point-to-point channel is a special case of a bipartite channel, the measures reduce to measures of classical communication for point-to-point channels. As it turns out, these reduced measures have been reported in prior work of Wang et al. on bounding the classical capacity of a quantum channel. As applications, we show that the measures are upper bounds on the forward classical capacity of a bipartite channel. The reduced measures are upper bounds on the classical capacity of a point-to-point quantum channel assisted by a classical feedback channel. Some of the various measures can be computed by semi-definite programming.
In a recent breakthrough, Bravyi, Gosset and K{o}nig (BGK) [Science, 2018] proved that simulating constant depth quantum circuits takes classical circuits $Omega(log n)$ depth. In our paper, we first formalise their notion of simulation, which we call possibilistic simulation. Then, from well-known results, we deduce that their circuits can be simulated in depth $O(log^{2} n)$. Separately, we construct explicit classical circuits that can simulate any depth-$d$ quantum circuit with Clifford and $t$ $T$-gates in depth $O(d+t)$. Our classical circuits use ${text{NOT, AND, OR}}$ gates of fan-in $leq 2$.
Quantum supermaps are transformations that map quantum operations to quantum operations. It is known that quantum supermaps which respect a definite, predefined causal order between their input operations correspond to fixed-order quantum circuits. A systematic understanding of the physical interpretation of more general types of quantum supermaps--in particular, those incompatible with a definite causal structure--is however lacking. Here we identify two new types of circuits that naturally generalise the fixed-order case and that likewise correspond to distinct classes of quantum supermaps, which we fully characterise. We first introduce quantum circuits with classical control of causal order, in which the order of operations is still well-defined, but not necessarily fixed in advance: it can in particular be established dynamically, in a classically-controlled manner, as the circuit is being used. We then consider quantum circuits with quantum control of causal order, in which the order of operations is controlled coherently. The supermaps described by these classes of circuits are physically realisable, and the latter encompasses all known examples of physically realisable processes with indefinite causal order, including the celebrated quantum switch. Interestingly, it also contains new examples arising from the combination of dynamical and coherent control of causal order, and we detail explicitly one such process. Nevertheless, we show that quantum circuits with quantum control of causal order can only generate causal correlations, compatible with a well-defined causal order. We furthermore extend our considerations to probabilistic circuits that produce also classical outcomes, and we demonstrate by an example how our characterisations allow us to identify new advantages for quantum information processing tasks that could be demonstrated in practice.
To achieve universal quantum computation via general fault-tolerant schemes, stabilizer operations must be supplemented with other non-stabilizer quantum resources. Motivated by this necessity, we develop a resource theory for magic quantum channels to characterize and quantify the quantum magic or non-stabilizerness of noisy quantum circuits. For qudit quantum computing with odd dimension $d$, it is known that quantum states with non-negative Wigner function can be efficiently simulated classically. First, inspired by this observation, we introduce a resource theory based on completely positive-Wigner-preserving quantum operations as free operations, and we show that they can be efficiently simulated via a classical algorithm. Second, we introduce two efficiently computable magic measures for quantum channels, called the mana and thauma of a quantum channel. As applications, we show that these measures not only provide fundamental limits on the distillable magic of quantum channels, but they also lead to lower bounds for the task of synthesizing non-Clifford gates. Third, we propose a classical algorithm for simulating noisy quantum circuits, whose sample complexity can be quantified by the mana of a quantum channel. We further show that this algorithm can outperform another approach for simulating noisy quantum circuits, based on channel robustness. Finally, we explore the threshold of non-stabilizerness for basic quantum circuits under depolarizing noise.
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.