Verifying Quantum Phase Estimation (QPE) using Prove-It
Abstract
The general-purpose interactive theorem-proving assistant called Prove-It was used to verify the Quantum Phase Estimation (QPE) algorithm, specifically claims about its outcome probabilities. Prove-It is unique in its ability to express sophisticated mathematical statements, including statements about quantum circuits, integrated firmly within its formal theorem-proving framework. We demonstrate our ability to follow a textbook proof to produce a formally certified proof, highlighting useful automation features to fill in obvious steps and make formal proving nearly as straightforward as informal theorem proving. Finally, we make comparisons with formal theorem-proving in other systems where similar claims about QPE have been proven.
Keywords
Cite
@article{arxiv.2304.02183,
title = {Verifying Quantum Phase Estimation (QPE) using Prove-It},
author = {Wayne M. Witzel and Warren D. Craft and Robert Carr and Deepak Kapur},
journal= {arXiv preprint arXiv:2304.02183},
year = {2024}
}
Comments
28 pages, 18 figures, 5 tables. Prove-It theorem-proving results available at http://pyproveit.org/ and Prove-It code available at https://github.com/PyProveIt/Prove-It