Theoretical and Practical High-Assurance Software Tools for Quantum Applications
Yuxiang Peng
Friday, November 18, 2022, 2:00-4:00 pm 
Abstract
Recent developments in high-precision manipulation of microscopic quantum systems push quantum applications to the brink of the first quantum advantage on realistic problems, such as simulation of quantum systems and big integer factorization. Research attentions to the realization of near-term devices focus on challenges from hardware errors. Another less noticed but equally important challenge is to faithfully implement high-level quantum algorithms. High-assurance software toolchains for quantum applications are essential in reducing human errors, breaking knowledge barriers across different fields, and improving productivity.
My research focuses on developing theoretical and practical tools to improve the assurance of software for quantum applications, broadly tackling problems in programming, debugging, and compiling quantum programs. Firstly, since most classical debugging techniques fail on quantum programs, we establish a framework via formal methods to mechanically certify the correctness of quantum programs and illustrate its power by certifying an implementation of Shor's algorithm, one of the most complicated quantum algorithms. Then, to ensure invariance when compilers translate programs through code transformation, we employ an algebraic approach to efficiently and succinctly validate quantum program equivalences via non-idempotent Kleene algebra. The aforementioned paradigm of quantum applications—programming and compiling quantum circuits to executable pulses on analog devices—induces impractically large overhead, hence we formulate analog quantum computing for quantum applications, skipping the gate abstraction. We present SimuQ, a framework for quantum simulation via analog quantum computing, to mitigate the inconveniences posed by programming quantum systems and engineering vast kinds of quantum devices. Lastly, to obtain high-quality pulses, we propose a differentiable framework for analog quantum computing, which significantly boosts the performance of quantum optimization and quantum control and can be integrated into SimuQ seamlessly.
My research focuses on developing theoretical and practical tools to improve the assurance of software for quantum applications, broadly tackling problems in programming, debugging, and compiling quantum programs. Firstly, since most classical debugging techniques fail on quantum programs, we establish a framework via formal methods to mechanically certify the correctness of quantum programs and illustrate its power by certifying an implementation of Shor's algorithm, one of the most complicated quantum algorithms. Then, to ensure invariance when compilers translate programs through code transformation, we employ an algebraic approach to efficiently and succinctly validate quantum program equivalences via non-idempotent Kleene algebra. The aforementioned paradigm of quantum applications—programming and compiling quantum circuits to executable pulses on analog devices—induces impractically large overhead, hence we formulate analog quantum computing for quantum applications, skipping the gate abstraction. We present SimuQ, a framework for quantum simulation via analog quantum computing, to mitigate the inconveniences posed by programming quantum systems and engineering vast kinds of quantum devices. Lastly, to obtain high-quality pulses, we propose a differentiable framework for analog quantum computing, which significantly boosts the performance of quantum optimization and quantum control and can be integrated into SimuQ seamlessly.
Examining Committee
Bio
Yuxiang Peng is a PhD student at the Department of Computer Science, University of Maryland, College Park. He is also affiliated to the Joint Center for Quantum Information and Computer Science. He is currently advised by Prof. Xiaodi Wu. His research interests are broadly in programming languages, quantum computing and physics. He received his bachelor's degrees from the Institute for Interdisciplinary Information Science and the Department of Mathematical Science, Tsinghua University, and his master's degree from the Department of Computer Science, University of Maryland, College Park.
This talk is organized by Tom Hurst