Efficiently Verifying Quantum Programs with Few T Gates
summary
Mechanized Heisenberg-style logic in the Rocq proof assistant verifies Clifford+T circuits by forwarding conjugation of polystring predicates, targeting circuits with low T count; validate and solve_placeholder tactics propagate predicates syntactically so side-conditions are simple well-formedness checks. Case studies include a Toffoli decomposition, graph-state families and the 7-qubit Steane encoder. Enhanced automation adds reflexive normalization and a preverified postcondition function, yielding ~1000x speedup but still fails beyond 7 T gates when Ts are spread across many qubits.
AI-written summary · about
chapters (14)
- 0:00Quantum program verification intro
- 1:08Static verification necessity
- 3:21T gates in circuit compilation
- 4:23Heisenberg logic for Clifford+T
- 6:55Poly group conjugation for T gates
- 9:02Entanglement checks with separability
- 11:12Automated proof generation rules
- 13:21Toughy gate decomposition
- 15:33Rule chaining bottlenecks
- 16:17Direct postcondition computation
- 18:31Quantum error correction verification
- 20:41Limitations and future work
- 21:46Conclusion and open-source
- 22:53Q&A
related talks
27mParameterized Verification of Quantum Circuits
22mEfficient Formal Verification of Quantum Error Correcting Programs
40mDemocratizing quantum formal verification: the path-sum way
32mOptimal Quantum Programs
15mAssertion-Based Optimization of Quantum Programs
45mClassical Verification of Quantum Computational Advantage
15mToward A Quantum Programming Language for Higher Level Formal Verification
42mQuantum program analysis: Verification and Testing