量子電路驗證方法與架構：模擬、等價性檢查與動態斷言

Abstract

驗證對於確保量子計算系統的正確性至關重要。然而，不同於傳統計算系統的驗證技術之成熟，量子計算至今仍嚴重缺乏系統化和自動化的驗證方法。我們發展了量子電路驗證的方法與框架，同時涵蓋靜態與動態驗證技術，包括模擬、等價性檢查、布林匹配以及動態斷言。 我們的量子電路模擬工具允許使用者計算滿足自定義性質的量子態的精確機率或期望值，為量子程式設計與測試提供有效的手段。實驗中的案例研究顯示，我們的模擬工具能夠超越現有工具的能力，提供精確的量子電路分析和驗證。 針對形式化驗證方法，有鑑於現有的等價性檢查方法缺乏足夠的通用性，難以處理日趨複雜的高級電路特性，因此我們提出了一個組合量子電路的一般模型，並由此定義了量子電路的部分等價關係，以及開發了相應的等價性檢查演算法。我們相信這些技術能夠涵蓋絕大多數──若非全部──的組合量子電路應用場景。從等價性的另一個角度來說，我們提供了第一個針對可逆邏輯電路的布林匹配問題的完整研究，包含傳統或量子演算法及其計算複雜度。值得注意的是，針對尋找輸入端的取反與排列以使兩個電路等價的問題，我們開發了多項式時間的量子演算法，而其經典對應方法的複雜度則為指數級。此一結果可被認為是設計自動化領域中首個指數級加速的演算法。 針對動態驗證，藉由利用量子電路的消失態，我們提出了第一個量子電路動態斷言的通用框架，並能夠在錯誤偵測能力與斷言電路複雜度之間提供靈活的權衡空間。實驗顯示了我們的方法在通用性與有效性方面的獨特優勢，能夠提升量子電路在各類基準測試中的執行效率與成功率。 本研究為量子程式驗證的未來奠定了廣泛的基礎，並希望所提出的方法與框架能推動量子程式設計自動化的發展。

Verification is essential for ensuring the correctness of quantum computing systems, yet systematic and automated approaches remain far behind their classical counterparts. We present methods and frameworks for quantum circuit verification, covering both static and dynamic approaches, including simulation, equivalence checking, Boolean matching, and runtime assertion. Our simulation tool allows users to query exact probabilities or expectation values of user-defined quantum state properties, thereby enhancing program design and testing. Case studies demonstrate its unique ability to support exact quantum circuit analysis and verification beyond the capabilities of existing tools. For formal verification, motivated by the lack of generality of existing equivalence checking methods in handling advanced circuit features, we propose a general model of composable quantum circuits, formalize partial equivalence relations, and develop corresponding algorithms, which are capable of encompassing most, if not all, composable quantum circuits. From another perspective on equivalence, we provide the first comprehensive characterization of algorithms and the computational complexity of Boolean matching reversible logic circuits. Notably, we develop polynomial-time quantum algorithms that identify input negations and permutations to make two circuits equivalent, while the classical complexity is exponential. This result arguably achieves the first exponential speedup for a design automation task. For dynamic verification, we introduce the first general framework for quantum circuit runtime assertion by exploring vanishing states of quantum programs, offering flexible trade-offs between error-detection power and assertion circuit complexity. Experiments show the unique benefits of our method in generality and effectiveness, improving quantum circuit execution efficiency and success rates in various benchmarks. This work establishes a versatile foundation for the future of quantum program verification, and we hope that the proposed methods and frameworks help advance the automation of quantum program design.