A Verified Optimizer for Quantum Circuits

被引：2

作者：

Hietala, Kesha ^{[1
,2
]}

Rand, Robert ^{[3
]}

Li, Liyi ^{[1
]}

Hung, Shih-Han ^{[4
]}

Wu, Xiaodi ^{[1
]}

Hicks, Michael ^{[1
,2
]}

机构：

[1] Univ Maryland, Baltimore, MD USA

[2] Univ Amazon, Seattle, WA USA

[3] Univ Chicago, Chicago, IL USA

[4] Univ Texas Austin, Austin, TX USA

来源：

ACM TRANSACTIONS ON PROGRAMMING LANGUAGES AND SYSTEMS | 2023年 / 45卷 / 03期

关键词：

Formal verification; quantum computing; circuit optimization; certified compilation;

D O I：

10.1145/3604630

中图分类号：

TP31 [计算机软件];

学科分类号：

081202 ; 0835 ;

摘要：

We present voqc, the first 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 small 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 programs denote complex-valued matrices, as is standard in quantum computation, but we treat matrices symbolically 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.

引用

页数：35

共 55 条

[41]

Smith RS, 2017, Arxiv, DOI arXiv:1608.03355

[42] Synthesis of quantum circuits for linear nearest neighbor architectures [J].

Saeedi, Mehdi ;

Wille, Robert ;

Drechsler, Rolf .

QUANTUM INFORMATION PROCESSING, 2011, 10 (03) :355-377

[43] t|ket⟩: a retargetable compiler for NISQ devices [J].

Sivarajah, Seyon ;

Dilkes, Silas ;

Cowtan, Alexander ;

Simmons, Will ;

Edgington, Alec ;

Duncan, Ross .

QUANTUM SCIENCE AND TECHNOLOGY, 2021, 6 (01)

[44] A Quantum Computational Compiler and Design Tool for Technology-Specific Targets [J].

Smith, Kaitlin N. ;

Thornton, Mitchell A. .

PROCEEDINGS OF THE 2019 46TH INTERNATIONAL SYMPOSIUM ON COMPUTER ARCHITECTURE (ISCA '19), 2019, :579-588

[45] ProjectQ: An Open Source Software Framework for Quantum Computing [J].

Steiger, Damian S. ;

Haner, Thomas ;

Troyer, Matthias .

QUANTUM, 2018, 2

[46] Not All Qubits Are Created Equal A Case for Variability-Aware Policies for NISQ-Era Quantum Computers [J].

Tannu, Swamit S. ;

Qureshi, Moinuddin K. .

TWENTY-FOURTH INTERNATIONAL CONFERENCE ON ARCHITECTURAL SUPPORT FOR PROGRAMMING LANGUAGES AND OPERATING SYSTEMS (ASPLOS XXIV), 2019, :987-999

[47] Giallar: Push-Button Verification for the Qiskit Quantum Compiler [J].

Tao, Runzhou ;

Shi, Yunong ;

Yao, Jianan ;

Li, Xupeng ;

Javadi-Abhari, Ali ;

Cross, Andrew W. ;

Chong, Frederic T. ;

Gu, Ronghui .

PROCEEDINGS OF THE 43RD ACM SIGPLAN INTERNATIONAL CONFERENCE ON PROGRAMMING LANGUAGE DESIGN AND IMPLEMENTATION (PLDI '22), 2022, :641-656

[48]

The Coq Development Team, 2019, Zenodo, DOI 10.5281/ZENODO.3476303

[49]

The INQWIRE Developers, 2022, INQWIRE QuantumLib

[50] Optimal quantum circuits for general two-qubit gates [J].

Vatan, F ;

Williams, C .

PHYSICAL REVIEW A, 2004, 69 (03) :032315-1

← 1 2 3 4 5 6 →