Formal methods for reliable, high-performance quantum computing

点击翻译按钮获取中文摘要

My research program aims to understand the real-world computational capabilities and practical advantages of quantum computers. On a theoretical level, quantum computation promises the ability to solve certain problems exponentially faster than the best known classical algorithms. Notable examples include integer factorization and computing discrete logarithms, which together break many conventional cryptographic methods, as well as the simulation of quantum systems. The latter in particular, serving as the original motivation for the development of quantum computers, has the potential for far-reaching impacts on society by facilitating advances in drug, material, and chemical design. A canonical first real-world application is the simulation of nitrogenase, an enzyme involved in the process of nitogren fixation needed for fertiziler production, which has resisted simulation even with modern super-computers. Advances in nitrogen and carbon fixation could have deep impacts on our ability to fight climate change. In practice however, executing large-scale quantum algorithms on real hardware involves a high degree of overhead, due to both the constraints of the computational model and the need for error correction. To properly characterize the advantages of error-corrected quantum computers, a practical accounting of this overhead in terms of concrete computational resources (e.g. time, number of qubits, classical processing power), known as resource estimation, is needed. On the other hand, quantum hardware is rapidly approaching potentially useful sizes and the practical applications of these smaller-scale, noisy devices needs to be determined through use and experimentation. In both cases, effective software tools are needed to program and compile these algorithms. Moreover, as quantum programs are exceedingly difficult to debug and next to impossible to simulate, methods of establishing the correctness of this quantum code are necessary. While for near-term applications errors often lead to headaches or failed experiments, for large-scale resource estimation an unreliable process can erode confidence in the estimates or lead to wildly inaccurate ones. The goal of this research program is to enable the development of reliable, high-performance and portable quantum software. I plan to develop novel methods for mathematically reasoning about quantum computation and apply these to the specification, formal verification, and optimization of quantum programs. I intend to integrate these into low-level quantum programming and specification languages so that optimized libraries of quantum code can be written and verified once, then re-used for years to come. I expect the contributions of this research program will have far reaching impacts on the practical usage and analysis of quantum computers by allowing algorithms to be easily and reliably translated from theory into practice.