Invited Talk: From Verified Compilation to Shor’s Algorithm
Programming quantum computers is challenging. Quantum algorithms are often probabilistic, and the unique aspects of quantum computation—superposition, entanglement, and state collapse due to measurement—can be hard for programmers to grasp. Program errors can be difficult (and expensive) to test and debug. These inherent challenges are compounded by near-term limitations on hardware resources like qubits and gates, both in terms of their number and their reliability.
To address these challenges, my collaborators and I have been applying formal methods to quantum programming.
We began by developing VOQC, a verified optimizer for quantum circuits. VOQC optimizes programs written in SQIR, the simple quantum intermediate language, which expresses circuits similarly to OpenQASM. VOQC is embedded in the Coq proof assistant, and we have proved that all of its transformations preserve their input programs’ semantics. Next, we used SQIR to express several well known quantum algorithms, notably including Grover’s search, the Quantum Fourier Transform, and Quantum Phase Estimation, and proved them correct. (While SQIR was designed as an IR, it is not far away from how people write quantum algorithms today.) Both efforts required novel developments in proof engineering. Finally, for the past year or so, we have developed and proved correct a full implementation of Shor’s prime factoring algorithm, which we can run (with simulation) end to end. As a hybrid quantum-classical algorithm, Shor’s ends up using Coq code (extracted to OCaml) for the classical parts (pre- and post-processing), and SQIR circuits for the quantum part (order finding).
Overall, we see significant promise in the use of formal methods for quantum computing, and we continue to expand the breadth and depth of our framework. All of our code is freely available online (including a Python front end to VOQC) at https://github.com/inQWIRE/SQIR
This is joint work with Kesha Hietala, Robert Rand, Yuxiang Peng, Runzhou Tao, Liyi Li, Shih-Han Hung, and Xiaodi Wu.
Michael Hicks is a Professor in the Computer Science department and UMIACS at the University of Maryland, where he co-directs the laboratory for Programming Languages research (PLUM); he is the former Director of the Maryland Cybersecurity Center (MC2) and the Past Chair of ACM SIGPLAN.
His research focuses on using programming languages and analyses to improve the security, reliability, and availability of software. He is perhaps best known for his work exploring dynamic software updating, a technique with which software can be updated without shutting it down. He has explored the design of new programming languages and analysis tools for helping programmers find bugs and software vulnerabilities, and for identifying suspicious or incorrect program executions. He was worked has combined ideas from PL and cryptography, e.g., to ensure privacy preserving computations. He also leads the development of a new security-oriented programming contest, “build-it, break-it, fix-it,” which has been offered to the public and to students in his Coursera class on software security. He has recently begun to explore programming languages for quantum computation.
Tue 22 JunDisplayed time zone: Eastern Time (US & Canada) change
09:00 - 11:45
|Invited Talk: From Verified Compilation to Shor’s Algorithm|
I: Michael Hicks University of Maryland at College ParkFile Attached
|qKleene: Verification of Quantum RAM Made Easy|
Giulia De Santis University of Verona, Roberto Giacobazzi University of Verona, Margherita Zorzi University of VeronaFile Attached
|JKQ: JKU Tools for Quantum Computing|
Wille Robert Johannes Kepler University, Linz, Stefan Hillmich Johannes Kepler University, Linz, Lukas Burgholzer Johannes Kepler University, LinzFile Attached
|Open Quantum Assembly Language|
Andrew Cross IBM T.J Watson Research Center, Ali Javadi-Abhari IBM T.J Watson Research Center, Thomas Alexander IBM T.J Watson Research Center, Lev Bishop IBM T.J Watson Research Center, Colm A. Ryan AWS Center for Quantum Computing, Steven Heidel AWS Center for Quantum Computing, Niel de Beaudrap University of Sussex, John Smolin IBM T.J Watson Research Center, Jay M. Gambetta IBM T.J Watson Research Center, Blake R. Johnson IBM T.J Watson Research CenterFile Attached
|Quantum and classical registers|
Dominique Unruh University of TartuFile Attached
|Addressable quantum gates|
Pablo Arrighi Université Paris-Saclay, CNRS, LMF, Marin Costes Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Christopher Cedzich Quantum Technology Group, Heinrich Heine Universität Düsseldorf, Ulysse Remond Université Paris-Saclay, CNRS, ENS Paris-Saclay, LMF, Benoit Valiron Université Paris-Saclay, CNRS, CentraleSupélec, LMFFile Attached