PIs: Kai-Min Chung, Yu-Fang Chen, and Hsiang-Shang Ko
The field of quantum computer science has emerged due to the rapid development in quantum computation technology. As many aspects of this interdisciplinary field are still in their infancy, it presents a unique and timely opportunity for researchers to make fundamental contributions, particularly in theoretical aspects.
We are dedicated to making fundamental theoretical contributions in quantum computer science. We bring together diverse expertise: Kai-Min has worked on quantum cryptography for almost a decade, and Yu-Fang and Hsiang-Shang, are both experts in programming language research. Leveraging the collaborative environment at the Institute for Information Industry (IIS), we have been working together on quantum computer science projects for over two years. Our research efforts are supported by a 4-year project on quantum computing from the National Science and Technology Council (NSTC), a 5-year Investigator Award from Academia Sinica, and a collaborative project at IIS. Drawing on our collective expertise, we focus on three main areas: quantum cryptography, quantum program verification, and high-level quantum programming languages. We elaborate on our research in these areas below.
Quantum Cryptography
Quantum cryptography is an interdisciplinary field that seeks to understand the role of quantum power in cryptography, acting as a double-edged sword. On the negative side, Shor's quantum algorithm can break many widely-used computational assumptions, such as factoring, RSA, and decisional Diffie-Hellman (DDH) assumptions, devastating most of the currently deployed public-key cryptography we use today. On the positive side, quantum capabilities enable cryptographic tasks that are impossible classically, such as the recently emerged research on unclonable cryptography (including quantum money, unclonable encryption, and cryptography with certifiable deletion) and computational quantum primitives (like pseudorandom states, one-way state generators, and EFI pairs). Advancements in quantum computation have spurred significant growth in quantum cryptography.
We have worked in this field for nearly a decade, making research contributions to various topics such as post-quantum zero-knowledge proofs, classical verification of quantum computations, secure multiparty quantum computation, and quantum time-space tradeoffs. We have also developed techniques in quantum cryptography to tackle questions in quantum computing and complexity theory. We highlight two of our past research below.
- On the Power of Hybrid Classical and Low-depth Quantum Computation : As near-term quantum computation will likely be restricted to low depth, hybrid computation models combining classical and low-depth quantum computation are essential for capturing the available computation power. In our joint work with Ching-Yi Lai and Nai-Hui Chia (STOC 2020; JACM 2023) [2], we investigated the power of such hybrid models. We developed cryptographic techniques to demonstrate oracle separation between BQP and two types of such hybrid models, proving Aaronson's conjecture and showing that Jozsa's conjecture cannot hold relative to oracles.
- Tight Quantum Time-Space Tradeoffs for Function Inversion: Understanding the hardness of the function inversion problem for inverting a random function with pre-computed advice is a fundamental problem in both cryptography and complexity theory. In joint work with Siyao Guo, Qipeng Liu, and Luowen Qian (FOCS 2020), developed new techniques to show tight quantum time-space tradeoffs for function inversion. Our results showed that the only advantage for quantum inverters is Grover's search algorithm, and quantum advice does not help to speed up Grover's search. We also showed quantum time-space tradeoffs for Yao's problem and salted cryptographic primitives such as collision-resistant hashing and pseudorandom generators.
Moving forward, two potential directions we plan to investigate are black-box separation among recently emerged computational quantum primitives and a new complexity theoretical study of computational problems underlying computational quantum primitives. Quantum cryptography is still a relatively young field. We are excited to continue our exploration with the goal of making fundamental contributions to the field.
Quantum Program Verification
Quantum computers emerged in the 1980s and gained interest after Peter Shor proposed the quantum prime factorization algorithm. Quantum software development is expected to grow, but ensuring its correctness will be challenging. Formal verification can guarantee software compliance with specifications and has a higher potential than testing due to the probabilistic nature of quantum computation. Current quantum formal verification technology is limited by the need for human guidance, lack of flexibility, and limited scale of programs it can handle. This project aims to improve state-of-the-art technologies by proposing two research directions using "automata theory" and " Satisfiability Modulo Theories (SMT)" decision procedures.
Automata theory has been used in computer-aided verification for four decades and has excellent mathematical properties. Recently, we have found that automata can be used to verify quantum circuits by compactly describing a set of binary trees and encoding the semantics of quantum logic gate operations. A quantum program verification algorithm can be developed using tree automata to describe all quantum states that satisfy the preconditions and postconditions, compute the quantum state set, and use the automata language inclusion algorithm to check if any quantum state violates the postcondition. This result will be published in PLDI, a flagship conference in programming language research. We further extended this approach to support the description of relational specifications. The results will be published in CAV, the major conference in formal verification. Our future work aims to expand our approach to support common program structures like loops, develop efficient automata operations and customized simplification algorithms, and explore support for more complex data types like quantum integers.
SMT technology started gaining momentum roughly two decades ago and has since become a widely adopted approach for automating software verification and testing. While SMT technology has not yet been equipped to handle quantum theory, making it challenging to use for the verification or testing of quantum programs. By modifying the existing array theory algorithm, we have discovered a way to incorporate support for quantum theory within SMT. This outcome is presently under review at a major conference.
High-level quantum programming language
Another important topic that we are exploring is high-level quantum programming languages. Most, if not all, of the quantum programming languages proposed so far describe quantum circuits, and are at a low abstraction level. Compared with classical computing, these quantum circuit languages roughly correspond to assembly languages, which are seldom used today; instead, most programmers prefer high-level languages —which provide more abstract and convenient computation models for them to work in— and rely on compilers to bridge the gap between abstract computation models and actual computer architectures. Such linguistic infrastructure remains immature for quantum computing, and should be developed.
We focus in particular on identifying suitable abstractions with which quantum algorithms can be conveniently designed, described, and understood (while making sure that these abstractions can be compiled to quantum circuits for execution). Instead of quantum circuits, quantum algorithm designers mainly rely on the linear-algebraic language inherited from quantum mechanics, but this language is still low-level in the sense that quantum computing concepts are buried beneath obscure and tedious expressions. It would be more desirable to have a high-level language where the quantum computing concepts are succinctly expressed and equipped with convenient reasoning principles.
More specifically, we are exploring the potential of ‘quantum picturalism’ for quantum algorithm design: Quantum picturalism seeks to reformulate quantum theory in a diagrammatic (but mathematically rigorous) language where quantum phenomena are easier to reason about, computational meanings become more explicit, and deep connections with other computation models can be established. With the help of the diagrammatic language, we are gaining new insights into some existing quantum algorithms, which we aim to distill into principles based on which a high-level quantum programming language can eventually be designed.