Publications
Click on a title to see the abstract. The authors of papers in theoretical computer science are listed by the alphabetical order of the last name, whereas in other fields (such as physics, machine learning, and programming languages) the authors are listed by contribution where the last author is usually the corresponding author. Also * means equal contribution.
 Fixing and Mechanizing the Security Proof of FiatShamir with Aborts and Dilithium

Manuel Barbosa, Gilles Barthe, Christian Doczkal, Jelle Don, Serge Fehr, Benjamin Grégoire, YuHsuan Huang, Andreas Hülsing, Yi Lee, and Xiaodi Wu.
to appear in CRYPTO 2023.
Abstract:
We extend and consolidate the security justification for the Dilithium signature scheme. In particular, we identify a subtle but crucial gap that appears in several ROM and QROM security proofs for signature schemes that are based on the FiatShamir with aborts paradigm, including Dilithium. The gap lies in the CMAtoNMA reduction and was uncovered when trying to formalize a variant of the QROM security proof by Kiltz, Lyubashevsky, and Schaffner (Eurocrypt 2018). The gap was confirmed by the authors, and there seems to be no simple patch for it. We provide new, fixed proofs for the affected CMAtoNMA reduction, both for the ROM and the QROM, and we perform a concrete security analysis for the case of Dilithium to show that the claimed security level is still valid after addressing the gap. Furthermore, we offer a fully mechanized ROM proof for the CMAsecurity of Dilithium in the EasyCrypt proof assistant. Our formalization includes several new tools and techniques of independent interest for future formal verification results.
 Quantum Natural Proof: A New Perspective of Hybrid QuantumClassical Program Verification

(by contribution) Liyi Li, Mingwei Zhu, Yi Lee, Le Chang, and Xiaodi Wu.
Manuscript, 2022. Github
Abstract:
Many quantum programs are assured by formal verification, but such verification is usually laborious and timeconsuming. This paper proposes quantum natural proof (QNP), an automated proof system for verifying hybrid quantumclassical algorithms. Natural proofs are a subclass of proofs that are amenable to completely automated reasoning, provide sound but incomplete procedures, and capture common reasoning tactics in program verification. The core of QNP is a typeguided quantum proof system, named Qafny, which views quantum operations as some classical array operations that can be modeled as proof rules in a classical separation logic framework, suitable for automated reasoning. We proved the soundness and completeness of the Qafny proof system as well as the soundness of the proof system compilation from Qafny to Dafny. By using the QNP implementation in Dafny, automated verification can be efficiently performed for many hybrid quantumclassical algorithms, including GHZ, Shor's, Grover's, and quantum walk algorithms, which saves a great amount of human effort. In addition, quantum programs written in Qafny can be compiled to quantum circuits so that every verified quantum program can be run on a quantum machine.
 A Scalable Classical Verification reveals the Gap of the StateOfTheArt Gaussian Boson Sampling Experiments

(by contribution) Yufan Zheng, Yingkang Cao, and Xiaodi Wu.
Manuscript, 2022.
Abstract:
Gaussian Boson Sampling (GBS) is one major candidate for establishing quantum computational advantage in the near term. Despite promising experimental progress, most existing validation schemes of GBS experiments merely rule out a few experimentallymotivated alternative physical hypotheses and fail to certify the device’s output distribution directly, which is critical for establishing the computational hardness. Inspired by the symmetry property of Hafnian functions, we propose a scalable classical verification scheme of GBS, based on symmetry testing via a coarsegrained statistical heuristic, with strong theoretical and empirical evidence for its validity. Theoretically, when symmetry properties are approximately established, we prove that the device's output distribution is close to GBS under a mild assumption of the device. Empirically, based on classical simulation of up to 20 modes, we observe that our protocol can successfully distinguish GBS devices from all known alternative physical hypotheses and is further resilient to a small photon loss in the experiment. We perform part of our verification scheme on Xanadu’s Borealis machine, which reveals a large inhomogeneity among alleged 216 squeezed modes that fail our symmetry test, and hence a gap for the claimed computational advantage based on GBS.
 SimuQ: A DomainSpecific Language For Quantum Simulation With Analog Compilation

(by contribution) Yuxiang Peng, Jacob Young, Pengyu Liu, and Xiaodi Wu.
Manuscript, 2022.Website
Links:
Abstract:
Hamiltonian simulation is one of the most promising applications of quantum computing. Recent experimental results suggest that continuoustime analog quantum simulation would be advantageous over the gatebased digital quantum simulation in the NISQ era. However, programming such analog quantum simulators is much more challenging due to the lack of a unified interface between hardware and software and the only few known examples are all hardwarespecific. We present SimuQ, the first domainspecific language for Hamiltonian simulation that supports pulselevel compilation to heterogeneous analog quantum simulators. Specifically, in SimuQ, frontend users will specify the target Hamiltonian evolution with a Hamiltonian specification language, and the programmability of analog simulators is specified through a new abstraction called the abstract analog instruction set by hardware providers. Through a solverbased compilation, SimuQ will generate the pulselevel instruction schedule on the target analog simulator for the desired Hamiltonian evolution, which has been demonstrated on pulsecontrolled superconducting (Qiskit OpenPulse) and neutralatom (Bloqade) systems, as well as on normal digital machines. We also show the advantage of the analog compilation over the digital one on IBM machines and the use of SimuQ for resource estimation for hypothetical analog machines.
 Distributed Quantum Sensing Network with Geographically Constrained Measurement Strategies

(by contribution) Yingkang Cao and Xiaodi Wu.
To appear at the 2023 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP 2023).
Abstract:
Distributed 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érRao bound (QCRB). This argument is incomplete in that QCRB assumes a team of allpowerful 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 singleparameter estimation. 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.
 Syntaxguided Synthesis of Quantum Unitary Programs

(by contribution) Haowei Deng, Runzhou Tao, Yuxiang Peng, and Xiaodi Wu.
Manuscript, 2022. Github
Links:
Abstract:
Quantum 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 lowlevel quantum details would hence be highly desirable. In this paper, we initiate the study of syntaxguided 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, a 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 quantum unitary programs for state preparation, quantum adder circuits, and quantum Fourier transformation, which can be readily transpiled to executable quantum programs on major commercial quantum platforms, e.g., Q#, IBM Qiskit, and AWS Braket.
 Quantum Hamiltonian Descent

(by contribution) Jiaqi Leng, Ethan Hickman, Joseph Li, and Xiaodi Wu.
More information at the accompanying website.
Links:
Abstract:
Gradient descent is a fundamental algorithm in both theory and practice for continuous optimization. Identifying its quantum counterpart would be appealing to both theoretical and practical quantum applications. A conventional approach to quantum speedups in optimization relies on the quantum acceleration of intermediate steps of classical algorithms while keeping the overall algorithmic trajectory and solution quality unchanged. We propose Quantum Hamiltonian Descent (QHD), which is derived from the path integral of dynamical systems referring to the continuoustime limit of classical gradient descent algorithms, as a truly quantum counterpart of classical gradient methods where the contribution from classicallyprohibited trajectories can significantly boost QHD’s performance for nonconvex optimization. Moreover, QHD is described as a Hamiltonian evolution efficiently simulatable on both digital and analog quantum computers. By embedding QHD’s Hamiltonian evolution into the one of the socalled Quantum Ising Machine (including DWave and others), we empirically observe that the DWaveimplemented QHD outperforms a selection of stateoftheart gradientbased classical solvers and the standard quantum adiabatic algorithm, based on the timetosolution metric, on nonconvex constrained quadratic programming instances up to 75 dimensions. Finally, we propose a “threephase picture” to explain the behavior of QHD, especially its difference from the quantum adiabatic algorithm.
 Analyzing Convergence in Quantum Neural Networks:
Deviations from Neural Tangent Kernels

(by contribution) Xuchen You, Shouvanik Chakrabarti, Boyang Chen and Xiaodi Wu.
To appear at ICML 2023.
Links:
Abstract:
A quantum neural network (QNN) is a parameterized mapping efficiently implementable on nearterm Noisy IntermediateScale Quantum (NISQ) computers. It can be used for supervised learning when combined with classical gradientbased 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 overparameterized 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 nonnegligible deviation from the tangent kernel regression derived at the random initialization. As a result of the deviation, we prove the atmost 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 overparameterization. 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.
 A Convergence Theory for Overparameterized Variational Quantum Eigensolvers

(by contribution) Xuchen You, Shouvanik Chakrabarti, and Xiaodi Wu.
QIP 2023.
Abstract:
The Variational Quantum Eigensolver (VQE) is a promising candidate for quantum applications on nearterm Noisy IntermediateScale Quantum (NISQ) computers. Despite a lot of empirical studies and recent progress in theoretical understanding on VQE's optimization landscape, the convergence for optimizing VQE is far less understood. We provide the first rigorous analysis of the convergence of VQEs in the overparameterization regime. By connecting the training dynamics with the Riemannian Gradient Flow on the unitsphere, we establish a threshold on the sufficient number of parameters for efficient convergence, which depends polynomially on the system dimension and the spectral ratio, a property of the problem Hamiltonian, and could be resilient to gradient noise to some extent. We further illustrate that this overparameterization threshold could be vastly reduced for specific VQE instances by establishing an ansatzdependent threshold paralleling our main result. We showcase that our ansatzdependent threshold could serve as a proxy of the trainability of different VQE ansatzes without performing empirical experiments, which hence leads to a principled way of evaluating ansatz design. Finally, we conclude with a comprehensive empirical study that supports our theoretical findings.
 A Formally Certified EndtoEnd Implementation of
Shor's Factorization Algorithm

(by contribution) Yuxiang Peng, Kesha Hietala, Runzhou Tao, Liyi Li, Robert Rand, Michael Hicks, and Xiaodi Wu.
To appear in the Proceedings of the National Academy of Sciences, 2023. Github
Abstract:
Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but these are only useful if computed answers are correct. While hardwarelevel decoherence errors have garnered significant attention, a less recognized obstacle to correctness is that of human programming errors – bugs. Techniques familiar to most programmers from the classical domain for avoiding, discovering, and diagnosing bugs do not easily transfer, at scale, to the quantum domain because of its unique characteristics. To address this problem, we have been working to adapt formal methods to quantum programming. With such methods, a programmer writes a mathematical specification alongside their program, and semiautomatically proves the program correct with respect to it. The proof's validity is automatically confirmed  certified by a “proof assistant.” Formal methods have successfully yielded highassurance classical software artifacts, and the underlying technology has produced certified proofs of major mathematical theorems. As a demonstration of the feasibility of applying formal methods to quantum programming, we present the first formally certified endtoend implementation of Shor's prime factorization algorithm, developed as part of a novel framework of applying the certified approach to general applications. By leveraging our framework, one can significantly reduce the effects of human errors and obtain highassurance implementation of largescale quantum applications in a principled way.
 Differentiable Analog Quantum Computing for Optimization and Control

Abstract:
We formulate the first differentiable analog quantum computing framework with a specific parameterization design at the analog signal (pulse) level to better exploit nearterm 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 gradientbased 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 Quantum Programming with Unbounded Loops

(by contribution) Wang Fang, Mingsheng Ying and Xiaodi Wu.
Manuscript, 2022.
Abstract:
The emergence of variational quantum applications has led to the development of automatic differentiation techniques in quantum computing. Recently, Zhu et al. 2020 have 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 closetooptimal parameters for several parameterized quantum applications.
 Quantum Variational Methods for Quantum Applications

(by contribution) Shouvanik Chakrabarti, Xuchen You, and Xiaodi Wu.
Invited Paper at the Special Session of ICCAD 2021.
Links:
Abstract:
Quantum Variational Methods are promising nearterm 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 nearterm 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 domainspecific quantum variational ansatzes. This paper proposes a theoryguided principle in order to tackle the training issue of quantum variational methods and highlights some successful examples.
 Verified Compilation of Quantum Oracles

Abstract:
Quantum algorithms often apply classical operations, such as arithmetic or predicate checks, over a quantum superposition of classical data; these socalled oracles are often the largest components of a quantum program. To ease the construction of efficient, correct oracle functions, this paper presents vqo, a highassurance 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 generalpurpose quantum assembly language—and allowed us to efficiently test properties of Oqasm programs using the QuickChick propertybased 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 QFTbased 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 stateoftheart but unverified quantum programming platform.
 Twoway Separations in Expressivity between Quantum Neural Networks and Feedforward ReLU Networks

(by contribution) Shouvanik Chakrabarti and Xiaodi Wu.
Manuscript, 2021.
Links:
Abstract:
Quantum Neural Networks (QNNs) have been proposed as a variational method to realize a quantum advantage on nearterm quantum computers. Despite the popularity of these models and some empirical evidence indicating their utility, there has yet to be a thorough analysis of their expressivity compared to classical parameterized models such as neural networks. In this work, we rigorously study separations in expressive power between QNNs and feedforward ReLU networks (ReNNs) with realvalued outputs, by investigating the model complexity (in terms of the input dimension and error) required to approximate various function classes. We discover advantages in expressivity in both directions: we demonstrate that constant and variabledepth ReNNs can be provably advantageous in expressing families of univariate and multivariate functions, while conversely QNNs have provable advantages over ReNNs of depth2 in approximating certain univariate functions. We further conjecture that QNNs have advantages over ReNNs with depth>2, and carry out an empirical study to support this hypothesis. We also empirically verify the demonstrated provable separations in expressivity.
 EasyPQC: Verifying PostQuantum Cryptography

Manuel Barbosa, Gilles Barthe, Xiong Fan, Benjamin Gregoire, ShihHan Hung, Jonathan Katz, PierreYves Strub, Xiaodi Wu, and Li Zhou.
In ACM Conference on Computer and Communication Security (CCS 2021).
Abstract:
EasyCrypt is a formal verification tool used extensively for formalizing concrete security proofs of cryptographic constructions. However, the EasyCrypt formal logics consider only classical attackers, which means that postquantum security proofs cannot be formalized and machinechecked with this tool. In this paper we prove that a natural extension of the EasyCrypt core logics permits capturing a wide class of postquantum cryptography proofs, settling a question raised by (Unruh, POPL 2019). Leveraging our positive result, we implement EasyPQC, an extension of EasyCrypt for postquantum security proofs, and use EasyPQC to verify postquantum security of two classic constructions: Full Domain Hash and GPV08 identitybased encryption.
 Scalable Verification of Quantum Supremacy based on Circuit Obfuscation

(by contribution) Shouvanik Chakrabarti, ChiNing Chou, KaiMin Chung, and Xiaodi Wu.
Manuscript, 2021. Github
Abstract:
Exciting experimental progress has been made recently to demonstrate quantum supremacy in the examples of random circuit sampling and Boson sampling, whose verification procedure is however exponentially expensive and hence extremely hard to scale to verify similar experiments of a slightly larger size. In this letter, we propose a practical and scalable scheme for verifiable quantum supremacy. Specifically, we define a type of quantum circuit obfuscators which significantly grows the size of the input circuit while keeping its original semantic. With such obfuscators, we can upgrade any circuitbased supremacy task to perform on larger size quantum machines while keeping the verification cost almost unchanged. The soundness of the upgraded protocol is supported by the hardness of the quantum counterpart of the minimum equivalent circuit problem. Inspired by the practical challenge in optimizing quantum circuits, we provide a construction of such obfuscators by roughly applying the reversed rewrites from existing quantum circuit optimizers in a random order. We have implemented a prototype of this construction and empirically verified its performance against all existing offtheshelf tools. It is worth noting that our construction is highly extensible and can be easily adjusted for specific supremacy tasks and experimental platforms.
 Automating NISQ Application Design with Meta Quantum Circuits with Constraints (MQCC)

(by contribution) Haowei Deng, Yuxiang Peng, Michael Hicks, and Xiaodi Wu.
ACM Transaction on Quantum Computing vol. 4, issue 3, article no.16, pp 129. 2023. Github
Abstract:
Nearterm intermediatescale quantum (NISQ) computers are likely to have very restricted hardware resources, where precisely controllable qubits are expensive, errorprone, and scarce. Application designers for such computers must investigate the best balance of tradeoffs 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 metaprogramming framework for quantum programs. Designers express their application as a succinct collection of normal quantum circuits stitched together by a set of (manually or automatically) added metalevel 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 demonstrate MQCC's expressiveness by easily encoding prior oneoff NISQ application designs multiprogramming (MP), crosstalk mitigation (CM) and building new ones, including a combined MPCM, and an approach to writing approximate quantum Fourier transformation and quantum phase estimation that smoothly trades off accuracy and resource use.
 Algebraic Reasoning of Quantum Programs via NonIdempotent Kleene Algebra

(by contribution)
Yuxiang Peng, Mingsheng Ying, and Xiaodi Wu.
In the Proceedings of the 43rd ACM SIGPLAN PLDI 2022.
Abstract:
We 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 exponentialsize 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 the Nonidempotent Kleena 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 whileprograms. 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.
 Exponentially Many Local Minima in Quantum Neural Networks

Abstract:
Quantum Neural Networks (QNNs), or the socalled 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 nearterm intermediatesize 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 underparameterized 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 nonlinear 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 gradientbased optimizers, which demonstrates the practical value of our findings.
 Sublinear Classical and Quantum Algorithms for General Matrix Games

(by contribution) Tongyang Li, Chunhao Wang, Shouvanik Chakrabarti, and Xiaodi Wu.
Appeared at the 35th AAAI Conference on Artificial Intelligence (AAAI 2021).
 Constantround Blind Classical Verification of Quantum Sampling

Abstract:
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. In this work, we explore further the feasibility of CVQC with the more general sampling problems in BQP and with the desirable blindness property. We contribute affirmative solutions to both as follows.
(1) Motivated by the sampling nature of many quantum applications (e.g., quantum algorithms for machine learning and quantum supremacy tasks), we initiate the study of CVQC for emph{quantum sampling problems} (denoted by SampBQP). Precisely, given an input and a quantum circuit , the goal of a classical client is to learn a sample of output over with the correct distribution up to a small error from an untrusted prover. We demonstrate its feasibility by constructing a fourmessage CVQC protocol for SampBQP based on the quantum Learning With Error assumption.
(2) The blindness of CVQC protocols refers to a property of the protocol where the prover learns nothing, and hence is blind, about the client's input. It is a highly desirable property that has been intensively studied for the delegation of quantum computation.
Somewhat surprisingly, we provide a simple yet powerful generic compiler that transforms any CVQC protocol to a blind one while preserving completeness and soundness errors.
Applying our compiler to (a parallel repetition of) Mahadev's protocol for BQP and our CVQC protocol for SampBQP yields the first constantround blind CVQC protocol for BQP and SampBQP respectively, with negligible completeness and soundness errors.
 A Verified Optimizer for Quantum Circuits

(by contribution) Kesha Hietala, Robert Rand, ShihHan Hung, Xiaodi Wu, and Michael Hicks.
Appeared as a distinguished paper at the 48th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2021). GitHub
Abstract:
We present VOQC, the first fully verified compiler for quantum circuits, written using the Coq proof assistant.
Quantum circuits are expressed as programs in a simple, lowlevel language called SQIR, 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 easy to write and verify a broad range of optimizations in VOQC, and even allow us to verify correctness
properties of interesting source SQIR programs.
 On the Theory and Practice of Invariantbased Verification of Quantum Programs

(by contribution) ShihHan Hung, Yuxiang Peng, Xin Wang, Shaopeng Zhu, and Xiaodi Wu.
Manuscript, 2019.
Abstract:
We investigate program verification, a fundamental and challenging task in quantum programming, based on quantum Hoare logic and quantum invariants. Ying et al. (POPL’17) have developed a framework based on semidefinite programs (SDPs) for computing quantum invariants for partial correctness, which is however expensive to use due to its exponential scaling in terms of the number of qubits. In this paper, we develop two approaches that can effectively reuse the information generated from quantum invariants so as to avoid repetitive costs in solving exponentially large SDPs. Our first contribution is the formulation of the master Hoare triple that encodes the complete information of quantum programs inspired by the ChoiJamiol{}kowski isomorphism. We demonstrate how to obtain the master Hoare triple by a single use of SDP, and once it is generated, how to obtain any other Hoare triple from the master one by a simple logic rule, and how master Hoare triples of subprograms can be reused to simplify the computation of quantum invariants of the main program. Our second contribution is the introduction of approximate quantum invariants and a framework to reuse invariants of any given quantum program to efficiently analyze its nearby (e.g., noisy, erroneous) programs without using SDPs. Finally, we demonstrate the use of our techniques on realistic quantum programs, such as quantum Hamiltonian simulation and RepeatUntilSuccess, with a huge numerical advantage over the previous SDP approach.
 On the Principles of Differentiable Quantum Programming Languages

(by contribution) Shaopeng Zhu, ShihHan Hung, Shouvanik Chakrabarti, and Xiaodi Wu.
In the Proceedings of the 41st ACM SIGPLAN PLDI 2020.
GitHub.
Abstract:
Variational Quantum Circuits (VQCs), or the socalled quantum neuralnetworks, are predicted to be one of the most important nearterm quantum applications, not only because of their similar promises as classical neuralnetworks, but also because of their feasibility on nearterm noisy intermediatesize quantum (NISQ) machines. The need for gradient information in the training procedure of VQC applications has stimulated the interest and development of autodifferentiation techniques on 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 nocloning) and provide a rigorous formulation of differentiation applied to boundedloop imperative quantum programs, its codetransformation rules, as well as a sound logic to reason about their correctness.
Moreover, we have implemented our code transformation in OCaml and demonstrated the resourceefficiency 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 autodifferentiation on quantum circuits without controls.
 Quantum algorithm for estimating volumes of convex bodies

Shouvanik Chakrabarti,
Andrew M. Childs, Tongyang Li, ShihHan Hung, Chunhao Wang, and Xiaodi Wu.
ACM Transaction on Quantum Computing, vol. 4, issue 3, article no.20, pp 160. Earlier appeared at QIP 2020 as a singletrack talk.
 Quantum Wasserstein Generative Adversarial Networks

Abstract:
The study of quantum generative models is wellmotivated, not only because of its importance in quantum machine learning and quantum chemistry but also because of the perspective of its implementation on nearterm 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 3qubit quantum circuit of 50 gates that well approximates a 3qubit 1d Hamiltonian simulation circuit that requires over 10k gates using standard techniques.
 Verified Optimization in a Quantum Intermediate Representation

Abstract:
We present sQIRe, a lowlevel language for quantum computing and verification. sQIRe uses a global register of quantum bits, allowing easy compilation to and from existing ‘quantum assembly’ languages and simplifying the verification process. We demonstrate the power of sQIRe as an intermediate representation of quantum programs by verifying a number of useful optimizations, and we demonstrate sQIRe's use as a tool for general verification by proving several quantum programs correct.
 Simulating large quantum circuits on a small quantum computer

 Sublinear quantum algorithms for training linear and kernelbased classifiers

 Quantitative Robustness Analysis of Quantum Programs

Abstract:
Quantum 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 costprohibitive. 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 whileprograms, 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 singlequibit errors; and (3) analyzing the robustness of a faulttolerant version of QBF.
 Quantum algorithms and lower bounds for convex optimization

 Quantum SDP Solvers: Large Speedups, Optimality, and Applications to Quantum Learning

Abstract:
We give two new quantum algorithms for solving semidefinite programs (SDPs) providing quantum speedups. We consider SDP instances with constraint matrices, each of dimension , rank at most , and sparsity . 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 , with the error of the solution. This gives an optimal dependence in terms of and a quadratic improvement over previous quantum algorithms (when ). The second algorithms assumes a fully quantum input model in which the input matrices are given as quantum states. We show its run time is , with an upper bound on the tracenorm of all input matrices. In particular the complexity depends only polylogarithmically in and polynomially in .
We apply the second SDP solver to the problem of learning a good description of a quantum state with respect to a set of measurements: Given measurements and a supply of copies of an unknown state , we show we can find in time a description of the state as a quantum circuit preparing a density matrix which has the same expectation values as on the measurements, up to error . 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 lowrank Hamiltonians, given quantum states encoding these Hamiltonians, with a polylogarithmic 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. (SODA 2017). We believe both techniques might be of independent interest.
 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. (link)
Abstract:
Estimation of Shannon and R{'e}nyi entropies of unknown discrete distributions is a fundamental problem in statistical property testing and an active research topic in both theoretical computer science and information theory. Tight bounds of the number of samples to estimate these entropies have been established in the classical setting, while little is known about their quantum counterparts. In this paper, we give the first quantum algorithms for estimating R{'e}nyi entropies (Shannon entropy being 1Renyi entropy). In particular, we demonstrate a quadratic quantum speedup for Shannon entropy estimation and a generic quantum speedup for R{'e}nyi entropy estimation for all ,
including a tight bound for the collisionentropy (2R{'e}nyi entropy) and also an analysis for the minentropy case (i.e., ). Moreover, we complement our quantum upper bounds with quantum lower bounds on R{'e}nyi entropy estimation for all .
Our approach is inspired by the pioneering work of Bravyi, Harrow, and Hassidim (BHH) on quantum algorithms for distributional property testing, however, with many new technical ingredients. For Shannon entropy estimation, we improve the performance of the BHH framework, especially its error dependence, using Montanaro's approach to estimating the expected output value of a quantum subroutine with bounded variance and giving a finetuned error analysis.
For general R{'e}nyi entropy estimation, we further develop a procedure that recursively approximates R{'e}nyi entropy for a sequence of s, which is in spirit similar to the cooling schedules in simulated annealing.
For special cases like integer and (i.e., the minentropy case), we reduce the entropy estimation problem to the distinctness and the distinctness problems respectively.
Finally, we exploit reductions as well as the polynomial method to obtain our lower bounds.
 RazMcKenzie simulation with the inner product gadget

 Computational Notions of Quantum MinEntropy

Abstract:
Computational notions of entropy have many applications in cryptography and complexity theory. These notions measure how much (min)entropy a source X has from the eyes of a computationally bounded party who may hold certain ?leakage information? B that is correlated with X. In this work, we initiate the study of computational entropy in the quantum setting, where X and/or B may become quantum states and the computationally bounded observer is modelled as a small quantum circuit. Specifically, we investigate to what extent the classical notions of computational entropy generalize to the quantum setting, and whether quantum analogues of classical theorems still hold. For example, we show:
There exist quantum states that are pseudorandom (i.e. they cannot be distinguished from the totally mixed state by polynomialsized quantum circuits) but have actual entropy 0 (i.e. are pure states). In contrast, a classical distribution needs superlogarithmic entropy to be pseudorandom.
We extend the classical Leakage Chain Rule for pseudoentropy to the case where the leakage information B is quantum (while X remains classical). Specifically, if X has pseudoentropy at least k against quantum distinguishers (i.e. it is indistinguishable from some distribution of minentropy at least k by polynomialsized quantum distinguishers) and B consists of at most a logarithmic number l of qubits, then X conditioned on B has pseudoentropy at least kl against quantum distinguishers.
We show that a general form of the classical Dense Model Theorem (interpreted as showing the equivalence between two definitions of pseudorelativeminentropy) does not extend to quantum states.
As an application, we construct the first quantum leakageresilient streamcipher in the quantum bounded storage model, assuming the existence of a quantumsecure PRG.
Along the way, we develop quantum analogues of a number of classical techniques (e.g. the Leakage Simulation Lemma, proven using a Nonuniform MinMax Theorem or Boosting), and also identify classical techniques (namely, Gap Amplification) that do not hold in the quantum setting. Moreover, we introduce a variety of notions that combine quantum information and quantum complexity, which raise a number of directions for future work.
 General randomness amplification with nonsignaling security

Abstract:
Highly unpredictable events appear to be abundant in life. However, when modeled rigorously,
their existence in nature is far from evident. In fact, the world can be deterministic
while at the same time the predictions of quantum mechanics are consistent with observations. Assuming that randomness does exist but only in a weak form,
could highly random events be possible? This fundamental question was first raised by Colbeck and Renner (Nature Physics, 8:450–453, 2012). In this work, we answer this question positively, without the various restrictions assumed in the previous works. More precisely, our protocol uses quantum devices, a single weak randomness source quantified by a general notion of nonsignaling minentropy, tolerates a constant amount of device imperfection, and the security is against an allpowerful nonsignaling adversary. Unlike the previous works proving nonsignaling security, our result does not rely on any structural restrictions or independence assumptions.
Thus it implies a stronger interpretation of the dichotomy statement articulated by Gallego et al. (Nature Communications, 4:2654, 2013): ‘‘either our world is fully deterministic or there exist in nature events that are fully random.’’
Note: This is a new work after our QIP 2014 paper, where the security proved is against a quantum, as opposed to nonsignaling, adversary.
 Limitations of semidefinite programs for separable states and entangled games

Aram Harrow, Anand Natarajan, Xiaodi Wu.
Appeared at QIP 2017. Communications in Mathematical Physics, Volume 366, Issue 2, pp 423468, 2019.
Abstract:
We introduce a method for using reductions to construct integrality
gaps for
semidefinite programs (SDPs). These imply new limitations on the
sumofsquares (SoS) hierarchy in two settings where previously no
round integrality gaps were known:
The set of separable (i.e. unentangled) quantum states, or equivalently, the norm of a matrix.
The set of quantum correlations; i.e. conditional probability
distributions achievable with local measurements on a shared
entangled state.
Integrality gaps for the norm had previously been sought due
to its connection to SmallSet Expansion (SSE) and Unique Games (UG).
In both cases nogo theorems were previously known based on computational assumptions such as the Exponential Time Hypothesis (ETH) which asserts that 3SAT requires exponential time to solve. Our unconditional results achieve the same parameters as all of these previous results (for separable states) or as some of the previous results (for quantum correlations). In some cases we can make use of the framework of LeeRaghavendraSteurer (LRS) to establish integrality gaps for any SDP, not only the SoS hierarchy. Our hardness result on separable states also yields a dimension lower bound of approximate disentanglers, answering a question of Aaronson et al.
These results can be viewed as limitations on the monogamy principle, the PPT test, the ability of Tsirelsontype bounds to restrict quantum correlations, as well as the SDP hierarchies of DohertyParriloSpedalieri, NavascuesPironioAcin and BertaFawziScholz. Indeed a wide range of past work in quantum information can be described as using an SDP on one of the above two problems and our results put broad limits on these lines of argument.
 Invariants of Quantum Programs: Characterizations and Generation

Abstract:
Program 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.
Interestingly, the notion of invariant can be defined for quantum programs in two different ways – additive invariants and multiplicative invariants – corresponding to two interpretations of implication in a continuous valued logic: the Lukasiewicz implication and the Godel implication. It is shown that both of them can be used to establish partial correctness of quantum programs.
The problem of generating additive invariants of quantum programs is addressed by reducing it to an SDP (Semidefinite Programming) problem. This approach is applied with an SDP solver to generate invariants of two important quantum algorithms – quantum walk and quantum Metropolis sampling. Our examples show that the generated invariants can be used to verify correctness of these algorithms and are helpful in optimizing quantum Metropolis sampling.
To our knowledge, this paper is the first attempt to define the notion of invariant and to develop a method of invariant generation for quantum programs.
 Tight SoSdegree bounds for approximate Nash equilibria

Links: preprint
Abstract:
Nash equilibria always exist, but are widely conjectured to require time to find that is exponential in the number of strategies, even for twoplayer games. By contrast, a simple quasipolynomial 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 by changing their strategy. The LMM algorithm can also be used to find an approximate Nash equilibrium with nearmaximal total welfare. Matching hardness results for this optimization problem were found assuming the hardness of the plantedclique 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 sumsquares (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 levels — matching our lower
bounds. The lower bounds involve a modification of the
BravermanKoWeinstein embedding of CSPs into strategic games and
techniques from sumofsquares proof systems. The upper bound
(i.e. analysis of the LP) uses informationtheory techniques that
have been recently applied to other linear and
semidefiniteprogramming hierarchies.
 Sampleoptimal tomography of quantum states

 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 881904.
Abstract:
We present a stronger version of the DohertyParriloSpedalieri (DPS) hierarchy of approximations for the set of separable states. Unlike DPS, our hierarchy converges exactly at a finite number of rounds for any fixed input dimension. This yields an algorithm for separability testing which is singly exponential in dimension and polylogarithmic in accuracy. Our analysis makes use of tools from algebraic geometry, but our algorithm is elementary and differs from DPS only by one simple additional collection of constraints.
 On the Limits of Communication with Nonlocal Resources

Abstract:
We obtain optimal bounds for the problem of conveying classical messages by communication between a sender and receiver who can utilize nonlocal correlations obeying the NonSignaling Principle. These include correlations arising from quantum entanglement, but also include ‘‘superquantum’’ correlations (e.g. those that maximally violate the CHSH inequality). Our result simultaneously simplifies and generalizes the result of Nayak and Salzman (JACM vol.53, issue 1, pp. 184–206).
 Parallel repetition for entangled kplayer games via fast quantum search

Abstract:
We present two parallel repetition theorems for the entangled value of multiplayer, oneround free games (games where the inputs come from a product distribution). Our first theorem shows that for a player free game with entangled value , the fold repetition of has entangled value at most , where is the answer length of any player. In contrast, the best known parallel repetition theorem for the emph{classical} value of twoplayer free games is , 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 where the players can output (possibly entangled) quantum states. For such games, the repeated entangled value is upper bounded by . We also show that the dependence of the exponent on is necessary: we exhibit a player free game and such that .
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: in particular, our first theorem crucially uses a quantum search protocol by Aaronson and Ambainis, which gives a quadratic Grover speedup 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.
 MultiSource Randomness Extractors Against Quantum Side Information, and their Applications

Abstract:
We study the problem of constructing multisource extractors in the quantum setting, which extract almost uniform random bits against an adversary who collects quantum side information from several initially independent classical random sources. This is a natural generalization of the two much studied problems of seeded randomness extraction against quantum side information, and classical independent source extractors. With new challenges such as potential entanglement in the side information, it is not a prior clear under what conditions do quantum multisource extractors exist; the only previous work in this setting is [KK12], where the classical innerproduct twosource extractors of [CG88] and [DEOR04] are shown to be quantum secure in the restricted Independent Adversary (IA) Model and entangled Bounded Storage (BS) Model.
In this paper we propose a new model called General Entangled (GE) Adversary Model, which allows arbitrary entanglement in the side information and subsumes both the IA model and the BS model. We proceed to show how to construct GEsecure quantum multisource extractors.
To that end, we propose another model called Onesided Adversary (OA) Model, which is weaker than all the above models. Somewhat surprisingly, we establish an equivalence between strong OAsecurity and strong GEsecurity. As a result, all classical multisource extractors can either directly work, or be modified to work in the GE model at the cost of one extra random source. Thus, our constructions essentially match the best known constructions of classical multisource extractors. This answers several open questions in [KK12,DPVR12].
We also apply our techniques to two important problems in cryptography and distributed computing — privacy amplification and network extractor. Both problems deal with converting secret weak random sources into secret uniform random bits in a communicating environment, with the presence of a passive adversary who has unlimited computational power and can see every message transmitted. We show that as long as the sources have certain amounts of conditional minentropy in our GE model (even with entangled quantum side information), we can design very efficient privacy amplification protocols and network extractors.
 Physical Randomness Extractors

Abstract:
How to generate provably true randomness with minimal assumptions? This question is important not only for the efficiency and the security of information processing, but also for understanding how extremely unpredictable events are possible in Nature. All current solutions require special structures in the initial source of randomness, or a certain independence relation among two or more sources. Both types of assumptions are impossible to test and difficult to guarantee in practice. Here we show how this fundamental limit can be circumvented by extractors that base security on the validity of physical laws and extract randomness from untrusted quantum devices. In conjunction with the recent work of Miller and Shi (arXiv:1402:0489), our physical randomness extractor uses just a single and general weak source, produces an arbitrarily long and nearuniform output, with a closetooptimal error, secure against allpowerful quantum adversaries, and tolerating a constant level of implementation imprecision. The source necessarily needs to be unpredictable to the devices, but otherwise can even be known to the adversary.
Our central technical contribution, the Equivalence Lemma, provides a general principle for proving composition security of untrusteddevice protocols. It implies that unbounded randomness expansion can be achieved simply by crossfeeding any two expansion protocols. In particular, such an unbounded expansion can be made robust, which is known for the first time. Another significant implication is, it enables the secure randomness generation and key distribution using public randomness, such as that broadcast by NIST's Randomness Beacon. Our protocol also provides a method for refuting local hidden variable theories under a weak assumption on the available randomness for choosing the measurement settings.
 Limits of Quantum Oneway Communication by Matrix Hypercontractive Inequality

Yaoyun Shi, Xiaodi Wu, and Wei Yu .
Manuscript, 2013.
 Epsilonnet method for optimizations over separable states

Yaoyun Shi and Xiaodi Wu .
Contributed talk at the 15th Workshop on Quantum Information Processing (QIP 2012). In the Proceedings of the 39th International Colloquium on Automata, Languages and Programming (ICALP 2012). Theoretical Computer Science, 2015 .
Abstract:
We give algorithms for the optimization problem: , where is a Hermitian matrix, and the variable is a bipartite separable quantum state. This problem lies at the heart of several problems in quantum computation and information, such as the complexity of QMA(2). While the problem is NPhard, our algorithms are better than brute force for several instances of interest. In particular, they give PSPACE upper bounds on promise problems admitting a QMA(2) protocol in which the verifier performs only logarithmic number of elementary gate on both proofs, as well as the promise problem of deciding if a bipartite local Hamiltonian has large or small ground energy. For , our algorithm runs in time exponential in . While the existence of such an algorithm was first proved recently by Brandao, Christandl and Yard in Proceedings of the 43rd annual ACM Symposium on Theory of Computation , 343–352, 2011, our algorithm is conceptually simpler.
 Parallel approximation of minmax problems with applications to classical and quantum zerosum games

Gus Gutoski and Xiaodi Wu .
Featured talk at the 15th Workshop on Quantum Information Processing (QIP 2012). In the Proceedings of the 27rd Annual IEEE Conference on Computational Complexity (CCC 2012). Computational Complexity, 22(2):385428, 2013, the special issue of CCC 2012.
Abstract:
This paper presents an efficient parallel algorithm for a new class of minmax problems based on the matrix multiplicative weights update method. Our algorithm can be used to find nearoptimal strategies for competitive twoplayer 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 competingprovers complexity classes collapse to PSPACE such as QRG, 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 semidefinite programs whose feasible region consists of tuples of semidefinite matrices that satisfy a ‘‘transcriptlike’’ consistency condition. Applied to this special case, our algorithm yields a direct polynomialspace simulation of multimessage quantum interactive proofs resulting in a firstprinciples proof of QIP=PSPACE.
 Parallelized Solution to Semidefinite Programmings in Quantum Complexity Theory

Xiaodi Wu .
Manuscript, 2010. Note: most of the techniques in this paper are applied and improved in the above paper. However, this paper contains more examples of the applications of such techniques.
Abstract:
In this paper we present an equilibrium value based framework for solving SDPs via the multiplicative weight update method which is different from the one in Kale's thesis [Kale07]. One of the main advantages of the new framework is that we can guarantee the convertibility from approximate to exact feasibility in a much more general class of SDPs than previous result. Another advantage is the design of the oracle which is necessary for applying the multiplicative weight update method is much simplified in the general case. This leads to an alternative and easier solutions to the SDPs used in the previous results QIP(2) PSPACE [JainUW09] and QMAM=PSPACE [JainJUW09]. Furthermore, we provide a generic form of SDPs which can be solved in the similar way. By parallelizing every step in our solution, we are able to solve a class of SDPs in NC. Although our motivation is from quantum computing, our result will also apply to any SDP which satisfies our conditions directly.
In addition to the new framework for solving SDPs, we also provide a novel framework which improves the range of equilibrium value problems that can be solved via the multiplicative weight update method. Before this work we are only able to calculate the equilibrium value where one of the two convex sets needs to be the set of density operators. Our work demonstrates that in the case when one set is the set of density operators with further linear constraints, we are still able to approximate the equilibrium value to high precision via the multiplicative weight update method.
 Equilibrium Value Method for the proof of QIP=PSPACE

Xiaodi Wu .
Manuscript, 2010.
Abstract:
We provide an alternative proof of QIP=PSPACE to the recent breakthrough result [JainJUW09]. Unlike solving some semidefinite program corresponding to the definition of the complexity class, our method starts with one QIPcomplete problem which computes the diamond norm between two admissible quantum channels. The key observation is that we can convert the computation of the diamond norm into the computation of some equilibrium value, which could be interesting for its own sake. The later problem, different from semidefinite programs, is generally more structured and easier to solve. The multiplicative weight update method is also used to solve the equilibrium value problem, however, in a relatively simpler way than the original proof [JainJUW09]. Furthermore, we provide a generalized form of equilibrium value problems which can be solved in the same way as well as comparisons to semidefinite programs.
 NonIdentity Check Remains QMAComplete for Short Circuits

Abstract:
In the NonIdentity Check problem, we are given a quantum circuit as input, and are asked whether it is far away from the identity or not. It is well known that this problem is QMAcomplete [JWB05]. In this note, it is shown that the NonIdentity Check problem remains QMAcomplete for circuits of short depth. Specifically, we prove that for constant depth quantum circuit in which each gate is given to bits of precision, the NonIdentity Check problem is QMAcomplete. It also follows that polylog depth circuit consisting of only gates from any universal gate set is QMAcomplete.
 Exact Quantum Search by Parallel Unitary Discrimination Schemes

(by contribution) Xiaodi Wu and Runyao Duan.
Physical Review A, 78, 012303 (2008). Selected for the July 2008 issue of Virtual Journal of Quantum Information.
 Verifierbased Algorithm for Unsorted Database Search Problem

(by contribution) Xiaodi Wu and Gui Lu Long.
International Journal of Quantum Information, vol.5 no.4, pp 597  604 (2007)
Abstract:
Unsorted database search problem is an important science and engineering problem. We proposed quantum algorithm to solve the problem by dividing the database binarily and then use a probabilistic verifier algorithm to determine if the item is within one part of the divided database. We analyzed the computational complexity of this algorithm, and found that in general, the number of steps is proportional to that in the standard Grover algorithm. However in some cases, it is less than that of the Grover algorithm.
 Data Processing and software realization of wavelengths of spectrum during CCD measurement (in Chinese)

(by contribution) Xiaodi Wu, Yongtao Huang and Xinkun Ma.
Experimental Technology and Management, vol. 24, no. 4 p4851 (2006)
DOI: 10.3969/j.issn.10024956.2007.04.015
