A Symbolic Approach to Verifying Quantum Systems

Simon J. Gay, Rajagopal Nagarajan

Xin Hong, Wei‐Jia Huang, Wei‐Chen Chien +5 more

With the rapid development of quantum computing, automatic verification of quantum circuits becomes more and more important. While several decision diagrams (DDs) have been introduced in quantum circuit simulation and verification, none of them supports symbolic computation. Algorithmic manipulations of symbolic objects, however, have been identified as crucial, if not indispensable, for several verification tasks. This paper proposes the first decision-diagram approach for operating symbolic objects and verifying quantum circuits with symbolic terms. As a notable example, our symbolic tensor decision diagrams (symbolic TDD) could verify the functionality of the 160-qubit quantum Fourier transform circuit within three minutes. Moreover, as demonstrated on Bernstein-Vazirani algorithm, Grover's algorithm, and the bit-flip error correction code, the symbolic TDD enables efficient verification of quantum circuits with user-supplied oracles and/or classical controls.

Paulo Mateus, Amı́lcar Sernadas

Alcântara, Pedro Antonio Soares de

In this work, we investigate the correspondence principle applied to mechanical systems symmetric under a compact Lie group by means of symbol correspondences. In the first part, we consider systems symmetric under SU(2), the so-called spin systems: we verify conditions under which symbol correspondences present localization of pure states at the semiclassical limit, which provides a new criterion for the emergence of classical dynamics; then, we introduce the notion of sequential quantization from which we get a new characterization of asymptotic localization. In the second part, we begin the study of symbol correspondences for systems symmetric under SU(3), the quark systems: we characterize the symbol correspondences for such systems and obtain some properties and formulas for twisted products induced on the spaces of symbols.

António Pereira, Rosália Rodrigues

Yu‐Fang Chen, Kai-Min Chung, Ondřej Lengál +2 more

Abstract We present a specification language and a fully automated tool named AutoQ for verifying quantum circuits symbolically. The tool implements the automata-based algorithm from [14] and extends it with the capabilities for symbolic reasoning. The extension allows to specify relational properties, i.e., relationships between states before and after executing a circuit. We present a number of use cases where we used AutoQ to fully automatically verify crucial properties of several quantum circuits, which have, to the best of our knowledge, so far been proved only with human help.