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 条

[21] Evolutionary Quantum Architecture Search for Parametrized Quantum Circuits [J].

Ding, Li ;

Spector, Lee .

PROCEEDINGS OF THE 2022 GENETIC AND EVOLUTIONARY COMPUTATION CONFERENCE COMPANION, GECCO 2022, 2022, :2190-2195

[22] EDA and Quantum Computing: The Key Role of Quantum Circuits [J].

Stok, Leon .

PROCEEDINGS OF THE 2021 INTERNATIONAL SYMPOSIUM ON PHYSICAL DESIGN, ISPD 2021, 2021, :111-111

[23] Quantum Circuits for Dynamic Runtime Assertions in Quantum Computation [J].

Zhou, Huiyang ;

Byrd, Gregory T. .

IEEE COMPUTER ARCHITECTURE LETTERS, 2019, 18 (02) :111-114

[24] Genetic algorithms as classical optimizer for the Quantum Approximate Optimization Algorithm [J].

Acampora, Giovanni ;

Chiatto, Angela ;

Vitiello, Autilia .

APPLIED SOFT COMPUTING, 2023, 142

[25] QANA: Quantum-based avian navigation optimizer algorithm [J].

Zamani, Hoda ;

Nadimi-Shahraki, Mohammad H. ;

Gandomi, Amir H. .

ENGINEERING APPLICATIONS OF ARTIFICIAL INTELLIGENCE, 2021, 104

[26] Split Compilation for Security of Quantum Circuits [J].

Saki, Abdullah Ash ;

Suresh, Aakarshitha ;

Topaloglu, Rasit Onur ;

Ghosh, Swaroop .

2021 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN (ICCAD), 2021,

[27] Equivalence Checking of Dynamic Quantum Circuits [J].

Hong, Xin ;

Feng, Yuan ;

Li, Sanjiang ;

Ying, Mingsheng .

2022 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER AIDED DESIGN, ICCAD, 2022,

[28] Binary Pooling Circuits for Quantum Computing [J].

Yetis, Hasan ;

Karakose, Mehmet .

2021 INTERNATIONAL CONFERENCE ON DECISION AID SCIENCES AND APPLICATION (DASA), 2021,

[29] Optimizing Quantum Circuits, Fast and Slow [J].

Xu, Amanda ;

Molavi, Abtin ;

Tannu, Swamit ;

Albarghouthi, Aws .

PROCEEDINGS OF THE 30TH ACM INTERNATIONAL CONFERENCE ON ARCHITECTURAL SUPPORT FOR PROGRAMMING LANGUAGES AND OPERATING SYSTEMS, VOL 1, ASPLOS 2025, 2025, :777-793

[30] A comprehensive study of quantum arithmetic circuits [J].

Wang, Siyi ;

Li, Xiufan ;

Lee, Wei Jie Bryan ;

Deb, Suman ;

Lim, Eugene ;

Chattopadhyay, Anupam .

PHILOSOPHICAL TRANSACTIONS OF THE ROYAL SOCIETY A-MATHEMATICAL PHYSICAL AND ENGINEERING SCIENCES, 2025, 383 (2288)

← 1 2 3 4 5 →