Symbolic (#161)

This PR introduced functionality for equivalence checking of parametrized circuits with QCEC. This PR is related to cda-tum/mqt-core#199 and cda-tum/zx#15 Signed-off-by: Lukas Burgholzer <[email protected]> Co-authored-by: Lukas Burgholzer <[email protected]> Co-authored-by: pre-commit-ci[bot] <66853113+pre-commit-ci[bot]@users.noreply.github.com> Co-authored-by: Lukas Burgholzer <[email protected]>
cda-tum · Oct 21, 2022 · 844731f · 844731f
1 parent 7ee46bc
commit 844731f
Show file tree

Hide file tree

Showing 22 changed files with 2,596 additions and 68 deletions.
diff --git a/.github/codecov.yml b/.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:

diff --git a/.gitmodules b/.gitmodules
@@ -1,5 +1,5 @@
 [submodule "extern/qfr"]
-	path = extern/qfr
-	url = https://github.com/cda-tum/qfr.git
+    path = extern/qfr
+    url = https://github.com/cda-tum/qfr.git
     branch = main
     shallow = true
diff --git a/docs/source/CompilationFlowVerification.ipynb b/docs/source/CompilationFlowVerification.ipynb
@@ -113,13 +113,13 @@
   "language_info": {
    "codemirror_mode": {
     "name": "ipython",
-    "version": 2
+    "version": 3
    },
    "file_extension": ".py",
    "mimetype": "text/x-python",
    "name": "python",
    "nbconvert_exporter": "python",
-   "pygments_lexer": "ipython2"
+   "pygments_lexer": "ipython3"
   }
  },
  "nbformat": 4,

diff --git a/docs/source/ParameterizedCircuits.ipynb b/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
+}
diff --git a/docs/source/Publications.rst b/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.