EDBT 2026 Demo / reviewers in the wild / expert
Xiaodi Wu 0001
dblp:66/8037-1
· DBLP profile ↗
39ranked-venue papers
1as first author
24since 2021 · last 2025
0000-0001-8877-9802ORCID · verified
Domains — the database's venue-derived domains; a paper can count in several
Theory of computation · 14 · 1 first-author · 4 since 2021Software engineering, systems software and programming languages · 11 · 8 since 2021Artificial intelligence and machine learning · 7 · 5 since 2021Security and privacy · 3 · 3 since 2021Systems, architecture and hardware · 2 · 2 since 2021Graphics, computer vision, multimedia, augmented reality and games · 2 · 2 since 2021Computer networks · 1 · 1 since 2021
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2025 | QHDOPT: A Software for Nonlinear Optimization with Quantum Hamiltonian DescentabstractWe develop an open-source, end-to-end software (named QHDOPT), which can solve nonlinear optimization problems using the quantum Hamiltonian descent (QHD) algorithm. QHDOPT offers an accessible interface and automatically maps tasks to various supported quantum backends (i.e., quantum hardware machines). These features enable users, even those without prior knowledge or experience in quantum computing, to utilize the power of existing quantum devices for nonlinear and nonconvex optimization tasks. In its intermediate compilation layer, QHDOPT employs SimuQ, an efficient interface for Hamiltonian-oriented programming, to facilitate multiple algorithmic specifications and ensure compatible cross-hardware deployment. The detailed documentation of QHDOPT is available at https://github.com/jiaqileng/QHDOPT . History: Accepted by Giacomo Nannicini, Area Editor for Quantum Computing and Operations Research. Accepted for Special Issue. Funding: This work was supported by the U.S. Department of Energy’s Advanced Research Projects Agency–Energy [Grant DE-SC0020273], the Alfred P. Sloan Foundation, the Simons Foundation [Simons Investigator Award 825053], the Simons Quantum Postdoctoral Fellowship, the National Science Foundation [Grants CCF-1816695, CCF-1942837, and ECCS-2045978], the Unitary Fund, and the Air Force Office of Scientific Research [Grant FA95502110051]. Supplemental Material: The software that supports the findings of this study is available within the paper and its Supplemental Information ( https://pubsonline.informs.org/doi/suppl/10.1287/ijoc.2024.0587 ) as well as from the IJOC GitHub software repository ( https://github.com/INFORMSJoC/2024.0587 ). The complete IJOC Software and Data Repository is available at https://informsjoc.github.io/ . Samuel Kushnir, Jiaqi Leng 0001, Yuxiang Peng 0004, Lei Fan 0006, Xiaodi Wu 0001 |
INFORMS J. Comput. | 5 |
| 2024 | Qafny: A Quantum-Program VerifierabstractBecause of the probabilistic/nondeterministic behavior of quantum programs, it is highly advisable to verify them formally to ensure that they correctly implement their specifications. Formal verification, however, also traditionally requires significant effort. To address this challenge, we present Qafny, an automated proof system based on the program verifier Dafny and designed for verifying quantum programs. At its core, Qafny uses a type-guided quantum proof system that translates quantum operations to classical array operations modeled within a classical separation logic framework. We prove the soundness and completeness of our proof system and implement a prototype compiler that transforms Qafny programs and specifications into Dafny for automated verification purposes. We then illustrate the utility of Qafny's automated capabilities in efficiently verifying important quantum algorithms, including quantum-walk algorithms, Grover's algorithm, and Shor's algorithm. Liyi Li 0002, Mingwei Zhu, Rance Cleaveland, Alexander Nicolellis, Yi Lee, Xiaodi Wu 0001 |
ECOOP | 7 |
| 2024 | Efficient Routing on Quantum Networks Using Adaptive ClusteringabstractWe introduce QuARC, Quantum Adaptive Routing using Clusters, a novel clustering-based entanglement routing protocol that leverages redundant, multi-path routing through multi-particle projective quantum measurements to enable high-throughput, low-overhead, starvation-free entanglement distribution. At its core, QuARC periodically reconfigures the underlying quantum network into clusters of different sizes, where each cluster acts as a small network that distributes entanglement across itself, and the end-to-end entanglement is established by further distributing between clusters. QuARC does not require a-priori knowledge of any physical parameters, and is able to adapt the network configuration using static topology information, and using local (within-cluster) measurements only. We present a comprehensive simulation-based evaluation that shows QuARC is robust against changes to physical network parameters, and maintains high throughput without starvation even as network sizes scale and physical parameters degrade. Connor Clayton, Xiaodi Wu 0001, Bobby Bhattacharjee |
ICNP | 2 |
| 2024 | Differentiable Quantum Computing for Large-scale Linear ControlabstractAs industrial models and designs grow increasingly complex, the demand for optimal control of large-scale dynamical systems has significantly increased. However, traditional methods for optimal control incur significant overhead as problem dimensions grow. In this paper, we introduce an end-to-end quantum algorithm for linear-quadratic control with provable speedups. Our algorithm, based on a policy gradient method, incorporates a novel quantum subroutine for solving the matrix Lyapunov equation. Specifically, we build a *quantum-assisted differentiable simulator* for efficient gradient estimation that is more accurate and robust than classical methods relying on stochastic approximation. Compared to the classical approaches, our method achieves a *super-quadratic* speedup. To the best of our knowledge, this is the first end-to-end quantum application to linear control problems with provable quantum advantage. Connor Clayton, Jiaqi Leng 0001, Gengzhi Yang, Yi-Ling Qiao, Ming C. Lin, Xiaodi Wu 0001 |
NeurIPS | 6 |
| 2024 | Quantum-centric supercomputing for materials science: A perspective on challenges and future directions
Yuri Alexeev, Maximilian Amsler, Marco Antonio Barroca, Sanzio Bassini, Torey Battelle, Daan Camps, David Casanova, Young Jay Choi, Fred Chong, Charles Chung, Christopher Codella, Antonio D. Córcoles, James Cruise, Alberto Di Meglio, Ivan Duran, Thomas Eckl, Sophia E. Economou, Stephan J. Eidenbenz, Bruce Elmegreen, Clyde Fare, Ismael Faro, Cristina Sanz Fernández, Rodrigo Neumann Barros Ferreira, Keisuke Fuji, Bryce Fuller, Laura Gagliardi, Giulia Galli, Jennifer R. Glick, Isacco Gobbi, Pranav Gokhale, Salvador de la Puente Gonzalez, Johannes Greiner, William Gropp, Michele Grossi, Emanuel Gull, Burns Healy, Matthew R. Hermes, Benchen Huang, Travis S. Humble, Nobuyasu Ito, Artur F. Izmaylov, Ali Javadi-Abhari, Douglas M. Jennewein, Shantenu Jha, Bert de Jong, Petar Jurcevic, William M. Kirby, Stefan Kister, Masahiro Kitagawa, Joel Klassen, Katherine Klymko, Kwangwon Koh, Masaaki Kondo, Doga Murat Kürkçüoglu, Krzysztof Kurowski, Teodoro Laino, Ryan Landfield, Matthew L. Leininger, Vicente Leyton-Ortega, Ang Li 0006, Meifeng Lin, Junyu Liu, Nicolás Lorente, André Luckow, Simon Martiel, Francisco Martín-Fernández, Margaret Martonosi, Claire Marvinney, Arcesio Castañeda Medina, Dirk Merten, Antonio Mezzacapo, Kristel Michielsen, Abhishek Mitra, Tushar Mittal, Kyungsun Moon, Joel Moore, Sarah Mostame, Mario Motta, Young-Hye Na, Yunseong Nam, Prineha Narang, Yu-ya Ohnishi, Daniele Ottaviani, Matthew Otten, Scott Pakin, Vincent R. Pascuzzi, Edwin Pednault, Tomasz Piontek, Jed W. Pitera, Patrick Rall, Gokul Subramanian Ravi, Niall Robertson, Matteo A. C. Rossi, Piotr Rydlichowski, Hoon Ryu, Georgy Samsonidze, Mitsuhisa Sato, Nishant Saurabh, Kunal Sharma, Soyoung Shin, George Slessman, Mathias Steiner, Iskandar Sitdikov, In-Saeng Suh, Eric D. Switzer, Joel Thompson, Synge Todo, Minh C. Tran, Dimitar Trenev, Christian Trott, Huan-Hsin Tseng, Norm M. Tubman, Esin Tureci, David García Valiñas, Sofia Vallecorsa, Christopher Wever, Konrad W. Wojciechowski, Xiaodi Wu 0001, Shinjae Yoo, Nobuyuki Yoshioka, Victor Wen-zhe Yu, Seiji Yunoki, Sergiy Zhuk, Dmitry Zubarev |
Future Gener. Comput. Syst. | 122 |
| 2024 | A Case for Synthesis of Recursive Quantum Unitary ProgramsabstractQuantum programs are notoriously difficult to code and verify due to unintuitive quantum knowledge associated with quantum programming. Automated tools relieving the tedium and errors associated with low-level quantum details would hence be highly desirable. In this paper, we initiate the study of program synthesis for quantum unitary programs that recursively define a family of unitary circuits for different input sizes, which are widely used in existing quantum programming languages. Specifically, we present QSynth, the first quantum program synthesis framework, including a new inductive quantum programming language, its specification, a sound logic for reasoning, and an encoding of the reasoning procedure into SMT instances. By leveraging existing SMT solvers, QSynth successfully synthesizes 10 quantum unitary programs including quantum arithmetic programs, quantum eigenvalue inversion, quantum teleportation and Quantum Fourier Transformation, which can be readily transpiled to executable programs on major quantum platforms, e.g., Q#, IBM Qiskit, and AWS Braket. Haowei Deng, Runzhou Tao 0001, Yuxiang Peng 0004, Xiaodi Wu 0001 |
Proc. ACM Program. Lang. | 4 |
| 2024 | SimuQ: A Framework for Programming Quantum Hamiltonian Simulation with Analog CompilationabstractQuantum Hamiltonian simulation, which simulates the evolution of quantum systems and probes quantum phenomena, is one of the most promising applications of quantum computing. Recent experimental results suggest that Hamiltonian-oriented analog quantum simulation would be advantageous over circuit-oriented digital quantum simulation in the Noisy Intermediate-Scale Quantum (NISQ) machine era. However, programming analog quantum simulators is much more challenging due to the lack of a unified interface between hardware and software. In this paper, we design and implement SimuQ, the first framework for quantum Hamiltonian simulation that supports Hamiltonian programming and pulse-level compilation to heterogeneous analog quantum simulators. 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. Through a solver-based compilation, SimuQ generates executable pulse schedules for real devices to simulate the evolution of desired quantum systems, which is demonstrated on superconducting (IBM), neutral-atom (QuEra), and trapped-ion (IonQ) quantum devices. Moreover, we demonstrate the advantages of exposing the Hamiltonian-level programmability of devices with native operations or interaction-based gates and establish a small benchmark of quantum simulation to evaluate SimuQ’s compiler with the above analog quantum simulators. Yuxiang Peng 0004, Jacob Young, Xiaodi Wu 0001 |
Proc. ACM Program. Lang. | 4 |
| 2024 | Differentiable Quantum Programming with Unbounded LoopsabstractThe emergence of variational quantum applications has led to the development of automatic differentiation techniques in quantum computing. Existing work has formulated differentiable quantum programming with bounded loops, providing a framework for scalable gradient calculation by quantum means for training quantum variational applications. However, promising parameterized quantum applications, e.g., quantum walk and unitary implementation, cannot be trained in the existing framework due to the natural involvement of unbounded loops. To fill in the gap, we provide the first differentiable quantum programming framework with unbounded loops, including a newly designed differentiation rule, code transformation, and their correctness proof. Technically, we introduce a randomized estimator for derivatives to deal with the infinite sum in the differentiation of unbounded loops, whose applicability in classical and probabilistic programming is also discussed. We implement our framework with Python and Q# and demonstrate a reasonable sample efficiency. Through extensive case studies, we showcase an exciting application of our framework in automatically identifying close-to-optimal parameters for several parameterized quantum applications. Wang Fang 0001, Mingsheng Ying, Xiaodi Wu 0001 |
ACM Trans. Softw. Eng. Methodol. | 3 |
| 2023 | 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 0003, Andreas Hülsing, Yi Lee, Xiaodi Wu 0001 |
CRYPTO (5) | 10 |
| 2023 | Distributed Quantum Sensing Network with Geographically Constrained Measurement StrategiesabstractDistributed quantum sensing network has the potential of enhancing the precision in estimating a global function of local parameters by utilizing an entangled probe, compared with that achieved with separable probes. This advantage is often characterized as a quadratic improvement of the quantum Cramér-Rao bound (QCRB). This argument is incomplete in that QCRB assumes a team of all-powerful sensors that can perform arbitrary joint measurements allowed by quantum mechanics. An immediate question arises as to whether such an advantage persists for isolated sensors with physically motivated constraints in their measurement strategies. In this paper, we first consider local operations and classical communication (LOCC) strategies and prove that the QCRB is indeed asymptotically attainable for arbitrary pure probe states, by extending previous work on single-parameter estimation [1]. We further numerically analyze a more restricted scenario where the sensors can only make independent local measurements, and provide evidence that the QCRB is not informative enough for comparing different probe states. Yingkang Cao, Xiaodi Wu 0001 |
ICASSP | 2 |
| 2023 | Analyzing Convergence in Quantum Neural Networks: Deviations from Neural Tangent KernelsabstractA quantum neural network (QNN) is a parameterized mapping efficiently implementable on near-term Noisy Intermediate-Scale Quantum (NISQ) computers. It can be used for supervised learning when combined with classical gradient-based optimizers. Despite the existing empirical and theoretical investigations, the convergence of QNN training is not fully understood. Inspired by the success of the neural tangent kernels (NTKs) in probing into the dynamics of classical neural networks, a recent line of works proposes to study over-parameterized QNNs by examining a quantum version of tangent kernels. In this work, we study the dynamics of QNNs and show that contrary to popular belief it is qualitatively different from that of any kernel regression: due to the unitarity of quantum operations, there is a non-negligible deviation from the tangent kernel regression derived at the random initialization. As a result of the deviation, we prove the at-most sublinear convergence for QNNs with Pauli measurements, which is beyond the explanatory power of any kernel regression dynamics. We then present the actual dynamics of QNNs in the limit of over-parameterization. The new dynamics capture the change of convergence rate during training and implies that the range of measurements is crucial to the fast QNN convergence. Xuchen You, Shouvanik Chakrabarti, Xiaodi Wu 0001 |
ICML | 4 |
| 2023 | A Verified Optimizer for Quantum CircuitsabstractWe present voqc , the first verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called sqir , a small quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of sqir programs. sqir programs denote complex-valued matrices, as is standard in quantum computation, but we treat matrices symbolically to reason about programs that use an arbitrary number of quantum bits. sqir ’s careful design and our provided automation make it possible to write and verify a broad range of optimizations in voqc , including full-circuit transformations from cutting-edge optimizers. Kesha Hietala, Robert Rand 0001, Liyi Li 0002, Shih-Han Hung, Xiaodi Wu 0001, Michael Hicks 0001 |
ACM Trans. Program. Lang. Syst. | 5 |
| 2023 | Quantum Algorithm for Estimating Volumes of Convex BodiesabstractEstimating the volume of a convex body is a central problem in convex geometry and can be viewed as a continuous version of counting. We present a quantum algorithm that estimates the volume of an n -dimensional convex body within multiplicative error ε using Õ(n 3 + n 2.5 /ε ) queries to a membership oracle and Õ(n 5 +n 4.5 /ε) additional arithmetic operations. For comparison, the best known classical algorithm uses Õ(n 3.5 +n 3 /ε 2 ) queries and Õ(n 5.5 +n 5 /ε 2 ) additional arithmetic operations. To the best of our knowledge, this is the first quantum speedup for volume estimation. Our algorithm is based on a refined framework for speeding up simulated annealing algorithms that might be of independent interest. This framework applies in the setting of “Chebyshev cooling,” where the solution is expressed as a telescoping product of ratios, each having bounded variance. We develop several novel techniques when implementing our framework, including a theory of continuous-space quantum walks with rigorous bounds on discretization error. To complement our quantum algorithms, we also prove that volume estimation requires Ω (√ n+1/ε) quantum membership queries, which rules out the possibility of exponential quantum speedup in n and shows optimality of our algorithm in 1/ε up to poly-logarithmic factors. Shouvanik Chakrabarti, Andrew M. Childs, Shih-Han Hung, Tongyang Li, Chunhao Wang, Xiaodi Wu 0001 |
ACM Trans. Quantum Comput. | 6 |
| 2023 | Automating NISQ Application Design with Meta Quantum Circuits with Constraints (MQCC)abstractNear-term intermediate scale quantum (NISQ) computers are likely to have very restricted hardware resources, where precisely controllable qubits are expensive, error-prone, and scarce. Programmers of such computers must therefore balance trade-offs among a large number of (potentially heterogeneous) factors specific to the targeted application and quantum hardware. To assist them, we propose Meta Quantum Circuits with Constraints (MQCC) , a meta-programming framework for quantum programs. Programmers express their application as a succinct collection of normal quantum circuits stitched together by a set of (manually or automatically) added meta-level choice variables, whose values are constrained according to a programmable set of quantitative optimization criteria. MQCC’s compiler generates the appropriate constraints and solves them via an SMT solver, producing an optimized, runnable program. We showcase a few MQCC’s applications for its generality including an automatic generation of efficient error syndrome extraction schemes for fault-tolerant quantum error correction with heterogeneous qubits and an approach to writing approximate quantum Fourier transformation and quantum phase estimation that smoothly trades off accuracy and resource use. We also illustrate that MQCC can easily encode prior one-off NISQ application designs- –multi-programming (MP) , crosstalk mitigation (CM) —as well as a combination of their optimization goals (i.e., a combined MP-CM). Haowei Deng, Yuxiang Peng 0004, Michael Hicks 0001, Xiaodi Wu 0001 |
ACM Trans. Quantum Comput. | 4 |
| 2022 | Constant-Round Blind Classical Verification of Quantum Sampling
Kai-Min Chung, Yi Lee, Han-Hsuan Lin, Xiaodi Wu 0001 |
EUROCRYPT (3) | 4 |
| 2022 | Differentiable Analog Quantum Computing for Optimization and ControlabstractWe formulate the first differentiable analog quantum computing framework with 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 {\em orders of magnitude}. Jiaqi Leng 0001, Yuxiang Peng 0004, Yi-Ling Qiao, Ming C. Lin, Xiaodi Wu 0001 |
NeurIPS | 5 |
| 2022 | Algebraic reasoning of Quantum programs via non-idempotent Kleene algebraabstractWe 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. The succinctness of algebraic reasoning would be especially desirable for scalable analysis of quantum programs, given the involvement of exponential-size matrices in most of the existing methods. 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 Non-idempotent Kleene Algebra (NKA) as a natural alternative and identify complete and sound semantic models for NKA as well as their quantum interpretations. In light of applications of KAT, we demonstrate algebraic proofs in NKA of quantum compiler optimization and the normal form of quantum while-programs. Moreover, we extend NKA with Tests (i.e., NKAT), where tests model quantum predicates following effect algebra, and illustrate how to encode propositional quantum Hoare logic as NKAT theorems. Yuxiang Peng 0004, Mingsheng Ying, Xiaodi Wu 0001 |
PLDI | 3 |
| 2022 | Verified compilation of Quantum oraclesabstractQuantum algorithms often apply classical operations, such as arithmetic or predicate checks, over a quantum superposition of classical data; these so-called oracles are often the largest components of a quantum program. To ease the construction of efficient, correct oracle functions, this paper presents VQO, a high-assurance framework implemented with the Coq proof assistant. The core of VQO is OQASM, the oracle quantum assembly language. OQASM operations move qubits between two different bases via the quantum Fourier transform, thus admitting important optimizations, but without inducing entanglement and the exponential blowup that comes with it. OQASM’s design enabled us to prove correct VQO’s compilers—from a simple imperative language called OQIMP to OQASM, and from OQASM to SQIR, a general-purpose quantum assembly language—and allowed us to efficiently test properties of OQASM programs using the QuickChick property-based testing framework. We have used VQO to implement a variety of arithmetic and geometric operators that are building blocks for important oracles, including those used in Shor’s and Grover’s algorithms. We found that VQO’s QFT-based arithmetic oracles require fewer qubits, sometimes substantially fewer, than those constructed using “classical” gates; VQO’s versions of the latter were nevertheless on par with or better than (in terms of both qubit and gate counts) oracles produced by Quipper, a state-of-the-art but unverified quantum programming platform. Liyi Li 0002, Finn Voichick, Kesha Hietala, Yuxiang Peng 0004, Xiaodi Wu 0001, Michael Hicks 0001 |
Proc. ACM Program. Lang. | 5 |
| 2021 | Sublinear Classical and Quantum Algorithms for General Matrix GamesabstractWe investigate sublinear classical and quantum algorithms for matrix games, a fundamental problem in optimization and machine learning, with provable guarantees. Given a matrix, sublinear algorithms for the matrix game were previously known only for two special cases: (1) the maximizing vectors live in the L1-norm unit ball, and (2) the minimizing vectors live in either the L1- or the L2-norm unit ball. We give a sublinear classical algorithm that can interpolate smoothly between these two cases: for any fixed q between 1 and 2, we solve, within some additive error, matrix games where the minimizing vectors are in an Lq-norm unit ball. We also provide a corresponding sublinear quantum algorithm that solves the same task with a quadratic improvement in dimensions of the maximizing and minimizing vectors. Both our classical and quantum algorithms are optimal in the dimension parameters up to poly-logarithmic factors. Finally, we propose sublinear classical and quantum algorithms for the approximate Carathéodory problem and the Lq-margin support vector machines as applications. Tongyang Li, Chunhao Wang, Shouvanik Chakrabarti, Xiaodi Wu 0001 |
AAAI | 4 |
| 2021 | EasyPQC: Verifying Post-Quantum CryptographyabstractEasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical at- tackers, which means that post-quantum security proofs cannot be formalized and machine-checked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of post-quantum cryptography proofs, settling a question raised by (Unruh, POPL 2019). Leveraging our positive result, we implement EasyPQC, an extension of EasyCrypt for post-quantum security proofs, and use EasyPQC to verify post- quantum security of three classic constructions: PRF-based MAC, Full Domain Hash and GPV08 identity-based encryption. Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Grégoire, Shih-Han Hung, Jonathan Katz, Pierre-Yves Strub, Xiaodi Wu 0001, Li Zhou 0013 |
CCS | 8 |
| 2021 | ICCAD Special Session Paper: Quantum Variational Methods for Quantum ApplicationsabstractQuantum Variational Methods are promising near-term applications of quantum machines, not only because of their potential advantages in solving certain computational tasks and understanding quantum physics but also because of their feasibility on near-term quantum machines. However, many challenges remain in order to unleash the full potential of quantum variational methods, especially in the design of efficient training methods for each domain-specific quantum variational ansatzes. This paper proposes a theory-guided principle in order to tackle the training issue of quantum variational methods and highlights some successful examples. Shouvanik Chakrabarti, Xuchen You, Xiaodi Wu 0001 |
ICCAD | 3 |
| 2021 | Exponentially Many Local Minima in Quantum Neural NetworksabstractQuantum Neural Networks (QNNs), or the so-called variational quantum circuits, are important quantum applications both because of their similar promises as classical neural networks and because of the feasibility of their implementation on near-term intermediate-size noisy quantum machines (NISQ). However, the training task of QNNs is challenging and much less understood. We conduct a quantitative investigation on the landscape of loss functions of QNNs and identify a class of simple yet extremely hard QNN instances for training. Specifically, we show for typical under-parameterized QNNs, there exists a dataset that induces a loss function with the number of spurious local minima depending exponentially on the number of parameters. Moreover, we show the optimality of our construction by providing an almost matching upper bound on such dependence. While local minima in classical neural networks are due to non-linear activations, in quantum neural networks local minima appear as a result of the quantum interference phenomenon. Finally, we empirically confirm that our constructions can indeed be hard instances in practice with typical gradient-based optimizers, which demonstrates the practical value of our findings. Xuchen You, Xiaodi Wu 0001 |
ICML | 2 |
| 2021 | A verified optimizer for Quantum circuitsabstractWe present VOQC, the first fully verified optimizer for quantum circuits, written using the Coq proof assistant. Quantum circuits are expressed as programs in a simple, low-level language called SQIR, a simple quantum intermediate representation, which is deeply embedded in Coq. Optimizations and other transformations are expressed as Coq functions, which are proved correct with respect to a semantics of SQIR programs. SQIR uses a semantics of matrices of complex numbers, which is the standard for quantum computation, but treats matrices symbolically in order to reason about programs that use an arbitrary number of quantum bits. SQIR's careful design and our provided automation make it possible to write and verify a broad range of optimizations in VOQC, including full-circuit transformations from cutting-edge optimizers. Kesha Hietala, Robert Rand 0001, Shih-Han Hung, Xiaodi Wu 0001, Michael Hicks 0001 |
Proc. ACM Program. Lang. | 4 |
| 2021 | Introduction to the Special issue on the Techniques of Programming Languages, Logic, and Formal Methods in Quantum Computingabstractintroduction Share on Introduction to the Special issue on the Techniques of Programming Languages, Logic, and Formal Methods in Quantum Computing Editor: Xiaodi Wu Department of Computer Science and Institute for Advanced Computer Studies, Joint Center for Quantum Information and Computer Science, University of Maryland, College Park Department of Computer Science and Institute for Advanced Computer Studies, Joint Center for Quantum Information and Computer Science, University of Maryland, College ParkView Profile Authors Info & Claims ACM Transactions on Quantum ComputingVolume 2Issue 4December 2021 Article No.: 15pp 1–3https://doi.org/10.1145/3488389Online:21 December 2021Publication History 0citation81DownloadsMetricsTotal Citations0Total Downloads81Last 12 Months81Last 6 weeks3 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access Xiaodi Wu 0001 |
ACM Trans. Quantum Comput. | 1 |
| 2020 | On the principles of differentiable quantum programming languagesabstractVariational Quantum Circuits (VQCs), or the so-called quantum neural-networks, are predicted to be one of the most important near-term quantum applications, not only because of their similar promises as classical neural-networks, but also because of their feasibility on near-term noisy intermediate-size quantum (NISQ) machines. The need for gradient information in the training procedure of VQC applications has stimulated the development of auto-differentiation techniques for quantum circuits. We propose the first formalization of this technique, not only in the context of quantum circuits but also for imperative quantum programs (e.g., with controls), inspired by the success of differentiable programming languages in classical machine learning. In particular, we overcome a few unique difficulties caused by exotic quantum features (such as quantum no-cloning) and provide a rigorous formulation of differentiation applied to bounded-loop imperative quantum programs, its code-transformation rules, as well as a sound logic to reason about their correctness. Moreover, we have implemented our code transformation in OCaml and demonstrated the resource-efficiency of our scheme both analytically and empirically. We also conduct a case study of training a VQC instance with controls, which shows the advantage of our scheme over existing auto-differentiation for quantum circuits without controls. Shaopeng Zhu, Shih-Han Hung, Shouvanik Chakrabarti, Xiaodi Wu 0001 |
PLDI | 4 |
| 2019 | Quantum SDP Solvers: Large Speed-Ups, Optimality, and Applications to Quantum LearningabstractWe give two new quantum algorithms for solving semidefinite programs (SDPs) providing quantum speed-ups. We consider SDP instances with m constraint matrices, each of dimension n, rank at most r, and sparsity s. The first algorithm assumes an input model where one is given access to an oracle to the entries of the matrices at unit cost. We show that it has run time O~(s^2 (sqrt{m} epsilon^{-10} + sqrt{n} epsilon^{-12})), with epsilon the error of the solution. This gives an optimal dependence in terms of m, n and quadratic improvement over previous quantum algorithms (when m ~~ n). The second algorithm assumes a fully quantum input model in which the input matrices are given as quantum states. We show that its run time is O~(sqrt{m}+poly(r))*poly(log m,log n,B,epsilon^{-1}), with B an upper bound on the trace-norm of all input matrices. In particular the complexity depends only polylogarithmically in n and polynomially in r. We apply the second SDP solver to learn a good description of a quantum state with respect to a set of measurements: Given m measurements and a supply of copies of an unknown state rho with rank at most r, we show we can find in time sqrt{m}*poly(log m,log n,r,epsilon^{-1}) a description of the state as a quantum circuit preparing a density matrix which has the same expectation values as rho on the m measurements, up to error epsilon. The density matrix obtained is an approximation to the maximum entropy state consistent with the measurement data considered in Jaynes' principle from statistical mechanics. As in previous work, we obtain our algorithm by "quantizing" classical SDP solvers based on the matrix multiplicative weight update method. One of our main technical contributions is a quantum Gibbs state sampler for low-rank Hamiltonians, given quantum states encoding these Hamiltonians, with a poly-logarithmic dependence on its dimension, which is based on ideas developed in quantum principal component analysis. We also develop a "fast" quantum OR lemma with a quadratic improvement in gate complexity over the construction of Harrow et al. [Harrow et al., 2017]. We believe both techniques might be of independent interest. Fernando G. S. L. Brandão, Amir Kalev, Tongyang Li, Cedric Yen-Yu Lin, Krysta M. Svore, Xiaodi Wu 0001 |
ICALP | 6 |
| 2019 | Sublinear quantum algorithms for training linear and kernel-based classifiersabstractWe investigate quantum algorithms for classification, a fundamental problem in machine learning, with provable guarantees. Given $n$ $d$-dimensional data points, the state-of-the-art (and optimal) classical algorithm for training classifiers with constant margin by Clarkson et al. runs in $\tilde{O}(n +d)$, which is also optimal in its input/output model. We design sublinear quantum algorithms for the same task running in $\tilde{O}(\sqrt{n} +\sqrt{d})$, a quadratic improvement in both $n$ and $d$. Moreover, our algorithms use the standard quantization of the classical input and generate the same classical output, suggesting minimal overheads when used as subroutines for end-to-end applications. We also demonstrate a tight lower bound (up to poly-log factors) and discuss the possibility of implementation on near-term quantum machines. Tongyang Li, Shouvanik Chakrabarti, Xiaodi Wu 0001 |
ICML | 3 |
| 2019 | Quantum Wasserstein Generative Adversarial NetworksabstractThe study of quantum generative models is well-motivated, not only because of its importance in quantum machine learning and quantum chemistry but also because of the perspective of its implementation on near-term quantum machines. Inspired by previous studies on the adversarial training of classical and quantum generative models, we propose the first design of quantum Wasserstein Generative Adversarial Networks (WGANs), which has been shown to improve the robustness and the scalability of the adversarial training of quantum generative models even on noisy quantum hardware. Specifically, we propose a definition of the Wasserstein semimetric between quantum data, which inherits a few key theoretical merits of its classical counterpart. We also demonstrate how to turn the quantum Wasserstein semimetric into a concrete design of quantum WGANs that can be efficiently implemented on quantum machines. Our numerical study, via classical simulation of quantum systems, shows the more robust and scalable numerical performance of our quantum WGANs over other quantum GAN proposals. As a surprising application, our quantum WGAN has been used to generate a 3-qubit quantum circuit of ~50 gates that well approximates a 3-qubit 1-d Hamiltonian simulation circuit that requires over 10k gates using standard techniques. Shouvanik Chakrabarti, Tongyang Li, Soheil Feizi, Xiaodi Wu 0001 |
NeurIPS | 5 |
| 2019 | Quantitative robustness analysis of quantum programsabstractQuantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major challenge in quantum programming is dealing with errors (quantum noise) during execution. Because quantum resources (e.g., qubits) are scarce, classical error correction techniques applied at the level of the architecture are currently cost-prohibitive. But while this reality means that quantum programs are almost certain to have errors, there as yet exists no principled means to reason about erroneous behavior. This paper attempts to fill this gap by developing a semantics for erroneous quantum while-programs, as well as a logic for reasoning about them. This logic permits proving a property we have identified, called є-robustness, which characterizes possible “distance” between an ideal program and an erroneous one. We have proved the logic sound, and showed its utility on several case studies, notably: (1) analyzing the robustness of noisy versions of the quantum Bernoulli factory (QBF) and quantum walk (QW); (2) demonstrating the (in)effectiveness of different error correction schemes on single-qubit errors; and (3) analyzing the robustness of a fault-tolerant version of QBF. Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks 0001, Xiaodi Wu 0001 |
Proc. ACM Program. Lang. | 6 |
| 2019 | Quantum Query Complexity of Entropy EstimationabstractEstimation of Shannon and Rényi entropies of unknown discrete distributions is a fundamental problem in statistical property testing. In this paper, we give the first quantum algorithms for estimating α-Rényi entropies (Shannon entropy being 1-Rényi entropy). In particular, we demonstrate a quadratic quantum speedup for Shannon entropy estimation and a generic quantum speedup for α-Rényi entropy estimation for all α ≥ 0 values, including tight bounds for the Shannon entropy, the Hartley entropy (α = 0), and the collision entropy (α = 2). We also provide quantum upper bounds for estimating min-entropy (α = +∞) as well as the Kullback-Leibler divergence. We complement our results with quantum lower bounds on α-Rényi entropy estimation for all α ≥ 0 values. Our approach is inspired by the pioneering work of Bravyi, Harrow, and Hassidim (BHH); however, with many new technical ingredients: 1) we improve the error dependence of the BHH framework by a fine-tuned error analysis together with Montanaro's approach to estimating the expected output of quantum subroutines for α = 0, 1; 2) we develop a procedure, similar to cooling schedules in simulated annealing, for general α ≥ 0, and 3) in the cases of integer α ≥ 2 and α = +∞, we reduce the entropy estimation problem to the α-distinctness and [log n]-distinctness problems, respectively. Tongyang Li, Xiaodi Wu 0001 |
IEEE Trans. Inf. Theory | 2 |
| 2017 | Invariants of quantum programs: characterisations and generationabstractProgram invariant is a fundamental notion widely used in program verification and analysis. The aim of this paper is twofold: (i) find an appropriate definition of invariants for quantum programs; and (ii) develop an effective technique of invariant generation for verification and analysis of quantum programs. Mingsheng Ying, Shenggang Ying, Xiaodi Wu 0001 |
POPL | 3 |
| 2017 | Sample-Optimal Tomography of Quantum StatesabstractIt is a fundamental problem to decide how many copies of an unknown mixed quantum state are necessary and sufficient to determine the state. Previously, it was known only that estimating states to error ε in trace distance required O(dr2/ε2) copies for a d-dimensional density matrix of rank r. Here, we give a theoretical measurement scheme (POVM) that requires O(dr/δ)ln (d/δ) copies to estimate ρ to error δ in infidelity, and a matching lower bound up to logarithmic factors. This implies O((dr/ε2)ln (d/ε)) copies suffice to achieve error ε in trace distance. We also prove that for independent (product) measurements, Ω(dr2/δ2)/ ln(1/δ) copies are necessary in order to achieve error δ in infidelity. For fixed d, our measurement can be implemented on a quantum computer in time polynomial in n. Jeongwan Haah, Aram W. Harrow, Zheng-Feng Ji, Xiaodi Wu 0001, Nengkun Yu |
IEEE Trans. Inf. Theory | 4 |
| 2016 | Tight SoS-Degree Bounds for Approximate Nash EquilibriaabstractNash equilibria always exist, but are widely conjectured to require time to find that is exponential in the number of strategies, even for two-player games. By contrast, a simple quasi-polynomial time algorithm, due to Lipton, Markakis and Mehta (LMM), can find approximate Nash equilibria, in which no player can improve their utility by more than epsilon by changing their strategy. The LMM algorithm can also be used to find an approximate Nash equilibrium with near-maximal total welfare. Matching hardness results for this optimization problem re found assuming the hardness of the planted-clique problem (by Hazan and Krauthgamer) and assuming the Exponential Time Hypothesis (by Braverman, Ko and Weinstein). In this paper we consider the application of the sum-squares (SoS) algorithm from convex optimization to the problem of optimizing over Nash equilibria. We show the first unconditional lower bounds on the number of levels of SoS needed to achieve a constant factor approximation to this problem. While it may seem that Nash equilibria do not naturally lend themselves to convex optimization, we also describe a simple LP (linear programming) hierarchy that can find an approximate Nash equilibrium in time comparable to that of the LMM algorithm, although neither algorithm is obviously a generalization of the other. This LP can be viewed as arising from the SoS algorithm at log(n) levels - matching our lower bounds. The lower bounds involve a modification of the Braverman-Ko-Weinstein embedding of CSPs into strategic games and techniques from sum-of-squares proof systems. The upper bound (i.e. analysis of the LP) uses information-theory techniques that have been recently applied to other linear- and semidefinite-programming hierarchies. Aram W. Harrow, Anand Natarajan 0001, Xiaodi Wu 0001 |
CCC | 3 |
| 2016 | Sample-optimal tomography of quantum statesabstractIt is a fundamental problem to decide how many copies of an unknown mixed quantum state are necessary and sufficient to determine the state. This is the quantum analogue of the problem of estimating a probability distribution given some number of samples. Jeongwan Haah, Aram W. Harrow, Zheng-Feng Ji, Xiaodi Wu 0001, Nengkun Yu |
STOC | 4 |
| 2015 | Parallel Repetition for Entangled k-player Games via Fast Quantum SearchabstractWe present two parallel repetition theorems for the entangled value of multi-player, one-round free games (games where the inputs come from a product distribution). Our first theorem shows that for a $k$-player free game $G$ with entangled value $\mathrm{val}^*(G) = 1 - ε$, the $n$-fold repetition of $G$ has entangled value $\mathrm{val}^*(G^{\otimes n})$ at most $(1 - ε^{3/2})^{Ω(n/sk^4)}$, where $s$ is the answer length of any player. In contrast, the best known parallel repetition theorem for the classical value of two-player free games is $\mathrm{val}(G^{\otimes n}) \leq (1 - ε^2)^{Ω(n/s)}$, due to Barak, et al. (RANDOM 2009). This suggests the possibility of a separation between the behavior of entangled and classical free games under parallel repetition. Our second theorem handles the broader class of free games $G$ where the players can output (possibly entangled) quantum states. For such games, the repeated entangled value is upper bounded by $(1 - ε^2)^{Ω(n/sk^2)}$. We also show that the dependence of the exponent on $k$ is necessary: we exhibit a $k$-player free game $G$ and $n \geq 1$ such that $\mathrm{val}^*(G^{\otimes n}) \geq \mathrm{val}^*(G)^{n/k}$. Our analysis exploits the novel connection between communication protocols and quantum parallel repetition, first explored by Chailloux and Scarpa (ICALP 2014). We demonstrate that better communication protocols yield better parallel repetition theorems: our first theorem crucially uses a quantum search protocol by Aaronson and Ambainis, which gives a quadratic speed-up for distributed search problems. Finally, our results apply to a broader class of games than were previously considered before; in particular, we obtain the first parallel repetition theorem for entangled games involving more than two players, and for games involving quantum outputs. Kai-Min Chung, Xiaodi Wu 0001, Henry S. Yuen |
CCC | 2 |
| 2015 | Epsilon-net method for optimizations over separable states
Yaoyun Shi, Xiaodi Wu 0001 |
Theor. Comput. Sci. | 2 |
| 2013 | Parallel Approximation of Min-Max Problems
Gus Gutoski, Xiaodi Wu 0001 |
Comput. Complex. | 2 |
| 2012 | Parallel Approximation of Min-max Problems with Applications to Classical and Quantum Zero-Sum GamesabstractThis paper presents an efficient parallel algorithm for a new class of min-max problems based on the matrix multiplicative weights update method. Our algorithm can be used to find near-optimal strategies for competitive two-player classical or quantum games in which a referee exchanges any number of messages with one player followed by any number of additional messages with the other. This algorithm considerably extends the class of games which admit parallel solutions, demonstrating for the first time the existence of a parallel algorithm for a game in which one player reacts adaptively to the other. As a consequence, we prove that several competing-provers complexity classes collapse to PSPACE such as QRG(2), SQG and two new classes called DIP and DQIP. A special case of our result is a parallel approximation scheme for a new class of semi definite programs whose feasible region consists of lists of semi definite matrices that satisfy a ``transcript-like'' consistency condition. Applied to this special case, our algorithm yields a direct polynomial-space simulation of multi-message quantum interactive proofs resulting in a first-principles proof of QIP=PSPACE. Gus Gutoski, Xiaodi Wu 0001 |
CCC | 2 |
| 2012 | Epsilon-Net Method for Optimizations over Separable States
Yaoyun Shi, Xiaodi Wu 0001 |
ICALP (1) | 2 |