Symbolic Reasoning about Quantum Circuits in Coq

• URL: http://arxiv.org/abs/2005.11023v4
• Date: Tue, 21 Dec 2021 08:13:19 GMT
• Title: Symbolic Reasoning about Quantum Circuits in Coq
• Authors: Wenjun Shi, Qinxiang Cao, Yuxin Deng, Hanru Jiang and Yuan Feng
• Abstract summary: A quantum circuit is a computational unit that transforms an input quantum state to an output one. We propose a symbolic approach to reasoning about quantum circuits.
• Score: 2.065777667168023
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: A quantum circuit is a computational unit that transforms an input quantum state to an output one. A natural way to reason about its behavior is to compute explicitly the unitary matrix implemented by it. However, when the number of qubits increases, the matrix dimension grows exponentially and the computation becomes intractable. In this paper, we propose a symbolic approach to reasoning about quantum circuits. It is based on a small set of laws involving some basic manipulations on vectors and matrices. This symbolic reasoning scales better than the explicit one and is well suited to be automated in Coq, as demonstrated with some typical examples.

Related papers

• Homology, Hopf Algebras and Quantum Code Surgery [55.2480439325792]
  We study quantum error-correction codes from an algebraic perspective.<n>We derive new methods of performing fault-tolerant quantum computation.<n>At its core, this thesis asks: what is lattice surgery?
  arXiv  Detail & Related papers  (2025-08-02T21:38:33Z)
• Hadamard-$Π$: Equational Quantum Programming [0.5852077003870417]
  We introduce a small quantum programming language extending the universal classical reversible programming language $Pi$ with a single primitive corresponding to the Hadamard gate.<n>The language comes equipped with a sound and complete categorical semantics that is specified by a purely equational theory.
  arXiv  Detail & Related papers  (2025-06-07T15:26:33Z)
• Matrix encoding method in variational quantum singular value decomposition [49.494595696663524]
  Conditional measurement is involved to avoid small success probability in ancilla measurement. The objective function for the algorithm can be obtained probabilistically via measurement of the state of a one-qubit subsystem.
  arXiv  Detail & Related papers  (2025-03-19T07:01:38Z)
• Experimental Demonstration of Logical Magic State Distillation [62.77974948443222]
  We present the experimental realization of magic state distillation with logical qubits on a neutral-atom quantum computer. Our approach makes use of a dynamically reconfigurable architecture to encode and perform quantum operations on many logical qubits in parallel.
  arXiv  Detail & Related papers  (2024-12-19T18:38:46Z)
• Geometric structure and transversal logic of quantum Reed-Muller codes [51.11215560140181]
  In this paper, we aim to characterize the gates of quantum Reed-Muller (RM) codes by exploiting the well-studied properties of their classical counterparts. A set of stabilizer generators for a RM code can be described via $X$ and $Z$ operators acting on subcubes of particular dimensions.
  arXiv  Detail & Related papers  (2024-10-10T04:07:24Z)
• Efficient conversion from fermionic Gaussian states to matrix product states [48.225436651971805]
  We propose a highly efficient algorithm that converts fermionic Gaussian states to matrix product states. It can be formulated for finite-size systems without translation invariance, but becomes particularly appealing when applied to infinite systems. The potential of our method is demonstrated by numerical calculations in two chiral spin liquids.
  arXiv  Detail & Related papers  (2024-08-02T10:15:26Z)
• Quantum sampling algorithms for quantum state preparation and matrix block-encoding [0.0]
  We first present an algorithm based on QRS that prepares a quantum state $|psi_frangle propto sumN_x=1 f(x)|xrangle$. We then adapt QRS techniques to the matrix block-encoding problem and introduce a QRS-based algorithm for block-encoding a given matrix $A = sum_ij A_ij |irangle langle j|$.
  arXiv  Detail & Related papers  (2024-05-19T03:46:11Z)
• 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 Complete Equational Theory for Quantum Circuits [58.720142291102135]
  We introduce the first complete equational theory for quantum circuits. Two circuits represent the same unitary map if and only if they can be transformed one into the other using the equations.
  arXiv  Detail & Related papers  (2022-06-21T17:56:31Z)
• FABLE: Fast Approximate Quantum Circuits for Block-Encodings [0.0]
  We propose FABLE, a method to generate approximate quantum circuits for block-encodings of matrices in a fast manner. FABLE circuits have a simple structure and are directly formulated in terms of one- and two-qubit gates. We show that FABLE circuits can be compressed and sparsified.
  arXiv  Detail & Related papers  (2022-04-29T21:06:07Z)
• Quantum Circuits in Additive Hilbert Space [0.0]
  We show how conventional circuits can be expressed in the additive space and how they can be recovered. In particular in our formalism we are able to synthesize high-level multi-controlled primitives from low-level circuit decompositions. Our formulation also accepts a circuit-like diagrammatic representation and proposes a novel and simple interpretation of quantum computation.
  arXiv  Detail & Related papers  (2021-11-01T19:05:41Z)
• Synthesis of Quantum Circuits with an Island Genetic Algorithm [44.99833362998488]
  Given a unitary matrix that performs certain operation, obtaining the equivalent quantum circuit is a non-trivial task. Three problems are explored: the coin for the quantum walker, the Toffoli gate and the Fredkin gate. The algorithm proposed proved to be efficient in decomposition of quantum circuits, and as a generic approach, it is limited only by the available computational power.
  arXiv  Detail & Related papers  (2021-06-06T13:15:25Z)
• Quantum Garbled Circuits [9.937090317971313]
  We show how to compute an encoding of a given quantum circuit and quantum input, from which it is possible to derive the output of the computation and nothing else. Our protocol has the so-called $Sigma$ format with a single-bit challenge, and allows the inputs to be delayed to the last round.
  arXiv  Detail & Related papers  (2020-06-01T17:07:01Z)
• Quantum Gram-Schmidt Processes and Their Application to Efficient State Read-out for Quantum Algorithms [87.04438831673063]
  We present an efficient read-out protocol that yields the classical vector form of the generated state. Our protocol suits the case that the output state lies in the row space of the input matrix. One of our technical tools is an efficient quantum algorithm for performing the Gram-Schmidt orthonormal procedure.
  arXiv  Detail & Related papers  (2020-04-14T11:05:26Z)
• Parallel Quantum Simulation of Large Systems on Small Quantum Computers [0.2348805691644085]
  NISQ networks permit computational and entanglement resources to be concentrated in interesting regions of Hilbert space. We provide Cirq and Qiskit code that translate infinite, translationally invariant matrix product state (iMPS) algorithms to finite-depth quantum circuit machines. Illustrative simulated output of these codes for achievable circuit sizes is given.
  arXiv  Detail & Related papers  (2020-03-26T18:05:45Z)

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.