Symbolic

.github/codecov.yml

@@ -29,8 +29,10 @@ flag_management:
         - "mqt/**/*.py"
       statuses:
         - type: project
+          threshold: 0.5%
         - type: patch
           target: 95%
+          threshold: 1%
 
 parsers:
   gcov:

.gitmodules

@@ -1,5 +1,5 @@
 [submodule "extern/qfr"]
     path = extern/qfr
     url = https://github.com/cda-tum/qfr.git
-    branch = symbolic
+    branch = main
     shallow = true

docs/source/ParameterizedCircuits.ipynb

@@ -0,0 +1,185 @@
+{
+ "cells": [
+  {
+   "cell_type": "markdown",
+   "id": "77a131e6",
+   "metadata": {},
+   "source": [
+    "# Verifying Parameterized Quantum Circuits\n",
+    "\n",
+    "## Variational Quantum Algorithms\n",
+    "\n",
+    "Variational quantum algorithms are a family of mixed quantum-classical algorithms that try to achieve a quantum advantage via low-depth circuits. This is achieved by offloading a substantial amount of computational work to a classical processor. The quantum circuits employed by variational quantum algorithms involve *parameterized gates* which depend on some a-priori uninstantiated variable.\n",
+    "\n",
+    "Variational quantum algorithms try to optimize the circuit's parameters in each iteration with the classical post-processor while the quantum circuit is used to compute the cost function that is being optimized. Because recompiling the quantum circuit in each of these iterations is a costly procedure, the circuit is usually compiled in *paramterized* form in which the parameters tuned by the classical optimization routine are not bound to specific values.\n",
+    "\n",
+    "As is the case with parameter-free circuits, errors can be made during the compilation process. Therefore verifying the correctness of compilations of parameterized quantum circuits is an important task for near-term quantum computing.\n",
+    "\n",
+    "\n",
+    "## Equivalence Checking of Parameterized Quantum Circuits\n",
+    "\n",
+    "Having unbound parameters in a quantum circuits brings new challenges to the task of quantum circuit verification as many data structures have difficulty supporting symbolic computations directly. However, *ZX-diagrams* are an exceptions to this as most rewrite rules used for equivalence checking with the the *ZX-calculus* only involve summation of parameters. \n",
+    "The ZX-calculus equivalence checker in QCEC cannot be used to prove non-equivalence of quantum circuits. To still show non-equivalence of parameterized quantum circuits QCEC uses a scheme of repeatedly instantiating a circuits parameters in such a way as to make the check as simple as possible while still guaranteeing that either equivalence or non-equivalence can be proven.\n",
+    "The resulting *equivalence checking flow* looks as follows\n",
+    "\n",
+    "![Equivalence Checking Flow for Parameterized Quantum Circuits](images/parameterized_flow.svg)\n",
+    "\n",
+    "## Using QCEC to Verify Parameterized Quantum Circuits\n",
+    "\n",
+    "Consider the following quantum circuit"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "977071d9",
+   "metadata": {},
+   "source": [
+    "## Using QCEC to Verify Parameterized Quantum Circuits\n",
+    "\n",
+    "Consider the following quantum circuit"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "03b73b17",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from qiskit import QuantumCircuit\n",
+    "from qiskit.circuit import Parameter\n",
+    "\n",
+    "alpha = Parameter('alpha')\n",
+    "beta = Parameter('beta')\n",
+    "\n",
+    "qc_lhs = QuantumCircuit(2)\n",
+    "qc_lhs.rz(alpha, 1)\n",
+    "qc_lhs.cx(0, 1)\n",
+    "qc_lhs.rz(beta, 1)\n",
+    "qc_lhs.cx(0, 1)\n",
+    "qc_lhs.draw(output='mpl')"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "3b85338e",
+   "metadata": {},
+   "source": [
+    "A well known commutation rule for the $R_Z$ gate, states that this circuit is equivalent to the following one"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "36df44b7",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "qc_rhs = QuantumCircuit(2)\n",
+    "qc_rhs.cx(0, 1)\n",
+    "qc_rhs.rz(beta, 1)\n",
+    "qc_rhs.cx(0, 1)\n",
+    "qc_rhs.rz(alpha, 1)\n",
+    "qc_rhs.draw(output='mpl')"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "8cae4862",
+   "metadata": {},
+   "source": [
+    "This equality can be proved with QCEC by using the `verify` method just as with any regular circuit"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "da9fa188",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "from mqt import qcec\n",
+    "\n",
+    "qcec.verify(qc_lhs, qc_rhs)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "59d13843",
+   "metadata": {},
+   "source": [
+    "QCEC also manages to show non-equivalence of parameterized quantum circuits. \n",
+    "It is easy to erroneously exchange the parameters in the above commutation rule."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "02f203af",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "qc_rhs_err = QuantumCircuit(2)\n",
+    "qc_rhs_err.cx(0, 1)\n",
+    "qc_rhs_err.rz(alpha, 1)\n",
+    "qc_rhs_err.cx(0, 1)\n",
+    "qc_rhs_err.rz(beta, 1)\n",
+    "qc_rhs_err.draw(output='mpl')"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "b64736b0",
+   "metadata": {},
+   "source": [
+    "QCEC will tell us that this is incorrect"
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "7e771154",
+   "metadata": {},
+   "outputs": [],
+   "source": [
+    "qcec.verify(qc_lhs, qc_rhs_err)"
+   ]
+  },
+  {
+   "cell_type": "markdown",
+   "id": "c9d9d3aa",
+   "metadata": {},
+   "source": [
+    "Check out the [reference documentation](library/VerifyCompilation.rst#mqt.qcec.verify_compilation) documentation for more information."
+   ]
+  },
+  {
+   "cell_type": "code",
+   "execution_count": null,
+   "id": "98d4cd4d",
+   "metadata": {},
+   "outputs": [],
+   "source": []
+  }
+ ],
+ "metadata": {
+  "kernelspec": {
+   "display_name": "general",
+   "language": "python",
+   "name": "general"
+  },
+  "language_info": {
+   "codemirror_mode": {
+    "name": "ipython",
+    "version": 3
+   },
+   "file_extension": ".py",
+   "mimetype": "text/x-python",
+   "name": "python",
+   "nbconvert_exporter": "python",
+   "pygments_lexer": "ipython3"
+  }
+ },
+ "nbformat": 4,
+ "nbformat_minor": 5
+}

docs/source/Publications.rst

@@ -9,8 +9,9 @@ Furthermore, if you use any of the particular algorithms such as
 
 - the compilation flow result verification scheme :cite:labelpar:`burgholzer2020verifyingResultsIBM`,
 - the dedicated stimuli generation schemes :cite:labelpar:`burgholzer2021randomStimuliGenerationQuantum`,
-- the transformation scheme for circuits containing non-unitaries :cite:labelpar:`burgholzer2022handlingNonUnitaries`, or
-- the equivalence checker based on ZX-diagrams :cite:labelpar:`peham2022equivalenceCheckingZXCalculus`,
+- the transformation scheme for circuits containing non-unitaries :cite:labelpar:`burgholzer2022handlingNonUnitaries`,
+- the equivalence checker based on ZX-diagrams :cite:labelpar:`peham2022equivalenceCheckingZXCalculus`, or
+- the method for checking equivalence of parameterized circuits :cite:labelpar:`peham2023EquivalenceCheckingParameterizedCircuits`
 
 please consider citing their respective papers as well. A full list of related papers is given below.
 

docs/source/library/Configuration.rst

@@ -14,3 +14,4 @@ The :class:`Configuration` class provides all the means to configure QCEC. All o
    configuration/Application
    configuration/Functionality
    configuration/Simulation
+   configuration/Parameterized

docs/source/library/configuration/Parameterized.rst

@@ -0,0 +1,6 @@
+Parameterized
+=============
+
+.. autoclass:: mqt.qcec.Configuration.Parameterized
+    :members:
+    :undoc-members:

docs/source/refs.bib

@@ -86,3 +86,11 @@ @article{peham2022equivalenceCheckingZXCalculus
     year = {2022},
     url = {https://www.cda.cit.tum.de/files/eda/2022_jetcas_equivalence_checking_of_quantum_circuits_with_the_zx_calculus.pdf}
 }
+
+@inproceedings{peham2023EquivalenceCheckingParameterizedCircuits,
+    title = {Equivalence Checking of Parameterized Quantum Circuits: {Verifying} the Compilation of Variational Quantum Algorithms},
+    booktitle = {Asia and South Pacific Design Automation Conference},
+    author = {Peham, Tom and Burgholzer, Lukas and Wille, Robert},
+    year = {2023},
+    url = {https://www.cda.cit.tum.de/files/eda/2023_aspdac_equivalence_checking_parameterized_quantum_circuits.pdf}
+}

include/Configuration.hpp

@@ -182,9 +182,9 @@ class Configuration {
       }
     }
 
-    auto& par                       = config["parameterized"];
-    par["tolerance"]                = parameterized.parameterizedTol;
-    par["addtional_instantiations"] = parameterized.nAdditionalInstantiations;
+    auto& par                        = config["parameterized"];
+    par["tolerance"]                 = parameterized.parameterizedTol;
+    par["additional_instantiations"] = parameterized.nAdditionalInstantiations;
 
     if (execution.runConstructionChecker || execution.runAlternatingChecker) {
       auto& fun              = config["functionality"];

include/EquivalenceCheckingManager.hpp

@@ -38,6 +38,7 @@ class EquivalenceCheckingManager {
     dd::CVec    cexInput{};
     dd::CVec    cexOutput1{};
     dd::CVec    cexOutput2{};
+    std::size_t performedInstantiations = 0U;
 
     [[nodiscard]] bool consideredEquivalent() const {
       switch (equivalence) {

mqt/qcec/bindings.cpp

@@ -96,16 +96,15 @@ static std::unique_ptr<EquivalenceCheckingManager> createManagerFromOptions(
     // Simulation
     const double fidelityThreshold = 1e-8,
 
-    const std::size_t maxSims = std::max(16U,
-                                         std::thread::hardware_concurrency() -
-                                             2U),
+    const std::size_t maxSims   = std::max(16U,
+                                           std::thread::hardware_concurrency() -
+                                               2U),
+    const StateType&  stateType = StateType::ComputationalBasis,
+    const std::size_t seed = 0U, const bool storeCEXinput = false,
+    const bool storeCEXoutput = false,
     // Parameterized
     const double      parameterizedTol          = 1e-12,
-    const std::size_t nAdditionalInstantiations = 0,
-    const StateType&  stateType                 = StateType::ComputationalBasis,
-    const std::size_t seed = 0U, const bool storeCEXinput = false,
-
-    const bool storeCEXoutput = false) {
+    const std::size_t nAdditionalInstantiations = 0) {
   Configuration configuration{};
   // Execution
   configuration.execution.numericalTolerance     = numericalTolerance;
@@ -153,7 +152,6 @@ static std::unique_ptr<EquivalenceCheckingManager> createManagerFromOptions(
   configuration.parameterized.parameterizedTol = parameterizedTol;
   configuration.parameterized.nAdditionalInstantiations =
       nAdditionalInstantiations;
-
   return createManagerFromConfiguration(circ1, circ2, configuration);
 }
 
@@ -291,10 +289,10 @@ PYBIND11_MODULE(pyqcec, m) {
          "alternating_scheme"_a = "proportional", "profile"_a = "",
          "trace_threshold"_a = 1e-8, "fidelity_threshold"_a = 1e-8,
          "max_sims"_a = std::max(16U, std::thread::hardware_concurrency() - 2U),
-         "parameterized_tolerance"_a   = 1e-12,
-         "additional_instantiations"_a = 0U,
          "state_type"_a = "computational_basis", "seed"_a = 0U,
-         "store_cex_input"_a = false, "store_cex_output"_a = false)
+         "store_cex_input"_a = false, "store_cex_output"_a = false,
+         "parameterized_tolerance"_a   = 1e-12,
+         "additional_instantiations"_a = 0U)
       .def(py::init([](const py::object& circ1, const py::object& circ2,
                        const Configuration& config) {
              return createManagerFromConfiguration(circ1, circ2, config);
@@ -509,6 +507,11 @@ PYBIND11_MODULE(pyqcec, m) {
                      &EquivalenceCheckingManager::Results::cexOutput2,
                      "State vector representation of the second circuit's "
                      "counterexample output state.")
+      .def_readwrite(
+          "performed_instantiations",
+          &EquivalenceCheckingManager::Results::performedInstantiations,
+          "Number of circuit instantiations that have been performed during "
+          "equivalence checking of parameterized quantum circuits.")
       .def("considered_equivalent",
            &EquivalenceCheckingManager::Results::consideredEquivalent,
            "Convenience function to check whether the obtained result is to be "
@@ -766,7 +769,7 @@ PYBIND11_MODULE(pyqcec, m) {
                      "Set threshold below which instantiated parameters shall "
                      "be considered zero.")
       .def_readwrite(
-          "addtitional_instantiations",
+          "additional_instantiations",
           &Configuration::Parameterized::nAdditionalInstantiations,
           "Number of instantiations shall be performed in addition to the "
           "default ones. "