Assertion-Based Optimization of Quantum Programs
summary
An assertion-based optimizer that uses Z-basis, probability-1 pre/postconditions and triviality rules removes redundant gates and qubits by proving operations are no-ops; a Python prototype built on ProjectQ and Z3 implements it and succeeds on mapping/GHZ, modular reduction, floating-point renormalization, and measurement-based uncomputation cases. Results include removal of long swap/CNOT chains, conversion of Toffoli-style sequences into Clifford+measurement, and exponential qubit savings for the position-register trick, demonstrating practical, automated circuit shrinking.
AI-written summary · about
chapters (14)
- 0:00Intro
- 0:19Quantum states
- 1:17Gates / Measurement
- 2:13Quantum circuits
- 3:16Motivation
- 4:31Assertions for optimization
- 7:14Triviality conditions
- 9:18Example: Optimizing mapped circuits
- 10:32Arithmetic in quantum applications
- 11:05Integer arithmetic
- 11:31Floating-point renormalization
- 12:24Optimizing the shift circuit
- 13:06Using preconditions
- 14:44Summary
related talks
32mOptimal Quantum Programs
24mA Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages
29mA Verified Optimizer for Quantum Circuits
24mSynthesizing Quantum-Circuit Optimizers
13mQbC: Quantum Correctness by Construction
22mEfficient Formal Verification of Quantum Error Correcting Programs
29mEfficiently Verifying Quantum Programs with Few T Gates
27mAn Expressive Assertion Language for Quantum Programs