Formal Verification of Quantum Programs

Presented by Jennifer Paykin, Galois

State-of-the-art quantum programming languages allow users to design and implement sophisticated quantum algorithms in terms of low-level primitives---circuits, unitary gates, and measurement. Such programs are difficult to debug using classical methods like benchmarking and unit testing because we cannot look inside a quantum computer to find out what went wrong in a quantum computation. Simulating quantum algorithms on classical computers is useful for small cases but intractable in general. So then how can we make sure that a quantum program is implementing the algorithm it is supposed to?

In this talk I will discuss how to use formal verification to prove the correctness of unbounded quantum circuits using QWIRE (https://github.com/inQWIRE/QWIRE), a small but expressive language for quantum circuits embedded in the Coq proof assistant. In QWIRE we can write programs, specify their correctness with respect to standard mathematical models, and prove that our implementations satisfy these specifications. I will illustrate several sorts of properties that one might want to verify using examples, and discuss some of the design decisions and trade-offs that go into any verification project.