  Variational quantum algorithms have been introduced as a promising class of
quantum-classical hybrid algorithms that can already be used with the noisy
quantum computing hardware available today by employing parameterized quantum
circuits. Considering the non-trivial nature of quantum circuit compilation and
the subtleties of quantum computing, it is essential to verify that these
parameterized circuits have been compiled correctly. Established equivalence
checking procedures that handle parameter-free circuits already exist. However,
no methodology capable of handling circuits with parameters has been proposed
yet. This work fills this gap by showing that verifying the equivalence of
parameterized circuits can be achieved in a purely symbolic fashion using an
equivalence checking approach based on the ZX-calculus. At the same time,
proofs of inequality can be efficiently obtained with conventional methods by
taking advantage of the degrees of freedom inherent to parameterized circuits.
We implemented the corresponding methods and proved that the resulting
methodology is complete. Experimental evaluations (using the entire parametric
ansatz circuit library provided by Qiskit as benchmarks) demonstrate the
efficacy of the proposed approach. The implementation is open source and
publicly available as part of the equivalence checking tool QCEC
(https://github.com/cda-tum/qcec) which is part of the Munich Quantum Toolkit
(MQT).
