鴻海研究院量子計算所謝明修所長與黃偉家研究員與來自台灣中研院、捷克等地的研究團隊，於 TACAS 2025（第31屆系統建構與分析工具與算法國際研討會）發表最新研究成果《AutoQ 2.0: From Verification of Quantum Circuits to Verification of Quantum Programs》。該論文已由 Springer 出版，收錄於 Lecture Notes in Computer Science 系列第15698卷，並開放存取。

AutoQ 2.0 是一款專為量子程式設計的自動驗證工具，擴展自先前的 AutoQ 1.0，從僅支援量子電路驗證，進一步涵蓋具備經典控制流程（如條件分支與迴圈）的完整量子程式。此項擴展克服了多項挑戰，包括處理量子測量所引發的狀態坍縮與正規化問題，以及將傳統程式驗證中的迴圈不變量技術應用於量子領域。

研究團隊成功利用 AutoQ 2.0 驗證了兩類無法僅以量子電路描述的進階量子演算法：重試直到成功（Repeat-Until-Success, RUS）演算法與基於弱測量的 Grover 搜尋演算法。實驗結果顯示，AutoQ 2.0 能高效驗證所有測試案例，其中 RUS 演算法可即時驗證，而在處理100個量子位元的 Grover 搜尋演算法時，驗證時間約為20分鐘。

此研究成果不僅代表台灣在量子計算與程式驗證領域的技術突破，也為全球量子軟體開發與驗證提供了新的工具與方法。AutoQ 2.0 的推出，預期將加速量子演算法的開發與部署，推動量子科技的實際應用。

論文全文可於 Springer 官方網站免費取得：

👉 https://link.springer.com/chapter/10.1007/978-3-031-90660-2_5