Verifying Quantum Circuits And Quantum Programs In Coq

Quantum computing is a new computing paradigm that follows the laws of quan-tum mechanics and regulates quantum information units for computing.It is more ef-ficient and secure than classical computing.However,the properties that give rise to these advantages,such as superposition and entanglement,also make quantum comput-ing complex and uncertain.Due to quantum non-clonability and decoherence effects,there are still many obstacles to large-scale and high-precision quantum computing.Therefore,it is very difficult to evaluate the correctness of quantum algorithms by exe-cuting or simulating quantum programs.In recent years,more and more research work has used formal verification methods to analyze the correctness of quantum algorithms.In this thesis,we first propose a method based on Dirac notation to symbolically reason about the behavior of quantum circuits.Then we define an imperative program-ming language that supports the interaction of classical and quantum data.Quantum circuit is the basic model of quantum computing,and quantum programs are also an important way to describe algorithms.They are key elements in the deployment of quantum computing.In order to avoid the state-space explosion problem in model checking,we choose to use interactive theorem provers to reason about the behavior of quantum circuits and quantum programs.The main contributions of this thesis are as follows:· We embed a matrix representation method based on Dirac notation in Coq.It utilizes some constructors,including scalar multiplication ·,matrix addition +,ma-trix multiplication ×,tensor multiplication ? and conjugate transpose Aof matrix A,and combines complex numbers C and the basic vectors [1 0]Tand [0 1]Tto con-struct terms,quantum states and quantum operations used in quantum computing.It improves the readability of the matrices.· Based on terms expressed in Dirac notation,we design a set of(semi)automated symbolic reasoning strategies to verify quantum circuits.These strategies are based on a set of inference rules.The key idea is to reduce matrix multiplication of the form i|j to scalars,and to reduce terms by assimilating identity matrices and eliminating zero matrices.This symbolic approach reasons about matrices by automatically rewriting them rather than actually computing them.It improves the efficiency of reasoning about the behavior of quantum circuits.· We formally define a classical-quantum imperative language in Coq.The clas-sical part of the language includes skip statements,classical assignments,condi-tional statements,and while loops.The quantum part of the language includes quantum unitary transformations and quantum measurements.Since quantum mea-surements yield probability distributions of states,branching information can be added to the semantics to distinguish all the different reachable states.· We prove the consistency of the operational and denotational semantics.In order to describe quantum programs more intuitively,we lift the denotational se-mantics from states to distributions of states,and prove the relationship between the two denotational semantics before and after a transformation.This thesis verifies the correctness of some typical quantum algorithms.First,some quantum algorithms are circuitized,and symbolic reasoning strategies are used to reason about the behavior of these quantum circuits.Quantum algorithms are further verbalized,using the defined quantum programming language,and finally combing the state transition specifications defined by the denotational semantics with the symbolic reasoning strategy to prove the correctness of quantum algorithms.In addition,we con-duct experiments to show that,compared with the method based on explicit matrix rep-resentation,the method based on Dirac notation improves the efficiency and readability of the reasoning process when verifying quantum algorithms.