arXiv:2205.02287 · Proceedings of the ACM on Programming Languages

Twist: sound reasoning for purity and entanglement in Quantum programs

Charles Yuan, Christopher M. McNally, Michael Carbin

Published Jan 12, 2022• 31 citations

Abstract

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%.

DOI: 10.1145/3498691

Related papers

Statistical assertions for validating patterns and finding bugs in quantum programs

Yipeng Huang, Margaret Martonosi

In support of the growing interest in quantum computing experimentation, programmers need new tools to write quantum algorithms as program code. Compared to debugging classical programs, debugging quantum programs is difficult because programmers have limited ability to probe the internal states of quantum programs; those states are difficult to interpret even when observations exist; and programmers do not yet have guidelines for what to check for when building quantum programs. In this work, we present quantum program assertions based on statistical tests on classical observations. These allow programmers to decide if a quantum program state matches its expected value in one of classical, superposition, or entangled types of states. We extend an existing quantum programming language with the ability to specify quantum assertions, which our tool then checks in a quantum program simulator. We use these assertions to debug three benchmark quantum programs in factoring, search, and chemistry. We share what types of bugs are possible, and lay out a strategy for using quantum programming patterns to place assertions and prevent bugs.

arXiv:1905.09721Proceedings - International Symposium on Computer Architecture/ProceedingsJun 14, 2019164 citations

Verification of Nondeterministic Quantum Programs

Yuan Feng, Yingte Xu

Nondeterministic choice is a useful program construct that provides a way to describe the behaviour of a program without specifying the details of possible implementations. It supports the stepwise refinement of programs, a method that has proven useful in software development. Nondeterminism has also been introduced in quantum programming, and termination of nondeterministic quantum programs has been extensively analysed. In this paper, we go beyond termination analysis to investigate the verification of nondeterministic quantum programs where properties are given by sets of hermitian operators on the associated Hilbert space. Hoare-type logic systems for partial and total correctness are proposed which turn out to be both sound and relatively complete with respect to their corresponding semantic correctness. To show the utility of these proof systems, we analyse some quantum algorithms such as quantum error correction scheme, Deutsch algorithm, and a nondeterministic quantum walk. Finally, a proof assistant prototype is implemented to aid in the automated reasoning of nondeterministic quantum programs.

arXiv:2302.07973International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS)Mar 20, 202311 citations

Hybrid Path-Sums for Hybrid Quantum Programs

Christophe Chareton, Jad Issa, Mathieu Nguyen +2 more

As quantum computing becomes an emerging reality, designing efficient quantum programming capabilities is becoming more and more important. Particularly, the debugging and validation of quantum programs is of paramount importance, as these programs are by definition hard to test. Static analysis and formal verification methods for quantum programs started to emerge a few years now, yet they often miss hybrid quantum/classical reasoning facilities with, e.g., generic quantum control, classical control and classical computation instructions. In this paper, we lay out the foundations of a framework for the automated formal verification of (full) hybrid quantum programs featuring both classical and quantum control, measurement and hybrid data structures. In particular, we propose: (1) a novel symbolic representation for describing and manipulating sets of hybrid quantum/classical states called Hybrid Path-Sums (HPS); (2) a set of rewriting rules providing a rich mechanism for simplifying and reasoning on these symbolic hybrid states, and (3) a core assertion language to specify equivalence of hybrid quantum programs, the satisfaction of properties on (parts of) hybrid states, and the extraction of probabilistic statements about the program behavior. We prove the correctness of the novel symbolic representation, of its rewriting system and of the specification system. Finally, we propose a full implementation of this framework as a dedicated symbolic execution engine for hybrid programs. We present an evaluation of a set of representative hybrid case-studies from the literature, showcasing the advantage of our approach and its efficiency compared to state-of-the-art solutions.

arXiv:2604.24578Proceedings of the ACM on Programming LanguagesJun 8, 20260 citations

CoqQ: Foundational Verification of Quantum Programs

Li Zhou, Gilles Barthe, Pierre-Yves Strub +2 more

CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (MathComp and MathComp Analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature.

arXiv:2207.11350Proceedings of the ACM on Programming LanguagesJan 9, 202335 citations

Formal Specification and Verification of Quantum Computing Algorithms

Jincheng Zhang

The verification of quantum computing algorithms presents a significant hurdle due to the probabilistic nature of quantum mechanics and the complex entanglement inherent in quantum computations. This paper proposes a novel approach to address this challenge by developing a formal language and a corresponding verification tool tailored explicitly for quantum algorithm specification and verification. The system leverages concepts from quantum information theory and formal methods to provide a rigorous framework for ensuring the correctness of quantum algorithms. We introduce a new formalism that allows for precise description of quantum circuits and their operations, combined with automated theorem proving techniques to systematically verify the algorithm's behavior against a given specification. The key innovation lies in the ability to reason about quantum states and measurements within a formal setting, enabling a more comprehensive understanding and validation of these algorithms. This work lays the foundation for increased confidence in the development and deployment of quantum computing technologies.

Sep 2, 20260 citations

A Framework for the Efficient Evaluation of Runtime Assertions on Quantum Computers

Damian Rovara, Lukas Burgholzer, Robert Wille

The continuous growth of quantum computing and the increasingly complex quantum programs resulting from it lead to unprecedented obstacles in ensuring program correctness. Runtime assertions are, therefore, becoming a crucial tool in the development of quantum programs. They assist developers in the debugging process and help to test and verify the program. However, while assertions can be implemented in a straightforward manner on classical computers, physical limitations of quantum computers pose considerable challenges for the evaluation of quantum assertions. Access to the quantum state of a program is limited, execution time is expensive and noise can significantly distort measurement outcomes. To address these problems, this work proposes a framework that assists developers in the evaluation of runtime assertions on real quantum computers. It translates a variety of assertions into sets of measurements, reduces execution overhead where possible and evaluates the measurement results after the execution even in the presence of noise. This approach substantially aids developers in the debugging process, enabling efficient assertion-driven debugging even in large programs. The proposed framework is available as an open-source implementation at https://github.com/munich-quantum-toolkit/debugger

arXiv:2505.03885IEEE International Conference on Quantum Software (QSW)Jul 1, 20260 citations