As quantum computing is rising in popularity, the amount of quantum programs and the number of developers writing them are increasing rapidly. Unfortunately, writing correct quantum programs is challenging due to various subtle rules developers need to be aware of. Empirical studies show that 40-82% of all bugs in quantum software are specific to the quantum domain. Yet, existing static bug detection frameworks are mostly unaware of quantum-specific concepts, such as circuits, gates, and qubits, and hence miss many bugs. This paper presents LintQ, a comprehensive static analysis framework for detecting bugs in quantum programs. Our approach is enabled by a set of abstractions designed to reason about common concepts in quantum computing without referring to the details of the underlying quantum computing platform. Built on top of these abstractions, LintQ offers an extensible set of nine analyses that detect likely bugs, such as operating on corrupted quantum states, redundant measurements, and incorrect compositions of sub-circuits. We apply the approach to a newly collected dataset of 7,568 real-world Qiskit-based quantum programs, showing that LintQ effectively identifies various programming problems with a precision of 80.5%. Comparing to a general-purpose linter and two existing, quantum-aware techniques shows that all problems found by LintQ during our evaluation are missed by prior work. LintQ hence takes an important step toward reliable software in the growing field of quantum computing.
翻译:随着量子计算日益普及,量子程序的数量及其开发者规模迅速增长。然而,由于开发者需遵循诸多微妙规则,编写正确的量子程序颇具挑战。实证研究表明,量子软件中40%-82%的缺陷属于量子领域特有缺陷。现有静态缺陷检测框架大多未能感知量子领域特定概念(如电路、门、量子比特),因此遗漏大量缺陷。本文提出LintQ,一个面向量子程序缺陷检测的综合静态分析框架。该方法通过一组抽象机制实现,这些抽象机制旨在推理量子计算中的常见概念,而无需涉及底层量子计算平台的细节。基于这些抽象,LintQ提供九个可扩展的分析单元,用于检测潜在缺陷,例如对损坏量子态的操作、冗余测量以及子电路的不正确组合。我们将该方法应用于新收集的7,568个基于Qiskit的真实量子程序数据集,结果表明LintQ能有效识别各类编程问题,精确率达80.5%。与通用型代码检查工具及两种现有量子感知技术对比发现,LintQ在评估中发现的所有问题均未被先前工作检出。因此,LintQ为蓬勃发展的量子计算领域迈向可靠软件迈出了重要一步。