Institute of Information Science, Academia Sinica

Quantum Computer Science Lab

Kai-Min Chung, Yu-Fang Chen, and Hsiang-Shang Ko

Our laboratory is dedicated to theoretical research in the interdisciplinary field of quantum computer science. Our main research areas include quantum cryptography, quantum program verification, and high-level quantum programming languages. We have been working on quantum cryptography for many years and made significant progress in several topics such as post-quantum zero-knowledge proofs, classical verification of quantum computations, secure multiparty quantum computation, and quantum time-space tradeoffs. We also developed techniques in quantum cryptography to answer questions in quantum computing and complexity theory. Our research published in STOC 2020 answered two conjectures proposed by Scott Aaronson and Richard Jozsa in 2005 regarding the computational power of low-depth quantum computation and classical computation hybrid models. Our results confirmed Aaronson's conjecture and gave a negative answer to Jozsa's conjecture relative to an oracle model.

In the field of quantum program verification, we have been working diligently to explore new research directions and address the limitations of existing technology. Two specific areas of focus have been automata theory and satisfiability modulo theories (SMT). To simplify the description of quantum states and process quantum logic gates, we have utilized tree automata. Through this work, we have established a framework for the automatic verification of quantum software, which combines automata theory and verification of quantum circuits. We are excited to share our progress and findings at PLDI 2023. Additionally, we have developed a quantum theory for SMT, which we hope will contribute to advancements in the field of quantum program verification. This result is currently under review at a major conference. We are optimistic about the potential impact of this project on the field of quantum software and verification.

In the area of high-level quantum programming languages, we are exploring the potential of quantum in quantum algorithm design in the hope of identifying principles that lead to a new generation of high-level quantum programming languages.

Ongoing Projects

• Investigator Award: Theoretical Exploration in Quantum Cryptography【Kai-Min Chung, 2021/01–2025/12】
• NSTC(Taiwan Quantum Program): Theoretical Development in Quantum Computer Science 【Kai-Min Chung, Bo-Ying Yang, Yu-Fang Chen, 2022/03–2023/02】
• NSTC: Theoretical Challenges and Opportunities in Post-Quantum Cryptography【Kai-Min Chung, 2020/07–2023/08】
• Air Force Defense Research Sciences Program (USA): Secure Multiparty Quantum Computation 【Kai-Min Chung, 2020/08–2023/09)
• IIS Project: Towards a high-level quantum-algorithmic programming language 【Hsiang-Shang Ko, Kai-Min Chung, 2023/01–2024/12】

Post-Quantum Crypto Lab

Bo-Yin Yang, Ruben Falko Niederhagen, Bow-Yaw Wang, and Kai-Min Chung

This laboratory is dedicated to the theoretical and practical research of cryptography that can survive the emergence of quantum computers. Our main research directions are post-quantum cryptography theory, implementation and verification. We have been working in the field of post-quantum cryptography for many years. Since 2021, we have several papers on the use of Fast Fourier Transform and Number Theoretic Transform (NTT) in the implementation of lattice cryptography. Due to our expertise on NTT, many state-of-the-art implementations in post-quantum cryptography are from our lab.

The lab has also participated in numerous entrants to the National Institute of Standards and Technology (NIST) competition. In the main competition, Rainbow and NTRU Prime (both participated by our research group advanced to the third round, and Classic McEliece advanced to the fourth round. SPHINCS+ did better and was selected as one of the future standards. We also submitted two works for the Supplementary Round of the NIST competition, one of which is the UOV (Unbalanced Oil and Vinegar) that everyone is optimistic about.

TIn addition to high speed, the lab's products also cooperate with the formal verification research group and produced the first verification of a central component of an important post-quantum cryptography primitive (the Number Theoretic Transform).

Ongoing Projects

• Investigator Award: Post-Quantum Cryptography Today【Bo-Yin Yang, 2020/01–2024/12】
• IIS Corporation Project: Post-Quantum Signature Schemes【Ruben Falko Niederhagen, Bo-Ying Yang, 2023/01–2025/12】
• IIS Corporation Project: Cryptography, a Challenge in the Age of Quantum Computing 【Bo-Ying Yang, Kai-Min Chung, Bo-Yao Wang, 2021/01–2024/12】

Programming Language and Formal Methods Lab

Hsiang-Shang Ko, Tyng-Ruey Chuang, Bow-Yaw Wang, Shin-Cheng Mu, and Yu-Fang Chen

Our laboratory is dedicated to developing technologies to ensure the correctness of programs. Our research in programming languages focuses on the grammatical, semantic, and practical issues of developing correct programs; our research in formal methods emphasizes the analysis of algorithmic, computational, and practical issues in real programs. We apply mathematical and formal techniques to explore our research questions, and we strive to develop tools and methodologies to help programmers write correct programs. We made a series of contributions in the reasoning about monadic programs, typed metaprogramming, low-level crypto code verification, quantum program verification, and formal verification of system code. These results were published in top international conferences, such as PLDI 2023, CHES 2022, ICFP 2022, CSL 2022, CAV 2021, and OSDI 2020. We have developed a programming environment: Guabao, which has already begun to be used in university course teaching. CryptoLine is a low-level cryptographic program verification tool. It automatically verifies many cryptographic implementations such as OpenSSL, BoringSSL, mbed TLS, pqm4, and ntt-polymul.

Ongoing Projects

• Intel project: Fast verified post-quantum software 【Bo-Yin Wang, Bow-Yaw Wang, 2021/08–2024/07】
• NSTC project: An Integrated Environment for Program Derivation and Verification Based on Weakest Precondition and Separation Logic 【Shin-Chung Mu, 2022/08–2024/07】
• Metaprogramming【Hsiang-Shang Ko,2020/ 08–2023/07】

Streaming Algorithm Lab

Meng-Tsung Tsai

The main research area of our lab is to devise space-efficient algorithms to solve fundamental graph and geometry problems. Our model of computation is known as the streaming model, in which algorithms are allowed to access the input in few passes using space sublinear in the input size. Our recent results include single-pass streaming algorithms for finding sparse spanning eulerian subgraphs, partitioning graphs into few forests, approximating min-leaf spanning trees, and few-pass streaming algorithms for computing the standard BFS and DFS trees. These results are known best and proven to be nearly optimal. Our techniques involve the new design of sparse certificates, which can be used to mitigate the data congestion between storage and computation units during computations.

Ongoing Projects

• INSTC project: Streaming Algorithms for Fundamental Graph and Geometry Problems (II) 【Meng-Tsung Tsai, 2020/08–2023/07】
• IIS Cooperation project: Mitigating Data Congestion by Sketching in Memory 【Hsiang-Yun Cheng and Meng-Tsung Tsai, 2022/01–2023/12】

Machine Learning Lab

Chi-Jen Lu

A common practice in machine learning is to learn a model (e.g., a classifier) in a batch way, in which one first collects a set of training examples and then learns a model from this training set. Afterwards, the learned model is used for all future testing data, but it remains fixed without being further updated. While this is sufficient for many scenarios, it may not work well for others. In fact, this does not seem to be the way we humans usually learn. This motivates us to study how to make machines learn in an online fashion, in which the learning process never stops as long as new data keeps arriving. For this, we first took several widely used batch algorithms and transformed them to work in the online setting. Moreover, we studied the general problem of making repeated online decisions in unknown and changing environments. We identified natural scenarios in which better online algorithms can be designed, and we extended the scope of the problem in several directions and developed new algorithms correspondingly.

Ongoing Projects

• NSTC project: Lifelong Learning with No Regret 【Chi-Jen Lu, 2020/08–2023/07】

Data-Centric Computing Lab

Tsan-sheng Hsu, Churn-Jung Liau, and Da-Wei Wang

Our Lab focuses on treating problems arising from data sets with common themes, including the following two topics. (1) Logics for Data Sets with Common Themes: Considerable amounts of information and knowledge are implicit in data sets with common themes. We intend to study the problems of knowledge representation and reasoning in data science using formal logic. With proper representation frameworks and logical formalisms, knowledge discovered from massive data can be used in data-intensive intelligent systems. (2) Efficient Data-Intensive Algorithms: With the rapid development of computer and communication technology, it has become much easier to access and store massive amounts of electronic data sets with common themes. We are interested in the research problems concerning efficient computation of these data sets, which include efficient epidemic simulation, visualization and construction of disease networks, and classical computer games.

Ongoing Projects

• NSTC project: Assessing level of difficulties for board game positions by integrating deep learning and algorithmic techniques and its applications【Tsan-sheng Hsu, 2022/08–2025/07】
• NSTC project: An Exploring Study on Building Affective Artificial Intelligence by Neural-Symbolic Computing【Churn-Jung Liau, 2021/08–2024/07】