Expanding the VOQC Toolkit

on YouTube ↗11m

" summary

Vox is a Coq-verified quantum optimizer: every transformation has a formal proof of semantic preservation and some helper proofs (the U3 combination routine is ~20 lines of code with ~1,500 lines of proof). Recent work adds the ibm gate set, semantics-preserving conversions among three gate sets, mapping that guarantees correctness up to a known qubit permutation and only uses allowed two-qubit edges, and a Python bridge. Evaluation maps 26 benchmarks to a 6x6 grid (geometric-mean gate reductions show optimizing before mapping helps most). Bindings: pybox and mlvox.

AI-written summary · about

" chapters (9)

1. 0:00VOQC: Verified Optimizer for Quantum Circuits
2. 1:35In This Talk
3. 1:52"IBM" Gate Set
4. 3:55Summary of Features
5. 4:33Circuit Mapping
6. 5:53Composing VOQC Transformations
7. 7:02(Light) Evaluation
8. 9:42Ongoing Work
9. 10:37Resources

" related talks

• 29mA Verified Optimizer for Quantum CircuitsMichael Hicks, Robert Rand, Kesha Hietala, Xiaodi Wu, Shih-Han Hung · POPL 2021
• 24mA Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum LanguagesKesha Hietala, Kartik Singhal · PLanQC 2020
• 17mQVM: Quantum Gate Virtualization MachineNathaniel Tornow, Emmanouil Giortamis, Pramod Bhatotia · PLDI 2025
• 22mCoqQ: Foundational Verification of Quantum ProgramsGilles Barthe, Li Zhou, Mingsheng Ying, Pierre-Yves Strub, Junyi Liu · POPL 2023
• 33mVerified Compilation of Quantum OraclesMichael Hicks · OOPSLA 2022
• 15mAssertion-Based Optimization of Quantum ProgramsThomas Häner, Torsten Hoefler, Matthias Troyer · OOPSLA 2020
• 15mQOS: Quantum Operating SystemNathaniel Tornow, Emmanouil Giortamis, Pramod Bhatotia, Francisco Romão · OSDI '25
• 19mSupporting End-Users in Realizing Quantum Computing ApplicationsRobert Wille, Damian Rovara, Nils Quetschlich, Lukas Burgholzer · WQS 2024