Certified Quantum Computation in Isabelle/HOL

• URL: http://arxiv.org/abs/2012.13925v1
• Date: Sun, 27 Dec 2020 11:45:49 GMT
• Title: Certified Quantum Computation in Isabelle/HOL
• Authors: Anthony Bordg, Hanna Lachnitt, Yijun He
• Abstract summary: We present an effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits. We discuss the design choices made and report on an outcome of our work in the field of quantum game theory.
• Score: 1.2730070122798456
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: In this article we present an ongoing effort to formalise quantum algorithms and results in quantum information theory using the proof assistant Isabelle/HOL. Formal methods being critical for the safety and security of algorithms and protocols, we foresee their widespread use for quantum computing in the future. We have developed a large library for quantum computing in Isabelle based on a matrix representation for quantum circuits, successfully formalising the no-cloning theorem, quantum teleportation, Deutsch's algorithm, the Deutsch-Jozsa algorithm and the quantum Prisoner's Dilemma. We discuss the design choices made and report on an outcome of our work in the field of quantum game theory.

Related papers

• Parallel Quantum Computing Simulations via Quantum Accelerator Platform Virtualization [44.99833362998488]
  We present a model for parallelizing simulation of quantum circuit executions. The model can take advantage of its backend-agnostic features, enabling parallel quantum circuit execution over any target backend.
  arXiv  Detail & Related papers  (2024-06-05T17:16:07Z)
• Quantum Subroutine for Variance Estimation: Algorithmic Design and Applications [80.04533958880862]
  Quantum computing sets the foundation for new ways of designing algorithms. New challenges arise concerning which field quantum speedup can be achieved. Looking for the design of quantum subroutines that are more efficient than their classical counterpart poses solid pillars to new powerful quantum algorithms.
  arXiv  Detail & Related papers  (2024-02-26T09:32:07Z)
• Efficient Quantum Modular Arithmetics for the ISQ Era [0.0]
  This study presents an array of quantum circuits, each precision-engineered for modular arithmetic functions. We provide a theoretical framework and practical implementations in the PennyLane quantum software.
  arXiv  Detail & Related papers  (2023-11-14T21:34:39Z)
• Quantum Algorithms for the computation of quantum thermal averages at work [0.0]
  We consider the practical implementation of the so-called Quantum-Quantum Metropolis algorithm. We simulate a basic system of three frustrated quantum spins and discuss its systematics.
  arXiv  Detail & Related papers  (2023-08-02T17:05:10Z)
• Quantum Machine Learning: from physics to software engineering [58.720142291102135]
  We show how classical machine learning approach can help improve the facilities of quantum computers. We discuss how quantum algorithms and quantum computers may be useful for solving classical machine learning tasks.
  arXiv  Detail & Related papers  (2023-01-04T23:37:45Z)
• QuantumSkynet: A High-Dimensional Quantum Computing Simulator [0.0]
  Current implementations of quantum computing simulators are limited to two-level quantum systems. Recent advances in high-dimensional quantum computing systems have demonstrated the viability of working with multi-level superposition and entanglement. We introduce QuantumSkynet, a novel high-dimensional cloud-based quantum computing simulator.
  arXiv  Detail & Related papers  (2021-06-30T06:28:18Z)
• On exploring the potential of quantum auto-encoder for learning quantum systems [60.909817434753315]
  We devise three effective QAE-based learning protocols to address three classically computational hard learning problems. Our work sheds new light on developing advanced quantum learning algorithms to accomplish hard quantum physics and quantum information processing tasks.
  arXiv  Detail & Related papers  (2021-06-29T14:01:40Z)
• Quantum walk processes in quantum devices [55.41644538483948]
  We study how to represent quantum walk on a graph as a quantum circuit. Our approach paves way for the efficient implementation of quantum walks algorithms on quantum computers.
  arXiv  Detail & Related papers  (2020-12-28T18:04:16Z)
• Proving Quantum Programs Correct [3.2513560268591735]
  It verifies the correctness of a range of quantum algorithms including Grover's algorithm and quantum phase estimation. It aims to highlight both the successes and challenges of formal verification in the quantum context.
  arXiv  Detail & Related papers  (2020-10-03T00:55:41Z)
• An Application of Quantum Annealing Computing to Seismic Inversion [55.41644538483948]
  We apply a quantum algorithm to a D-Wave quantum annealer to solve a small scale seismic inversions problem. The accuracy achieved by the quantum computer is at least as good as that of the classical computer.
  arXiv  Detail & Related papers  (2020-05-06T14:18:44Z)
• Quantum simulation of quantum field theories as quantum chemistry [9.208624182273288]
  Conformal truncation is a powerful numerical method for solving generic strongly-coupled quantum field theories. We show that quantum computation could not only help us understand fundamental physics in the lattice approximation, but also simulate quantum field theory methods directly.
  arXiv  Detail & Related papers  (2020-04-28T01:20:04Z)

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.