Quantum Abstract Interpretation
summary
Claims that abstract interpretation can verify quantum program assertions in polynomial time by representing abstract states as tuples of local projections and proving an α/γ Galois connection that yields sound abstract steps. Concretely it tensors identities to expand local reduced density matrices, imports nearby local information, applies the gate, then projects back, which loses some entanglement and can produce top elements but remains tractable. Implementation verifies Bernstein‑Vazirani, GHZ and a Grover loop invariant on up to 300 qubits on a laptop.
AI-written summary · about
chapters (26)
- 0:00Quantum verification challenges
- 1:09Simulating quantum programs intractable
- 3:38Quantum computers as accelerators
- 5:44Quantum polynomial time limits
- 7:29Breakthroughs for quantum viability
- 9:36Quantum error correction and coherence
- 11:21Verifying quantum programs QMA-complete
- 12:22Abstract interpretation for quantum programs
- 14:31Hard cases in quantum computing T gate
- 16:35Assertions in quantum programs projections
- 19:02Density matrices and abstraction
- 21:47Local projections entanglement loss
- 23:55Galois connection for quantum abstract interpretation
- 26:26Abstract interpreter implementation
- 27:29Grover's algorithm verification example
- 30:43Experimental results scalability
- 32:29Future directions open problems
- 33:14Q&A Debugging quantum experiments
- 33:56Q&A Control flow and loops
- 34:41Q&A Selecting abstract domains
- 35:23Q&A Abstract interpretation scalability
- 36:48Q&A Density matrix insights
- 37:30Q&A Parameterizing abstractions
- 38:56Q&A Running analysis on quantum computers
- 39:38Q&A Parallelization GPU optimization
- 40:19Closing remarks
related talks
16mProjection-Based Runtime Assertions for Testing and Debugging Quantum Programs
42mQuantum program analysis: Verification and Testing
32mTheory, Design, and Implementation of Projection-based Assertions for Quantum Debugging
21mInteractive Proofs for Synthesizing Quantum States and Unitaries
27mAn Expressive Assertion Language for Quantum Programs
18mSAQR-QC: A Logic for Scalable but Approximate Quantitative Reasoning about Quantum(…)
23mA Unified Assertion-Based Framework for Classical-Quantum Program Verification
15mAssertion-Based Optimization of Quantum Programs