希伯特空間位元切片：精確量子電路模擬與驗證之規模擴展

近年來，量子計算大幅度地進展且被認為即將改變目前的計算規範。量子電路模擬與驗證在量子硬體與軟體系統的開發工具鏈中扮演關鍵的角色。然而，由於龐大的量子態希伯特空間 (Hilbert space)，在傳統電腦中表示量子態與量子電路極具挑戰性，儘管已出現為數眾多的研究探討相關問題，量子電路模擬 (simulation) 與等價性檢查 (equivalence checking) 的難度依然不可小覷。在此篇論文中，我們以兩個面向增進了量子電路模擬與等價性檢查: 精確度以及規模可擴展性 (scalability)。前者是藉由使用複數的代數表示形式；後者則是藉由數字表示之位元切片以及使用象徵性布林函數之操作取代矩陣與向量之乘法。實驗結果顯示本篇論文提出之方法在許多的量子電路上皆可得到優於當前最新技術的表現。本篇的模擬方法有效地模擬量子電路，其量子位元最高可到達萬之數量級；本篇的等價性檢查方法修正了當前技術產生之錯誤結果，且在確保正確結果的同時加速了檢查流程。

關鍵字

量子計算；量子電路；電路模擬；等價性檢查；二元決策圖；代數表示

並列摘要

Quantum computing is greatly advanced in recent years and is expected to transform the computation paradigm in the near future. Quantum circuit simulation and equivalence checking play key roles in the toolchain for the development of quantum hardware and software systems. However, due to the enormous Hilbert space of quantum states, representing quantum states and circuits with classical computers is notoriously challenging, resulting in difficulties of quantum circuit simulation and equivalence checking, despite notable efforts have been made. In this thesis, we enhance quantum circuit simulation and equivalence checking in two dimensions: accuracy and scalability. The former is achieved by using an algebraic representation of complex numbers; the latter is achieved by bit-slicing the number representation and replacing matrix-vector and matrix-matrix multiplication with symbolic Boolean function manipulation. Experimental results demonstrate the superiority of our method to the state-of-the-art over various quantum circuits. For simulation, our method can efficiently simulate circuits with up to tens of thousands of qubits. For equivalence checking, our method overcomes the incorrect results produced by the state-of-the-art and can always conduct accurate checking, even along with speed-ups.