Verifying Quantum Circuits in GAP
summary
Implementation called Quantum GAP provides exact matrix arithmetic over cyclotomic and algebraic field extensions and verifies 30 decompositions from prior papers. It checks ancilla management and validates rotational gates by reducing sines and cosines to arithmetic in roots of unity and computing degree-based sampling cutoffs (combinatorial bounds versus polynomial interpolation). A working GAP library and symbolic-to-matrix pipeline exist, and preliminary finite-sampling bounds are derived though the final proof and large-scale experiments remain in progress.
AI-written summary · about
chapters (16)
- 0:00Quantum circuit verification
- 0:21Equivalence checking
- 2:27Motivation for matrix verification
- 3:51Challenges in matrix computation
- 4:53Algebraic number fields in GAP
- 6:16Understanding algebraic extensions
- 8:22Roots of unity and GAP efficiency
- 9:28Verifying parameterized circuits
- 10:54Limitations of techniques
- 11:34Polynomial degree bounds
- 13:20Rational linear sums of angles
- 14:24Interpolation vs combinatorial methods
- 15:29Sampling with roots of unity
- 15:51Inductive patterns
- 16:12Recap and future work
- 16:45Q&A
related talks
17mQGAT: A Generate-and-Test Paradigm for Quantum Circuits
18mAn Automata-Based Framework for Verification and Bug Hunting in Quantum Circuits
48mThe Quantum Games PCP: Results and Confessions
17mOptimization and Synthesis of Quantum Circuits with Global Gates
27mParameterized Verification of Quantum Circuits
40mDemocratizing quantum formal verification: the path-sum way
21mCobble: Compiling Block Encodings for Quantum Computational Linear Algebra
27mQuantum Circuits Are Just a Phase