Research Overview: Toward End-to-End Quantum ApplicationsThis is an exciting yet challenging era for quantum computing. While early-stage quantum computers are now accessible via the cloud, the resources needed to fully realize their potential far exceed current capabilities. Bridging the gap between theory and practice is crucial to translating quantum computing’s theoretical promise into real-world applications. This requires not only advancing quantum hardware but also developing theory for practical quantum applications, efficient and reliable operating/control systems, and intuitive yet effective programming interfaces to enable a full-stack application-oriented co-design to maximize the utility of quantum hardware for practical applications. Research GoalsMy research aims to fill the aforementioned gaps, i.e., provide the foundation of end-to-end quantum applications. To this end, I actively explore the intersection of quantum computing with diverse disciplines, including theoretical computer science, machine learning, control theory, formal methods, programming languages, and computer architecture. This multidisciplinary approach brings fresh (and necessary) perspectives and expertise to advance practical and scalable quantum computing. I deem my holistic software-hardware-algorithmic co-design approach as a unique feature of my research, which has been published in prestigious venues of all relevant fields such as general venues (PNAS, Nature Communication), quantum information (QIP, PRL), programming languages (POPL, PLDI, OOPSLA), machine learning (ICML, NeurIPS, AAAI), security & cryptography (Eurocrypt, CRYTPO, CCS), operations research (INFORMS Journal on Computing), theoretical computer science (STOC, CCC, ICALP), computer networks (ICNP), and signal processing (ICASSP). Hamiltonian-oriented Quantum Algorithm Design and ProgrammingThe conventional design of quantum algorithms is centered around the abstraction of quantum circuits and relies on a digital mindset for application design and implementation. While serving as an elegant mathematical interface, circuit-based digital abstraction usually fails to capture the native programmability of quantum devices, and incurs large overheads, which significantly restricts its near-term feasibility where the computing resource is the major limitation. Historically, circuit-based digital abstraction has been successful in scaling up the design and implementation of modern classical computing chips, however, under the condition of the abundance of computing resources where correctness becomes a major issue for scalability. The benefit of circuit-based digital abstraction for quantum computing is conceivably restrictive when the limitation of quantum computing resources is the major bottleneck in the near term. We hence propose to use quantum Hamiltonian evolution as the central object in end-to-end quantum application design, the so-called Hamiltonian-oriented paradigm, based on the observation that Hamiltonian evolution is a native abstraction for both low-level hardware control and high-level quantum applications. We illustrate that the Hamiltonian-oriented design not only allows more efficient implementation of known quantum algorithms but also inspires novel quantum algorithms, especially in optimization and scientific computing, which are hard to perceive in the circuit model. We also develop a programming infrastructure for easy implementation of Hamiltonian-based quantum applications for domain experts on heterogeneous quantum devices. Quantum Hamiltonian DescentGradient-based methods are important optimization techniques that are prevalent in both theoretical and empirical studies. A genuine quantum counterpart of gradient-based methods is however missing. Inspired by the correspondence between gradient-based methods and physics-inspired dynamical systems, we propose a quantization of such correspondence based on the path integral formulation of quantum mechanics, which in turn implies a quantum extension of gradient descent called the quantum Hamiltonian descent (QHD). We proved QHD’s convergence for any non-convex function with a unique non-degenerate global minimum and observed its faster-converging rate than any classical algorithms and the quantum adiabatic algorithm over a benchmark set of hard instances in non-convex optimization. Excitingly, QHD could be realized on either circuit-based or analog (e.g., quantum simulators) quantum machines for a scalable empirical study. Our finding also opens the possibility of a unified framework for both quantum and classical gradient-based methods. Publications:
Hamiltonian EmbeddingThe realization of quantum computing is fundamentally based on the precise manipulation of Hilbert spaces of underlying quantum devices. The conventional wisdom relies on circuit synthesis techniques to decompose sophisticated operations on Hilbert space to a set of universal elementary gates. Although providing a universal solution in principle, this hardware-agnostic strategy typically leads to deep quantum circuits for interesting quantum algorithms, which makes them infeasible for implementation on near-term quantum devices. We propose a technique named Hamiltonian embedding that simulates a desired Hamiltonian evolution by embedding it into the evolution of a large and structured quantum system, which, however, allows more efficient manipulation via hardware-native operations. We conduct a systematic study of this embedding technique and demonstrate a significant computational resource save for implementing prominent quantum applications. As a result, we can experimentally realize quantum walks on complicated graphs (e.g., binary trees, glued-tree graphs), quantum spatial search, and the simulation of real-space Schrödinger equations on trapped-ion and neutral-atom platforms today. Given the fundamental role of Hamiltonian evolution in quantum algorithm design, our technique significantly expands the horizon of implementable quantum advantage in the NISQ era. Publications:
Differentiable Analog Quantum ComputingWe formulate the first differentiable analog quantum computing framework with a specific parameterization design at the analog signal (pulse) level to better exploit near-term quantum devices via variational methods. We further propose a scalable approach to estimate the gradients of quantum dynamics using a forward pass with Monte Carlo sampling, which leads to a quantum stochastic gradient descent algorithm for scalable gradient-based training in our framework. Applying our framework to quantum optimization and control, we observe a significant advantage of differentiable analog quantum computing against SOTAs based on parameterized digital quantum circuits by orders of magnitude. Publications:
Full-Stack Software & System Co-design for Quantum ApplicationsEnd-to-end quantum application design benefits greatly from a full-stack, open-source, and reconfigurable quantum software system that interfaces seamlessly with domain users and quantum hardware. We demonstrate the feasibility of such a holistic approach and contribute to co-design automation, particularly by addressing challenges like quantum noise and limited system sizes using theoretical insights and machine learning techniques. Domain-specific Abstraction & Programming.A central challenge in programming language design is creating ab- stractions that help developers maximize the potential of target computing devices. To address this for resource-constrained near-term quantum computers, we propose a new quantum programming language, SIMUQ (SIM- Ulation language for Quantum) (POPL’24). Inspired by pioneering languages like FORTRAN and SIMULA, SIMUQ treats Hamiltonian evolution as a fundamental abstraction for quantum computation, a counterpart to floating-point arithmetic in classical, and supports compilation to both gate-based and pulse-programmable quantum backends. It has garnered significant commercial interest, including collaborations with AWS Braket, Mathematica, and Matlab, and was a finalist for the University of Maryland’s Innovation of the Year award. Publications:
Quantum Real-time & Network Systems.In an ongoing project on quantum control systems, we introduce RISC-Q, an open-source generator for system-on-chip (SoC) designs tailored for quantum controllers and compatible with RISC-V. Adopting a software-oriented, agile hardware design approach, RISC-Q provides a high-level, configurable framework for creating custom controllers deployable on FPGA, ASIC, or similar platforms to address diverse quantum control needs. RISC-Q-generated controllers can execute instructions compiled by SIMUQ, together forming a minimal example of a full-stack software for quantum simulation. This is further exemplified by QHDOPT which is built on top of SIMUQ. This integration enables co-design with minimal overhead, enhancing efficiency and adaptability in quantum application development. In another ongoing project, we are developing a programming interface for software-defined quantum networks, inspired by frameworks like Frenetic, along with a holistic simulator to evaluate quantum network protocols at scale. Building on our recent work, QuARC—a clustering-based entanglement routing protocol (ICNP’24) — this project explores the general design space of realistic quantum network protocols to ensure robustness against changes in physical network parameters while sustaining high throughput without starvation. Publications:
Software Foundation of Quantum ComputingFormally 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 accomplished 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:
Quantum 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 the 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:
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:
Variational Quantum MethodsQuantum Neural-networks (i.e., parameterized quantum circuits) are important and promising candidates for applications of quantum machine learning. My research aims to conduct a theory-guided comprehensive investigation in this regard, including functionality (e.g., representation learning, generative models), training methods (e.g., landscape characterization, under/over-parameterization), 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 toward 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. 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:
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 optimize 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 ApplicationsMy pioneering theoretical proposal to decompose large quantum circuits into smaller, manageable circuits for execution on quantum machines has now been adopted as a foundational technique by industry leaders such as IBM and AWS. Now known as “circuit knitting,” this approach is playing a key role in the roadmaps of major companies to scale quantum applications over the next decade.
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 devices leak information to the outside world not just through input-output interaction, but through physical characteristics of computation such as power consumption, timing, and electromagnetic 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 advent of quantum computing has introduced the risk of quantum attacks on modern communication security techniques. Protecting today’s sensitive information from future threats requires deploying robust defenses soon. However, post-quantum security analysis is complex, error-prone, and requires specialized expertise, delaying practical adoption. To address this, I develop formal methods for automated security analysis of cryptographic systems against quantum attacks, automating expert analysis and facilitating deployment. For instance, we extended EasyCrypt to evaluate quantum adversaries (CCS’21) and formally certify NIST’s post-quantum standardization finalists. Notably, during this process, we uncovered a critical flaw in the published security proof of the Dilithium signature scheme (a NIST finalist) and provided a theoretical and certified fix (CRYPTO’23). Publications:
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. Publications:
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:
|