{
"cells": [
{
"cell_type": "markdown",
"metadata": {},
"source": [
"# Equivalence Checking of Parameterized Quantum Circuits\n",
"\n",
"[](https://mindspore-website.obs.cn-north-4.myhuaweicloud.com/notebook/master/mindquantum/en/advanced/mindspore_equivalence_checking_of_PQC.ipynb) \n",
"[](https://mindspore-website.obs.cn-north-4.myhuaweicloud.com/notebook/master/mindquantum/en/advanced/mindspore_equivalence_checking_of_PQC.py) \n",
"[](https://gitee.com/mindspore/docs/blob/master/docs/mindquantum/docs/source_en/advanced/equivalence_checking_of_PQC.ipynb)\n",
"\n",
"## Introduction\n",
"\n",
"Before running on a quantum device, a parameterized quantum circuit needs to be compiled into a new circuit consisting of the set of quantum gates supported by the device. Therefore, it is necessary to check the equivalence of the two circuits before and after compilation. In the paper Equivalence Checking of Parameterized Quantum Circuits, a method for checking the equivalence of parameterized quantum circuits based on ZX calculus is proposed. This tutorial attempts to reproduce the method in the MindSpore Quantum architecture.\n",
"\n",
"Paper link: https://doi.org/10.1145/3566097.3567932"
]
},
{
"cell_type": "code",
"execution_count": 1,
"metadata": {},
"outputs": [],
"source": [
"# import libraries\n",
"from mindquantum.core.circuit import Circuit\n",
"import numpy as np\n",
"from mindquantum.core.gates import H, CNOT, RX, RZ\n",
"from mindquantum.core.circuit import dagger"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Step 1\n",
"\n",
"Prepare the quantum circuits.\n",
"\n",
"Take the TwoLocal-Circular circuit in the Qiskit circuits library as an example. The TwoLocal circuit is a parameterized circuit composed of alternating rotation layers and entanglement layers. Rotation layer consists of single qubit gates acting on all qubits. Entanglement layer consists of double qubit gates to entangle qubits according to the entanglement strategy.\n",
"\n",
"Construct a TwoLocal-Circular circuit acting on 127-bit qubits, consisting of three sets of rotation layers and entanglement layers alternately, containing a total of 508 parameters. The rotation layer is [RX](https://www.mindspore.cn/mindquantum/docs/en/master/core/gates/mindquantum.core.gates.RX.html) gates acting on each qubit. The entanglement layer is a [CNOT](https://www.mindspore.cn/mindquantum/docs/en/master/core/gates/mindquantum.core.gates.CNOTGate.html) gate on the first qubit controlled by the last qubit and [CNOT](https://www.mindspore.cn/mindquantum/docs/en/master/core/gates/mindquantum.core.gates.CNOTGate.html) gates on the next qubit controlled by the previous qubit."
]
},
{
"cell_type": "code",
"execution_count": 2,
"metadata": {
"tags": []
},
"outputs": [],
"source": [
"# ansatz = rotation layer + entanglement layer\n",
"def build_ansatz(n_qubits, depth):\n",
" circ = Circuit() # initialize a quantum circuit\n",
"\n",
" for i in range(depth):\n",
" for j in range(n_qubits):\n",
" circ += RX(f'theta{i*n_qubits+j}').on(j) # RX gate on each qubit\n",
" # CNOT gate on the first qubit controlled by the last qubit\n",
" circ += CNOT.on(0, n_qubits-1)\n",
" for j in range(n_qubits-1):\n",
" # CNOT gate on the next qubit controlled by the previous qubit\n",
" circ += CNOT.on(j+1, j)\n",
"\n",
" for j in range(n_qubits):\n",
" circ += RX(f'theta{depth*n_qubits+j}').on(j) # RX gate on each qubit\n",
"\n",
" return circ"
]
},
{
"cell_type": "code",
"execution_count": 3,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 3,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"# example ansatz: 3 qubits and 1 layer\n",
"build_ansatz(3, 1).svg()"
]
},
{
"cell_type": "code",
"execution_count": 4,
"metadata": {
"tags": []
},
"outputs": [
{
"data": {
"text/html": [
"
\n"
],
"text/plain": [
"\u001b[1;38;2;255;0;0m Circuit Summary \u001b[0m\n",
"╭───────────────────────┬───────────────────────────────────────────────────────────────────╮\n",
"│\u001b[1m \u001b[0m\u001b[1;38;2;59;59;149mInfo\u001b[0m\u001b[1m \u001b[0m\u001b[1m \u001b[0m│\u001b[1m \u001b[0m\u001b[1;38;2;59;59;149mvalue\u001b[0m\u001b[1m \u001b[0m\u001b[1m \u001b[0m│\n",
"├───────────────────────┼───────────────────────────────────────────────────────────────────┤\n",
"│ \u001b[1mNumber of qubit\u001b[0m │ 127 │\n",
"├───────────────────────┼───────────────────────────────────────────────────────────────────┤\n",
"│ \u001b[1mTotal number of gate\u001b[0m │ 2794 │\n",
"│ Barrier │ 0 │\n",
"│ Noise Channel │ 0 │\n",
"│ Measurement │ 0 │\n",
"├───────────────────────┼───────────────────────────────────────────────────────────────────┤\n",
"│ \u001b[1mParameter gate\u001b[0m │ 1016 │\n",
"│ 508 ansatz parameters │ \u001b[38;2;72;201;176mtheta507, theta506, theta505, theta504, theta503, theta502, \u001b[0m │\n",
"│ │ \u001b[38;2;72;201;176mtheta501, theta500, theta499, theta498...\u001b[0m │\n",
"╰───────────────────────┴───────────────────────────────────────────────────────────────────╯\n"
]
},
"metadata": {},
"output_type": "display_data"
}
],
"source": [
"# complete circuit\n",
"circ1_inv = dagger(circ1) # dagger() reverse the circuit\n",
"# complete circuit = reversion of initial circuit + circuit after compilation\n",
"circ_all = circ1_inv + circ2\n",
"circ_all.summary() # summary complete circuit"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Setp 2\n",
"\n",
"Draw the complete circuit into ZX diagram.\n",
"\n",
"The equivalence checking of parameterized quantum circuits is based on the ZX calculus. Then the quantum circuits need to be converted into ZX diagrams.\n",
"\n",
"The quantum gate is the vertex in the ZX diagram, divided into 3 colors. The [H](https://www.mindspore.cn/mindquantum/docs/en/master/core/gates/mindquantum.core.gates.HGate.html) gate is represented as a yellow vertex, the [RX](https://www.mindspore.cn/mindquantum/docs/en/master/core/gates/mindquantum.core.gates.RX.html) gate is a red vertex with parameters, and the [RZ](https://www.mindspore.cn/mindquantum/docs/en/master/core/gates/mindquantum.core.gates.RZ.html) gate is a green vertex with parameters. The target qubit of the [CNOT](https://www.mindspore.cn/mindquantum/docs/en/master/core/gates/mindquantum.core.gates.CNOTGate.html) gate is a red vertex, and the control qubit is a green vertex, which two are neighbors. The vertices of two adjacent quantum gates on the same qubit are neighbors to each other.\n",
"\n",
"Start by defining the vertex class and graph class."
]
},
{
"cell_type": "code",
"execution_count": 9,
"metadata": {},
"outputs": [],
"source": [
"class Vertex:\n",
" def __init__(self, name, color, qubit, neighbor, phase=0.0):\n",
" self.name = name # the number of the vertex\n",
" self.color = color # the color of the vertex\n",
" self.phase = phase # the parameter of the vertex\n",
" self.qubit = qubit # the qubit of the vertex\n",
" self.neighbor = neighbor # the neighbor of the vertex"
]
},
{
"cell_type": "code",
"execution_count": 10,
"metadata": {},
"outputs": [],
"source": [
"# graph class\n",
"class Graph:\n",
" def __init__(self):\n",
" self.vertices = {}\n",
" # count: the total number of vertices\n",
" # which only increases but does not decrease\n",
" # count is also used to name new vertices\n",
" self.count = 0\n",
"\n",
" # add an edge from the start to the end\n",
" def add_edge(self, from_vertex, to_vertex):\n",
" self.vertices[from_vertex].neighbor.append(to_vertex)\n",
"\n",
" # add vertex\n",
" def add_vertex(self, color, qubit, neighbor, phase=0.0):\n",
" name = self.count\n",
" self.count += 1\n",
" # add edges from the current vertex to its neighbors\n",
" self.vertices[name] = Vertex(name, color, qubit, neighbor, phase)\n",
" for v in neighbor: # add edges from its neighbors to it\n",
" self.add_edge(v, name)\n",
"\n",
" def print(self):\n",
" print(\"==================graph message==================\")\n",
" for v in self.vertices.values():\n",
" print(v.name, '\\t', v.neighbor, '\\t', v.color, '\\t', v.phase)\n",
" print('\\n')\n",
"\n",
" # clear the loops produced during adding or deleting\n",
" # there is no loop in ZX-diagram(loop which made of a single edge)\n",
" def clear(self):\n",
" for v in self.vertices.values():\n",
" while v.name in v.neighbor:\n",
" # remove the vertex from its own neighbors\n",
" self.vertices[v.name].neighbor.remove(v.name)\n",
"\n",
" # delete vertex\n",
" def delete_vertex(self, name):\n",
" for v in self.vertices.values():\n",
" while name in v.neighbor:\n",
" # delete edges whose end is the current vertex\n",
" self.vertices[v.name].neighbor.remove(name)\n",
" # delete edges whose start is the current vertex\n",
" self.vertices.pop(name)\n",
"\n",
" # if two circuits are equivalent\n",
" def equiv(self):\n",
" # if equivalent, after simplification, there is no vertex\n",
" if not self.vertices:\n",
" print(\"Equivalent!\")\n",
" else:\n",
" print(\"Not sure!\")"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Then draw the quantum circuit into a ZX diagram.\n",
"\n",
"Traverse all the quantum gates in the circuit and plot them as vertices in the ZX diagram. If there is no gate on the current qubit, the current quantum gate has no neighbors. If there has at least one quantum gate on the current qubit, the current quantum gate and the last quantum gate on the qubit are neighbors. The [CNOT](https://www.mindspore.cn/mindquantum/docs/en/master/core/gates/mindquantum.core.gates.CNOTGate.html) gate adds a neighbor relationship between the control qubit and the target qubit."
]
},
{
"cell_type": "code",
"execution_count": 11,
"metadata": {},
"outputs": [],
"source": [
"def draw_graph(circ):\n",
" g = Graph()\n",
" # last_name saves the last vertex on each qubit\n",
" last_name = [-1] * circ.n_qubits\n",
" for gate in circ: # traverse all the quantum gates\n",
" if gate.name == 'H': # H gate = yellow vertex\n",
" # there are vertices on the current qubit\n",
" if last_name[gate.obj_qubits[0]] != -1:\n",
" g.add_vertex('yellow', gate.obj_qubits[0],\n",
" [last_name[gate.obj_qubits[0]]])\n",
" else: # there is no vertex on the current qubit\n",
" g.add_vertex('yellow', gate.obj_qubits[0], [])\n",
" # update the last vertex on the current qubit to the current vertex\n",
" last_name[gate.obj_qubits[0]] = g.count-1\n",
" if gate.name == 'RX': # RX gate = red vertex\n",
" if last_name[gate.obj_qubits[0]] != -1:\n",
" g.add_vertex('red', gate.obj_qubits[0],\n",
" [last_name[gate.obj_qubits[0]]], gate.coeff)\n",
" else:\n",
" g.add_vertex('red', gate.obj_qubits[0], [], gate.coeff)\n",
" last_name[gate.obj_qubits[0]] = g.count-1\n",
" if gate.name == 'RZ': # RZ gate = green vertex\n",
" if last_name[gate.obj_qubits[0]] != -1:\n",
" g.add_vertex('green', gate.obj_qubits[0],\n",
" [last_name[gate.obj_qubits[0]]], gate.coeff)\n",
" else:\n",
" g.add_vertex('green', gate.obj_qubits[0], [], gate.coeff)\n",
" last_name[gate.obj_qubits[0]] = g.count-1\n",
" if gate.name == 'CNOT':\n",
" # control qubit = green vertex\n",
" if last_name[gate.obj_qubits[1]] != -1:\n",
" g.add_vertex('green', gate.obj_qubits[1],\n",
" [last_name[gate.obj_qubits[1]]])\n",
" else:\n",
" g.add_vertex('green', gate.obj_qubits[1], [])\n",
" last_name[gate.obj_qubits[1]] = g.count-1\n",
" # target qubit = red vertex\n",
" if last_name[gate.obj_qubits[0]] != -1:\n",
" g.add_vertex('red', gate.obj_qubits[0],\n",
" [last_name[gate.obj_qubits[0]], g.count-1])\n",
" else:\n",
" g.add_vertex('red', gate.obj_qubits[0], [g.count-1])\n",
" last_name[gate.obj_qubits[0]] = g.count-1\n",
" return g"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Finally, draw the complete quantum circuit into a ZX diagram."
]
},
{
"cell_type": "code",
"execution_count": 12,
"metadata": {
"tags": []
},
"outputs": [],
"source": [
"g = draw_graph(circ_all)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Step 3\n",
"\n",
"Simplify the ZX diagram\n",
"\n",
"The ZX calculus consists of ZX diagrams and reduction rules, according to which the vertices and neighbor relations in the ZX diagram are simplified.\n",
"\n",
"Here lists some of the rules, and will not be repeated one by one.\n",
"\n",
"rule 1: red or green vertices with parameter 0 that are not adjacent to vertices on other qubits can be deleted.\n",
"\n",
""
]
},
{
"cell_type": "code",
"execution_count": 13,
"metadata": {},
"outputs": [],
"source": [
"def rule_1(g: Graph):\n",
" # during the ZX calculus, the vertices will increase or decrease\n",
" # use list() to get all the initial vertices\n",
" for v1 in list(g.vertices.keys()):\n",
" # whether the current vertex has been deleted during simplification\n",
" if v1 not in g.vertices.keys():\n",
" continue # deleted, pass\n",
" v1 = g.vertices[v1]\n",
" # parameter = 0\n",
" if v1.phase == 0 or list(v1.phase.values()) == [0.0]*len(list(v1.phase.values())):\n",
" # whether the current vertex is related to vertices on other qubits\n",
" # and if so, it cannot be deleted\n",
" flag = True\n",
" for v2 in v1.neighbor:\n",
" v2 = g.vertices[v2]\n",
" # related to vertices on other qubits\n",
" if v2.qubit != v1.qubit:\n",
" flag = False\n",
" break\n",
" if flag: # not related to vertices on other qubits\n",
" for v2 in v1.neighbor:\n",
" v2 = g.vertices[v2]\n",
" # connect the previous vertex to the next vertex\n",
" v2.neighbor.extend(v1.neighbor)\n",
" g.clear() # remove rings that may arise\n",
" g.delete_vertex(v1.name) # delete the current vertex"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"rule 2: two adjacent, red or green vertices of the same color can be merged.\n",
"\n",
""
]
},
{
"cell_type": "code",
"execution_count": 14,
"metadata": {},
"outputs": [],
"source": [
"def rule_2(g: Graph):\n",
" for v1 in list(g.vertices.keys()):\n",
" if v1 not in g.vertices.keys():\n",
" continue\n",
" v1 = g.vertices[v1]\n",
" if v1.color == 'red' or v1.color == 'green': # red or green\n",
" for v2 in v1.neighbor: # adjacent\n",
" v2 = g.vertices[v2]\n",
" if v2.color == v1.color: # same color\n",
" v2.phase = v2.phase + v1.phase # add the parameters\n",
" # merge these two vertices\n",
" v2.neighbor.extend(v1.neighbor)\n",
" g.clear()\n",
" for v3 in v1.neighbor: # update the neighbors\n",
" v3 = g.vertices[v3]\n",
" v3.neighbor.append(v2.name)\n",
" g.clear()\n",
" # delete the vertex that has been merged\n",
" g.delete_vertex(v1.name)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"rule 3: green vertices whose neighbors are yellow vertices can become red vertices and remove adjacent yellow vertices.\n",
"\n",
""
]
},
{
"cell_type": "code",
"execution_count": 15,
"metadata": {},
"outputs": [],
"source": [
"def rule_3(g: Graph):\n",
" for v1 in list(g.vertices.keys()):\n",
" if v1 not in g.vertices.keys():\n",
" continue\n",
" v1 = g.vertices[v1]\n",
" if v1.color == 'green':\n",
" flag = True # if all neighbors yellow\n",
" for v2 in v1.neighbor:\n",
" v2 = g.vertices[v2]\n",
" if v2.color != 'yellow': # not all neighbors yellow\n",
" flag = False\n",
" break\n",
" if flag: # all neighbors yellow\n",
" v1.color = 'red' # turn into red\n",
" v1_neighbor = list(v1.neighbor)\n",
" for v2 in v1_neighbor: # delete these yellow vertices\n",
" v2 = g.vertices[v2]\n",
" v1.neighbor.extend(v2.neighbor)\n",
" g.clear()\n",
" for v3 in v2.neighbor:\n",
" v3 = g.vertices[v3]\n",
" v3.neighbor.append(v1.name)\n",
" g.clear()\n",
" g.delete_vertex(v2.name)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"rule 4: two edges between adjacent red and green vertices can be deleted.\n",
"\n",
""
]
},
{
"cell_type": "code",
"execution_count": 16,
"metadata": {},
"outputs": [],
"source": [
"def rule_4(g: Graph):\n",
" for v1 in list(g.vertices.keys()):\n",
" if v1 not in g.vertices.keys():\n",
" continue\n",
" v1 = g.vertices[v1]\n",
" if v1.color == 'green':\n",
" for v2 in v1.neighbor:\n",
" v2 = g.vertices[v2]\n",
" # adjacent red and green vertices with two edges\n",
" if v2.color == 'red' and v2.neighbor.count(v1.name) == 2:\n",
" # delete these two edges\n",
" while v2.name in g.vertices[v1.name].neighbor:\n",
" v1.neighbor.remove(v2.name)\n",
" while v1.name in g.vertices[v2.name].neighbor:\n",
" v2.neighbor.remove(v1.name)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Then, use the above rules to simplify the ZX diagram. If no vertex is deleted in a round, the simplification is considered to be complete."
]
},
{
"cell_type": "code",
"execution_count": 17,
"metadata": {},
"outputs": [],
"source": [
"def simplify(g: Graph):\n",
" temp = [] # whether vertices have been deleted in the current round\n",
" # if no vertex is removed in the current round\n",
" # the simplification is considered complete\n",
" while temp != list(g.vertices.keys()):\n",
" temp = list(g.vertices.keys())\n",
" rule_3(g)\n",
" rule_2(g)\n",
" rule_4(g)\n",
" rule_1(g)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"The complete circuit is large in scale, and a single-layer circuit acting on three qubits can be constructed for testing."
]
},
{
"cell_type": "code",
"execution_count": 18,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 18,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"test_circ1 = build_ansatz(3, 1)\n",
"test_circ1_inv = dagger(test_circ1)\n",
"test_circ2 = compile_circuit(test_circ1)\n",
"\n",
"test_circ_all = test_circ1_inv + test_circ2\n",
"\n",
"test_circ_all.svg()"
]
},
{
"cell_type": "code",
"execution_count": 19,
"metadata": {
"tags": []
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"==================graph message==================\n",
"0 \t [4] \t red \t -theta5\n",
"1 \t [3] \t red \t -theta4\n",
"2 \t [5] \t red \t -theta3\n",
"3 \t [1, 4, 6] \t green \t 0.0\n",
"4 \t [0, 3, 7] \t red \t 0.0\n",
"5 \t [2, 6, 8] \t green \t 0.0\n",
"6 \t [3, 5, 10] \t red \t 0.0\n",
"7 \t [4, 8, 9] \t green \t 0.0\n",
"8 \t [5, 7, 11] \t red \t 0.0\n",
"9 \t [7, 18] \t red \t -theta2\n",
"10 \t [6, 15] \t red \t -theta1\n",
"11 \t [8, 12] \t red \t -theta0\n",
"12 \t [11, 13] \t yellow \t 0.0\n",
"13 \t [12, 14] \t green \t theta0\n",
"14 \t [13, 22] \t yellow \t 0.0\n",
"15 \t [10, 16] \t yellow \t 0.0\n",
"16 \t [15, 17] \t green \t theta1\n",
"17 \t [16, 24] \t yellow \t 0.0\n",
"18 \t [9, 19] \t yellow \t 0.0\n",
"19 \t [18, 20] \t green \t theta2\n",
"20 \t [19, 21] \t yellow \t 0.0\n",
"21 \t [20, 22, 26] \t green \t 0.0\n",
"22 \t [14, 21, 23] \t red \t 0.0\n",
"23 \t [22, 24, 27] \t green \t 0.0\n",
"24 \t [17, 23, 25] \t red \t 0.0\n",
"25 \t [24, 26, 30] \t green \t 0.0\n",
"26 \t [21, 25, 33] \t red \t 0.0\n",
"27 \t [23, 28] \t yellow \t 0.0\n",
"28 \t [27, 29] \t green \t theta3\n",
"29 \t [28] \t yellow \t 0.0\n",
"30 \t [25, 31] \t yellow \t 0.0\n",
"31 \t [30, 32] \t green \t theta4\n",
"32 \t [31] \t yellow \t 0.0\n",
"33 \t [26, 34] \t yellow \t 0.0\n",
"34 \t [33, 35] \t green \t theta5\n",
"35 \t [34] \t yellow \t 0.0\n",
"\n",
"\n"
]
}
],
"source": [
"# draw the testing circuit into a ZX diagram\n",
"test_g = draw_graph(test_circ_all)\n",
"test_g.print()"
]
},
{
"cell_type": "code",
"execution_count": 20,
"metadata": {
"tags": []
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"before simplification:\n",
"Not sure!\n",
"after simplification:\n",
"Equivalent!\n"
]
}
],
"source": [
"# simplify the testing circuit\n",
"print(\"before simplification:\")\n",
"test_g.equiv()\n",
"\n",
"simplify(test_g)\n",
"\n",
"print(\"after simplification:\")\n",
"test_g.equiv()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"After passing the simplification function test, we can try to simplify the ZX diagram of the complete circuit. The result shows that the two circuits before and after compilation are equivalent."
]
},
{
"cell_type": "code",
"execution_count": 21,
"metadata": {
"tags": []
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"before simplification:\n",
"Not sure!\n"
]
},
{
"name": "stdout",
"output_type": "stream",
"text": [
"after simplification:\n",
"Equivalent!\n"
]
}
],
"source": [
"# simplify the complete circuit\n",
"print(\"before simplification:\")\n",
"g.equiv()\n",
"\n",
"simplify(g)\n",
"\n",
"print(\"after simplification:\")\n",
"g.equiv()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Step 4\n",
"\n",
"If ZX Calculus not sure then verify by instantiating the parameter.\n",
"\n",
"The ZX calculus cannot directly give the result of the equivalent circuits. In this case, we need to instantiate the parameters in the circuits to determine whether the two circuits after instantiation are equivalent."
]
},
{
"cell_type": "code",
"execution_count": 22,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 22,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"# counterexample\n",
"neq_circ1 = Circuit()\n",
"neq_circ1 += H.on(1)\n",
"neq_circ1 += RX(f'theta{0}').on(2)\n",
"neq_circ1 += CNOT.on(0, 1)\n",
"neq_circ1 += RZ(f'theta{1}').on(0)\n",
"neq_circ1 += CNOT.on(2, 1)\n",
"neq_circ1 += CNOT.on(0, 1)\n",
"neq_circ1 += RX(f'theta{2}').on(2)\n",
"\n",
"neq_circ1.svg()"
]
},
{
"cell_type": "code",
"execution_count": 23,
"metadata": {},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 23,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"neq_circ2 = Circuit()\n",
"neq_circ2 += H.on(1)\n",
"neq_circ2 += RX(f'theta{0}').on(2)\n",
"neq_circ2 += CNOT.on(0, 1)\n",
"neq_circ2 += RZ(f'theta{1}').on(0)\n",
"neq_circ2 += CNOT.on(2, 1)\n",
"neq_circ2 += CNOT.on(0, 1)\n",
"neq_circ2 += RX({f'theta{0}': 1, f'theta{1}': 1, f'theta{2}': 1}).on(2)\n",
"\n",
"neq_circ2.svg()"
]
},
{
"cell_type": "code",
"execution_count": 24,
"metadata": {
"tags": []
},
"outputs": [
{
"data": {
"image/svg+xml": [
""
],
"text/plain": [
""
]
},
"execution_count": 24,
"metadata": {},
"output_type": "execute_result"
}
],
"source": [
"neq_circ1_inv = dagger(neq_circ1)\n",
"neq_circ_all = neq_circ1_inv + neq_circ2 # construct the complete circuit of the counterexample\n",
"neq_circ_all.svg()"
]
},
{
"cell_type": "code",
"execution_count": 25,
"metadata": {
"tags": []
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"before simplification:\n",
"Not sure!\n",
"after simplification:\n",
"Not sure!\n"
]
}
],
"source": [
"# draw the counterexample into ZX diagram and simplify it\n",
"neq_g = draw_graph(neq_circ_all)\n",
"print(\"before simplification:\")\n",
"neq_g.equiv()\n",
"\n",
"simplify(neq_g)\n",
"\n",
"print(\"after simplification:\")\n",
"neq_g.equiv()"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"In this case, after simplification, there are still undeleted vertices in the ZX diagram. So the ZX calculus cannot determine its equivalence and needs to be verified by instantiating parameters.\n",
"\n",
"The instantiation has two steps:\n",
"\n",
"First, directly compare whether the matrices of the two circuits are equivalent after instantiation according to the map function, and stop if not.\n",
"\n",
"Second, if the instantiation according to the map function does not get the result, randomly instantiate the parameters, and then directly compare whether the matrices of the two circuits after instantiation are equivalent. If unequivalent, the two circuits are unequivalent, otherwise equivalent."
]
},
{
"cell_type": "code",
"execution_count": 26,
"metadata": {},
"outputs": [],
"source": [
"# instantiation according to the map function\n",
"def map_para(n, r):\n",
" para = {}\n",
" for i in range(n):\n",
" para[f'theta{i}'] = (2*np.pi/((i+1)*r)-np.pi)\n",
" return para\n",
"\n",
"\n",
"# randomly instantiate the parameters\n",
"def random_para(n):\n",
" para = {}\n",
" for i in range(n):\n",
" para[f'theta{i}'] = (np.random.uniform(np.pi, -np.pi))\n",
" return para"
]
},
{
"cell_type": "code",
"execution_count": 27,
"metadata": {
"tags": []
},
"outputs": [],
"source": [
"# verify by instantiating parameters\n",
"def verify_by_para(circ1, circ2, r):\n",
" # there are n parameters in the circuit\n",
" n = len(list(set(circ1.params_name+circ2.params_name)))\n",
" flag = True # whether the previous r-1 round has a result\n",
" for i in range(r-1): # instantiation according to the map function\n",
" para = map_para(n, i+1)\n",
" # whether the matrices of the two circuits are equivalent\n",
" if np.array_equal(circ1.matrix(para), circ2.matrix(para)):\n",
" continue\n",
" else:\n",
" print('Not equivalent!')\n",
" flag = False # get a result\n",
" break\n",
"\n",
" if flag: # randomly instantiate the parameters\n",
" para = random_para(n)\n",
" if np.array_equal(circ1.matrix(para), circ2.matrix(para)):\n",
" print('Equivalent!')\n",
" else:\n",
" print('Not equivalent!')"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"Verify the equivalence of the two counterexample circuits by instantiation."
]
},
{
"cell_type": "code",
"execution_count": 28,
"metadata": {
"tags": []
},
"outputs": [
{
"name": "stdout",
"output_type": "stream",
"text": [
"Not equivalent!\n"
]
}
],
"source": [
"verify_by_para(neq_circ1, neq_circ2, 5)"
]
},
{
"cell_type": "markdown",
"metadata": {},
"source": [
"## Final step: merge the above process into a complete function"
]
},
{
"cell_type": "code",
"execution_count": 29,
"metadata": {
"tags": []
},
"outputs": [],
"source": [
"def ZXcalculus(circ1, circ2):\n",
" circ1_inv = dagger(circ1) # reverse the initial circuit\n",
" circ = circ1_inv + circ2 # construct the complete circuit\n",
" g = draw_graph(circ) # draw the complete circuit into ZX diagram\n",
" print(\"before simplification:\")\n",
" g.equiv()\n",
" simplify(g) # simplify by the rules\n",
" print(\"after simplification:\")\n",
" if not g.vertices: # get a result by ZX calculus\n",
" g.equiv()\n",
" else: # need to verify by instantiation\n",
" g.equiv()\n",
" print(\"verify by instantiation:\")\n",
" verify_by_para(circ1, circ2, 5)"
]
},
{
"cell_type": "code",
"execution_count": 30,
"metadata": {},
"outputs": [
{
"data": {
"text/html": [
"\n",
"