Type-Based Verification of Connectivity Constraints in Lattice Surgery

• URL: http://arxiv.org/abs/2409.00529v1
• Date: Sat, 31 Aug 2024 19:31:19 GMT
• Title: Type-Based Verification of Connectivity Constraints in Lattice Surgery
• Authors: Ryo Wakizaka, Yasunari Suzuki, Atsushi Igarashi,
• Abstract summary: Fault-tolerant quantum computation using lattice surgery can be abstracted as operations on graphs. $mathcalQ_LS$ is a first-order quantum programming language to formalize the execution model of surgery operations.
• Score: 0.196629787330046
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Fault-tolerant quantum computation using lattice surgery can be abstracted as operations on graphs, wherein each logical qubit corresponds to a vertex of the graph, and multi-qubit measurements are accomplished by connecting the vertices with paths between them. Operations attempting to connect vertices without a valid path will result in abnormal termination. As the permissible paths may evolve during execution, it is necessary to statically verify that the execution of a quantum program can be completed. This paper introduces a type-based method to statically verify that well-typed programs can be executed without encountering halts induced by surgery operations. Alongside, we present $\mathcal{Q}_{LS}$, a first-order quantum programming language to formalize the execution model of surgery operations. Furthermore, we provide a type checking algorithm by reducing the type checking problem to the offline dynamic connectivity problem.

Related papers

• Towards Dynamic Message Passing on Graphs [104.06474765596687]
  We propose a novel dynamic message-passing mechanism for graph neural networks (GNNs) It projects graph nodes and learnable pseudo nodes into a common space with measurable spatial relations between them. With nodes moving in the space, their evolving relations facilitate flexible pathway construction for a dynamic message-passing process.
  arXiv  Detail & Related papers  (2024-10-31T07:20:40Z)
• Low-overhead fault-tolerant quantum computation by gauging logical operators [0.7673339435080445]
  Recent progress has uncovered quantum error-correcting codes with sparse connectivity requirements and constant qubit overhead. Existing schemes for fault-tolerant logical measurement do not always achieve low qubit overhead. We present a low-overhead method to implement fault-tolerant logical measurement in a quantum error-correcting code by treating the logical operator as a symmetry and gauging it.
  arXiv  Detail & Related papers  (2024-10-03T05:04:12Z)
• Algorithmic Fault Tolerance for Fast Quantum Computing [37.448838730002905]
  We show that fault-tolerant logical operations can be performed with constant time overhead for a broad class of quantum codes. We prove that the deviation from the ideal measurement result distribution can be made exponentially small in the code distance. Our work sheds new light on the theory of fault tolerance, potentially reducing the space-time cost of practical fault-tolerant quantum computation by orders of magnitude.
  arXiv  Detail & Related papers  (2024-06-25T15:43:25Z)
• Bisimulation Learning [55.859538562698496]
  We compute finite bisimulations of state transition systems with large, possibly infinite state space. Our technique yields faster verification results than alternative state-of-the-art tools in practice.
  arXiv  Detail & Related papers  (2024-05-24T17:11:27Z)
• Full Characterization of the Depth Overhead for Quantum Circuit Compilation with Arbitrary Qubit Connectivity Constraint [6.799314463590596]
  In some physical implementations of quantum computers, 2-qubit operations can be applied only on certain pairs of qubits. In this paper, we fully characterize the depth overhead by the routing number of the underlying constraint graph.
  arXiv  Detail & Related papers  (2024-02-04T08:29:41Z)
• NodeFormer: A Scalable Graph Structure Learning Transformer for Node Classification [70.51126383984555]
  We introduce a novel all-pair message passing scheme for efficiently propagating node signals between arbitrary nodes. The efficient computation is enabled by a kernerlized Gumbel-Softmax operator. Experiments demonstrate the promising efficacy of the method in various tasks including node classification on graphs.
  arXiv  Detail & Related papers  (2023-06-14T09:21:15Z)
• Compilation of algorithm-specific graph states for quantum circuits [55.90903601048249]
  We present a quantum circuit compiler that prepares an algorithm-specific graph state from quantum circuits described in high level languages. The computation can then be implemented using a series of non-Pauli measurements on this graph state.
  arXiv  Detail & Related papers  (2022-09-15T14:52:31Z)
• A circuit-level protocol and analysis for twist-based lattice surgery [3.222802562733787]
  Lattice surgery is a technique for performing fault-tolerant quantum computation in two dimensions. We provide an explicit twist-based lattice surgery protocol and its requisite connectivity layout. We also provide new stabilizer measurement circuits for measuring twist defects.
  arXiv  Detail & Related papers  (2022-01-14T21:16:27Z)
• Universal quantum computing with twist-free and temporally encoded lattice surgery [3.222802562733787]
  We introduce a decoder capable of correcting spacelike and timelike errors during lattice surgery protocols. We compute logical failure rates of a lattice surgery protocol for a biased circuit-level noise model. We propose a layout for a quantum processor that is more efficient for rectangular surface codes exploiting noise bias.
  arXiv  Detail & Related papers  (2021-09-06T21:18:01Z)
• Differentiable Causal Discovery from Interventional Data [141.41931444927184]
  We propose a theoretically-grounded method based on neural networks that can leverage interventional data. We show that our approach compares favorably to the state of the art in a variety of settings.
  arXiv  Detail & Related papers  (2020-07-03T15:19:17Z)
• Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
  A fundamental component of neural network verification is the computation of bounds on the values their outputs can take. We propose a novel approach based on Lagrangian Decomposition. We show that we obtain bounds comparable with off-the-shelf solvers in a fraction of their running time.
  arXiv  Detail & Related papers  (2020-02-24T17:55:10Z)

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.