Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs

• URL: http://arxiv.org/abs/2101.08939v5
• Date: Thu, 20 Mar 2025 02:17:35 GMT
• Title: Hoare meets Heisenberg: A Lightweight Logic for Quantum Programs
• Authors: Aarthi Sundaram, Robert Rand, Kartik Singhal, Brad Lackey,
• Abstract summary: We show that Gottesman's (1998) semantics for Clifford circuits based on the Heisenberg representation gives rise to a lightweight Hoare-like logic.<n>Our applications include (i) certifying whether auxiliary qubits can be safely disposed of, (ii) checking theity of a gate with respect to a given stabilizer code, and (iv) computing post-measurement states.
• Score: 0.932065750652415
• License: http://creativecommons.org/licenses/by-nc-sa/4.0/
• Abstract: We show that Gottesman's (1998) semantics for Clifford circuits based on the Heisenberg representation gives rise to a lightweight Hoare-like logic for efficiently characterizing a common subset of quantum programs. Our applications include (i) certifying whether auxiliary qubits can be safely disposed of, (ii) determining if a system is separable across a given bipartition, (iii) checking the transversality of a gate with respect to a given stabilizer code, and (iv) computing post-measurement states for computational basis measurements. Further, this logic is extended to accommodate universal quantum computing by deriving Hoare triples for the $T$-gate, multiply-controlled unitaries such as the Toffoli gate, and some gate injection circuits that use associated magic states. A number of interesting results emerge from this logic, including a lower bound on the number of $T$ gates necessary to perform a multiply-controlled $Z$ gate.

Related papers

• A Universal Circuit Set Using the $S_3$ Quantum Double [0.5231056284485742]
  We give an explicit construction of the circuits for creating, moving, and measuring all non-trivial anyons. We encode each physical degree of freedom of $mathcalD(S_3)$ into a novel, quantum, error-correcting code. Our proposal offers a promising path to realize robust universal topological quantum computation in the NISQ era.
  arXiv  Detail & Related papers  (2024-11-14T18:58:41Z)
• Classical certification of quantum gates under the dimension assumption [0.1874930567916036]
  We develop an efficient method for certifying single-qubit quantum gates in a black-box scenario. We prove that the method's sample complexity grows as $mathrmO(varepsilon-1)$. We show that the proposed method can be used to certify a gate set universal for single-qubit quantum computation.
  arXiv  Detail & Related papers  (2024-01-30T13:40:39Z)
• A two-circuit approach to reducing quantum resources for the quantum lattice Boltzmann method [41.66129197681683]
  Current quantum algorithms for solving CFD problems use a single quantum circuit and, in some cases, lattice-based methods. We introduce the a novel multiple circuits algorithm that makes use of a quantum lattice Boltzmann method (QLBM) The problem is cast as a stream function--vorticity formulation of the 2D Navier-Stokes equations and verified and tested on a 2D lid-driven cavity flow.
  arXiv  Detail & Related papers  (2024-01-20T15:32:01Z)
• One Gate Scheme to Rule Them All: Introducing a Complex Yet Reduced Instruction Set for Quantum Computing [8.478982715648547]
  Scheme for qubits with $XX+YY$ coupling realizes any two-qubit gate up to single-qubit gates. We observe marked improvements across various applications, including generic $n$-qubit gate synthesis, quantum volume, and qubit routing.
  arXiv  Detail & Related papers  (2023-12-09T19:30:31Z)
• Realization of Scalable Cirac-Zoller Multi-Qubit Gates [5.309268373861329]
  The universality in quantum computing states that any quantum computational task can be decomposed into a finite set of logic gates operating on one and two qubits. Practical processor designs benefit greatly from availability of multi-qubit gates that operate on more than two qubits. Here, we take advantage of novel performance benefits of long ion chains to realize fully programmable and scalable high-fidelity Cirac-Zoller gates.
  arXiv  Detail & Related papers  (2023-01-18T14:34:24Z)
• Universal qudit gate synthesis for transmons [44.22241766275732]
  We design a superconducting qudit-based quantum processor. We propose a universal gate set featuring a two-qudit cross-resonance entangling gate. We numerically demonstrate the synthesis of $rm SU(16)$ gates for noisy quantum hardware.
  arXiv  Detail & Related papers  (2022-12-08T18:59:53Z)
• Efficient Bipartite Entanglement Detection Scheme with a Quantum Adversarial Solver [89.80359585967642]
  Proposal reformulates the bipartite entanglement detection as a two-player zero-sum game completed by parameterized quantum circuits. We experimentally implement our protocol on a linear optical network and exhibit its effectiveness to accomplish the bipartite entanglement detection for 5-qubit quantum pure states and 2-qubit quantum mixed states.
  arXiv  Detail & Related papers  (2022-03-15T09:46:45Z)
• Universal logic with encoded spin qubits in silicon [1.5796098351442824]
  Qubits encoded in a decoherence-free subsystem and realized in exchange-coupled silicon quantum dots are promising candidates for fault-tolerant quantum computing. Key difficulties are that encoded entangling gates require a large number of control pulses and high-yielding quantum dot arrays. Here we show a device made using the single-layer etch-defined gate architecture that achieves both the required functional yield needed for full control and the coherence necessary for thousands of exchange pulses to be applied.
  arXiv  Detail & Related papers  (2022-02-08T02:23:46Z)
• Approaching the theoretical limit in quantum gate decomposition [0.0]
  We propose a novel numerical approach to decompose general quantum programs in terms of single- and two-qubit quantum gates with a $CNOT$ gate count. Our approach is based on a sequential optimization of parameters related to the single-qubit rotation gates involved in a pre-designed quantum circuit used for the decomposition.
  arXiv  Detail & Related papers  (2021-09-14T15:36:22Z)
• Quantum simulation of $\phi^4$ theories in qudit systems [53.122045119395594]
  We discuss the implementation of quantum algorithms for lattice $Phi4$ theory on circuit quantum electrodynamics (cQED) system. The main advantage of qudit systems is that its multi-level characteristic allows the field interaction to be implemented only with diagonal single-qudit gates.
  arXiv  Detail & Related papers  (2021-08-30T16:30:33Z)
• Finding the disjointness of stabilizer codes is NP-complete [77.34726150561087]
  We show that the problem of calculating the $c-disjointness, or even approximating it to within a constant multiplicative factor, is NP-complete. We provide bounds on the disjointness for various code families, including the CSS codes,$d codes and hypergraph codes. Our results indicate that finding fault-tolerant logical gates for generic quantum error-correcting codes is a computationally challenging task.
  arXiv  Detail & Related papers  (2021-08-10T15:00:20Z)
• Realization of arbitrary doubly-controlled quantum phase gates [62.997667081978825]
  We introduce a high-fidelity gate set inspired by a proposal for near-term quantum advantage in optimization problems. By orchestrating coherent, multi-level control over three transmon qutrits, we synthesize a family of deterministic, continuous-angle quantum phase gates acting in the natural three-qubit computational basis.
  arXiv  Detail & Related papers  (2021-08-03T17:49:09Z)
• Efficient quantum programming using EASE gates on a trapped-ion quantum computer [1.9610635155358869]
  We focus on the recently invented efficient, arbitrary, simultaneously entangling (EASE) gates, available on a trapped-ion quantum computer. We show an $n$-qubit Clifford circuit can be implemented using $6log(n)$ EASE gates, an $n$-qubit multiply-controlled NOT gate can be implemented using $3n/2$ EASE gates, and an $n$-qubit permutation can be implemented using six EASE gates.
  arXiv  Detail & Related papers  (2021-07-15T20:03:23Z)
• Random quantum circuits anti-concentrate in log depth [118.18170052022323]
  We study the number of gates needed for the distribution over measurement outcomes for typical circuit instances to be anti-concentrated. Our definition of anti-concentration is that the expected collision probability is only a constant factor larger than if the distribution were uniform. In both the case where the gates are nearest-neighbor on a 1D ring and the case where gates are long-range, we show $O(n log(n)) gates are also sufficient.
  arXiv  Detail & Related papers  (2020-11-24T18:44:57Z)
• QUANTIFY: A framework for resource analysis and design verification of quantum circuits [69.43216268165402]
  QUANTIFY is an open-source framework for the quantitative analysis of quantum circuits. It is based on Google Cirq and is developed with Clifford+T circuits in mind. For benchmarking purposes QUANTIFY includes quantum memory and quantum arithmetic circuits.
  arXiv  Detail & Related papers  (2020-07-21T15:36:25Z)
• Improving the Performance of Deep Quantum Optimization Algorithms with Continuous Gate Sets [47.00474212574662]
  Variational quantum algorithms are believed to be promising for solving computationally hard problems. In this paper, we experimentally investigate the circuit-depth-dependent performance of QAOA applied to exact-cover problem instances. Our results demonstrate that the use of continuous gate sets may be a key component in extending the impact of near-term quantum computers.
  arXiv  Detail & Related papers  (2020-05-11T17:20:51Z)
• Simple implementation of high fidelity controlled-$i$SWAP gates and quantum circuit exponentiation of non-Hermitian gates [0.0]
  The $i$swap gate is an entangling swapping gate where the qubits obtain a phase of $i$ if the state of the qubits is swapped. We present a simple implementation of the controlled-$i$swap gate.
  arXiv  Detail & Related papers  (2020-02-26T19:00:01Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.