Symbolic Execution for Quantum Error Correction Programs

• URL: http://arxiv.org/abs/2311.11313v3
• Date: Sun, 28 Apr 2024 04:03:35 GMT
• Title: Symbolic Execution for Quantum Error Correction Programs
• Authors: Wang Fang, Mingsheng Ying,
• Abstract summary: We define QSE, a symbolic execution framework for quantum programs. We introduce symbolic stabilizer states, which symbolize the phases of stabilizer generators, for the efficient analysis of quantum error correction (QEC) programs. We implement QSE with the support of symbolic stabilizer states in a prototype tool named QuantumSE.jl.
• Score: 3.018910972030221
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: We define QSE, a symbolic execution framework for quantum programs by integrating symbolic variables into quantum states and the outcomes of quantum measurements. The soundness of QSE is established through a theorem that ensures the correctness of symbolic execution within operational semantics. We further introduce symbolic stabilizer states, which symbolize the phases of stabilizer generators, for the efficient analysis of quantum error correction (QEC) programs. Within the QSE framework, we can use symbolic expressions to characterize the possible discrete Pauli errors in QEC, providing a significant improvement over existing methods that rely on sampling with simulators. We implement QSE with the support of symbolic stabilizer states in a prototype tool named QuantumSE.jl. Our experiments on representative QEC codes, including quantum repetition codes, Kitaev's toric codes, and quantum Tanner codes, demonstrate the efficiency of QuantumSE.jl for debugging QEC programs with over 1000 qubits. In addition, by substituting concrete values in symbolic expressions of measurement results, QuantumSE.jl is also equipped with a sampling feature for stabilizer circuits. Despite a longer initialization time than the state-of-the-art stabilizer simulator, Google's Stim, QuantumSE.jl offers a quicker sampling rate in the experiments.

Related papers

• SparQSim: Simulating Scalable Quantum Algorithms via Sparse Quantum State Representations [3.7112784544167248]
  We present SparQSim, a quantum simulator implemented in C++ inspired by the Feynman-based method. SparQSim operates at the register level by storing only the nonzero components of the quantum state.
  arXiv  Detail & Related papers  (2025-03-19T11:23:26Z)
• Quantum Compressive Sensing Meets Quantum Noise: A Practical Exploration [8.260432715157027]
  We present a practical implementation of Quantum Compressive Sensing (QCS) on Amazon Braket. QCS is a quantum data-driven approach to compressive sensing where the state of the tensor network is represented by a quantum state over a set of entangled qubits. We discuss potential long-term directions aimed at unlocking the full potential of quantum compressive sensing for applications such as signal recovery and image processing.
  arXiv  Detail & Related papers  (2025-01-21T18:10:03Z)
• Quantum Wasserstein Compilation: Unitary Compilation using the Quantum Earth Mover's Distance [2.502222151305252]
  We present a quantum Wasserstein compilation (QWC) cost function based on the quantum Wasserstein distance of order 1. An estimation method based on measurements of local Pauli-observable is utilized in a generative adversarial network to learn a given quantum circuit.
  arXiv  Detail & Related papers  (2024-09-09T17:46:40Z)
• QuantumSEA: In-Time Sparse Exploration for Noise Adaptive Quantum Circuits [82.50620782471485]
  QuantumSEA is an in-time sparse exploration for noise-adaptive quantum circuits. It aims to achieve two key objectives: (1) implicit circuits capacity during training and (2) noise robustness. Our method establishes state-of-the-art results with only half the number of quantum gates and 2x time saving of circuit executions.
  arXiv  Detail & Related papers  (2024-01-10T22:33:00Z)
• Demonstration of fault-tolerant Steane quantum error correction [0.7174990929661688]
  This study presents the implementation of multiple rounds of fault-tolerant Steane QEC on a trapped-ion quantum computer. Various QEC codes are employed, and the results are compared to a previous experimental approach utilizing flag qubits.
  arXiv  Detail & Related papers  (2023-12-15T12:32:49Z)
• Quantum Algorithms for State Preparation and Data Classification based on Stabilizer Codes [0.0]
  We propose a prototype quantum circuit model for classification of classical data. A quantum neural network (QNN) layer is realized by a stabilizer code which consists of many stabilizers. We also consider the first challenge to most applications of quantum computers, including data classification.
  arXiv  Detail & Related papers  (2023-09-18T19:02:54Z)
• symQV: Automated Symbolic Verification of Quantum Programs [0.0]
  We present symQV, a symbolic execution framework for writing and verifying quantum computations. symQV can automatically verify that a quantum program complies with a first-order specification.
  arXiv  Detail & Related papers  (2022-12-05T13:46:27Z)
• Probing finite-temperature observables in quantum simulators of spin systems with short-time dynamics [62.997667081978825]
  We show how finite-temperature observables can be obtained with an algorithm motivated from the Jarzynski equality. We show that a finite temperature phase transition in the long-range transverse field Ising model can be characterized in trapped ion quantum simulators.
  arXiv  Detail & Related papers  (2022-06-03T18:00:02Z)
• Circuit Symmetry Verification Mitigates Quantum-Domain Impairments [69.33243249411113]
  We propose circuit-oriented symmetry verification that are capable of verifying the commutativity of quantum circuits without the knowledge of the quantum state. In particular, we propose the Fourier-temporal stabilizer (STS) technique, which generalizes the conventional quantum-domain formalism to circuit-oriented stabilizers.
  arXiv  Detail & Related papers  (2021-12-27T21:15:35Z)
• QECV: Quantum Error Correction Verification [15.05397810840915]
  We propose QECV, a verification framework that can efficiently verify the formal correctness of stabilizer codes. We derive a sound quantum Hoare logic proof system with a set of inference rules for QECV to efficiently reason about the correctness of QEC programs.
  arXiv  Detail & Related papers  (2021-11-26T19:40:53Z)
• Tensor Network Quantum Virtual Machine for Simulating Quantum Circuits at Exascale [57.84751206630535]
  We present a modernized version of the Quantum Virtual Machine (TNQVM) which serves as a quantum circuit simulation backend in the e-scale ACCelerator (XACC) framework. The new version is based on the general purpose, scalable network processing library, ExaTN, and provides multiple quantum circuit simulators. By combining the portable XACC quantum processors and the scalable ExaTN backend we introduce an end-to-end virtual development environment which can scale from laptops to future exascale platforms.
  arXiv  Detail & Related papers  (2021-04-21T13:26:42Z)
• Sampling Overhead Analysis of Quantum Error Mitigation: Uncoded vs. Coded Systems [69.33243249411113]
  We show that Pauli errors incur the lowest sampling overhead among a large class of realistic quantum channels. We conceive a scheme amalgamating QEM with quantum channel coding, and analyse its sampling overhead reduction compared to pure QEM.
  arXiv  Detail & Related papers  (2020-12-15T15:51:27Z)
• Quantum circuit architecture search for variational quantum algorithms [88.71725630554758]
  We propose a resource and runtime efficient scheme termed quantum architecture search (QAS) QAS automatically seeks a near-optimal ansatz to balance benefits and side-effects brought by adding more noisy quantum gates. We implement QAS on both the numerical simulator and real quantum hardware, via the IBM cloud, to accomplish data classification and quantum chemistry tasks.
  arXiv  Detail & Related papers  (2020-10-20T12:06:27Z)

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.