A Verified Optimizer for Quantum Circuits

on YouTube ↗29m

" summary

VOQC is a fully verified optimizer for quantum circuits implemented in the Coq proof assistant over the SQIR intermediate language; all transformations are proven semantics-preserving on a matrix/density-matrix semantics. The implementation verifies common and nonlocal rewrites (e.g., X propagation, rotation merging), circuit mapping to hardware connectivity, and automation for matrix equalities. Evaluation runs on 28 benchmark programs (45–several thousand gates, 5–96 qubits), matches or beats unverified Python tools in speed, and produces no validation failures on those benchmarks.

AI-written summary · about

" chapters (28)

1. 0:00A Verified Optimizer for Quantum Circuits
2. 0:19Writing Quantum Programs is Hart
3. 1:12Quantum Machines are Limitet
4. 2:03Quantum Compilers are complicated • Quantum compilers need to perform sophisticated transformations to account for limited resources, hardware constraints
5. 2:53Verified Compiler Stack
6. 3:55SQIR and VOQC
7. 5:03Outline
8. 6:09Operators
9. 6:54Multiple Qubits
10. 7:04Measurement 2.0
11. 7:38Entanglement
12. 8:17Multi-Qubit Unitaries
13. 9:06General Quantum States
14. 10:06Circuits Quantum programs are often written as circuits
15. 10:40Quantum Programming
16. 11:30SQIR: Small Quantum Intermediate Representation
17. 15:24Designed for Proof
18. 16:48Proofs so Far
19. 17:35VOQC: A Verified Optimizer for Quantum Circus
20. 18:48Example: X Propagation
21. 19:41Verifying Matrix Equivalences
22. 20:04Grid Normal Form
23. 21:03More Interesting: Rotation Merging
24. 22:51Also: Circuit Mapping
25. 24:07Evaluation
26. 24:37Benchmark
27. 26:06No Bugs!
28. 27:39Summary and Future Work

" related talks

• 11mExpanding the VOQC ToolkitKesha Hietala · PLanQC 2021
• 24mA Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum LanguagesKesha Hietala, Kartik Singhal · PLanQC 2020
• 33mVerified Compilation of Quantum OraclesMichael Hicks · OOPSLA 2022
• 22mCoqQ: Foundational Verification of Quantum ProgramsGilles Barthe, Li Zhou, Mingsheng Ying, Pierre-Yves Strub, Junyi Liu · POPL 2023
• 15mToward A Quantum Programming Language for Higher Level Formal VerificationFinn Voichick · PLanQC 2021
• 15mAssertion-Based Optimization of Quantum ProgramsThomas Häner, Torsten Hoefler, Matthias Troyer · OOPSLA 2020
• 17mQVM: Quantum Gate Virtualization MachineNathaniel Tornow, Emmanouil Giortamis, Pramod Bhatotia · PLDI 2025
• 22mEfficient Formal Verification of Quantum Error Correcting ProgramsLi Zhou, Mingsheng Ying, Qifan Huang, Wang Fang, Mengyu Zhao · PLDI 2025