Formal Computer Validation of the Quantum Phase Estimation Algorithm

While peer review and scientific consensus provide some assurance to the validity of ideas, people do make mistakes that can slip through the cracks. A plethora of formal methods tools exist and are in use in a variety of settings where high assurance is demanded. Existing tools, however, require a great deal of expertise and lack versatility, demanding a non-trivial translation between a high-level description of a problem and the formal system. Our software, called Prove-It, allows a nearly direct translation between human-recognizable formulations and the underlying formal system. While Prove-It is not designed for particularly efficient automation, a primary goal of other formal methods tools, it is extremely flexible in following a desired line of reasoning (proof structure). This approach is particularly valuable for validating proofs that are already known. We will demonstrate a validation of the Quantum Phase Estimation Algorithm using Prove-It. Sandia National Laboratories is a multi-program laboratory managed and operated by Sandia Corporation, a wholly owned subsidiary of Lockheed Martin Corporation, for the U.S. Department of Energy’s National Nuclear Security Administration under contract DE-AC04-94AL85000.