Hybrid Path-Sums for Hybrid Quantum Programs
summary
Presents a formalism called Hybrid Path-Sums (HPS), a symbolic representation plus rewriting rules and a core assertion language, and ships a working symbolic execution engine that verifies hybrid quantum/classical programs with measurement, classical control and probabilistic specs. Claims several orders-of-magnitude speedups over prior tools, computes phase estimation probabilities on 300 wires with 10 tries in <3 minutes, proves equivalence of unitary circuits up to 500 qubits, and encodes bounded repeat-until-success and small error‑correction examples.
AI-written summary · about
chapters (13)
- 0:00Hybrid quantum program analysis
- 1:23Simulating hybrid quantum programs
- 3:11Static analysis vs testing in quantum
- 4:57Symbolic reasoning for verification
- 5:38Path sums for unitary circuits
- 9:51Extending path sums to hybrids
- 11:59Rules for hybrid path sum interference
- 13:24Assertion language for hybrid states
- 14:05Phase estimation results
- 15:08Quantum error correction formalized
- 15:52Scaling large quantum circuits
- 16:15Summary and future
- 16:56Q&A
related talks
40mDemocratizing quantum formal verification: the path-sum way
22mLocal Reasoning about Probabilistic Behaviour for Classical-Quantum Programs
42mQuantum program analysis: Verification and Testing
20mLarge-scale hybrid quantum computing solution of linear systems of equations
15mToward A Quantum Programming Language for Higher Level Formal Verification
18mAutomated distribution of quantum circuits via hypergraph partitioning
21mAnalyzing quantum programs using the power of interaction
16mCompiling and Running High-level Quantum Programs