Verifying the Equivalence of Parameterized Quantum Circuits
summary
Claims that parameterized-circuit equivalence reduces to checking Laurent polynomial identities and gives concrete degree bounds computed from a circuit's parameter coefficients. Uses a deterministic five-point interpolation check for single-parameter rewrites and a probabilistic multivariate sampling bound for k parameters, assumes rational multiples of pi, and implements a proof-of-concept GitHub implementation using matrices with cyclotomic gate set entries and an efficient bound predicate summing absolute coefficient contributions.
AI-written summary · about
chapters (11)
- 0:00Verifying quantum circuits
- 3:09Parameterized circuit equivalence
- 5:56Prior verification methods
- 8:22Circuits and rotation gates
- 10:29Verification with control Z
- 14:18Generalizing multiple parameters
- 16:07Degree bounds without expansion
- 17:32Implementation and future work
- 18:25Q&A on implementation
- 20:08Q&A on coefficients and bounds
- 21:36Q&A on Laurent polynomials
related talks
20mOptimal compilation of parametrised quantum circuits
15mAssertion-Based Optimization of Quantum Programs
19mEquality Saturation for Quantum Circuit Optimization
22mHow to Synthesize Quantum-Circuit Optimizers
18mQuantum Probabilistic Model Checking for Time-Bounded Properties
18mEquivalence and Similarity Refutation for Probabilistic Programs
37mPolynomial Identity Testing via Evaluation of Rational Functions
32mOptimal Quantum Programs