A Verified Optimizer for Quantum Circuits
A Verified Optimizer for Quantum Circuits
复制标题
DOI：
10.1145/3434318
复制
发表时间：
2021-01-01
影响因子：
1.8
通讯作者：
Hicks, Michael
中科院分区：
文献类型：
--
作者：
Hietala, Kesha;Rand, Robert;Hicks, Michael
我们提出了VOQC，第一个完全验证的量子电路优化器，使用Coq证明助手编写。量子电路用一种简单的低级语言SQIR表示为程序，SQIR是一种简单的量子中间表示，它深深嵌入在Coq中。优化和其他转换表示为Coq函数，这是正确的SQIR程序的语义。SQIR使用复数矩阵的语义，这是量子计算的标准，但为了推理使用任意数量量子比特的程序，它象征性地处理矩阵。SQIR的精心设计和我们提供的自动化使得在VOQC中编写和验证广泛的优化成为可能，包括来自尖端优化器的全电路转换。
We present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. SQIR uses a semantics of matrices of complex numbers, which is the standard for quantum computation, but treats matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. SQIR'S careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers.