



01921nas a2200205   4500008004100000245009400041210006900135260001500204520125300219653004301472653002701515653003401542653003101576100001301607700001701620700001201637700001401649700001501663856003701678       2022                        eng d00aQuantum Natural Proof: A New Perspective of Hybrid Quantum-Classical Program Verification0 aQuantum Natural Proof A New Perspective of Hybrid QuantumClassic  c11/11/20223 a<p>Many quantum programs are assured by formal verification, but such verification is usually laborious and time-consuming. This paper proposes quantum natural proof (QNP), an automated proof system for verifying hybrid quantum-classical algorithms. Natural proofs are a subclass of proofs that are amenable to completely automated reasoning, provide sound but incomplete procedures, and capture common reasoning tactics in program verification. The core of QNP is a type-guided quantum proof system, named Qafny, which views quantum operations as some classical array operations that can be modeled as proof rules in a classical separation logic framework, suitable for automated reasoning. We proved the soundness and completeness of the Qafny proof system as well as the soundness of the proof system compilation from Qafny to Dafny. By using the QNP implementation in Dafny, automated verification can be efficiently perform for many hybrid quantum-classical algorithms, including GHZ, Shor&#39;s, Grover&#39;s, and quantum walk algorithms, which saves a great amount of human efforts. In addition, quantum programs written in Qafny can be compiled to quantum circuits so that every verified quantum program can be run on a quantum machine.</p>10aFOS: Computer and information sciences10aFOS: Physical sciences10aProgramming Languages (cs.PL)10aQuantum Physics (quant-ph)1 aLi, Liyi1 aZhu, Mingwei1 aLee, Yi1 aChang, Le1 aWu, Xiaodi  uhttps://arxiv.org/abs/2211.06411