arXiv:1511.01572 · Electronic Proceedings in Theoretical Computer Science

Analysis of Quantum Entanglement in Quantum Programs using Stabilizer Formalism

Kentaro Honda

Published Nov 3, 2015• 14 citations

Abstract

Quantum entanglement plays an important role in quantum computation and communication. It is necessary for many protocols and computations, but causes unexpected disturbance of computational states. Hence, static analysis of quantum entanglement in quantum programs is necessary. Several papers studied the problem. They decided qubits were entangled if multiple qubits unitary gates are applied to them, and some refined this reasoning using information about the state of each separated qubit. However, they do not care about the fact that unitary gate undoes entanglement and that measurement may separate multiple qubits. In this paper, we extend prior work using stabilizer formalism. It refines reasoning about separability of quantum variables in quantum programs.

DOI: 10.4204/eptcs.195.19

Related papers

Static Entanglement Analysis of Quantum Programs

Shangzhou Xia, Jianjun Zhao

Quantum entanglement plays a crucial role in quantum computing. Entangling information has important implications for understanding the behavior of quantum programs and avoiding entanglement-induced errors. Entanglement analysis is a static code analysis technique that determines which qubit may entangle with another qubit and establishes an entanglement graph to represent the whole picture of interactions between entangled qubits. This paper presents the first static entanglement analysis method for quantum programs developed in the practical quantum programming language Q#. Our method first constructs an interprocedural control flow graph (ICFG) for a Q# program and then calculates the entanglement information not only within each module but also between modules of the program. The analysis results can help improve the reliability and security of quantum programs.

arXiv:2304.05049IEEE/ACM International Workshop on Quantum Software Engineering (Q-SE)May 1, 202313 citations

Classical Analysis of Quantum Computation

Kentaro Honda

Quantum computation is based on quantum physics and different from classical computation based on classical physics.It has non-classical characteristics such as quantum superposition principle, uncertainty principle, and no-cloning theorem and has been mainly studied by original methodology.However, it does not mean we cannot investigate quantum computation using traditional methods that have been studied in non-quantum area.We believe that quite a lot of methods are useful to investigate quantum computation and it is important to find such methods.When they are found, they will accelerate the research of quantum computation using the knowledge about them.Moreover, due to their classical nature, they will naturally help us to analyse quantum computation using classical computers.In order to support the idea, we show two classical methodologies, abstract interpretation and classical public-key cryptography, enhance analysis in two topics of quantum computation, entanglement in quantum programming languages and blind quantum computation protocols.The behaviour of entangled quantum system is counterintuitive.Therefore, it is important to know how entangled states are in quantum programs without executing them.In order to statistically analyse the problem, it was proposed to apply the abstract interpretation technique to the analysis.However, the proposed method does not store information about entangled states and ignores the fact that an operator on multiple qubits may undo entanglements, and hence the method only gives a rough approximation.We combine the method with the stabiliser formalism.We show abstract interpretation can be used to efficiently analyse the existence of entanglement in quantum programs with higher precision.Blind quantum computation protocols give users having no powerful quantum devices a method to delegate their quantum computation to remote quantum servers without leaking any crucial information about their computation.Some protocols enable users to verify whether the quantum servers honestly do the delegated computation, but no protocols give third parties ways to analyse the computation.We propose a new blind quantum computation protocol using a classical public-key encryption scheme.Our protocol is based on an existing protocol, but third parties, who have only classical computers and check the classical message between users and quantum servers, can analyse the computation and verify whether users obtain the correct outcomes or not.These results show classical methodology, which achieves a development outside the area of quantum computation, may be useful for investigation of quantum computation.

Mar 24, 20160 citations

Twist: sound reasoning for purity and entanglement in Quantum programs

Charles Yuan, Christopher M. McNally, Michael Carbin

Quantum programming languages enable developers to implement algorithms for quantum computers that promise computational breakthroughs in classically intractable tasks. Programming quantum computers requires awareness of entanglement , the phenomenon in which measurement outcomes of qubits are correlated. Entanglement can determine the correctness of algorithms and suitability of programming patterns. In this work, we formalize purity as a central tool for automating reasoning about entanglement in quantum programs. A pure expression is one whose evaluation is unaffected by the measurement outcomes of qubits that it does not own, implying freedom from entanglement with any other expression in the computation. We present Twist, the first language that features a type system for sound reasoning about purity. The type system enables the developer to identify pure expressions using type annotations. Twist also features purity assertion operators that state the absence of entanglement in the output of quantum gates. To soundly check these assertions, Twist uses a combination of static analysis and runtime verification. We evaluate Twist’s type system and analyses on a benchmark suite of quantum programs in simulation, demonstrating that Twist can express quantum algorithms, catch programming errors in them, and support programs that existing languages disallow, while incurring runtime verification overhead of less than 3.5%.

arXiv:2205.02287Proceedings of the ACM on Programming LanguagesJan 12, 202231 citations

Entanglement in the stabilizer formalism

David A. Fattal, Toby S. Cubitt, Y. Yamamoto +2 more

We define a multi-partite entanglement measure for stabilizer states, which can be computed efficiently from a set of generators of the stabilizer group. Our measure applies to qubits, qudits and continuous variables.

arXiv:quant-ph/0406168Jun 23, 200469 citations

Entanglement verification using local unitary stabilizers

David W. Lyons, Scott N. Walck

Local unitary stabilizer subgroups constitute powerful invariants for distinguishing various types of multipartite entanglement. In this paper, we show how stabilizers can be used as a basis for entanglement verification protocols on distributed quantum networks using minimal resources. As an example, we develop and analyze the performance of a protocol to verify membership in the space of Werner states, that is, multiqubit states that are invariant under the action of any one-qubit unitary applied to all the qubits.

arXiv:1303.6497Physical Review AJun 19, 20132 citations

Lecture notes on quantum entanglement: From stabilizer states to stabilizer channels

Amir R. Arab

We study mathematical, physical and computational aspects of the stabilizer formalism arising in quantum information and quantum computation. The measurement process of Pauli observables with its algorithm is given. It is shown that to detect genuine entanglement we need a full set of stabilizer generators and the stabilizer witness is coarser than the GHZ (Greenberger–Horne–Zeilinger) witness. We discuss stabilizer codes and construct a stabilizer code from a given linear code. We also discuss quantum error correction, error recovery criteria and syndrome extraction. The symplectic structure of the stabilizer formalism is established and it is shown that any stabilizer code is unitarily equivalent to a trivial code. The structure of graph codes as stabilizer codes is identified by obtaining the respective stabilizer generators. The distance of embeddable stabilizer codes in lattices is obtained. We discuss the Knill–Gottesman theorem, tableau representation and frame representation. The runtime of simulating stabilizer gates is obtained by applying stabilizer matrices. Furthermore, an algorithm for updating global phases is given. Resolution of quantum channels into stabilizer channels is shown. We discuss capacity achieving codes to obtain the capacity of the quantum erasure channel. Finally, we discuss the shadow tomography problem and an algorithm for constructing classical shadow is given.

Frontiers of PhysicsApr 16, 20243 citations