Quantum abstract interpretation
Quantum abstract interpretation
复制标题
DOI：
10.1145/3453483.3454061
复制
发表时间：
2021-06
期刊：
影响因子：
--
通讯作者：
Nengkun Yu;J. Palsberg
中科院分区：
文献类型：
--
作者：
Nengkun Yu;J. Palsberg
在量子计算中，信息的基本单位是量子比特。一般量子程序的模拟需要量子比特数量的指数时间，这使得在当前的超级计算机上模拟超过50个量子比特是不可行的。因此，为了理解更大的程序，我们转向静态技术。在本文中，我们提出了一个抽象的量子程序的解释，我们用它来自动验证断言在多项式时间。我们的关键见解是让一个抽象的状态是一个元组的投影。对于这样的域，我们提出了抽象和具体化功能，形成一个伽罗瓦连接，我们用它们来定义抽象操作。我们在笔记本电脑上的实验已经验证了关于Bernstein-Vazirani，GHZ和Grover基准的断言，具有300个量子位。
In quantum computing, the basic unit of information is a qubit. Simulation of a general quantum program takes exponential time in the number of qubits, which makes simulation infeasible beyond 50 qubits on current supercomputers. So, for the understanding of larger programs, we turn to static techniques. In this paper, we present an abstract interpretation of quantum programs and we use it to automatically verify assertions in polynomial time. Our key insight is to let an abstract state be a tuple of projections. For such domains, we present abstraction and concretization functions that form a Galois connection and we use them to define abstract operations. Our experiments on a laptop have verified assertions about the Bernstein-Vazirani, GHZ, and Grover benchmarks with 300 qubits.