Scalable Equivalence Checking and Verification of Shallow Quantum Circuits

Explore a 15-minute conference presentation from OOPSLA 2025 that introduces Projection-Based Equivalence Checking (PBEC), a novel approach for verifying whether two shallow quantum circuits perform equivalent computations. Learn how researchers from Stony Brook University and University of Wisconsin developed decision procedures that can verify quantum circuit equivalence on classical computers in linear time and space for any fixed circuit depth. Discover the key insight that local projections serve as constraints to fully characterize quantum circuit output states, enabling efficient verification without exponential resource requirements. Examine experimental results demonstrating the method's scalability, including verification of 100-qubit circuits with various connectivity patterns and depths, with performance ranging from 0.20 seconds for simple cases to under 32 seconds for complex arbitrary input scenarios. Understand how this constraint representation extends beyond equivalence checking to enable both static and runtime assertion verification for quantum circuits, providing sound and complete methods for assertions expressed as conjunctions of local projections. Gain insights into practical quantum circuit verification techniques essential for ensuring correctness of quantum circuit transformations and optimizations in NISQ (Noisy Intermediate-Scale Quantum) computing applications.