Parameterized Verification of Quantum Circuits
summary
Presents a fully automatic framework that verifies relational properties of size‑parameterized quantum programs by modeling infinite families of quantum states with synchronized weighted tree automata and parameterized gates with transducers for parameterized gates. Verification reduces to checking functional inclusion/equivalence of SWTAs, decidable by comparing domains and reducing differences to finite linear transition systems solved with Karr‑style invariant computation; emptiness is PSPACE‑complete. A C++ prototype composes transducers, checks images and equivalence, and verifies benchmarks (Grover, Bernstein‑Vazirani, adders, error correction) in milliseconds to seconds, with the reversible adder as the slowest case.
AI-written summary · about
chapters (9)
- 0:00Parameterized quantum circuits
- 3:12What are parameterized quantum circuits
- 7:21Regular model checking for quantum states
- 10:30Synchronized weighted tree automata
- 16:54Limitations of automata
- 21:50Weighted tree transducers for gates
- 23:16Benchmarking results
- 24:40Future work
- 25:07Q&A
related talks
18mAn Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits
40mDemocratizing quantum formal verification: the path-sum way
29mEfficiently Verifying Quantum Programs with Few T Gates
15mToward A Quantum Programming Language for Higher Level Formal Verification
23mA Unified Assertion-Based Framework for Classical-Quantum Program Verification
42mQuantum program analysis: Verification and Testing
22mEfficient Formal Verification of Quantum Error Correcting Programs
15mScalable Equivalence Checking and Verification of Shallow Quantum Circuits