Scalable Equivalence Checking and Verification of Shallow Quantum Circuits
summary
Projection-Based Equivalence Checking constructs a constraint representation of a shallow circuit’s output as a conjunction of local projections that act on constant-size forward cones, so the output is the unique state satisfying those constraints. For fixed depth the decision procedures run linear in n for fixed depth on a classical machine, avoiding exponential state-vector simulation. Experiments: computing constraints for a random 100-qubit depth-6 1D circuit takes 129.64s; equivalence of two random 100-qubit depth-3 1D circuits is 4.46s for fixed input and ≤31.96s for arbitrary inputs (depth-2: 0.20s / 0.44s).
AI-written summary · about
chapters (11)
- 0:00Introduction
- 1:07Motivation for equivalence checking
- 3:40Complexity theory challenges
- 5:07Projection-based representations
- 6:10Problem formulation
- 6:53Local projector representation
- 8:44Fixed input equivalence algorithm
- 9:51Complexity and scalability
- 11:41Compiler verification applications
- 12:03Conclusion
- 12:25Q&A
related talks
01h 10mQuantum Advantage with Shallow Clifford Circuits
27mParameterized Verification of Quantum Circuits
45mClassical Verification of Quantum Computational Advantage
51mOn constant T-depth circuits
42mLearning Shallow Quantum Circuits and Quantum States Prepared by Shallow Circuits in Polynomial Time
22mEfficient Formal Verification of Quantum Error Correcting Programs
29mEfficiently Verifying Quantum Programs with Few T Gates
33mSpoofing Linear Cross-Entropy Benchmarking in Shallow Quantum Circuits