Research Overview: Toward End-to-End Quantum ApplicationsThis is an exciting time for quantum computing! With the availability of prototypes of quantum machines, especially the recently established quantum supremacy and two 53-qubit machines from both Google and IBM, it becomes possible for quantum computing researchers to go beyond purely theoretical studies and to investigate the implementation and actual performance of real-world quantum applications. A paramount goal of quantum computing research is to bridge the gap between theoretical studies and the limitation of real-world QC hardware to achieve end-to-end quantum applications. Research GoalsMy research aims to fill the gap between purely theoretical study of quantum applications and experimental implementation of quantum hardware. In particular, I believe that research on end-to-end applications would benefit from end-to-end thinking. My research aims to identify and contribute to the research where the ideas from computer science in general, i.e., computational thinking, can help facilitate the implementation of end-to-end quantum applications. To that end, my research investigates a broad range of perspectives of quantum computing, including its theoretical foundation and applications, applications and system engineering of near-term quantum devices, the software foundation (programming languages and system) of quantum computing, and the computer-aided design for quantum devices. My research has also been published in prestigious venues of all relevant fields such as quantum information (e.g., QIP), theoretical computer science (e.g., STOC, CCC, ICALP), machine learning (e.g., ICML, NeurIPS, AAAI), and programming languages (e.g., POPL, PLDI). Quantum Applications in Optimization and Machine LearningProvable Quantum Advantages for Optimization and Machine LearningMy recent research aims to understand the landscape of provable quantum advantages in optimization and machine learning, a major targeted domain of quantum applications. To that end, I have developed quantum algorithms with polynomial speed-ups over classical ones for semidefinite programs (SDPs), general convex optimization, training linear and kernelized classifiers, and estimating volumes of high-dimensional convex bodies. My algorithms also hint at possible exponential quantum speed-ups when using quantum data as inputs/outputs of SDPs and the principal component analysis problem. Publications:
Quantum Algorithms for Property TestingAnother well-motivated topic is the property test of quantum and classical distributions. I have closed a long-standing gap between the upper and the lower bound of the sample complexity of testing the whole information of quantum states, so-called quantum tomography, which is a fundamental step to verify the preparation of the experimental setup. I also demonstrated the quantum speed-up in estimating the Shannon and Renyi entropies of classical distributions. Publications:
Variational Quantum Methods and Quantum Neural-NetworksQuantum Neural-networks (i.e., parameterized quantum circuits) are important and promising candidates for applications of quantum machine learning. My research aims to conduct a comprehensive investigation in this regard, including functionality (e.g., representation learning, generative models), training methods (e.g., landscape characterization, the efficiency of gradient and non-gradient based optimization methods), and separation between quantum and classical neural-networks. Publications:
Differentiable Quantum Programming Languages & Quantum Neuro-Symbolic ApplicationsInspired by the emerging paradigm shift from deep learning towards differentiable programming promoted by prominent classical machine learning researchers, I have initiated the formalization of differentiable quantum programming. This project not only provides the auto-differentiation technique for quantum programs, in particular the possibility of using quantum programs to compute the gradients of another quantum program, for the scalability of gradient-based training in quantum machine learning. It also opens the possibility of designing novel quantum “neuro-symbolic” applications that combine program features/synthesis with simple neural-networks. The study of their classical counterpart, although still in its infancy, has already shown great potential and promise over conventional neural-networks. We demonstrated, for the first time, one such example for quantum machine learning.
Software Foundation of Quantum ComputingQuantum Program Analysis & VerificationQuantum programs are error-prone and their verification is challenging due to the limit of standard software assurance techniques in the quantum setting. My research investigates the verification of quantum programs via their static analysis with the help of quantum Hoare logic. A prominent approach for program verification is to generate invariants and inductive assertions, which is already a highly non-trivial task even classically. I made the first proposal of quantum invariants and demonstrated its use in quantum program verification, which can be generated by semidefinite programs (SDPs). We also investigate algebraic reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra. One prominent example of such is the famous Kleene Algebra with Tests (KAT), which has furnished both theoretical insights and practical tools. A few key features of KAT including the idempotent law and the nice properties of classical tests, however, fail to hold in the context of quantum programs due to their unique quantum features, especially in branching. We propose the Non-idempotent Kleena Algebra (NKA) as a natural alternative, and identify complete and sound semantic models for NKA as well as their appropriate quantum interpretations, which hence enables algebraic proofs in NKA of quantum compiler optimization and the normal form of quantum while-programs. Publications:
Formally Verified Software Tool-chain for Quantum ComputingThe complexity of quantum computing and the limitations of near-term quantum devices suggest that the development of sophisticated quantum algorithms and clever optimizations is more likely to have mistakes. This calls for verifying every stage of quantum computation, from the software tools used to generate quantum circuits to the architecture and system design. We are inspired by formal methods applied in safety-critical domains to ensure the correctness of code by construction, especially in the example of CompCert (a C compiler written and proved correct in Coq) and the NSF project of deep specification (a project to develop specifications of software toolchains to prove end-to-end correctness of whole systems). A verified quantum computing stack would ensure that each level of quantum computation is implemented satisfying certain specifications and the correctness of the final system, which would have a wide practical impact. This approach is especially appealing to quantum computing since alternative software assurance techniques are very limited due to the substantial expense involved in the quantum setting. As an important first step, we have built a proved-correct optimizing compiler for quantum algorithms to optimize the gate count, the depth of circuits, etc., while adhering to any architectural constraints. To that end, we developed an infrastructure for reasoning about quantum programs/operations in Coq, which is so expressive and flexible that we recently accomplish an end-to-end implementation of Shor's algorithm, with both classical and quantum parts as well as a formal correctness proof of everything, in Coq. Publications:
Design of Quantum Programming LanguagesQuantum circuits, which are simple to understand, have served as the main description language for most quantum applications so far. However, there are also many challenges and limitations when using quantum circuits as the only description language of quantum applications both in theory and in practice. We are inspired to investigate the more appropriate abstractions as well as the language design built on top of these abstractions for various quantum applications, such as variational quantum algorithms and quantum simulation. We are also working on the formulation of useful classical semantic constructs, e.g., recursion and abstract data types, in the context of quantum programming languages. Quantum Architecture Engineering for NISQ eraNear-term quantum computers are likely to have very restricted hardware resources, where precisely controllable qubits are expensive, error-prone, and scarce. Therefore, application designers for such near-term intermediate-size quantum (NISQ) computers are forced to investigate the best balance of trade-offs among a large number of (potentially heterogeneous) factors specific to the targeted application and quantum hardware. Noise-Analysis of Quantum ApplicationsWe believe that one way to attack these problems is to set aside a one-size-fits-all approach to fault tolerance and instead consider elevating the question of errors and related architecture-specific resource optimization to the level of the programming language and algorithm design. In particular, inspired by techniques in approximate computing that optimizes computation on unreliable classical hardware, we've built formal semantics and a logic for reasoning about reliability in the presence of noise in quantum computation. Publications:
Meta-Programming Framework for Automating NISQ Application DesignWe propose Meta Quantum Circuits with Constraints (MQCC), a meta-programming framework for quantum programs, to assist the balance of trade-offs in NISQ application design. Designers express their application as a succinct collection of normal quantum circuits stitched together by a set of meta-level choice variables, whose values are constrained according to a programmable set of quantitative optimization criteria. MQCC?s compiler automatically generates the appropriate constraints, hands them to a solver (e.g., a Satisfiability Modulo Theories (SMT) solver), and from the solution produces an optimized, runnable program. We demonstrate MQCC's expressiveness through an extensive case study, demonstrating that ideas from previous examples of NISQ application design – such as multi-programming, cost-effective uncomputation, and crosstalk mitigation, as well as their combination – can be readily implemented in MQCC, and produce comparable results. Publications:
Leveraging Small Quantum Machines for NISQ ApplicationsTo accelerate NISQ quantum applications on small quantum machines, we designed a systematic framework of decomposing quantum computation into small pieces and then combining simulation results from each piece for the final output. A particular application is, e.g., a practical scheme to implement a 60-qubit quantum computation with only 45-qubit quantum machines.
Treating NISQ Machines as Analog MachinesRecent research results suggest a promising approach to designing resource-efficient NISQ applications by breaking high-level abstractions, such as quantum circuits, and directly compiling applications to the pulse-level control of quantum machines. This approach essentially treats near-term quantum computers as analog quantum machines. We are inspired to identify qualitative/quantitative advantages of treating near-term quantum computers as analog quantum machines. To that end, we will investigate the robustness and the interpretability of the generated control pulses, as well as the scalability of variational algorithms generating these pulses. Moreover, we aim to study the optimal pulse-control-inspired ansatz design for variational quantum methods, as well as their implementation based on the pulse-level, rather than the gate-level, compilation. Cryptography & Security in the Quantum RegimeTamper-resilient Cryptography under Physical AssumptionsDevices, classical or quantum, are subject to tampering in cryptographic settings, especially due to the proliferation of side-channel attacks. These attacks exploit the fact that de- vices leak information to the outside world not just through input-output interaction, but through physical characteristics of computation such as power consumption, timing, and electro-magnetic radiation. Research on this topic explores two possible solutions to protect cryptographic systems from (quantum) side-channel attacks.
Both device-independent and leakage-resilient cryptography can be deemed as tamper-resilient cryptography under physical assumptions. My future plan is to bring these cryptographic designs closer to practice, with better efficiency and broader functionality. Publications:
(Practical) Delegation and Verification of Quantum ComputationIn a recent breakthrough, Mahadev constructed a classical verification of quantum computation (CVQC) protocol for a classical client to delegate decision problems in BQP to an untrusted quantum prover under computational assumptions. We explore further the feasibility of CVQC with the more general sampling problems in BQP and with the desirable blindness property, and contribute affirmative solutions to both. We also investigate the lightweight verification of quantum supremacy, where all existing protocols, either based on classical simulation or public-key quantum cryptography, are too expensive to serve the purpose of practical verification. We propose a circuit-obfuscation-based verification scheme for quantum supremacy that is scalable and has some complexity-theoretic support based on the quantum minimum equivalent circuit problem (QMECP). We also implement a prototype of our circuit obfuscator which has the desired empirical performance against the attack from all the off-the-shelf tools. Publications:
Mechanized and Automated Security Analysis of Cryptographic Systems under Quantum AttacksThe emergence of quantum computing technology has promised unprecedented improvement in our computational ability, which, however, also leads to quantum attacks that would put many security techniques for modern communication in peril in the not-too-distant future. The defense against quantum attacks should ideally be deployed in the near future to protect today's secret information from future quantum attacks, especially in security-critical domains like hardware signatures or block-chains, both with very long life cycles. Inspired by the success of the development of formal methods in the security analysis for large, real-world cryptographic systems, we are excited to develop and apply formal method techniques in quantum cryptography for automated security analysis of cryptographic systems under quantum attacks. Formally generated security analysis will provide not only efficient and high assurance proofs that can replace the tedious and error-prone analysis for experts, but also independently verifiable proofs that can be used by security practitioners without much quantum knowledge. One of our ultimate goals is to formally verify candidates of cryptographic systems from the NIST quantum-secure cryptography standardization. Computer-aided Design of Quantum DevicesThe design complexity/productivity of quantum devices will conceivably significantly increase as the quantum devices become more complicated. A lot of existing quantum devices are relatively small, and their design is mostly done by manual analysis. Achieving this requires leading experts on this topic, and is usually is time-consuming, and error-prone. Scaling up this approach for slightly larger or more complicated quantum devices seems very challenging, and less effective. A natural candidate to replace human manual design is computer-aided design. Inspired by the success of classical hardware description languages (HDLs) as an integral part of electronic design automation (EDA) systems, we are inspired to develop quantum HDL (QHDL) for the design of quantum devices. To that end, we will develop formal abstractions of various experimental platforms for quantum devices (e.g., superconducting qubits, neutral atoms), building on top of which we will develop design automation, automatic control generation, and formal verification. We will also directly link the precise description of quantum devices to the high-level quantum programming languages on the software developer's side, which will enable a hardware-software co-design framework for quantum applications. Quantum Sensing NetworksThe demand for highly accurate position and time information, provided by localization and synchronization methods, respectively, is growing rapidly. However, classical localization and synchronization methods are approaching their limits. Utilizing quantum properties promises to push these boundaries beyond classical limitations and provide unprecedented accuracy. We aim to develop theoretical and practical methodologies for the design and analysis of quantum localization and synchronization networks. These methodologies consist of statistical models and distributed algorithms to harness quantum phenomena for beyond-classical localization and synchronization. Earlier Theoretical Studies in Quantum Information and ComputationEntanglement, Quantum Correlations, and Sum-of-SquaresResearch on this topic studies many aspects of one of the key quantum features, entanglement and non-locality. I attack this topic by exploring a surprising connection between quantum information and the sum-of-squares (SOS) proof in approximation algorithms and the famous Unique Games Conjecture (UGC). This connection allows one to leverage technical advances in one field to apply to the other. Specific problems that I am working on include the characterization of separable (unentangled) states, the complexity of quantum Merlin-Arthur games with unentangled provers (QMA(2)), the possibility of a quantum-inspired approach to attack the UGC. Publications:
Quantum Computational ComplexityInteractive proof systems have been a central model in complexity theory with applications ranging from the PCP theorem in the hardness of approximation to cryptography. It studies problems with efficiently verifiable proofs via interactions between a polynomial-time verifier and all-powerful provers, where the verifier determines the validity of the proofs. My main contribution on this topic is the development of the Equilibrium Value Method to obtain space-efficient simulations of quantum interactive proof systems, including QIP=PSPACE, QRG(2)=PSPACE. Recently, I have been working on the quantum variant of the PCP theorem in the interactive proof setting. As a concrete first step, I have obtained a parallel repetition result for entangled k-player games. Publications:
|