計畫成員 : 鐘楷閔、陳郁方、柯向上
量子計算機科學領域由於量子計算技術的快速發展而嶄露頭角。這個跨學科領域的各方面仍處於起步階段，為研究人員提供了一個獨特且及時的機會，可以在理論方面做出基礎性貢獻。
我們致力於在量子計算科學領域做出基礎性的理論貢獻。我們匯集了不同專業背景的研究人員，其中鐘楷閔研究員已從事量子密碼學研究近十年，而陳郁方研究員和柯向上助研究員則是編程語言研究的專家。在本所鼓勵跨領域合作的環境下，我們已在量子計算科學進行合作研究工作超過兩年。我們的研究工作得到了國家科學及技術委員會(NSTC)的四年期量子計算計畫、中央研究院五年期深耕研究計畫以及本所合作計畫的支持。我們專注於三個主要研究領域：量子密碼學、量子程序驗證和高級量子編程語言。以下我們將對這些領域的研究進行詳細的說明。
量子密碼學
量子密碼學是一個跨學科領域，旨在瞭解量子能力對密碼學的作用。它具有雙面刃的性質。負向方面，Shor 的量子演算法可以破解許多廣泛使用的計算假設，如質因數分解、RSA和Diffie-Hellman(DDH)假設，將會破解當今大部分使用中的公鑰加密技術。而在正向方面，量子能力使得在經典情況下不可能完成的密碼學目標成為可能，例如最近快速發展中的幾個量子密碼學的研究課題：不可複製密碼學(unclonable cryptography)（包括量子貨幣(quantum money)、不可複製加密(unclonable encryption)和具有可證明刪除功能的密碼學(cryptography with certifiable deletion)）和計算量子基元(computational quantum primitives)（例如偽隨機狀態(pseudorandom quantum state)、單向狀態生成器(one-way state generators)和EFI對(EFI pairs)）。量子計算的進步推動了近期量子密碼學的快速發展。
我們投入這個領域研究近十年，對後量子零知識證明(post-quantum zero-knowledge proofs)、量子計算的經典驗證(classical verification of quantum computation)、安全的多方量子計算(secure multiparty quantum computation)和量子時間-空間折衷(quantum time-space tradeoffs)等各種主題做出了研究貢獻。我們還藉由開發量子密碼學技術來回答量子計算和複雜性理論中的問題。以下是我們過去研究的兩個亮點：
- 混合經典和低深度量子計算模型的計算能力：由於近期量子計算因計算雜訊將會受限於低深度計算，結合經典計算和低深度量子計算的混合計算模型就對應了目前可實現的計算模型，了解其計算能力是個重要的基礎問題。在我們和 賴青沂 和 賈乃輝 共同合作的工作中（STOC 2020；JACM 2023）[2]，我們研究了這種混合模型的能力。我們發展量子密碼學的技術證明了不限深度量子計算模型(BQP) 比兩種混合模型計算能力強大 (具體來說, 我們證明了模型間的Oracle Separation)。我們的結果證明了 Scott Aaronson 的猜想，並證明了相對於Oracle，Richard Jozsa 的猜想不成立。
- 求反函數問題(function inversion)的緊緻量子時間-空間折衷(quantum time-space tradeoff)：求反函數問題的量子時間-空間折衷問題，是密碼學和複雜性理論中的一個基礎性問題。在我們和郭思瑤、劉啟鵬和錢洛文共同合作的工作中（FOCS 2020），我們開發證明技術對此問題給出完整的解答。我們的結果顯示，量子演算法對求反函數問題的唯一的優勢是 Grover 的搜尋演算法，而量子預處理(quantum preprocessing)並不能幫助加速 Grover 演算法。我們還證明了對其他密碼學計算問題的量子時間-空間折衷。
展望未來，我們規劃探討的兩個研究方向如下：證明最近發展的計算量子基元之間的黑盒分離(black-box separation)，以及計算量子基元所涉及的計算問題的複雜性理論研究。量子密碼學仍然是一個相對年輕的領域。我們非常期待繼續探索，持續在這個領域做出基礎的理論貢獻。
量子程式驗證
量子電腦的概念，大約在1980年代開始萌芽。之後Peter Shor提出量子質因數分解演算法，動搖到眾多加密演算法的根本假設，開始受到高度重視。最近幾年，量子電腦硬體的逐漸成熟，對應的量子軟體開發技術也日益受到重視。可以預見的，軟體的規模會不斷地增加，確保設計出來的程式正確無誤的難度也會高速提升。這現象在傳統軟體已經很普遍，任何有一定規模的軟體程式，無可避免的都會有大大小小的錯誤，最後只能和這些錯誤共存。只有在早期就將維護軟體品質的新技術引入開發流程，量子軟體才有機會擺脫過去的窘境，避免同樣錯誤發生。
形式化驗證是唯一能確保軟體完全符合規範的技術。比較起傳統軟體，他在量子軟體的發展具有更高的潛力。傳統靠測試來維護軟體品質的方法，在量子軟體不再適用，因為量子計算具有機率性，而且量測會造成量子狀態的塌陷。但目前量子形式化驗證技術仍然有需要人類引導，不能全自動化，只能檢查固定的性質，缺乏彈性等等的限制。在這個計畫中，我們將建議兩個可行的研究方向來突破現有技術的限制，一個是基於「自動機理論」(automata theory)的方法，一個是基於「SMT」(satisfiability module theories)的決策程序。因為現在正是量子軟體研究的起飛期，尤其時全自動的形式化驗證技術，更是處於嬰兒階段。我們認為在這個時間點切入，有很大的機會能產生具有高度影響力的成果。
從四十年前電腦輔助驗證的草創階段，自動機理論在就一直是重要的研究主題。自動機的許多數學特性讓他成為電腦輔助驗證最常使用的計算模型。最近我們發展了一個基於自動機理論的量子程式驗證方法。量子狀態可以表示為一顆二元樹，機率(振幅)就標注在葉節點。樹狀自動機(tree automata)可以精簡的描述二元樹的集合。而樹狀自動機間的轉換(transduction)，可以描述量子邏輯閘的語意。量子程式有無符合規格的問題，就可以化簡為樹狀自動機語言包含的問題。最近我們更近一步的把這個方法延伸至關聯式性質的驗證。這些成果分別會發表在PLDI和CAV。這兩者分別是程式語言和形式化驗證研究的頂級會議。
SMT大概在二十年前開始綻露頭角，成為自動化軟體驗證和測試的主流技術。目前SMT技術並沒有支援量子理論(quantum theory)，因此不容易直接使用來驗證或測試量子程式。但是我們近期的突破可能會讓他變為可行。我們發現可能可以透過調整目前陣列理論(array theory)的演算法，創造出SMT的量子理論的支援。這成果目前正在一個主要會議的審查階段。
高階量子程式語言
我們正在探索的另一個重要題目是高階量子程式語言。目前提出的量子程式語言大部分都是用來描述量子電路，抽象程度偏低。若與古典計算的狀況對照，量子電路語言大致對應於組合語言。然而組合語言現在已經很少使用，大部分人會選用高階語言 — 亦可想成比較抽象方便的計算模型 — 來寫程式，然後靠編譯器將抽象計算模型和實際運行的電腦架構連接起來。這樣的基礎設施在量子計算領域仍不成熟，亟需發展。
我們特別著重發掘量子演算法的抽象結構，藉以方便地設計、描述、理解量子演算法（同時也確保這些抽象結構能夠編譯為量子電路，實際進行計算）。設計量子演算法時，相較於量子電路，更有用的是繼承自量子力學的線性代數語言，但這個語言仍偏低階，量子計算的概念往往深藏在晦澀冗長的算式之中。較理想的高階語言應能簡要表示出量子計算的概念，並能方便以這些概念進行推論。
更具體而言，我們正在探索「圖像量子理論」（quantum picturalism）在量子演算法設計方面的潛力：圖像量子理論的目標是用一套圖像化（但不失數學嚴謹度）的語言重建量子理論，希望能夠簡化對量子現象的推論、突顯計算意義、並建立與其他計算模型的深層聯繫。透過這套圖像語言，我們已對一些現有的量子演算法有了新的理解。接下來我們希望能從這些經驗歸納出普遍原則，作為高階量子程式語言的設計基礎。