研究人員
量子資訊科學實驗室
鐘楷閔、陳郁方、柯向上
本實驗室致力於量子與資訊科學結合之跨領域理論研究，主要研究方向為量子密碼學、量子程式驗證與高階量子程式語言。在量子密碼學領域我們已耕耘多年，在如後量子零知識證明 (Post-Quantum Zero-Knowledge Proofs)、古典驗證量子計算 (Classical Verification of Quantum Computations)、安全多方量子計算 (Secure Multiparty Quantum Computation)、量子時間空間權衡 (Quantum Time-Space Tradeoffs) 等課題上取得重要研究成果。我們也通過發展量子密碼學的技術來回答關於量子計算與複雜度理論的問題，我們發表在 STOC 2020 的研究成果回答了 Scott Aaronson 與 Richard Jozsa 在 2005 年提出的關於低深度量子計算與古典計算混合模型之計算能力的兩個猜想:我們的結果肯定了 Aaronson 的猜想並對 Jozsa 的猜想在相對於一預言機模型 (Oracle Model) 下給了否定的答案。在量子程式驗證領域，我們針對兩個研究方向來突破現有技術的限制，一個是基於「自動機理論」 (automata theory) 的方法，一個是基於「SMT」 (satisfiability modulo theories) 的決策程序。我們用樹狀自動機 (tree automata) 來精簡的描述量子狀態和處理量子邏輯閘，基於此建立了一套自動量子軟體驗證的框架，這是第一次自動機理論和量子電路驗證的結合。我們一系列的成果將會在 PLDI 2023 和 CAV 2023 發表。此外，我們也發展了一套 SMT 的量子理論，讓量子程式驗證能完整在此框架下運作。這成果正在一個主要會議的審查階段。我們相信這個計畫有很大的潛力能對量子軟體和驗證產生深遠的影響。在高階量子程式語言方面，我們正在探索「圖像量子理論」(Quantum Picturalism)在量子演算法設計方面的潛力，作為高階量子程式語言的設計基礎。
目前主要計畫
- 院內深耕計畫:量子密碼學的理論研究【鐘楷閔， 2021/01–2025/12】
- 國科會量子國家隊計畫:量子計算機科學之理論發展-量子計算機科學之理論發展(1/5)【鐘楷閔、楊柏因、陳郁方，2022/03–2023/02】
- 國科會:後量子密碼學在理論上的挑戰與機會【鐘楷閔，2020/07-2023/08】
- 美國空軍基礎科學研究中心計畫:安全多方的量子計算【鐘楷閔，2020-08-01–2023-09-03】
- 所內合作計畫:Towards a high-level quantum-al- gorithmic programming language【柯向上、鐘楷閔，2023/01–2024/12】
後量子密碼學實驗室
楊柏因、倪儒本、王柏堯、鐘楷閔
本實驗室致力於量子電腦出現後仍可存續的密碼學的理論和實務研究，主要研究方向為後量子密碼學理論、實作與其驗證。在後量子密碼學領域我們已耕耘多年。特別是在2021年以下，我們在快速傅立葉變換與數論轉換 (Number Theoretic Transform) 使用於晶格密碼學實作上有多篇論文。由於本實驗室在 NTT 上的實作能力。最近在後量子的實作面上有很多最佳的實作程式出自本實驗室。
本實驗室同時也參與了很多件美國國家標準與技術研究院(NIST)的競賽。在正賽中，本研究群參與的 Rainbow 和 NTRU Prime 打進第三輪，SPHINCS+ 被選為標準。Classic McEliece 則進入第四輪。我們還投稿了兩件競賽補充輪 (Supplementary Round) 的作品， 其中一件是大家看好的 UOV (Unbalanced Oil and Vinegar)。本實驗室的出品除了速度之外，還和形式驗證的研究群合作，我們是最初做出後量子密碼學的中心部件的驗證的團隊。
目前主要計畫
- 院內深耕計畫:刻不容緩的後量子密碼學【楊柏因，2020/01–2024/12】
- 所內合作計畫:Post-Quantum Signature Schemes【倪儒本、楊柏因，2023/01–2025/12】
- 所內合作計畫:Cryptography, a Challenge in the Age of Quantum Computing【楊柏因、鐘楷閔、王柏堯，2021/01–2024/12】
程式語言與形式化方法實驗室
柯向上、穆信成、王柏堯、莊庭瑞、陳郁方
本實驗室致力於發展保證程式正確性之技術。我們在程式語言方面的研究，著重於發展正確程式之語法、語意、及實務上之議題;在形式方法方面的研究，強調分析真實程式中演算法、計算、以及實際方面之課題。我們應用數學及形式技術以探討我們的研究問題，亦致力於發展工具及方法論以幫助程式開發者寫作正確程式。我們在單子 (monadic) 程式的論證與推導，後設程式(metaprograms)的雙模態型別論(bi-modal type theory)設計，泛資料型別程式庫(datatype-generic libraries)，泛資料型別程式庫(datatype-generic libraries)，低階密碼程式 (low-level crypto code) 驗證技術，量子程式自動驗證 (quantum program verification)，和系統程式的形式化驗證 (formal verification of system code) 方面有許多具體成果。這些結果都發表在頂級國際會議，如 PLDI 2023、CHES 2022、ICFP 2022、CSL 2022、 CAV 2021、OSDI 2020。在系統開發方面，我們開發了一個程式設計環境:Guabao，目前已經開始運用於大學課程教學。CryptoLine 為低階密碼學程式驗證工具，他被運用在眾多密碼學實作如 OpenSSL、 BoringSSL、mbed TLS、pqm4、ntt-polymul 的自動化驗證中。
目前主要計畫
- 美商英特爾亞太科技有限公司台灣分公司計畫:快速驗證之後量子軟體【楊柏因、王柏堯，2021/08–2024/07】
- 國科會計畫:基於最弱初始條件與分離邏輯的程式推導與驗證整合環境【穆信成，2022/08–2024/07】
- 國科會計畫:後設編程之型別基礎【柯向上，2020/08–2023/07】
串流式演算法實驗室
蔡孟宗
實驗室的研究主題是:在使用少量空間的前提下，設計演算法解決基礎圖論和幾何問題。我們的計算方式在文獻上被稱為串流式計算，亦即限制演算法只能使用遠少於輸入大小的空間看過輸入很少次來完成計算。 我們近期設計了僅讀取輸入一次的串流式演算法來找尋稀疏生成尤拉子圖、拆解輸入圖成少量無環子圖、近似最少葉生成樹，以及僅讀取輸入幾次的串流式演算法來完成深度及廣度搜尋。這些結果都是該問題目前已知最佳的演算法而且被證明不會遠落後於任何未問世的演算法。我的演算法設計技巧常利用了新設計的稀疏資料概括，可以被用來緩解計算端和存取端之間的資料傳輸壅塞。
目前主要計畫
- 國科會計畫:基礎圖論與幾何問題的串流資料演算法 (II)【蔡孟宗，2020/08–2023/07】
- 所內合作計畫:透過記憶體端之資料概括緩解傳輸壅塞【鄭湘筠、蔡孟宗，2022/01–2023/12】
機器學習實驗室
呂及人
機器學習中一種典型的方法是以批次方式來訓練模型 ( 例如分類器 )。這種方法，首先會收集一組訓練樣本來訓練模型。之後，所學的模型套用在所有未來的資料， 但它永遠保持不變，不再進一步更新。雖然這在許多情境下行得通，但某些其他情況可能就不適用。事實上，這似乎不是人類通常學習的方式。這促使我們研究如何使機器可以用線上的方式學習，只要新資料不斷到來，學習過程就永遠不會停止。首先，我們將幾種廣泛使用的批次演算法成功轉換為線上式的演算法。此外，我們還研究了如何在未知和變化環境中進行重複線上決策的問題。我們找出了一些自然的情境，可以得到更好效能的線上算法。此外，我們也在多個方向上推廣了這個問題，並設計出對應的新演算法。
目前主要計畫
- 國科會計畫:無悔式的終身學習【呂及人，2020/08–2023/07】
資料相關運算實驗室
徐讚昇、廖純中、王大為
本實驗室從事包含下列各項資料相關運算問題研究。 (1)資料集之邏輯與知識表達:資料之中隱藏許多有用的資訊與知識，我們將以形式邏輯的方法來探討相關的知識表徵與推理問題。(2)資料集相關之高速演算法設計:近年來資訊很容易在線上取得。我們研究如何利用這些資料集進行快速計算。研究題目包含傳染性疾病散播模型之快速動態計算理論與演算法組實驗室模擬、疾病網路之建構和視覺化呈現、電腦對局理論和實作。
目前主要計畫
- 國科會計畫:結合深度學習和演算法技巧的棋類盤面難易程度判定及其應用之研究【徐讚昇，2022/ 08–2025/07】
- 國科會計畫:以「神經網路-符號邏輯整合運算」技術建構「人工情感智慧」系統的探索性研究【廖純中，2021/08–2024/07】
- 國科會AI計畫:邁向2030年智慧醫療大健康跨域計畫【王大為，2022/11–2023/10】