Abstract:  Quantum computers can solve tasks infeasible for classical computers. Given the rapid progress toward constructing quantum devices, a major challenge is to verify the correctness of quantum computation, especially as the devices reach scales that rule out classical simulation. In this talk, we present research progress toward efficient verification of quantum computation, in the following two aspects. First, the correctness of quantum designs is usually claimed with mathematical proofs written by human experts. However, by-hand proofs inevitably have bugs due to the complexity of reasoning. To detect potential flaws, we exploit formal methods to rigorously validate the correctness of quantum designs. Specifically, we provide a framework for formally verifying quantum circuit optimizations and quantum algorithms. Secondly, we study how a classical system commands an adversarial quantum system to realize arbitrary quantum dynamics. In particular, we construct protocols for demonstrating how a completely classical device can verify the correctness of an untrusted quantum computer for problems solvable in quantum polynomial time.  

Please use this link to attend the virtual seminar:

https://bluejeans.com/486377316/6893

Meeting ID: 486377316 / Participant Passcode: 6893