A Verified Optimizer for Quantum Circuits & Verified Translation Between Low-Level Quantum Languages
summary
A verified optimizer named Box implements peephole rules (X/Z propagation, gate cancellation) plus rotation‑merging and a naive swap‑based mapper, all formalized in a new IR called Squire and extracted from Coq to OCaml. The development is about 8,000 lines of Coq (≈1,500 for the core), with a standalone OpenQASM (open chasm) parser (~400 lines), and a 29‑benchmark evaluation that yields substantial gate and T‑count reductions comparable to prior research while preserving semantics — i.e., transformations are provably correct.
AI-written summary · about
chapters (12)
- 0:00A Verified Optimizer for Quantum Circuits
- 0:18Verified Compiler Stack
- 5:13VOQC Transformations
- 7:20Example: XIZ Propagation
- 9:25Proof Overview
- 11:48Verifying Matrix Equivalences
- 13:22Experiment
- 13:59Results
- 15:49Unitary SOIR and OpenQASM have fairly similar abstract syntax
- 17:06Denotational semantics of SOIR and Open QASM correspond
- 18:17Sernantic preservation properties are maintained during translation
- 19:02OpenQASM parser written in OCaml programming language
related talks
29mA Verified Optimizer for Quantum Circuits
11mExpanding the VOQC Toolkit
15mAssertion-Based Optimization of Quantum Programs
33mVerified Compilation of Quantum Oracles
15mToward A Quantum Programming Language for Higher Level Formal Verification
33mFrom Verified Compilation to Shor's Algorithm
22mCoqQ: Foundational Verification of Quantum Programs
01h 10mThe Rise & Collapse of a Quantum State