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

共 50 条

[31] Quantum realization of some quaternary circuits [J].

Khan, Md. Mahmud Muntakim ;

Biswas, Ayan Kumar ;

Chowdhury, Shuvro ;

Tanzid, Mehbuba ;

Mohsin, Kazi Mohammad ;

Hasan, Masud ;

Khan, Asif Islam .

2008 IEEE REGION 10 CONFERENCE: TENCON 2008, VOLS 1-4, 2008, :1983-+

[32] Equivalence Checking of Sequential Quantum Circuits [J].

Wang, Qisheng ;

Li, Riling ;

Ying, Mingsheng .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2022, 41 (09) :3143-3156

[33] Advanced Equivalence Checking for Quantum Circuits [J].

Burgholzer, Lukas ;

Wille, Robert .

IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2021, 40 (09) :1810-1824

[34] Quantum Computing: Circuits, Algorithms, and Applications [J].

Shafique, Muhammad Ali ;

Munir, Arslan ;

Latif, Imran .

IEEE ACCESS, 2024, 12 :22296-22314

[35] Pseudo-dimension of quantum circuits [J].

Matthias C. Caro ;

Ishaun Datta .

Quantum Machine Intelligence, 2020, 2

[36] Characterizing the Reproducibility of Noisy Quantum Circuits [J].

Dasgupta, Samudra ;

Humble, Travis S. .

ENTROPY, 2022, 24 (02)

[37] Simulating Quantum Circuits by Model Counting [J].

Mei, Jingyi ;

Bonsangue, Marcello ;

Laarman, Alfons .

COMPUTER AIDED VERIFICATION, PT III, CAV 2024, 2024, 14683 :555-578

[38] Pseudo-dimension of quantum circuits [J].

Caro, Matthias C. ;

Datta, Ishaun .

QUANTUM MACHINE INTELLIGENCE, 2020, 2 (02)

[39] Partial Equivalence Checking of Quantum Circuits [J].

Chen, Tian-Fu ;

Jiang, Jie-Hong R. ;

Hsieh, Min-Hsiu .

2022 IEEE INTERNATIONAL CONFERENCE ON QUANTUM COMPUTING AND ENGINEERING (QCE 2022), 2022, :594-604

[40] Compaction of Topological Quantum Circuits by Modularization [J].

Asai, Kota ;

Yamashita, Shigeru .

IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 2019, E102A (04) :624-632

← 1 2 3 4 5 →