Verifying Repeat-Until-Success Circuits with AutoQ
summary
A new characterization theorem pins exactly which two‑qubit Repeat‑Until‑Success (RUS) circuits implement single‑qubit unitaries, and AutoQ is extended into an AutoQ lightweight verifier that checks Hoare‑style pre/inv/post conditions fully automatically without SMT. Verification runs in under a second on each benchmark, the theory shows checking the computational basis plus one entangled vector suffices to cover all inputs, and the tool uncovers multiple correctness bugs in literature RUS circuits and confirms their fixed versions.
AI-written summary · about
chapters (10)
- 0:00AutoQ verification project
- 2:06Verifying iOS circuits
- 3:33Verification as logical triples
- 5:01Handling loops in quantum programs
- 7:15Nonlinearity in RS circuits
- 8:42Entangled states guarantee
- 10:27Color consistency for correctness
- 11:55Final verification results
- 13:44Parameterized verification
- 14:25Q&A
related talks
18mAn Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits
22mEfficient Formal Verification of Quantum Error Correcting Programs
27mParameterized Verification of Quantum Circuits
18mSAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum(…)
29mEfficiently Verifying Quantum Programs with Few T Gates
22mOptimal Two-Qubit Circuits for Universal Fault-Tolerant Quantum Computation
23mAutomating Quantum Hoare Logic with Automata (Work-In-Progress)
21mQurts: Automatic Quantum Uncomputation by Affine Types with Lifetime