Research Overview: Toward End-to-End Quantum Applications

This is an exciting time for quantum computing where early-stage quantum computers become available at your fingertips through clouds. Conventional computer science study of quantum computing has focused on its algorithm and complexity perspective. While providing insights into its power and limits in the asymptotic regime, this kind of theoretical study fails to capture the opportunities and restrictions of realistic quantum machines or to address the challenges in building efficient and reliable systems that operate them.

Research Goals

My research aims to identify and fill these gaps, accompanying hardware development, for the actual deployment of practical end-to-end quantum applications, i.e., provide the foundation of end-to-end quantum applications. To that end, I am integrating ideas from the study of theoretical computer science, machine learning, formal methods, programming languages, and computer architecture with decades of research on quantum information. I deem this 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 (e.g., PNAS), quantum information (e.g., QIP, Phys.Rev.Lett), programming languages (e.g., POPL, PLDI, OOPSLA), machine learning (e.g., ICML, NeurIPS, AAAI), cryptography and security (e.g., CCS, Crypto, EuroCrypt), and theoretical computer science (e.g., STOC, CCC, ICALP). An overview of my existing research and future plans is as follows.

Hamiltonian-oriented Quantum Algorithm Design and Programming

The 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 Descent

Gradient-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.


  • Quantum Hamiltonian Descent. Jiaqi Leng, Ethan Hickman, Joseph Li, and Xiaodi Wu. Manuscript, 2023. (website)

  • A Quantum-Classical Performance Separation in Nonconvex Optimization. Jiaqi Leng, Yufan Zheng, and Xiaodi Wu. Manuscript, 2023.

  • QHDOPT: A Software for Nonlinear Optimization with Quantum Hamiltonian Decent. Samuel Kushnir, Jiaqi Leng, Yuxiang Peng, Lei Fan, and Xiaodi Wu. Manuscript 2024. Github

Hamiltonian Embedding

The 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.


  • Expanding hardware-efficiently manipulable Hilbert space by Hamiltonian embedding. Jiaqi Leng, Joseph Li, Yuxiang Peng, and Xiaodi Wu. Manuscript 2024. Available at 2401.08550.

Differentiable Analog Quantum Computing

We 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.


  • Differentiable Analog Quantum Computing for Optimization and Control. Jiaqi Leng, Yuxiang Peng, Yi-Ling Qiao, Ming Lin, and Xiaodi Wu. NeurIPS 2022.

Hamiltonian-oriented Programming Infrastructure

Classical analog computing, with a relaxed requirement on hardware, predates digital computers and has played an important role in many domain applications. Conceivably, applications based on analog quantum machines will become a major milestone for near-term quantum computing. However, programming analog quantum simulators is much more challenging due to the lack of a unified interface between hardware and software. To remedy the situation, we have built a domain-specific modeling language for quantum simulation (called SIMUQ) inspired by the pioneering work of Simula, which allows the description of quantum evolution itself beyond any circuit-based model. The new abstraction provides structured information about the actual physics to simulate and allows more automation and optimization by compilers. More importantly, it also enables analog compilation to heterogeneous analog quantum simulators on various experimental platforms. Specifically, in SimuQ, front-end users specify the target quantum system with Hamiltonian Modeling Language, and the Hamiltonian-level programmability of analog quantum simulators is specified through a new abstraction called the abstract analog instruction set (AAIS) and programmed in AAIS Specification Language by hardware providers. Building on top of SIMUQ, we plan to develop DSLs for domain applications, such as the simulation of high-energy physics & condensed physics, and analog computational tasks.


  • SimuQ: A Domain-Specific Language For Quantum Simulation With Analog Compilation. Yuxiang Peng, Jacob Young, Pengyu Liu, and Xiaodi Wu. POPL 2024. Website

Software Foundation of Quantum Computing

Formally Verified Software Tool-chain for Quantum Computing

The 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.


  • A Formally Certified End-to-End Implementation of Shor's Factorization Algorithm. Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, and Xiaodi Wu. Proceedings of the National Academy of Sciences, 2023. Available at arXiv:2204.07112. GitHub

  • Verified Compilation of Quantum Oracles. Liyi Li, Finnegan S Voichick, Kesha Hietala, Yuxiang Peng, Xiaodi Wu, and Michael Hicks. OOPSLA 2022. Available at arXiv:2112.06700.

  • A Verified Optimizer for Quantum Circuits. Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. Distinguished Paper at POPL 2021. (GitHub).

  • Verified Optimization in a Quantum Intermediate Representation. Kesha Hietala, Robert Rand, Shih-Han Hung, Xiaodi Wu, and Michael Hicks. Extended Abstract at QPL 2019. Available at arXiv:1904.06319.

Quantum Program Analysis & Verification

Quantum 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.


  • Qafny: Quantum Program Verification Through Type-guided Classical Separation Logic. Liyi Li, Mingwei Zhu, Rance Cleaveland, Yi Lee, Le Chang, and Xiaodi Wu. Manuscript 2022. Available at arXiv:2211.06411.

  • Algebraic Reasoning of Quantum Programs via Non-Idempotent Kleene Algebra. Yuxiang Peng, Mingsheng Ying, and Xiaodi Wu. PLDI 2022. Available at arXiv:2110.07018

  • On the Theory and Practice of Invariant-based Verification of Quantum Programs. Shih-han Hung, Yuxiang Peng, Xin Wang, Shaopeng Zhu, and Xiaodi Wu. Manuscript, 2019.

  • Invariants of Quantum Programs: Characterizations and Generation. Mingsheng Ying, Shenggang Ying, and Xiaodi Wu. POPL 2017.

Quantum Applications in Optimization and Machine Learning

Provable Quantum Advantages for Optimization and Machine Learning

My 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.


  • Sublinear Classical and Quantum Algorithms for General Matrix Games. Tongyang Li, Chunhao Wang, Shouvanik Chakrabarti, Xiaodi Wu. Appeared at the 35th AAAI Conference on Artificial Intelligence (AAAI 2021).

  • Quantum algorithm for volume estimation of convex bodies. Shouvanik Chakrabarti, Andrew Childs, Shih-han Hung, Tongyang Li, Chunhao Wang, and Xiaodi Wu. QIP 2020. arXiv:1908.03903.

  • Sublinear quantum algorithms for training linear and kernel-based classifiers. Tongyang Li, Shouvanik Chakrabarti, and Xiaodi Wu. In the proceedings of the 36th International Conference on Machine Learning (ICML 2019). Also available at arXiv:1904.02276.

  • Quantum SDP Solvers: Large Speed-ups, Optimality, and Applications to Quantum Learning. Fernando G. S. L. Brandao, Amir Kalev, Tongyang Li, Cedric Yen-Yu Lin, Krysta M. Svore, and Xiaodi Wu. arXiv: 1710.02581v2. QIP 2019. ICALP 2019.

  • Quantum algorithms and lower bounds for convex optimization. Shouvanik Chakrabarti, Andrew M. Childs, Tongyang Li, and Xiaodi Wu. arXiv: 1809.01731. QIP 2019.

Variational Quantum Methods

Quantum 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.


  • A Convergence Theory for Over-parameterized Variational Quantum Eigensolvers. Xuchen You, Shouvanik Chakrabarti, and Xiaodi Wu. QIP 2023. ArXiv:2205.12481

  • Analyzing Convergence in Quantum Neural Networks: Deviations from Neural Tangent Kernels. Xuchen You, Shouvanik Chakrabarti, Boyang Chen, and Xiaodi Wu. ICML 2023.

  • Two-way Separations in Expressivity between Quantum Neural Networks and Feed-forward ReLU Networks. Shouvanik Chakrabarti and Xiaodi Wu. manuscript, 2021.

  • Exponentially Many Local Minima in Shallow Quantum Neural Networks. Xuchen You and Xiaodi Wu. In the Proceedings of the 38th International Conference on Machine Learning (ICML 2021).

  • Quantum Wasserstein Generative Adversarial Networks. Shouvanik Chakrabarti, Yiming Huang, Tongyang Li, Soheil Feizi, and Xiaodi Wu. In the Proceedings of the 33rd Annual Conference on Neural Information Processing Systems (NeurIPS 2019).

Differentiable Quantum Programming Languages & Quantum Neuro-Symbolic Applications

Inspired 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.


  • Differentiable Quantum Programming with Unbounded Loops. Wang Fang, Mingsheng Ying and Xiaodi Wu. ACM Transactions on Software Engineering and Methodology, 2023.

  • Differentiable Analog Quantum Computing for Optimization and Control. Jiaqi Leng, Yuxiang Peng, Yi-Ling Qiao, Ming Lin, and Xiaodi Wu. NeurIPS 2022.

  • On the Principles of Differentiable Quantum Programming Languages. Shaopeng Zhu, Shih-han Hung, Shouvanik Chakrabarti, and Xiaodi Wu. In the Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2020).

Quantum Algorithms for Property Testing

Another 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.


  • Quantum query complexity of entropy estimation. Tongyang Li and Xiaodi Wu. IEEE Transaction on Information Theory, Vol. 65, Issue 5, pages 2899 - 2921, May 2019. arXiv: 1710.06025.

  • Sample-optimal tomography of quantum states. Jeongwan Haah, Aram W. Harrow, Zhengfeng Ji, Xiaodi Wu, Nengkun Yu. QIP 2016 and STOC 2016.

Quantum Architecture Engineering for NISQ era

Near-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 Applications

We 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.


  • Quantitative Robustness Analysis of Quantum Programs. Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, and Xiaodi Wu. POPL 2019.

Meta-Programming Framework for Automating NISQ Application Design

We 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.


  • Automating NISQ Application Design with Meta Quantum Circuits with Constraints (MQCC). Haowei Deng, Yuxiang Peng, Michael Hicks, and Xiaodi Wu. ACM Transaction on Quantum Computing. Github

Leveraging Small Quantum Machines for NISQ Applications

To 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.

  • Simulating large quantum circuits on a small quantum computer. Tianyi Peng, Aram Harrow, Maris Ozols, and Xiaodi Wu. Physical Review Letters 125, 150504. Available at arXiv:1904.00102.

Cryptography & Security in the Quantum Regime

Tamper-resilient Cryptography under Physical Assumptions

Devices, 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 electromagnetic radiation. Research on this topic explores two possible solutions to protect cryptographic systems from (quantum) side-channel attacks.

  • Device-independent Cryptography: In this setting, none of the devices can be a priori trusted: security is based solely on simple tests performed by honest users on the input-output behavior of their devices. The security analysis guarantees that any set of devices meeting reasonable physical assumptions (e.g., spatial separations of devices that prohibit mutual communication) and conducting an acceptable interaction will lead to a secure outcome, regardless of the actual process inside the devices. My research focuses on generating uniform random bits in this setting under minimal assumptions. Check the recent review in Nature (Certified randomness in quantum physics) about this research direction and my work.

  • Leakage-resilient Cryptography: Modern computing environment, such as cloud computing where computation no longer takes place on private machines under our control, makes a lot of classical cryptographic systems victims to all kinds of side-channel attacks. The leakage can be quantum. Collecting and storing quantum side information is technically much less challenging than building fully-fledged quantum computers, and could become realistic in the near future. My research focuses on studying the role of quantum side information in both information-theoretical and computational settings. In a recent result, I initiated the study of computational notions of entropy in the quantum setting and developed the first quantum leakage-resilient cryptographic protocol.

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.


  • Computational Notions of Quantum Min-Entropy. Yi-Hsiu Chen, Kai-Min Chung, Ching-Yi Lai, Salil P. Vadhan, and Xiaodi Wu. QCrypt 2017. arXiv: 1704.07309.

  • General randomness amplification with non-signaling security. Kai-Min Chung, Yaoyun Shi, and Xiaodi Wu. QIP 2017.

  • Multi-Source Randomness Extractors Against Quantum Side Information, and their Applications. Kai-Min Chung, Xin Li, and Xiaodi Wu. arXiv:1411.2315.

  • Physical Randomness Extractors. Kai-Min Chung, Yaoyun Shi, and Xiaodi Wu. Plenary talk at QIP 2014.

(Practical) Delegation and Verification of Quantum Computation

In 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.


  • A Scalable Classical Verification reveals the Gap of the State-Of-The-Art Gaussian Boson Sampling Experiments. Yufan Zheng, Yingkang Cao, and Xiaodi Wu. Manuscript, 2022

  • Constant-round Blind Classical Verification of Quantum Sampling. Kai-Min Chung, Yi Lee, Han-Hsuan Lin, and Xiaodi Wu. Eurocrypt, 2022.

  • Scalable Verification of Quantum Supremacy based on Circuit Obfuscation. Shouvanik Chakrabarti, Chi-Ning Chou, Kai-Min Chung, and Xiaodi Wu. Manuscript, 2022.

Mechanized and Automated Security Analysis of Cryptographic Systems under Quantum Attacks

The 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.


  • Fixing and Mechanizing the Security Proof of Fiat-Shamir with Aborts and Dilithium. Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, Yu-Hsuan Huang, Andreas Hülsing, Yi Lee, Xiaodi Wu. CRYPTO 2023.

  • EasyPQC: Verifying Post-Quantum Cryptography. Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Gregoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu, and Li Zhou. CCS 2021.

Computer-aided Design of Quantum Devices

Existing quantum devices are relatively small, and their design is mostly done manually, which requires domain experts, and is usually time-consuming, and error-prone. Scaling up this approach for slightly larger or more complicated quantum devices seems very challenging. A natural alternative is to enable the computer-aided design of quantum devices or even let the design bootstrap on existing quantum devices. We are motivated to develop quantum hardware description languages (QHDL) inspired by classical hardware description languages. To that end, we will develop formal abstractions of various quantum experimental platforms, building on top of which we will develop design automation, automatic control generation, and formal verification. Some of our ongoing efforts include (1) the extension of SPICE to support circuit QED for super-conducting qubits, the simulation of which will be delegated to SimuQ, and in turn, enables a quantum-aided design of quantum devices; (2) the automatic generation of machine specifications in AAIS for the analog compilation in SimuQ. By exposing quantum hardware specifications to high-level quantum programming languages, we will build a hardware-software co-design framework for quantum applications.

Quantum Sensing Networks

The 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.


  • Distributed Quantum Sensing Network with Geographically Constrained Measurement Strategies. Yingkang Cao and Xiaodi Wu. IEEE International Conference on Acoustics, Speech and Signal Processing 2023.

Earlier Theoretical Studies in Quantum Information and Computation

Entanglement, Quantum Correlations, and Sum-of-Squares

Research 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.


  • Limitations of semidefinite programs for separable states and entangled games. Aram Harrow, Anand Natarajan, Xiaodi Wu. QIP 2017. Communications in Mathematical Physics, Volume 366, Issue 2, pp 423–468, 2019.

  • Tight SoS-degree bounds for approximate Nash equilibria. Aram Harrow, Anand Natarajan, Xiaodi Wu. CCC 2016.

  • An improved semidefinite programming hierarchy for testing entanglement. Aram Harrow, Anand Natarajan, Xiaodi Wu. Communications in Mathematical Physics, June 2017, Volume 352, Issue 3, pp 881– 904.

  • Epsilon-net method for optimizations over separable states. Yaoyun Shi and Xiaodi Wu. QIP 2012, ICALP 2012. Theoretical Computer Science, Volume 598, Pages 51–63.

Quantum Computational Complexity

Interactive 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.


  • Parallel repetition for entangled k-player games via fast quantum search. Kai-Min Chung, Xiaodi Wu and Henry Yuen. CCC 2015.

  • Epsilon-net method for optimizations over separable states. Yaoyun Shi and Xiaodi Wu. QIP 2012, ICALP 2012. Theoretical Computer Science, Volume 598, Pages 51-63.

  • Parallel approximation of min-max problems with applications to classical and quantum zero-sum games Gus Gutoski and Xiaodi Wu. QIP 2012, CCC 2012. Computational Complexity, 22(2):385-428, 2013, the special issue of CCC 2012.

  • Equilibrium Value Method for the proof of QIP=PSPACE. Xiaodi Wu . arXiv:1004.0264.