Publications

AI agents are moving from advisory interfaces into systems that execute consequential operations: issuing refunds, reserving scarce inventory, provisioning cloud resources, and initiating financial transfers. These workflows require governance over effects, not only over model outputs. Existing safeguards often decide whether an action is allowed from the information available when the action is requested. For stateful policies, that request-time view may be incomplete: budgets, inventory, approval status, and risk signals can change before the effect occurs, making an earlier authorization or approval stale. This paper studies stateful governance for concurrent agentic systems. We identify stale authorization as the core failure mode and define policy-state serializability, a correctness condition requiring committed effects to be explainable as authorized against the policy state immediately before they occur. We present MasuGate, a runtime architecture that keeps policies as reviewable programs while coordinating the state and effects needed to preserve their decisions. In experiments with a PostgreSQL-backed prototype of MasuGate, the system prevents stale authorizations missed by baselines that pass policy state as ordinary request context, preserves delayed approvals while unrelated work proceeds, keeps policy evolution mostly in policy text rather than trusted provider code, and avoids policy violations in a scripted, LLM-free procurement workflow where agent-governance baselines produce stale authorizations over shared budgets and inventory. More broadly, MasuGate suggests a path for integrating stateful governance boundaries into agent frameworks and provider-backed domains where agents act on shared resources.

Noise flooding is a standard defense against decryption attacks on approximate homomorphic encryption, but its security proof is unusually sensitive to composition. Replacing each of $q$ adaptive decryption answers with a statistically close simulation and applying an ordinary hybrid argument loses linearly in $q$. The cryptographic proof instead accumulates conditional Kullback-Leibler (KL) costs and converts to statistical distance once, giving the parameter-critical square-root loss.

We machine-check this argument using Rocq and SSProve. Given any fully homomorphic encryption scheme that is approximately correct and IND-CPA secure, we formalize a reduction for every $q$-query IND-CPAD adversary and prove $\Pr[\mathsf{IND\text{-}CPAD}_{\mathsf{NF}}^{\mathcal A}=1] \leq \beta_{\mathsf{CPA}}(\mathcal B_{\mathcal A,q}) + \frac{\sqrt{qn}}{2\gamma}.$ where $n$ is the plaintext dimension and $\gamma$ is the flooding-width multiplier. Our proof constructs a new relational program logic over SSProve semantics. Its Pythagorean judgment composes conditional KL budgets without converting them to statistical distance, and a verified trace compiler lifts a local oracle rule to arbitrary adaptive programs with a single final conversion.

We present quOS, a preemptive multitasking operating system for quantum computers. quOS introduces quantum processes, which execute quantum programs in isolation from one another while sharing the same quantum hardware. Because quantum computers lack hardware support for context switching—quantum state cannot be saved and restored due to the no-cloning theorem and measurement-induced collapse. quOS introduces virtual context switching at shot boundaries. On current noisy quantum hardware, quantum programs need to be executed repeatedly to produce a valid result; each repetition is a shot. By preempting execution between shots, QuOS interleaves programs without needing to preserve intermediate quantum state, enabling dynamic multiplexing of quantum hardware and supporting a range of preemptive scheduling policies. A key obstacle to fine-grained multiplexing is the substantial latency incurred by existing hardware when loading and dispatching quantum programs. To address this, we co-design quOS with an FPGA-based quantum control system that reduces loading and dispatch latency by several orders of magnitude, enabling efficient execution in small shot batches and making fine-grained interleaving practical on current hardware. We have implemented quOS and evaluated its performance. Our experimental results on IBM Quantum hardware show that quOS can maintain high utilization and throughput, while providing an order of magnitude lower latency and improved fairness than currently available IBM Quantum infrastructure.

Quantum error-correcting codes (QECCs) sit between noisy quantum hardware and reliable computation, so the code parameters used in practice must be trustworthy. The single number that summarizes a code's strength is its distance, yet certifying a distance lower bound is NP-hard in general, placing it beyond the reach of pen-and-paper proofs as well as direct proof-assistant scripting. As a result, distance values in the literature come either from non-scaling hand proofs, or from unverified solvers that leave a trust gap exactly where the code is supposed to provide a guarantee. We present Lean-QEC, the first Lean 4 formalization of stabilizer-code theory that delivers end-to-end, machine-checked distance certificates at industrial code sizes. Lean-QEC formalizes the linear algebra of qubit states, the Pauli group, stabilizer codes, the binary symplectic representation, classical coding theory, and the CSS and Bivariate Bicycle families. To break the combinatorial barrier, Lean-QEC translates the distance condition into a Boolean satisfiability formula through a verified reduction. The pipeline scales through a BitVec-flattened encoding that replaces Lean's Matrix representation, and an error-location encoding that reduces the variable count from $n$ to $k\lceil \log_2 n\rceil$. With these, we obtain automatically-generated Lean-checked distance proofs for a large range of industrially viable qLDPC codes within the Bivariate Bicycle and Generalized Bicycle families, including [[90, 8, 10]] and [[70, 6, 9]] BB codes, with the formulation scaling up to 144 qubits when performed outside the Lean kernel. The resulting library is reusable and is designed to plug into broader Lean-based efforts toward end-to-end verification of fault-tolerant quantum computation.

Post-training pruning reduces LLM inference cost, but its layer-wise reconstruction problems require solving many row-wise mixed-integer quadratic programs (MIQPs). Existing methods avoid solving these problems directly and instead rely on fast pruning heuristics. We propose QIPrune, a quantum-inspired pruning framework that combines QIHD, a GPU-accelerated MIQP solver, with a progressive reconstruction objective that accounts for activations produced by the progressively pruned model. On toy-scale row-wise instances, QIHD achieves Gurobi-comparable objective values while substantially improving over SparseGPT and Wanda in local reconstruction. At a more practical scale, QIPrune reduces final MSE of the logits across most OPT and LLaMA-family models under both 50% unstructured and 2:4 semi-structured sparsity. Ablations show that solver fidelity and objective alignment are complementary: either component alone is insufficient, while their combination yields the strongest end-to-end reconstruction.

We propose a versatile and efficient algorithmic framework for optimizing fermion-to-qubit mappings by generalizing the idea of randomized block coordinate descent. Our greedy approach, termed Randomized Subsystem Descent, iteratively samples a tractable subsystem from the full Hamiltonian, performs optimization within the subsystem under a given metric, and then reintegrates the updated subsystem into the global operator. Restricting the optimization to a subsystem at each iteration ensures computational efficiency, bypassing the dimensional bottlenecks that usually hinder global search heuristics. We benchmark our algorithm on one- and two-dimensional lattice hopping models, the Hubbard model with up to $16 \times 16$ sites, alongside a collection of molecular electronic-structure Hamiltonians with up to 54 modes and more than 180,000 Pauli strings. Across all benchmarks, our method consistently provides appreciable reduction in (weighted) Pauli weight, suggesting that Randomized Subsystem Descent is a practical and scalable framework for lowering the resource overhead of finding hardware-efficient Hamiltonian encodings.

Non-Hermitian many-body systems can be spectrally unstable, so small perturbations may induce large eigenvalue shifts. The pseudospectrum quantifies this instability and provides a perturbation-robust diagnostic. For inverse-polynomially small $\epsilon$, we show that deciding whether a point $z\in\mathbb{C}$ is $\epsilon$-close to the spectrum is PSPACE-hard for $5$-local operators, whereas deciding whether $z$ lies in the $\epsilon$-pseudospectrum is QMA-complete for $4$-local operators. This identifies pseudospectrum membership as a natural computational target. We then present a concrete end-to-end quantum framework for deciding pseudospectrum membership, which combines a singular-value estimation step with a dissipative state preparation algorithm. Our Quantum Singular-value Gaussian-filtered Search (QSIGS) combines quantum singular value transformation (QSVT) with classical post-processing to achieve Heisenberg-limited query scaling for singular-value estimation. To prepare suitable input states, we introduce an algorithmic Lindbladian protocol for approximate ground right singular vectors and prove its effectiveness for the Hatano--Nelson model. Finally, we demonstrate the full pipeline on a trapped-ion quantum computer and distinguish points inside and outside the target pseudospectrum near the exceptional point of a minimal non-Hermitian qubit model.

Quantum error correction (QEC) is essential for realizing large-scale, fault-tolerant quantum computation, yet its practical implementation remains a major engineering challenge. In particular, QEC demands precise real-time control of a large number of qubits and low-latency, high-throughput and accurate decoding of error syndromes. While most prior work has focused primarily on decoder design, the overall performance of any QEC system depends critically on all its subsystems including control, communication, and decoding, as well as their integration.

To address this challenge, we present an open-source, fully integrated QEC system built on RISC-Q, a generator for RISC-V–based quantum control architectures. Implemented on RFSoC FPGAs, our system prototype integrates real-time qubit control, a scalable distributed multi-board architecture, and the state-of-the-art hardware QEC decoder within a low-latency, high-throughput decoding pipeline, forming a complete hardware platform ready for deployment with superconducting qubits.

Experimental evaluation on a three-board prototype based on AMD ZCU216 RFSoCs demonstrates an end-to-end QEC decoding-feedback latency of 446 ns for a distance-3 surface code, including syndrome aggregation, network communication, syndrome decoding, and error distribution. Extrapolating from measured subsystem performance and state-of-the-art decoder benchmarks, the architecture can achieve sub-microsecond decoding-feedback latency up to a distance-21 surface code ($\sim$881 physical qubits) when scaled to larger hardware configurations.

High-quality, high-rate entanglement generation over quantum links is a requirement for primitives such as quantum teleportation. Here, we define a new optimization framework for maintaining performance in long-distance entanglement distribution based on hardware-level considerations. This framework provides an opportunity to surpass state-of-the-art quantum link performance through software-based techniques, potentially by orders of magnitude over the currently accepted standard practices.

We apply our framework to develop a link control protocol and evaluate it using data from a 62km over-air fiber. In the face of significant time-varying noise, our protocol compensates by adaptively tuning hardware-level parameters and using control-theoretic decision processes to apply those adjustments effectively.

We employ trace-driven simulations to demonstrate the efficacy of our adaptation scheme, and our results indicate that our link control protocol performs within 85% of an unrealistic "optimal'' deployment operating over a perfectly noiseless system.

Transport phenomena play a key role in a variety of application domains, and efficient simulation of these dynamics remains an outstanding challenge. While quantum computers offer potential for significant speedups, existing algorithms either lack rigorous theoretical guarantees or demand substantial quantum resources, preventing scalable and efficient validation on realistic quantum hardware. To address this gap, we develop a comprehensive framework for simulating classes of transport equations, offering both rigorous theoretical guarantees -- including exponential speedups in specific cases -- and a systematic, hardware-efficient implementation. Central to our approach is the Hamiltonian embedding technique, a white-box approach for end-to-end simulation of sparse Hamiltonians that avoids abstract query models and retains near-optimal asymptotic complexity. Empirical resource estimates indicate that our approach can yield an order-of-magnitude (e.g., $42\times$) reduction in circuit depth given favorable problem structures. We then apply our framework to solve linear and nonlinear transport PDEs, including the first experimental demonstration of a 2D advection equation on a trapped-ion quantum computer.

Quantum computing is entering a period in which progress will be shaped as much by advances in computer science as by improvements in hardware. The central thesis of this report is that early fault-tolerant quantum computing shifts many of the primary bottlenecks from device physics alone to computer-science-driven system design, integration, and evaluation. While large-scale, fully fault-tolerant quantum computers remain a long-term objective, near- and medium-term systems will support early fault-tolerant computation with small numbers of logical qubits and tight constraints on error rates, connectivity, latency, and classical control. How effectively such systems can be used will depend on advances across algorithms, error correction, software, and architecture. This report identifies key research challenges for computer scientists and organizes them around these four areas, each centered on a fundamental question.

We introduce a protocol that modifies dynamical decoupling (DD) sequences to be robust to static $ZZ$ crosstalk when implemented with bounded control on 2-colorable qubit topologies. The protocol, which relies on modifications of the pulse timing, can be applied to any sequence with equidistant $\pi$ pulses. We motivate the method using suppression conditions identified through time-dependent perturbation theory. Theoretical findings are supported by demonstrations of widely studied sequences on several superconducting qubit devices offered by the IBM Quantum Platform. Using up to 20 qubits on fixed-coupler devices, we observe an at least 3 times improvement in the fidelity decay rate via our approach when compared with nonrobust DD variants. In addition, we leverage our approach to assess the impact of $ZZ$ errors on tunable-coupler devices. We find that $ZZ$-robust sequences perform nearly equivalently to nonrobust DD, affirming the reduced impact of such errors in a tunable-coupler architecture. Nevertheless, our demonstrations indicate that fixed-coupler devices, when subject to DD protection, can outperform tunable-coupler devices. Our method broadens the scope of practical DD protocols: with modest overhead and a reasonable constraint on the qubit topology, the method attains significant performance improvements on modern quantum computing devices.

Quantum computing imposes stringent requirements for the precise control of large-scale qubit systems, including, for example, microsecond-latency feedback and nanosecond-precision timing of gigahertz signals – demands that far exceed the capabilities of conventional real-time systems. The rapidly evolving and highly diverse nature of quantum control necessitates the development of specialized hardware accelerators. While a few custom real-time systems have been developed to meet the tight timing constraints of specific quantum platforms, they face major challenges in scaling and adapting to increasingly complex control demands – largely due to fragmented toolchains and limited support for design automation.

To address these limitations, we present RISC-Q – an open-source flexible generator for Quantum Control System-on-Chip (QCSoC) designs, featuring a programming interface compatible with the RISC-V ecosystem. Developed using SpinalHDL, RISC-Q enables efficient automation of highly parameterized and modular QCSoC architectures, supporting agile and iterative development to meet the evolving demands of quantum control. We demonstrate that RISC-Q can surpass the performance of existing QCSoCs with significantly reduced development effort, facilitating efficient exploration of the hardware-software co-design space for rapid prototyping and customization.

Hamiltonian learning is a cornerstone for advancing accurate many-body simulations, improving quantum device performance, and enabling quantum-enhanced sensing. Existing readily deployable quantum metrology techniques primarily focus on achieving Heisenberg-limited precision in one- or two-qubit systems. In contrast, general Hamiltonian learning theories address broader classes of unknown Hamiltonian models but are highly inefficient due to the absence of prior knowledge about the Hamiltonian. There remains a lack of efficient and practically realizable Hamiltonian learning algorithms that directly exploit the known structure and prior information of the Hamiltonian, which are typically available for a given quantum computing platform. In this work, we present the first Hamiltonian learning algorithm that achieves both Cramer-Rao lower bound saturated optimal precision and robustness to realistic noise, while exploiting device structure for quadratic reduction in experimental cost for fully connected Hamiltonians. Moreover, this approach enables simultaneous in-situ estimation of all Hamiltonian parameters without requiring the decoupling of non-learnable interactions during the same experiment, thereby allowing comprehensive characterization of the system's intrinsic contextual errors. Notably, our algorithm does not require deep circuits and remains robust against both depolarizing noise and time-dependent coherent errors. We demonstrate its effectiveness with a detailed experimental proposal along with supporting numerical simulations on Rydberg atom quantum simulators, showcasing its potential for high-precision Hamiltonian learning in the NISQ era.

We demonstrate provable (sub)exponential quantum speedups in both discrete and continuous optimization, achieved through simple and natural quantum optimization algorithms, namely the quantum adiabatic algorithm for discrete optimization and quantum Hamiltonian descent for continuous optimization. Our result builds on the Gilyén–Hastings–Vazirani (sub)exponential oracle separation for adiabatic quantum computing. With a sequence of perturbative reductions, we compile their construction into two standalone objective functions, whose oracles can be directly leveraged by the plain adiabatic evolution and Schrödinger operator evolution for discrete and continuous optimization, respectively.

Non-smooth optimization models play a fundamental role in various disciplines, including engineering, science, management, and finance. However, classical algorithms for solving such models often struggle with convergence speed, scalability, and parameter tuning, particularly in high-dimensional and non-convex settings. In this paper, we explore how quantum mechanics can be leveraged to overcome these limitations. Specifically, we investigate the theoretical properties of the Quantum Hamiltonian Descent (QHD) algorithm for non-smooth optimization in both continuous and discrete time. First, we propose continuous-time variants of the general QHD algorithm and establish their global convergence and convergence rate for non-smooth convex and strongly convex problems through a novel Lyapunov function design. Furthermore, we prove the finite-time global convergence of continuous-time QHD for non-smooth non-convex problems under mild conditions (i.e., locally Lipschitz). In addition, we propose discrete-time QHD, a fully digitized implementation of QHD via operator splitting (i.e., product formula). We find that discrete-time QHD exhibits similar convergence properties even with large time steps. Finally, numerical experiments validate our theoretical findings and demonstrate the computational advantages of QHD over classical non-smooth non-convex optimization algorithms.

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

Many promising quantum applications depend on the efficient quantum simulation of an exponentially large sparse Hamiltonian, a task known as sparse Hamiltonian simulation, which is fundamentally important in quantum computation. Although several theoretically appealing quantum algorithms have been proposed for this task, they typically require a black-box query model of the sparse Hamiltonian, rendering them impractical for near-term implementation on quantum devices.

In this paper, we propose a technique named $\textit{Hamiltonian embedding}$. This technique simulates a desired sparse Hamiltonian by embedding it into the evolution of a larger and more structured quantum system, allowing for more efficient simulation through hardware-efficient operations. We conduct a systematic study of this new technique and demonstrate significant savings in computational resources for implementing prominent quantum applications. As a result, we can now experimentally realize quantum walks on complicated graphs (e.g., binary trees, glued-tree graphs), quantum spatial search, and the simulation of real-space Schrödinger equations on current trapped-ion and neutral-atom platforms. Given the fundamental role of Hamiltonian evolution in the design of quantum algorithms, our technique markedly expands the horizon of implementable quantum advantages in the NISQ era.

Large-scale non-convex optimization problems, often involving mixed-integer variables, arise naturally in domains such as finance and medical imaging. Conventional CPU-based solvers rely on sequential decision-making, which limits their ability to leverage modern hardware accelerators like GPUs. Motivated by recent advances in quantum optimization, particularly Quantum Hamiltonian Descent (QHD), we introduce Quantum-Inspired Hamiltonian Descent (QIHD), a family of algorithms designed for efficient large-scale optimization on GPU clusters. QIHD reformulates optimization tasks as classical dynamical systems and exploits massively parallel GPU simulations to accelerate computation. Despite being classical, QIHD inherits distinctive QHD-like properties—such as tunneling—and demonstrates similar empirical behavior. We provide a scalable GPU implementation in JAX for mixed-integer quadratic programming (MIQP) problems, capable of handling millions of nonzero elements within seconds. Extensive benchmarks on large-scale MIQP problems show that QIHD consistently outperforms the state-of-the-art CPU-based solver Gurobi when time budgets are limited, highlighting its potential as a practical and scalable optimization framework.

This paper develops a model of quantum behavior that is intended to support the abstract yet accurate design and functional verification of quantum communication protocols. The work is motivated by the need for conceptual tools for the development of quantum-communication systems that are usable by non-specialists in quantum physics while also correctly capturing at a useful abstraction the underlying quantum phenomena. Our approach involves defining a quantum abstract machine (QAM) whose operations correspond to well-known quantum circuits; these operations, however, are given direct abstract semantics in a style similar to that of Berry's and Boudol's Chemical Abstract Machine. This paper defines the QAM's semantics and shows via examples how it may be used to model and reason about existing quantum communication protocols.

Computational models are an essential tool for the design, characterization, and discovery of novel materials. Hard computational tasks in materials science stretch the limits of existing high-performance supercomputing centers, consuming much of their simulation, analysis, and data resources. Quantum computing, on the other hand, is an emerging technology with the potential to accelerate many of the computational tasks needed for materials science. In order to do that, the quantum technology must interact with conventional high-performance computing in several ways: approximate results validation, identification of hard problems, and synergies in quantum-centric supercomputing. In this paper, we provide a perspective on how quantum-centric supercomputing can help address critical computational problems in materials science, the challenges to face in order to solve representative use cases, and new suggested directions.

Achieving noise resilience is an outstanding challenge in Hamiltonian-based quantum computation. To this end, energy-gap protection provides a promising approach, where the desired quantum dynamics are encoded into the ground space of a penalty Hamiltonian that suppresses unwanted noise processes. However, existing approaches either explicitly require high-weight penalty terms that are not directly accessible in current hardware, or utilize non-commuting $2$-local Hamiltonians, which typically leads to an exponentially small energy gap. In this work, we provide a general recipe for designing error-resilient Hamiltonian simulations, making use of an excited encoding subspace stabilized by solely $2$-local commuting Hamiltonians. Our results thus overcome a no-go theorem previously derived for ground-space encoding that prevents noise suppression schemes with such Hamiltonians. Importantly, our method is scalable as it only requires penalty terms that scale polynomially with system size. To illustrate the utility of our approach, we further apply this method to a variety of $1$- and $2$-dimensional many-body spin models, potentially extending the duration of high-fidelity simulation by orders of magnitude in current hardware.

We study computational problems related to the Schrödinger operator $H = -\Delta + V$ in the real space under the condition that (i) the potential function $V$ is smooth and has its value and derivative bounded within some polynomial of $n$ and (ii) $V$ only consists of $O(1)$-body interactions. We prove that (i) simulating the dynamics generated by the Schrödinger operator implements universal quantum computation, i.e., it is BQP-hard, and (ii) estimating the ground energy of the Schrödinger operator is as hard as estimating that of local Hamiltonians with no sign problem (a.k.a. stoquastic Hamiltonians), i.e., it is StoqMA-complete. This result is particularly intriguing because the ground energy problem for general bosonic Hamiltonians is known to be QMA-hard and it is widely believed that $\texttt{StoqMA}\varsubsetneq \texttt{QMA}$.

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

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

Quantum reservoir computing (QRC) has been proposed as a paradigm for performing machine learning with quantum processors where the training takes place in the classical domain, avoiding the issue of barren plateaus in parameterized-circuit quantum neural networks. It is natural to consider using a quantum processor based on microwave superconducting circuits to classify microwave signals that are analog—continuous in time. However, while there have been theoretical proposals of analog QRC, to date QRC has been implemented using the circuit model—imposing a discretization of the incoming signal in time. In this paper we show how a quantum superconducting circuit comprising an oscillator coupled to a qubit can be used as an analog quantum reservoir for a variety of classification tasks, achieving high accuracy on all of them. Our work demonstrates processing of ultra-low-power microwave signals within our superconducting circuit, a step towards achieving a quantum sensing-computational advantage on impinging microwave signals.

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

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

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

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

In this paper, we identify a family of nonconvex continuous optimization instances, each $d$-dimensional instance with $2^d$ local minima, to demonstrate a quantum-classical performance separation. Specifically, we prove that the recently proposed Quantum Hamiltonian Descent (QHD) algorithm [Leng et al., arXiv:2303.01471] is able to solve any $d$-dimensional instance from this family using $\widetilde{\mathcal{O}}(d^3)$ quantum queries to the function value and $\widetilde{\mathcal{O}}(d^4)$ additional 1-qubit and 2-qubit elementary quantum gates. On the other side, a comprehensive empirical study suggests that representative state-of-the-art classical optimization algorithms/solvers (including Gurobi) would require a super-polynomial time to solve such optimization instances.

We propose a novel quantum algorithm for solving linear optimization problems by quantum-mechanical simulation of the central path. While interior point methods follow the central path with an iterative algorithm that works with successive linearizations of the perturbed KKT conditions, we perform a single simulation working directly with the nonlinear complementarity equations. This approach yields an algorithm for solving linear optimization problems involving $m$ constraints and $n$ variables to $\varepsilon$-optimality using $\mathcal{O} \left( \sqrt{m + n} \frac{R_{1}}{\varepsilon}\right)$ queries to an oracle that evaluates a potential function, where $R_{1}$ is an $\ell_{1}$-norm upper bound on the size of the optimal solution. In the standard gate model (i.e., without access to quantum RAM) our algorithm can obtain highly-precise solutions to LO problems using at most $\mathcal{O} \left( \sqrt{m + n} \textsf{nnz} (A) \frac{R_1}{\varepsilon}\right)$ elementary gates, where $\textsf{nnz} (A)$ is the total number of non-zero elements found in the constraint matrix.

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 Fiat-Shamir with aborts paradigm, including Dilithium. The gap lies in the CMA-to-NMA 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 CMA-to-NMA 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 CMA-security of Dilithium in the EasyCrypt proof assistant. Our formalization includes several new tools and techniques of independent interest for future formal verification results.

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 experimentally-motivated 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 coarse-grained 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. 

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

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 continuous-time limit of classical gradient descent algorithms, as a truly quantum counterpart of classical gradient methods where the contribution from classically-prohibited trajectories can significantly boost QHD's performance for non-convex optimization. Moreover, QHD is described as a Hamiltonian evolution efficiently simulatable on both digital and analog quantum computers. By embedding the dynamics of QHD into the evolution of the so-called Quantum Ising Machine (including D-Wave and others), we empirically observe that the D-Wave-implemented QHD outperforms a selection of state-of-the-art gradient-based classical solvers and the standard quantum adiabatic algorithm, based on the time-to-solution metric, on non-convex constrained quadratic programming instances up to 75 dimensions. Finally, we propose a "three-phase picture" to explain the behavior of QHD, especially its difference from the quantum adiabatic algorithm.

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

Quantum computing technology may soon deliver revolutionary improvements in algorithmic performance, but it is useful only if computed answers are correct. While hardware-level 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 the 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 high-assurance 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 a formally certified end-to-end implementation of Shor’s prime factorization algorithm, developed as part of a framework for applying the certified approach to general applications. By leveraging our framework, one can significantly reduce the effects of human errors and obtain a high-assurance implementation of large-scale quantum applications in a principled way.

Near-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).

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

Estimating 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 $\epsilon$ using $\tilde{O}(n^{3}+n^{2.5}/\epsilon)$ queries to a membership oracle and $\tilde{O}(n^{5}+n^{4.5}/\epsilon)$ additional arithmetic operations. For comparison, the best known classical algorithm uses $\tilde{O}(n^{3.5}+n^{3}/\epsilon^{2})$ queries and $\tilde{O}(n^{5.5}+n^{5}/\epsilon^{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 $\Omega(\sqrt n+1/\epsilon)$ quantum membership queries, which rules out the possibility of exponential quantum speedup in $n$ and shows optimality of our algorithm in $1/\epsilon$ up to poly-logarithmic factors.

The Variational Quantum Eigensolver (VQE) is a promising candidate for quantum applications on near-term Noisy Intermediate-Scale Quantum (NISQ) computers. Despite a lot of empirical studies and recent progress in theoretical understanding of 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 over-parameterization regime. By connecting the training dynamics with the Riemannian Gradient Flow on the unit-sphere, 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 ansatz-dependent threshold paralleling our main result. We showcase that our ansatz-dependent 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.

We 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 orders of magnitude.

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

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

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 quantum sampling problems (denoted by SampBQP). More precisely, in a CVQC protocol for a SampBQP problem, the prover and the verifier are given an input $x\in \{0,1\}^n$ and a quantum circuit $C$, and the goal of the classical client is to learn a sample from the output $z \leftarrow C(x)$ up to a small error, from its interaction with an untrusted prover. We demonstrate its feasibility by constructing a four-message 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. We provide a simple yet powerful generic compiler that transforms any CVQC protocol to a blind one while preserving its completeness and soundness errors as well as the number of rounds. Applying our compiler to (a parallel repetition of) Mahadev's CVQC protocol for BQP and our CVQC protocol for SampBQP yields the first constant-round blind CVQC protocol for BQP and SampBQP respectively, with negligible and inverse polynomial soundness errors respectively, and negligible completeness errors.

This abstract presents recent extensions to voqc, a verified optimizer for quantum circuits, first presented at POPL 2021 [Hietala et al. 2021b]. All code described in this abstract is freely available online.

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

Quantum Neural Networks (QNNs) have been proposed as a variational method to realize a quantum advantage on near-term 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 real-valued 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 variable-depth ReNNs can be provably advantageous in expressing families of univariate and multivariate functions, while conversely QNNs have provable advantages over ReNNs of depth-2 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.

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

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 how-ever 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 circuit-based 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 off-the-shelf tools. It is worth noting that our construction is highly extensible and can be easily adjusted for specific supremacy tasks and experimental platforms.

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

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

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

Limited quantum memory is one of the most important constraints for near-term quantum devices. Understanding whether a small quantum computer can simulate a larger quantum system, or execute an algorithm requiring more qubits than available, is both of theoretical and practical importance. In this Letter, we introduce cluster parameters $K$ and $d$ of a quantum circuit. The tensor network of such a circuit can be decomposed into clusters of size at most $d$ with at most $K$ qubits of inter-cluster quantum communication. We propose a cluster simulation scheme that can simulate any $(K,d)$-clustered quantum circuit on a $d$-qubit machine in time roughly $2^{O(K)}$, with further speedups possible when taking more fine-grained circuit structure into account. We show how our scheme can be used to simulate clustered quantum systems -- such as large molecules -- that can be partitioned into multiple significantly smaller clusters with weak interactions among them. By using a suitable clustered ansatz, we also experimentally demonstrate that a quantum variational eigensolver can still achieve the desired performance for estimating the energy of the BeH$_2$ molecule while running on a physical quantum device with half the number of required qubits.

While recent work suggests that quantum computers can speed up the solution of semidefinite programs, little is known about the quantum complexity of more general convex optimization. We present a quantum algorithm that can optimize a convex function over an $n$-dimensional convex body using $\tilde{O}(n)$ queries to oracles that evaluate the objective function and determine membership in the convex body. This represents a quadratic improvement over the best-known classical algorithm. We also study limitations on the power of quantum computers for general convex optimization, showing that it requires $\tilde{\Omega}(\sqrt{n})$ evaluation queries and $\Omega(\sqrt{n})$ membership queries.

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 Choi-Jamioł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 sub-programs 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 Repeat-Until-Success, with a huge numerical advantage over the previous SDP approach.

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

We present sqire, a low-level 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.

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

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 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 $\epsilon$-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.

We 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 $\tilde{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 \approx 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 $\tilde{O}(\sqrt{m}+\mathrm{poly}(r))\cdot\mathrm{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}\cdot\mathrm{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.

Estimation of Shannon and Ré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 on 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 $\alpha$-Rényi entropies (Shannon entropy being 1-Renyi entropy). In particular, we demonstrate a quadratic quantum speedup for Shannon entropy estimation and a generic quantum speedup for $\alpha$-Rényi entropy estimation for all $\alpha\geq 0$, including a tight bound for the collision-entropy (2-Rényi entropy). We also provide quantum upper bounds for extreme cases such as the Hartley entropy (i.e., the logarithm of the support size of a distribution, corresponding to $\alpha=0$) and the min-entropy case (i.e., $\alpha=+\infty$), as well as the Kullback-Leibler divergence between two distributions. Moreover, we complement our results with quantum lower bounds on $\alpha$-Rényi entropy estimation for all $\alpha\geq 0$.

Semidefinite programs (SDPs) are a framework for exact or approximate optimization that have widespread application in quantum information theory. We introduce a new method for using reductions to construct integrality gaps for SDPs. These are based on new limitations on the sum-of-squares (SoS) hierarchy in approximating two particularly important sets in quantum information theory, where previously no $\omega(1)$-round integrality gaps were known: the set of separable (i.e. unentangled) states, or equivalently, the $2 \rightarrow 4$ norm of a matrix, and the set of quantum correlations; i.e. conditional probability distributions achievable with local measurements on a shared entangled state. In both cases no-go theorems were previously known based on computational assumptions such as the Exponential Time Hypothesis (ETH) which asserts that 3-SAT 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 Lee-Raghavendra-Steurer (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 Watrous and Aaronson et al. These results can be viewed as limitations on the monogamy principle, the PPT test, the ability of Tsirelson-type bounds to restrict quantum correlations, as well as the SDP hierarchies of Doherty-Parrilo-Spedalieri, Navascues-Pironio-Acin and Berta-Fawzi-Scholz.

In this note we show that the Raz-McKenzie simulation algorithm which lifts deterministic query lower bounds to deterministic communication lower bounds can be implemented for functions $f$ composed with the Inner Product gadget $g_{IP}(x,y) = \sum_i x_iy_i \mathrm{mod} \, 2$ of logarithmic size. In other words, given a function $f: \{0,1\}^n \to \{0,1\}$ with deterministic query complexity $D(f)$, we show that the deterministic communication complexity of the composed function $f \circ g_{IP}^n$ is $\Theta( D(f) \log n)$, where $f \circ g_{IP}^n (x,y) = f( g_{IP}(x^1,y^1),\ldots,g_{IP}(x^n,y^n))$ where $x = (x^1,\ldots,x^n)$, $y = (y^1,\ldots,y^n)$ and each $x^i$ and $y^i$ are $O(\log n)$ bit strings. In [Raz, McKenzie FOCS 1997] and [Göös, et al. FOCS 2015], the simulation algorithm is implemented for functions composed with the Indexing gadget, where the size of the gadget is polynomial in the input length of the outer function $f$.

We initiate the study of computational entropy in the quantum setting. We investigate to what extent the classical notions of computational entropy generalize to the quantum setting, and whether quantum analogues of classical theorems hold. Our main results are as follows. (1) The classical Leakage Chain Rule for pseudoentropy can be extended to the case that the leakage information is quantum (while the source remains classical). Specifically, if the source has pseudoentropy at least $k$, then it has pseudoentropy at least $k-\ell$ conditioned on an $\ell$-qubit leakage. (2) As an application of the Leakage Chain Rule, we construct the first quantum leakage-resilient stream-cipher in the bounded-quantum-storage model, assuming the existence of a quantum-secure pseudorandom generator. (3) We show that the general form of the classical Dense Model Theorem (interpreted as the equivalence between two definitions of pseudo-relative-min-entropy) does not extend to quantum states. Along the way, we develop quantum analogues of some classical techniques (e.g. the Leakage Simulation Lemma, which is proven by a Non-uniform Min-Max Theorem or Boosting). On the other hand, we also identify some classical techniques (e.g. Gap Amplification) that do not work in the quantum setting. Moreover, we introduce a variety of notions that combine quantum information and quantum complexity, and this raises several directions for future work.

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 non-signaling min-entropy, tolerates a constant amount of device imperfection, and the security is against an all-powerful non-signaling adversary. Unlike the previous works proving non-signaling 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): ‘‘[e]ither 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 non-signaling, adversary.

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 Łukasiewicz implication and the Gödel 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 optimising 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.

It 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 $\epsilon$ in trace distance required $O(dr^2/\epsilon^2)$ copies for a $d$-dimensional density matrix of rank $r$. Here, we give a theoretical measurement scheme (POVM) that requires $O (dr/ \delta ) \ln (d/\delta)$ copies of $\rho$ to error $\delta$ in infidelity, and a matching lower bound up to logarithmic factors. This implies $O( (dr / \epsilon^2) \ln (d/\epsilon) )$ copies suffice to achieve error $\epsilon$ in trace distance. We also prove that for independent (product) measurements, $\Omega(dr^2/\delta^2) / \ln(1/\delta)$ copies are necessary in order to achieve error $\delta$ in infidelity. For fixed $d$, our measurement can be implemented on a quantum computer in time polynomial in $n$.

We present a stronger version of the Doherty-Parrilo-Spedalieri (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.

Nash 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 were 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.

We obtain optimal bounds for the problem of conveying classical messages by communication between a sender and a receiver who can utilize non-local correlations obeying the Non-Signaling Principle. These include correlations arising from quantum entanglement, but also include ‘‘super-quantum’’ 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).

We 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 - \epsilon$, the $n$-fold repetition of $G$ has entangled value $\mathrm{val}^*(G^{\otimes n})$ at most $(1 - \epsilon^{3/2})^{\Omega(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 - \epsilon^2)^{\Omega(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 - \epsilon^2)^{\Omega(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: in particular, our first theorem crucially uses a quantum search protocol by Aaronson and Ambainis, which gives a quadratic Grover 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.

We give algorithms for the optimization problem: $\max_\rho \langle Q,\rho\rangle$, where $Q$ is a Hermitian matrix, and the variable $\rho$ 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 NP-hard, 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 $Q\ge0$, our algorithm runs in time exponential in $\|Q\|_F$. While the existence of such an algorithm was first proved recently by Brandão, Christandl and Yard [Proceedings of the 43rd annual ACM Symposium on Theory of Computation, 343--352, 2011], our algorithm is conceptually simpler.

We study the problem of constructing multi-source extractors in the quantum setting, which extract almost uniform random bits against quantum side information collected from several initially independent classical random sources. This is a natural generalization of seeded randomness extraction against quantum side information and classical independent source extraction. With new challenges such as potential entanglement in the side information, it is not a prior clear under what conditions do quantum multi-source extractors exist; the only previous work is [KK12], where the classical inner-product two-source 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 GE-secure quantum multi-source extractors. To that end, we propose another model called One-sided Adversary (OA) Model, which is weaker than all the above models. Somewhat surprisingly, we establish equivalence between strong OA-security and strong GE-security. As a result, all classical multi-source 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 multi-source extractors. We also apply our techniques to two important problems in cryptography and distributed computing --- privacy amplification and network extractor. We show that as long as the sources have certain amounts of conditional min-entropy in our GE model (even with entangled quantum side information), we can design very efficient privacy amplification protocols and network extractors.

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 near-uniform output, with a close-to-optimal error, secure against all-powerful 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 untrusted-device protocols. It implies that unbounded randomness expansion can be achieved simply by cross-feeding 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.

An important discovery in quantum information processing is that quantum one-way communication protocols can be exponentially more efficient than classical protocols. Those extraordinary quantum advantages were demonstrated through the Hidden Matching Problem and its variants, where the underlying basic task is to determine the parity of some $k=2$ bits of an $n$-bit string. We prove that for larger values of $k$, the quantum complexities of those problems increase exponentially from $O(\log n)$ to $\Omega(n^{1-2/k})$, which is almost tight and renders any super-polynomial quantum-classical gaps impossible. Our results also rule out a ‘‘quantum argument’’, in the sense of Kerenidis and de Wolf (Journal of Computer and System Sciences, 69(3)395–420, 2004), for proving any super-polynomial lower bound on Locally Decodable Codes for more than $2$ queries. Our proofs are new applications of the matrix Hypercontractive Inequality developed by Ben-Aroya, Regev, and de Wolf (FOCS 2008).

This paper presents an efficient parallel approximation scheme for a new class of min-max problems. The algorithm is derived from the matrix multiplicative weights update method and can be used to find near-optimal strategies for competitive two-party classical or quantum interactions in which a referee exchanges any number of messages with one party followed by any number of additional messages with the other. It considerably extends the class of interactions which admit parallel solutions, demonstrating for the first time the existence of a parallel algorithm for an interaction in which one party 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 specific class of semidefinite programs whose feasible region consists of lists of semidefinite 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.

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 general cases. This leads to an alternative and easier solutions to the SDPs used in the previous results QIP(2)$\subseteq$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 directly to any SDP which satisfies our conditions. 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.

We provide an alternative proof of QIP=PSPACE to the recent breakthrough result. Unlike solving some semidefinite programs that captures the computational power of quantum interactive proofs, our method starts with one QIP-Complete 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. The later problem, different from the former semidefinite programs, is of better form, easier to solve and could be interesting for its own sake. The multiplicative weight update method is also applied to solve the equilibrium value problem, however, in a relatively simpler way than the one in the original proof. As a direct byproduct, we also provide a NC algorithm to compute the diamond norm of a class of quantum channels. Furthermore, we provide a generalized form of equilibrium value problems that can be solved in the same way as well as comparisons to semidefinite programs.

The Non-Identity Check problem asks whether a given a quantum circuit is far away from the identity or not. It is well known that this problem is QMA-Complete [JWB05]. In this note, it is shown that the Non-Identity Check problem remains QMA-Complete for circuits of short depth. Specifically, we prove that for constant depth quantum circuit in which each gate is given to at least $\Omega(\log n)$ bits of precision, the Non-Identity Check problem is QMA-Complete. It also follows that the hardness of the problem remains for polylogarithmic depth circuit consisting of only gates from any universal gate set and for logarithmic depth circuit using some specific universal gate set.

We study the unsorted database search problem with items $N$ from the viewpoint of unitary discrimination. Instead of considering the famous $O(\sqrt{N})$ Grover's the bounded-error algorithm for the original problem, we seek for the results about the exact algorithms, i.e. the ones succeed with certainty. Under the standard oracle model $\sum_j (-1)^{\delta_{\tau j}}|j\rangle\langle j|$, we demonstrate a tight lower bound $\frac{2}{3}N+o(N)$ of the number of queries for any parallel scheme with unentangled input states. With the assistance of entanglement, we obtain a general lower bound $\frac{1}{2}(N-\sqrt{N})$. We provide concrete examples to illustrate our results. In particular, we show that the case of $N=6$ can be solved exactly with only two queries by using a bipartite entangled input state. Our results indicate that in the standard oracle model the complexity of exact quantum search with one unique solution can be strictly less than that of the calculation of OR function.

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.