Formal methods for reliable, high-performance quantum computing

可靠、高性能量子计算的形式化方法

• 批准号: RGPIN-2022-03319
• 负责人: Amy, Matthew
• 金额: $ 2.11万
• 依托单位: Simon Fraser University
• 依托单位国家: 加拿大
• 项目类别: Discovery Grants Program - Individual
• 财政年份: 2022
• 资助国家: 加拿大
• 起止时间: 2022-01-01 至 2023-12-31
• 项目状态: 已结题
• 来源: https://www.nserc-crsng.gc.ca/ase-oro/Details-Detailles_eng.asp?id=750546
• 关键词: Formal; methods; reliable; performance; quantum

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.

我的研究项目旨在了解量子计算机的现实计算能力和实际优势。在理论层面上，量子计算有望比最知名的经典算法更快地以指数方式解决某些问题。值得注意的例子包括整数因子分解和计算离散算法，它们一起打破了许多传统的加密方法，以及量子系统的模拟。特别是后者，作为量子计算机发展的原始动力，通过促进药物，材料和化学设计的进步，有可能对社会产生深远的影响。典型的第一个现实世界的应用是模拟固氮酶，这是一种参与肥料生产所需的固氮酶固定过程的酶，即使用现代超级计算机也无法模拟。氮和碳固定方面的进展可能对我们应对气候变化的能力产生深远影响。然而，在实践中，由于计算模型的约束和纠错的需要，在真实的硬件上执行大规模量子算法涉及高度的开销。为了正确地描述纠错量子计算机的优点，需要在具体的计算资源（例如时间，量子位数，经典处理能力）方面对这种开销进行实际核算，称为资源估计。另一方面，量子硬件正在迅速接近潜在有用的尺寸，这些小规模、有噪声的设备的实际应用需要通过使用和实验来确定。在这两种情况下，需要有效的软件工具来编程和编译这些算法。此外，由于量子程序非常难以调试，几乎不可能模拟，因此建立这种量子代码的正确性的方法是必要的。对于短期应用程序，错误通常会导致头痛或失败的实验，而对于大规模资源估计，不可靠的过程可能会削弱对估计的信心或导致非常不准确的估计。该研究计划的目标是开发可靠，高性能和便携式量子软件。我计划开发量子计算数学推理的新方法，并将其应用于量子程序的规范，形式验证和优化。我打算将这些集成到低级量子编程和规范语言中，以便优化的量子代码库可以一次性编写和验证，然后在未来几年内重复使用。我希望这个研究项目的贡献将对量子计算机的实际使用和分析产生深远的影响，使算法能够轻松可靠地从理论转化为实践。