Verifying Quantum Phase Estimation (QPE) using Prove-It

TL;DR

The ability to follow a textbook proof to produce a formally certified proof is demonstrated, highlighting useful automation features to fill in obvious steps and make formal proving nearly as straightforward as informal theorem proving.

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.

Figures (18)

• Figure 1: Excerpt from the proof notebook for _mod_add_closure (local QPE) theorem, showing the interactive steps (left) and the Prove-It-generated formal proof (right).
• Figure 2: Quantum circuit implementing the QPE algorithm. From initial first-register state $\ket{0}_{t}$ and second register state $\ket{u}$, we apply Hadamards to the first register lines, controlled $U^{2^j}$ to the second register, and an inverse quantum Fourier transform $\text{QFT}^{\dagger}$ to the first register, leading to first-register measurement $\ket{2^t \tilde{\varphi}}$, where $\tilde{\varphi}$ is an estimate of the phase.
• Figure 3: Illustration of the bounds $\frac{2}{\pi}\theta \le |1 - e^{i\theta}| \le 2$ for $\theta \in [0, \pi]$ and $\sin{\theta} \ge \frac{2}{\pi}\theta$ for $\theta \in [0, \frac{\pi}{2}]$, utilized in the proof of _alpha_sqrd_upper_bound (\ref{['eq:thm_alpha_sqrd_upper_bound']}), and the bound $\sin\theta < \theta$ for $\theta > 0$ used in the proof of _best_guarantee_delta_nonzero (\ref{['eq:thm_best_guarantee_delta_nonzero']}).
• Figure 4: Comparison of Nielsen & Chuang's Nielsen_Chuang:2010 original upper bound vs. our new, tighter upper bound on the probability of "failure" versus the number of unit steps $e$ away from the "best" floor-based estimate $b_{f}$.
• Figure 5: Obtaining a sub-proof from within a proof in Prove-It.