Showing 1–50 of 78 results for author: Ying, M

Deep Learning-based Joint Channel Prediction and Multibeam Precoding for LEO Satellite Internet of Things

Authors: Ming Ying, Xiaoming Chen, Qiao Qi, Wolfgang Gerstacker

Abstract: Low earth orbit (LEO) satellite internet of things (IoT) is a promising way achieving global Internet of Everything, and thus has been widely recognized as an important component of sixth-generation (6G) wireless networks. Yet, due to high-speed movement of the LEO satellite, it is challenging to acquire timely channel state information (CSI) and design effective multibeam precoding for various Io… ▽ More Low earth orbit (LEO) satellite internet of things (IoT) is a promising way achieving global Internet of Everything, and thus has been widely recognized as an important component of sixth-generation (6G) wireless networks. Yet, due to high-speed movement of the LEO satellite, it is challenging to acquire timely channel state information (CSI) and design effective multibeam precoding for various IoT applications. To this end, this paper provides a deep learning (DL)-based joint channel prediction and multibeam precoding scheme under adverse environments, e.g., high Doppler shift, long propagation delay, and low satellite payload. {Specifically, this paper first designs a DL-based channel prediction scheme by using convolutional neural networks (CNN) and long short term memory (LSTM), which predicts the CSI of current time slot according to that of previous time slots. With the predicted CSI, this paper designs a DL-based robust multibeam precoding scheme by using a channel augmentation method based on variational auto-encoder (VAE).} Finally, extensive simulation results confirm the effectiveness and robustness of the proposed scheme in LEO satellite IoT. △ Less

Submitted 27 May, 2024; originally announced May 2024.

Comments: IEEE Transactions on Wireless Communications, 2024

Waste Factor and Waste Figure: A Unified Theory for Modeling and Analyzing Wasted Power in Radio Access Networks for Improved Sustainability

Authors: Theodore S. Rappaport, Mingjun Ying, Nicola Piovesan, Antonio De Domenico, Dipankar Shakya

Abstract: This paper introduces Waste Factor (W), also denoted as Waste Figure (WF) in dB, a promising new metric for quantifying energy efficiency in a wide range of circuits and systems applications, including data centers and RANs. Also, the networks used to connect data centers and AI computing engines with users for ML applications must become more power efficient. This paper illustrates the limitation… ▽ More This paper introduces Waste Factor (W), also denoted as Waste Figure (WF) in dB, a promising new metric for quantifying energy efficiency in a wide range of circuits and systems applications, including data centers and RANs. Also, the networks used to connect data centers and AI computing engines with users for ML applications must become more power efficient. This paper illustrates the limitations of existing energy efficiency metrics that inadequately capture the intricate energy dynamics of RAN components. We delineate the methodology for applying W across various network configurations, including MISO, SIMO, and MIMO systems, and demonstrate the effectiveness of W in identifying energy optimization opportunities. Our findings reveal that W not only offers nuanced insights into the energy performance of RANs but also facilitates informed decision-making for network design and operational efficiency. Furthermore, we show how W can be integrated with other KPIs to guide the development of optimal strategies for enhancing network energy efficiency under different operational conditions. Additionally, we present simulation results for a distributed multi-user MIMO system at 3.5, 17, and 28 GHz, demonstrating overall network power efficiency on a per square kilometer basis, and show how overall W decreases with an increasing number of base stations and increasing carrier frequency. This paper shows that adopting W as a figure of merit can significantly contribute to the sustainability and energy optimization of next-generation wireless communication networks, paving the way for greener and more sustainable, energy-efficient 5G and 6G technologies. △ Less

Submitted 13 May, 2024; originally announced May 2024.

Comments: 26 pages, 21 figures, 5 tables

Using Waste Factor to Optimize Energy Efficiency in Multiple-Input Single-Output (MISO) and Multiple-Input Multiple-Output (MIMO) Systems

Authors: Mingjun Ying, Dipankar Shakya, Theodore S. Rappaport

Abstract: This paper introduces Waste Factor (W) and Waste Figure (WF) to assess power efficiency in any multiple-input multiple-output (MIMO) or single-input multiple-output (SIMO) or multiple-input single-output (MISO) cascaded communication system. This paper builds upon the new theory of Waste Factor, which systematically models added wasted power in any cascade for parallel systems such as MISO, SIMO,… ▽ More This paper introduces Waste Factor (W) and Waste Figure (WF) to assess power efficiency in any multiple-input multiple-output (MIMO) or single-input multiple-output (SIMO) or multiple-input single-output (MISO) cascaded communication system. This paper builds upon the new theory of Waste Factor, which systematically models added wasted power in any cascade for parallel systems such as MISO, SIMO, and MIMO systems, which are prevalent in current wireless networks. Here, we also show the advantage of W compared to conventional metrics for quantifying and analyzing energy efficiency. This work explores the utility of W in assessing energy efficiency in communication channels, within Radio Access Networks (RANs). △ Less

Submitted 2 May, 2024; originally announced May 2024.

Comments: 6 pages, 6 figures

Atomicity in Distributed Quantum Computing

Authors: Zhicheng Zhang, Mingsheng Ying

Abstract: Atomicity is a ubiquitous assumption in distributed computing, under which actions are indivisible and appear sequential. In classical computing, this assumption has several theoretical and practical guarantees. In quantum computing, although atomicity is still commonly assumed, it has not been seriously studied, and a rigorous basis for it is missing. Classical results on atomicity do not directl… ▽ More Atomicity is a ubiquitous assumption in distributed computing, under which actions are indivisible and appear sequential. In classical computing, this assumption has several theoretical and practical guarantees. In quantum computing, although atomicity is still commonly assumed, it has not been seriously studied, and a rigorous basis for it is missing. Classical results on atomicity do not directly carry over to distributed quantum computing, due to new challenges caused by quantum entanglement and the measurement problem from the underlying quantum mechanics. In this paper, we initiate the study of atomicity in distributed quantum computing. A formal model of (non-atomic) distributed quantum system is established. Based on the Dijkstra-Lamport condition, the system dynamics and observable dynamics of a distributed quantum system are defined, which correspond to the quantum state of and classically observable events in the system, respectively. Within this framework, we prove that local actions can be regarded as if they were atomic, up to the observable dynamics of the system. △ Less

Submitted 29 April, 2024; originally announced April 2024.

Comments: 36 pages, 5 figures

Verification of Recursively Defined Quantum Circuits

Authors: Mingsheng Ying, Zhicheng Zhang

Abstract: Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and economically programmed. In this paper, we present a proof system for formal verification of the correctness of recursively defined quantum circuits. The soundness and (relative) completeness of the proof system are established. To demonstratin… ▽ More Recursive techniques have recently been introduced into quantum programming so that a variety of large quantum circuits and algorithms can be elegantly and economically programmed. In this paper, we present a proof system for formal verification of the correctness of recursively defined quantum circuits. The soundness and (relative) completeness of the proof system are established. To demonstrating its effectiveness, a series of application examples of the proof system are given, including (multi-qubit) controlled gates, a quantum circuit generating (multi-qubit) GHZ (Greenberger-Horne-Zeilinger) states, recursive definition of quantum Fourier transform, quantum state preparation, and quantum random-access memories (QRAM). △ Less

Submitted 8 April, 2024; originally announced April 2024.

Symbolic Execution for Quantum Error Correction Programs

Authors: Wang Fang, Mingsheng Ying

Abstract: We define QSE, a symbolic execution framework for quantum programs by integrating symbolic variables into quantum states and the outcomes of quantum measurements. The soundness of QSE is established through a theorem that ensures the correctness of symbolic execution within operational semantics. We further introduce symbolic stabilizer states, which symbolize the phases of stabilizer generators,… ▽ More We define QSE, a symbolic execution framework for quantum programs by integrating symbolic variables into quantum states and the outcomes of quantum measurements. The soundness of QSE is established through a theorem that ensures the correctness of symbolic execution within operational semantics. We further introduce symbolic stabilizer states, which symbolize the phases of stabilizer generators, for the efficient analysis of quantum error correction (QEC) programs. Within the QSE framework, we can use symbolic expressions to characterize the possible discrete Pauli errors in QEC, providing a significant improvement over existing methods that rely on sampling with simulators. We implement QSE with the support of symbolic stabilizer states in a prototype tool named QuantumSE.jl. Our experiments on representative QEC codes, including quantum repetition codes, Kitaev's toric codes, and quantum Tanner codes, demonstrate the efficiency of QuantumSE.jl for debugging QEC programs with over 1000 qubits. In addition, by substituting concrete values in symbolic expressions of measurement results, QuantumSE.jl is also equipped with a sampling feature for stabilizer circuits. Despite a longer initialization time than the state-of-the-art stabilizer simulator, Google's Stim, QuantumSE.jl offers a quicker sampling rate in the experiments. △ Less

Submitted 28 April, 2024; v1 submitted 19 November, 2023; originally announced November 2023.

Comments: 41pages, 11 figures. v2: fix inappropriate use of Stim. v3: Extended version of PLDI 2024 publication

SymPhase: Phase Symbolization for Fast Simulation of Stabilizer Circuits

Authors: Wang Fang, Mingsheng Ying

Abstract: This paper proposes an efficient stabilizer circuit simulation algorithm that only traverses the circuit forward once. We introduce phase symbolization into stabilizer generators, which allows possible Pauli faults in the circuit to be accumulated explicitly as symbolic expressions in the phases of stabilizer generators. This way, the measurement outcomes are also symbolic expressions, and we can… ▽ More This paper proposes an efficient stabilizer circuit simulation algorithm that only traverses the circuit forward once. We introduce phase symbolization into stabilizer generators, which allows possible Pauli faults in the circuit to be accumulated explicitly as symbolic expressions in the phases of stabilizer generators. This way, the measurement outcomes are also symbolic expressions, and we can sample them by substituting the symbolic variables with concrete values, without traversing the circuit repeatedly. We show how to integrate symbolic phases into the stabilizer tableau and maintain them efficiently using bit-vector encoding. A new data layout of the stabilizer tableau in memory is proposed, which improves the performance of our algorithm (and other stabilizer simulation algorithms based on the stabilizer tableau). We implement our algorithm and data layout in a Julia package named SymPhase.jl, and compare it with Stim, the state-of-the-art simulator, on several benchmarks. We show that SymPhase.jl has superior performance in terms of sampling time, which is crucial for generating a large number of samples for further analysis. △ Less

Submitted 21 November, 2023; v1 submitted 7 November, 2023; originally announced November 2023.

Comments: 7 pages, 3 figures; v2: fix inappropriate use of Stim

Quantum Recursive Programming with Quantum Case Statements

Authors: Mingsheng Ying, Zhicheng Zhang

Abstract: We introduce a novel scheme of quantum recursive programming, in which large unitary transformations, i.e. quantum gates, can be recursively defined using quantum case statements, which are quantum counterparts of conditionals and case statements extensively used in classical programming. A simple programming language for supporting this kind of quantum recursion is defined, and its semantics is f… ▽ More We introduce a novel scheme of quantum recursive programming, in which large unitary transformations, i.e. quantum gates, can be recursively defined using quantum case statements, which are quantum counterparts of conditionals and case statements extensively used in classical programming. A simple programming language for supporting this kind of quantum recursion is defined, and its semantics is formally described. A series of examples are presented to show that some quantum algorithms can be elegantly written as quantum recursive programs. △ Less

Submitted 3 November, 2023; originally announced November 2023.

Statistical Limits of Adaptive Linear Models: Low-Dimensional Estimation and Inference

Authors: Licong Lin, Mufang Ying, Suvrojit Ghosh, Koulik Khamaru, Cun-Hui Zhang

Abstract: Estimation and inference in statistics pose significant challenges when data are collected adaptively. Even in linear models, the Ordinary Least Squares (OLS) estimator may fail to exhibit asymptotic normality for single coordinate estimation and have inflated error. This issue is highlighted by a recent minimax lower bound, which shows that the error of estimating a single coordinate can be enlar… ▽ More Estimation and inference in statistics pose significant challenges when data are collected adaptively. Even in linear models, the Ordinary Least Squares (OLS) estimator may fail to exhibit asymptotic normality for single coordinate estimation and have inflated error. This issue is highlighted by a recent minimax lower bound, which shows that the error of estimating a single coordinate can be enlarged by a multiple of $\sqrt{d}$ when data are allowed to be arbitrarily adaptive, compared with the case when they are i.i.d. Our work explores this striking difference in estimation performance between utilizing i.i.d. and adaptive data. We investigate how the degree of adaptivity in data collection impacts the performance of estimating a low-dimensional parameter component in high-dimensional linear models. We identify conditions on the data collection mechanism under which the estimation error for a low-dimensional parameter component matches its counterpart in the i.i.d. setting, up to a factor that depends on the degree of adaptivity. We show that OLS or OLS on centered data can achieve this matching error. In addition, we propose a novel estimator for single coordinate inference via solving a Two-stage Adaptive Linear Estimating equation (TALE). Under a weaker form of adaptivity in data collection, we establish an asymptotic normality property of the proposed estimator. △ Less

Submitted 28 October, 2023; v1 submitted 30 September, 2023; originally announced October 2023.

Comments: This paper is accepted at NeurIPS 2023

Detecting Violations of Differential Privacy for Quantum Algorithms

Authors: Ji Guan, Wang Fang, Mingyu Huang, Mingsheng Ying

Abstract: Quantum algorithms for solving a wide range of practical problems have been proposed in the last ten years, such as data search and analysis, product recommendation, and credit scoring. The concern about privacy and other ethical issues in quantum computing naturally rises up. In this paper, we define a formal framework for detecting violations of differential privacy for quantum algorithms. A det… ▽ More Quantum algorithms for solving a wide range of practical problems have been proposed in the last ten years, such as data search and analysis, product recommendation, and credit scoring. The concern about privacy and other ethical issues in quantum computing naturally rises up. In this paper, we define a formal framework for detecting violations of differential privacy for quantum algorithms. A detection algorithm is developed to verify whether a (noisy) quantum algorithm is differentially private and automatically generate bugging information when the violation of differential privacy is reported. The information consists of a pair of quantum states that violate the privacy, to illustrate the cause of the violation. Our algorithm is equipped with Tensor Networks, a highly efficient data structure, and executed both on TensorFlow Quantum and TorchQuantum which are the quantum extensions of famous machine learning platforms -- TensorFlow and PyTorch, respectively. The effectiveness and efficiency of our algorithm are confirmed by the experimental results of almost all types of quantum algorithms already implemented on realistic quantum computers, including quantum supremacy algorithms (beyond the capability of classical algorithms), quantum machine learning models, quantum approximate optimization algorithms, and variational quantum eigensolvers with up to 21 quantum bits. △ Less

Submitted 9 September, 2023; originally announced September 2023.

Journal ref: In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS 2023)

Adaptive Linear Estimating Equations

Authors: Mufang Ying, Koulik Khamaru, Cun-Hui Zhang

Abstract: Sequential data collection has emerged as a widely adopted technique for enhancing the efficiency of data gathering processes. Despite its advantages, such data collection mechanism often introduces complexities to the statistical inference procedure. For instance, the ordinary least squares (OLS) estimator in an adaptive linear regression model can exhibit non-normal asymptotic behavior, posing c… ▽ More Sequential data collection has emerged as a widely adopted technique for enhancing the efficiency of data gathering processes. Despite its advantages, such data collection mechanism often introduces complexities to the statistical inference procedure. For instance, the ordinary least squares (OLS) estimator in an adaptive linear regression model can exhibit non-normal asymptotic behavior, posing challenges for accurate inference and interpretation. In this paper, we propose a general method for constructing debiased estimator which remedies this issue. It makes use of the idea of adaptive linear estimating equations, and we establish theoretical guarantees of asymptotic normality, supplemented by discussions on achieving near-optimal asymptotic variance. A salient feature of our estimator is that in the context of multi-armed bandits, our estimator retains the non-asymptotic performance of the least square estimator while obtaining asymptotic normality property. Consequently, this work helps connect two fruitful paradigms of adaptive inference: a) non-asymptotic inference using concentration inequalities and b) asymptotic inference via asymptotic normality. △ Less

Submitted 7 November, 2023; v1 submitted 14 July, 2023; originally announced July 2023.

Comments: Paper is accepted at NeurIPS 2023

Exploiting Tensor-based Bayesian Learning for Massive Grant-Free Random Access in LEO Satellite Internet of Things

Authors: Ming Ying, Xiaoming Chen, Xiaodan Shao

Abstract: With the rapid development of Internet of Things (IoT), low earth orbit (LEO) satellite IoT is expected to provide low power, massive connectivity and wide coverage IoT applications. In this context, this paper provides a massive grant-free random access (GF-RA) scheme for LEO satellite IoT. This scheme does not need to change the transceiver, but transforms the received signal to a tensor decompo… ▽ More With the rapid development of Internet of Things (IoT), low earth orbit (LEO) satellite IoT is expected to provide low power, massive connectivity and wide coverage IoT applications. In this context, this paper provides a massive grant-free random access (GF-RA) scheme for LEO satellite IoT. This scheme does not need to change the transceiver, but transforms the received signal to a tensor decomposition form. By exploiting the characteristics of the tensor structure, a Bayesian learning algorithm for joint active device detection and channel estimation during massive GF-RA is designed. Theoretical analysis shows that the proposed algorithm has fast convergence and low complexity. Finally, extensive simulation results confirm its better performance in terms of error probability for active device detection and normalized mean square error for channel estimation over baseline algorithms in LEO satellite IoT. Especially, it is found that the proposed algorithm requires short preamble sequences and support massive connectivity with a low power, which is appealing to LEO satellite IoT. △ Less

Submitted 3 December, 2022; originally announced December 2022.

Comments: IEEE Transactions on Communications, 2022

Fault Models in Superconducting quantum circuits

Authors: Qifan Huang, Boxi Li, Minbo Gao, Mingsheng Ying

Abstract: Fault models are indispensable for many EDA tasks, so as for design and implementation of quantum hardware. In this article, we propose a fault model for superconducting quantum systems. Our fault model reflects the real fault behavior in control signals and structure of quantum systems. Based on it, we conduct fault simulation on controlled-Z gate and quantum circuits by QuTiP. We provide fidelit… ▽ More Fault models are indispensable for many EDA tasks, so as for design and implementation of quantum hardware. In this article, we propose a fault model for superconducting quantum systems. Our fault model reflects the real fault behavior in control signals and structure of quantum systems. Based on it, we conduct fault simulation on controlled-Z gate and quantum circuits by QuTiP. We provide fidelity benchmarks for incoherent faults and test patterns of minimal test repetitions for coherent faults. Results show that with 34 test repetitions a 10% control noise can be detected, which help to save test time and memory. △ Less

Submitted 1 December, 2022; originally announced December 2022.

Comments: 7 pages, 10 figures

Differentiable Quantum Programming with Unbounded Loops

Authors: Wang Fang, Mingsheng Ying, Xiaodi Wu

Abstract: The emergence of variational quantum applications has led to the development of automatic differentiation techniques in quantum computing. Recently, Zhu et al. (PLDI 2020) have formulated differentiable quantum programming with bounded loops, providing a framework for scalable gradient calculation by quantum means for training quantum variational applications. However, promising parameterized quan… ▽ More The emergence of variational quantum applications has led to the development of automatic differentiation techniques in quantum computing. Recently, Zhu et al. (PLDI 2020) have formulated differentiable quantum programming with bounded loops, providing a framework for scalable gradient calculation by quantum means for training quantum variational applications. However, promising parameterized quantum applications, e.g., quantum walk and unitary implementation, cannot be trained in the existing framework due to the natural involvement of unbounded loops. To fill in the gap, we provide the first differentiable quantum programming framework with unbounded loops, including a newly designed differentiation rule, code transformation, and their correctness proof. Technically, we introduce a randomized estimator for derivatives to deal with the infinite sum in the differentiation of unbounded loops, whose applicability in classical and probabilistic programming is also discussed. We implement our framework with Python and Q#, and demonstrate a reasonable sample efficiency. Through extensive case studies, we showcase an exciting application of our framework in automatically identifying close-to-optimal parameters for several parameterized quantum applications. △ Less

Submitted 8 November, 2022; originally announced November 2022.

Comments: Codes are available at https://github.com/njuwfang/DifferentiableQPL

CoqQ: Foundational Verification of Quantum Programs

Authors: Li Zhou, Gilles Barthe, Pierre-Yves Strub, Junyi Liu, Mingsheng Ying

Abstract: CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on s… ▽ More CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive program logic for proving properties of programs. CoqQ is foundational: the program logic is formally proved sound with respect to a denotational semantics based on state-of-art mathematical libraries (mathcomp and mathcomp analysis). CoqQ is also practical: assertions can use Dirac expressions, which eases concise specifications, and proofs can exploit local and parallel reasoning, which minimizes verification effort. We illustrate the applicability of CoqQ with many examples from the literature. △ Less

Submitted 22 July, 2022; originally announced July 2022.

Verifying Fairness in Quantum Machine Learning

Authors: Ji Guan, Wang Fang, Mingsheng Ying

Abstract: Due to the beyond-classical capability of quantum computing, quantum machine learning is applied independently or embedded in classical models for decision making, especially in the field of finance. Fairness and other ethical issues are often one of the main concerns in decision making. In this work, we define a formal framework for the fairness verification and analysis of quantum machine learni… ▽ More Due to the beyond-classical capability of quantum computing, quantum machine learning is applied independently or embedded in classical models for decision making, especially in the field of finance. Fairness and other ethical issues are often one of the main concerns in decision making. In this work, we define a formal framework for the fairness verification and analysis of quantum machine learning decision models, where we adopt one of the most popular notions of fairness in the literature based on the intuition -- any two similar individuals must be treated similarly and are thus unbiased. We show that quantum noise can improve fairness and develop an algorithm to check whether a (noisy) quantum machine learning model is fair. In particular, this algorithm can find bias kernels of quantum data (encoding individuals) during checking. These bias kernels generate infinitely many bias pairs for investigating the unfairness of the model. Our algorithm is designed based on a highly efficient data structure -- Tensor Networks -- and implemented on Google's TensorFlow Quantum. The utility and effectiveness of our algorithm are confirmed by the experimental results, including income prediction and credit scoring on real-world data, for a class of random (noisy) quantum decision models with 27 qubits ($2^{27}$-dimensional state space) tripling ($2^{18}$ times more than) that of the state-of-the-art algorithms for verifying quantum machine learning models. △ Less

Submitted 22 July, 2022; originally announced July 2022.

Birkhoff-von Neumann Quantum Logic as an Assertion Language for Quantum Programs

Authors: Mingsheng Ying

Abstract: A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties (e.g. correctness) of quantum programs. Surprisingly, such a logic is missing in the literature, and the existing first-order Birkhoff-von Neumann quantum logic deals with only classical variables and quantifications over them. In this paper, we fill in this gap by in… ▽ More A first-order logic with quantum variables is needed as an assertion language for specifying and reasoning about various properties (e.g. correctness) of quantum programs. Surprisingly, such a logic is missing in the literature, and the existing first-order Birkhoff-von Neumann quantum logic deals with only classical variables and quantifications over them. In this paper, we fill in this gap by introducing a first-order extension of Birkhoff-von Neumann quantum logic with universal and existential quantifiers over quantum variables. Examples are presented to show our logic is particularly suitable for specifying some important properties studied in quantum computation and quantum information. We further incorporate this logic into quantum Hoare logic as an assertion logic so that it can play a role similar to that of first-order logic for classical Hoare logic and BI-logic for separation logic. In particular, we show how it can be used to define and derive quantum generalisations of some adaptation rules that have been applied to significantly simplify verification of classical programs. It is expected that the assertion logic defined in this paper - first-order quantum logic with quantum variables - can be combined with various quantum program logics to serve as a solid logical foundation upon which verification tools can be built using proof assistants such as Coq and Isabelle/HOL. △ Less

Submitted 4 May, 2022; originally announced May 2022.

New Quantum Algorithms for Computing Quantum Entropies and Distances

Authors: Qisheng Wang, Ji Guan, Junyi Liu, Zhicheng Zhang, Mingsheng Ying

Abstract: We propose a series of quantum algorithms for computing a wide range of quantum entropies and distances, including the von Neumann entropy, quantum Rényi entropy, trace distance, and fidelity. The proposed algorithms significantly outperform the prior best (and even quantum) ones in the low-rank case, some of which achieve exponential speedups. In particular, for $N$-dimensional quantum states of… ▽ More We propose a series of quantum algorithms for computing a wide range of quantum entropies and distances, including the von Neumann entropy, quantum Rényi entropy, trace distance, and fidelity. The proposed algorithms significantly outperform the prior best (and even quantum) ones in the low-rank case, some of which achieve exponential speedups. In particular, for $N$-dimensional quantum states of rank $r$, our proposed quantum algorithms for computing the von Neumann entropy, trace distance and fidelity within additive error $\varepsilon$ have time complexity of $\tilde O(r/\varepsilon^2)$, $\tilde O(r^5/\varepsilon^6)$ and $\tilde O(r^{6.5}/\varepsilon^{7.5})$, respectively. By contrast, prior quantum algorithms for the von Neumann entropy and trace distance usually have time complexity $Ω(N)$, and the prior best one for fidelity has time complexity $\tilde O(r^{12.5}/\varepsilon^{13.5})$. The key idea of our quantum algorithms is to extend block-encoding from unitary operators in previous work to quantum states (i.e., density operators). It is realized by developing several convenient techniques to manipulate quantum states and extract information from them. The advantage of our techniques over the existing methods is that no restrictions on density operators are required; in sharp contrast, the previous methods usually require a lower bound on the minimal non-zero eigenvalue of density operators. △ Less

Submitted 30 May, 2024; v1 submitted 25 March, 2022; originally announced March 2022.

Comments: Final version. 58 pages, 5 tables, 1 figure. Minor corrections to Theorem 3.1, Theorem 3.4, and Corollary 3.5

Journal ref: IEEE Transactions on Information Theory, Early Access, 2024

Algebraic Reasoning of Quantum Programs via Non-idempotent Kleene Algebra

Authors: Yuxiang Peng, Mingsheng Ying, Xiaodi Wu

Abstract: We investigate the algebraic reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra. One prominent example of such is the famous Kleene Algebra with Tests (KAT), which has furnished both theoretical insights and practical tools. The succinctness of algebraic reasoning would be especially desirable for scalable analysis of quantum programs, given… ▽ More 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. △ Less

Submitted 28 March, 2022; v1 submitted 13 October, 2021; originally announced October 2021.

Comments: extended version, 23 pages, 6 figures, to appear at the 43rd ACM SIGPLAN PLDI 2022

Reasoning about Recursive Quantum Programs

Authors: Zhaowei Xu, Mingsheng Ying, Benoît Valiron

Abstract: Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of quantum while-p… ▽ More Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of quantum while-programs. However, there are as yet no general methods for reasoning about (mutual) recursive procedures and ancilla quantum data structure in quantum computing (with measurement). We fill the gap in this paper by proposing a parameterized quantum assertion logic and, based on which, designing a quantum Hoare logic for verifying parameterized recursive quantum programs with ancilla data and probabilistic control. The quantum Hoare logic can be used to prove partial, total, and even probabilistic correctness (by reducing to total correctness) of those quantum programs. In particular, two counterexamples for illustrating incompleteness of non-parameterized assertions in verifying recursive procedures, and, one counterexample for showing the failure of reasoning with exact probabilities based on partial correctness, are constructed. The effectiveness of our logic is shown by three main examples -- recursive quantum Markov chain (with probabilistic control), fixed-point Grover's search, and recursive quantum Fourier sampling. △ Less

Submitted 24 July, 2021; originally announced July 2021.

Verification of Distributed Quantum Programs

Authors: Yuan Feng, Sanjiang Li, Mingsheng Ying

Abstract: Distributed quantum systems and especially the Quantum Internet have the ever-increasing potential to fully demonstrate the power of quantum computation. This is particularly true given that developing a general-purpose quantum computer is much more difficult than connecting many small quantum devices. One major challenge of implementing distributed quantum systems is programming them and verifyin… ▽ More Distributed quantum systems and especially the Quantum Internet have the ever-increasing potential to fully demonstrate the power of quantum computation. This is particularly true given that developing a general-purpose quantum computer is much more difficult than connecting many small quantum devices. One major challenge of implementing distributed quantum systems is programming them and verifying their correctness. In this paper, we propose a CSP-like distributed programming language to facilitate the specification and verification of such systems. After presenting its operational and denotational semantics, we develop a Hoare-style logic for distributed quantum programs and establish its soundness and (relative) completeness with respect to both partial and total correctness. The effectiveness of the logic is demonstrated by its applications in the verification of quantum teleportation and local implementation of non-local CNOT gates, two important algorithms widely used in distributed quantum systems. △ Less

Submitted 30 April, 2021; originally announced April 2021.

Comments: arXiv admin note: text overlap with arXiv:2008.06812

Journal ref: ACM Transactions on Computational Logic (TOCL) 23, 3 (2022), 1-40

Model Checking for Verification of Quantum Circuits

Authors: Mingsheng Ying

Abstract: In this talk, we will describe a framework for assertion-based verification (ABV) of quantum circuits by applying model checking techniques for quantum systems developed in our previous work, in which: (i) Noiseless and noisy quantum circuits are modelled as operator- and super-operator-valued transition systems, respectively, both of which can be further represented by tensor networks. (ii) Q… ▽ More In this talk, we will describe a framework for assertion-based verification (ABV) of quantum circuits by applying model checking techniques for quantum systems developed in our previous work, in which: (i) Noiseless and noisy quantum circuits are modelled as operator- and super-operator-valued transition systems, respectively, both of which can be further represented by tensor networks. (ii) Quantum assertions are specified by a temporal extension of Birkhoff-von Neumann quantum logic. Their semantics is defined based on the design decision: they will be used in verification of quantum circuits by simulation on classical computers or human reasoning rather than by quantum physics experiments (e.g. testing through measurements); (iii) Algorithms for reachability analysis and model checking of quantum circuits are developed based on contraction of tensor networks. We observe that many optimisation techniques for computing relational products used in BDD-based model checking algorithms can be generalised for contracting tensor networks of quantum circuits. △ Less

Submitted 22 April, 2021; originally announced April 2021.

Approximate Equivalence Checking of Noisy Quantum Circuits

Authors: Xin Hong, Mingsheng Ying, Yuan Feng, Xiangzhen Zhou, Sanjiang Li

Abstract: We study the fundamental design automation problem of equivalence checking in the NISQ (Noisy Intermediate-Scale Quantum) computing realm where quantum noise is present inevitably. The notion of approximate equivalence of (possibly noisy) quantum circuits is defined based on the Jamiolkowski fidelity which measures the average distance between output states of two super-operators when the input is… ▽ More We study the fundamental design automation problem of equivalence checking in the NISQ (Noisy Intermediate-Scale Quantum) computing realm where quantum noise is present inevitably. The notion of approximate equivalence of (possibly noisy) quantum circuits is defined based on the Jamiolkowski fidelity which measures the average distance between output states of two super-operators when the input is chosen at random. By employing tensor network contraction, we present two algorithms, aiming at different situations where the number of noises varies, for computing the fidelity between an ideal quantum circuit and its noisy implementation. The effectiveness of our algorithms is demonstrated by experimenting on benchmarks of real NISQ circuits. When compared with the state-of-the-art implementation incorporated in Qiskit, experimental results show that the proposed algorithms outperform in both efficiency and scalability. △ Less

Submitted 3 June, 2021; v1 submitted 22 March, 2021; originally announced March 2021.

A Quantum Interpretation of Bunched Logic for Quantum Separation Logic

Authors: Li Zhou, Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu

Abstract: We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states. In our model, the separating conjunction of BI describes separable quantum states. We develop a program logic where pre- and post-conditions are BI formulas describing quantum states -- the program logic can be seen as a counterpart of separation logic for imperative quan… ▽ More We propose a model of the substructural logic of Bunched Implications (BI) that is suitable for reasoning about quantum states. In our model, the separating conjunction of BI describes separable quantum states. We develop a program logic where pre- and post-conditions are BI formulas describing quantum states -- the program logic can be seen as a counterpart of separation logic for imperative quantum programs. We exercise the logic for proving the security of quantum one-time pad and secret sharing, and we show how the program logic can be used to discover a flaw in Google Cirq's tutorial on the Variational Quantum Algorithm (VQA). △ Less

Submitted 30 January, 2021; originally announced February 2021.

Comments: 52 pages

Software Pipelining for Quantum Loop Programs

Authors: Jingzhe Guo, Mingsheng Ying

Abstract: We propose a method for performing software pipelining on quantum for-loop programs, exploiting parallelism in and across iterations. We redefine concepts that are useful in program optimization, including array aliasing, instruction dependency and resource conflict, this time in optimization of quantum programs. Using the redefined concepts, we present a software pipelining algorithm exploiting i… ▽ More We propose a method for performing software pipelining on quantum for-loop programs, exploiting parallelism in and across iterations. We redefine concepts that are useful in program optimization, including array aliasing, instruction dependency and resource conflict, this time in optimization of quantum programs. Using the redefined concepts, we present a software pipelining algorithm exploiting instruction-level parallelism in quantum loop programs. The optimization method is then evaluated on some test cases, including popular applications like QAOA, and compared with several baseline results. The evaluation results show that our approach outperforms loop optimizers exploiting only in-loop optimization chances by reducing total depth of the loop program to close to the optimal program depth obtained by full loop unrolling, while generating much smaller code in size. This is the first step towards optimization of a quantum program with such loop control flow as far as we know. △ Less

Submitted 23 December, 2020; originally announced December 2020.

Quantum Algorithm for Lexicographically Minimal String Rotation

Authors: Qisheng Wang, Mingsheng Ying

Abstract: Lexicographically minimal string rotation (LMSR) is a problem to find the minimal one among all rotations of a string in the lexicographical order, which is widely used in equality checking of graphs, polygons, automata and chemical structures. In this paper, we propose an $O(n^{3/4})$ quantum query algorithm for LMSR. In particular, the algorithm has average-case query complexity… ▽ More Lexicographically minimal string rotation (LMSR) is a problem to find the minimal one among all rotations of a string in the lexicographical order, which is widely used in equality checking of graphs, polygons, automata and chemical structures. In this paper, we propose an $O(n^{3/4})$ quantum query algorithm for LMSR. In particular, the algorithm has average-case query complexity $O(\sqrt n \log n)$, which is shown to be asymptotically optimal up to a polylogarithmic factor, compared to its $Ω\left(\sqrt{n/\log n}\right)$ lower bound. Furthermore, we show that our quantum algorithm outperforms any (classical) randomized algorithms in both worst and average cases. As an application, it is used in benzenoid identification and disjoint-cycle automata minimization. △ Less

Submitted 13 November, 2023; v1 submitted 16 December, 2020; originally announced December 2020.

Comments: Final version, with minor revision. 44 pages, 6 algorithms, 4 tables, 1 figure

Journal ref: Theory of Computing Systems, 68(1): 29-74, 2024

Symbolic Verification of Quantum Circuits

Authors: Mingsheng Ying, Zhengfeng Ji

Abstract: This short note proposes a symbolic approach for representing and reasoning about quantum circuits using complex, vector or matrix-valued Boolean expressions. A major benefit of this approach is that it allows us to directly borrow the existing techniques and tools for verification of classical logic circuits in reasoning about quantum circuits. This short note proposes a symbolic approach for representing and reasoning about quantum circuits using complex, vector or matrix-valued Boolean expressions. A major benefit of this approach is that it allows us to directly borrow the existing techniques and tools for verification of classical logic circuits in reasoning about quantum circuits. △ Less

Submitted 4 October, 2020; originally announced October 2020.

A Tensor Network based Decision Diagram for Representation of Quantum Circuits

Authors: Xin Hong, Xiangzhen Zhou, Sanjiang Li, Yuan Feng, Mingsheng Ying

Abstract: Tensor networks have been successfully applied in simulation of quantum physical systems for decades. Recently, they have also been employed in classical simulation of quantum computing, in particular, random quantum circuits. This paper proposes a decision diagram style data structure, called TDD (Tensor Decision Diagram), for more principled and convenient applications of tensor networks. This n… ▽ More Tensor networks have been successfully applied in simulation of quantum physical systems for decades. Recently, they have also been employed in classical simulation of quantum computing, in particular, random quantum circuits. This paper proposes a decision diagram style data structure, called TDD (Tensor Decision Diagram), for more principled and convenient applications of tensor networks. This new data structure provides a compact and canonical representation for quantum circuits. By exploiting circuit partition, the TDD of a quantum circuit can be computed efficiently. Furthermore, we show that the operations of tensor networks essential in their applications (e.g., addition and contraction), can also be implemented efficiently in TDDs. A proof-of-concept implementation of TDDs is presented and its efficiency is evaluated on a set of benchmark quantum circuits. It is expected that TDDs will play an important role in various design automation tasks related to quantum circuits, including but not limited to equivalence checking, error detection, synthesis, simulation, and verification. △ Less

Submitted 21 August, 2021; v1 submitted 5 September, 2020; originally announced September 2020.

Robustness Verification of Quantum Classifiers

Authors: Ji Guan, Wang Fang, Mingsheng Ying

Abstract: Several important models of machine learning algorithms have been successfully generalized to the quantum world, with potential speedup to training classical classifiers and applications to data analytics in quantum physics that can be implemented on the near future quantum computers. However, quantum noise is a major obstacle to the practical implementation of quantum machine learning. In this wo… ▽ More Several important models of machine learning algorithms have been successfully generalized to the quantum world, with potential speedup to training classical classifiers and applications to data analytics in quantum physics that can be implemented on the near future quantum computers. However, quantum noise is a major obstacle to the practical implementation of quantum machine learning. In this work, we define a formal framework for the robustness verification and analysis of quantum machine learning algorithms against noises. A robust bound is derived and an algorithm is developed to check whether or not a quantum machine learning algorithm is robust with respect to quantum training data. In particular, this algorithm can find adversarial examples during checking. Our approach is implemented on Google's TensorFlow Quantum and can verify the robustness of quantum machine learning algorithms with respect to a small disturbance of noises, derived from the surrounding environment. The effectiveness of our robust bound and algorithm is confirmed by the experimental results, including quantum bits classification as the "Hello World" example, quantum phase recognition and cluster excitation detection from real world intractable physical problems, and the classification of MNIST from the classical world. △ Less

Submitted 31 May, 2021; v1 submitted 17 August, 2020; originally announced August 2020.

Quantum Hoare logic with classical variables

Authors: Yuan Feng, Mingsheng Ying

Abstract: Hoare logic provides a syntax-oriented method to reason about program correctness and has been proven effective in the verification of classical and probabilistic programs. Existing proposals for quantum Hoare logic either lack completeness or support only quantum variables, thus limiting their capability in practical use. In this paper, we propose a quantum Hoare logic for a simple while language… ▽ More Hoare logic provides a syntax-oriented method to reason about program correctness and has been proven effective in the verification of classical and probabilistic programs. Existing proposals for quantum Hoare logic either lack completeness or support only quantum variables, thus limiting their capability in practical use. In this paper, we propose a quantum Hoare logic for a simple while language which involves both classical and quantum variables. Its soundness and relative completeness are proven for both partial and total correctness of quantum programs written in the language. Remarkably, with novel definitions of classical-quantum states and corresponding assertions, the logic system is quite simple and similar to the traditional Hoare logic for classical programs. Furthermore, to simplify reasoning in real applications, auxiliary proof rules are provided which support standard logical operation in the classical part of assertions, and of super-operator application in the quantum part. Finally, a series of practical quantum algorithms, in particular the whole algorithm of Shor's factorisation, are formally verified to show the effectiveness of the logic. △ Less

Submitted 30 April, 2021; v1 submitted 15 August, 2020; originally announced August 2020.

Comments: ACM Transactions on Quantum Computing, to appear

Journal ref: ACM Transactions on Quantum Computing 2, 4 (2021),1-43

Quantum Random Access Stored-Program Machines

Authors: Qisheng Wang, Mingsheng Ying

Abstract: Random access machines (RAMs) and random access stored-program machines (RASPs) are models of computing that are closer to the architecture of real-world computers than Turing machines (TMs). They are also convenient in complexity analysis of algorithms. The relationships between RAMs, RASPs and TMs are well-studied. However, clear relationships between their quantum counterparts are still missing… ▽ More Random access machines (RAMs) and random access stored-program machines (RASPs) are models of computing that are closer to the architecture of real-world computers than Turing machines (TMs). They are also convenient in complexity analysis of algorithms. The relationships between RAMs, RASPs and TMs are well-studied. However, clear relationships between their quantum counterparts are still missing in the literature. We fill in this gap by formally defining the models of quantum random access machines (QRAMs) and quantum random access stored-program machines (QRASPs) and clarifying the relationships between QRAMs, QRASPs and quantum Turing machines (QTMs). In particular, we show that $\textbf{P} \subseteq \textbf{EQRAMP} \subseteq \textbf{EQP} \subseteq \textbf{BQP} = \textbf{BQRAMP}$, where $\textbf{EQRAMP}$ and $\textbf{BQRAMP}$ stand for the sets of problems that can be solved by polynomial-time QRAMs with certainty and bounded-error, respectively. At the heart of our proof, is a standardisation of QTM with an extended halting scheme, which is of independent interest. △ Less

Submitted 10 September, 2022; v1 submitted 6 March, 2020; originally announced March 2020.

Comments: Final version. 69 pages, 1 figure, 6 tables, 7 algorithms

MSC Class: 68Q05 (Primary) 81P68; 68Q12 (Secondary) ACM Class: F.1.1

Journal ref: Journal of Computer and System Sciences, 131: 13-63, 2023

Proq: Projection-based Runtime Assertions for Debugging on a Quantum Computer

Authors: Gushu Li, Li Zhou, Nengkun Yu, Yufei Ding, Mingsheng Ying, Yuan Xie

Abstract: In this paper, we propose Proq, a runtime assertion scheme for testing and debugging quantum programs on a quantum computer. The predicates in Proq are represented by projections (or equivalently, closed subspaces of the state space), following Birkhoff-von Neumann quantum logic. The satisfaction of a projection by a quantum state can be directly checked upon a small number of projective measureme… ▽ More In this paper, we propose Proq, a runtime assertion scheme for testing and debugging quantum programs on a quantum computer. The predicates in Proq are represented by projections (or equivalently, closed subspaces of the state space), following Birkhoff-von Neumann quantum logic. The satisfaction of a projection by a quantum state can be directly checked upon a small number of projective measurements rather than a large number of repeated executions. On the theory side, we rigorously prove that checking projection-based assertions can help locate bugs or statistically assure that the semantic function of the tested program is close to what we expect, for both exact and approximate quantum programs. On the practice side, we consider hardware constraints and introduce several techniques to transform the assertions, making them directly executable on the measurement-restricted quantum computers. We also propose to achieve simplified assertion implementation using local projection technique with soundness guaranteed. We compare Proq with existing quantum program assertions and demonstrate the effectiveness and efficiency of Proq by its applications to assert two ingenious quantum algorithms, the Harrow-Hassidim-Lloyd algorithm and Shor's algorithm. △ Less

Submitted 29 May, 2020; v1 submitted 28 November, 2019; originally announced November 2019.

Comments: A major revision, in submission

Quantum Weakest Preconditions for Reasoning about Expected Runtimes of Quantum Programs (Extended Version)

Authors: Junyi Liu, Li Zhou, Gilles Barthe, Mingsheng Ying

Abstract: We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition. Then, we show that the expected runtime of a quantum program can be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimension… ▽ More We study expected runtimes for quantum programs. Inspired by recent work on probabilistic programs, we first define expected runtime as a generalisation of quantum weakest precondition. Then, we show that the expected runtime of a quantum program can be represented as the expectation of an observable (in physics). A method for computing the expected runtimes of quantum programs in finite-dimensional state spaces is developed. Several examples are provided as applications of this method, including computing the expected runtime of quantum Bernoulli Factory -- a quantum algorithm for generating random numbers. In particular, using our new method, an open problem of computing the expected runtime of quantum random walks introduced by Ambainis et al. (STOC 2001) is solved. △ Less

Submitted 14 July, 2022; v1 submitted 28 November, 2019; originally announced November 2019.

Decompose-and-Integrate Learning for Multi-class Segmentation in Medical Images

Authors: Yizhe Zhang, Michael T. C. Ying, Danny Z. Chen

Abstract: Segmentation maps of medical images annotated by medical experts contain rich spatial information. In this paper, we propose to decompose annotation maps to learn disentangled and richer feature transforms for segmentation problems in medical images. Our new scheme consists of two main stages: decompose and integrate. Decompose: by annotation map decomposition, the original segmentation problem is… ▽ More Segmentation maps of medical images annotated by medical experts contain rich spatial information. In this paper, we propose to decompose annotation maps to learn disentangled and richer feature transforms for segmentation problems in medical images. Our new scheme consists of two main stages: decompose and integrate. Decompose: by annotation map decomposition, the original segmentation problem is decomposed into multiple segmentation sub-problems; these new segmentation sub-problems are modeled by training multiple deep learning modules, each with its own set of feature transforms. Integrate: a procedure summarizes the solutions of the modules in the previous stage; a final solution is then formed for the original segmentation problem. Multiple ways of annotation map decomposition are presented and a new end-to-end trainable K-to-1 deep network framework is developed for implementing our proposed "decompose-and-integrate" learning scheme. In experiments, we demonstrate that our decompose-and-integrate segmentation, utilizing state-of-the-art fully convolutional networks (e.g., DenseVoxNet in 3D and CUMedNet in 2D), improves segmentation performance on multiple 3D and 2D datasets. Ablation study confirms the effectiveness of our proposed learning scheme for medical images. △ Less

Submitted 7 June, 2019; originally announced June 2019.

Comments: To appear in MICCAI 2019

Model Checking Applied to Quantum Physics

Authors: Ji Guan, Yuan Feng, Andrea Turrini, Mingsheng Ying

Abstract: Model checking has been successfully applied to verification of computer hardware and software, communication systems and even biological systems. In this paper, we further push the boundary of its applications and show that it can be adapted for applications in quantum physics. More explicitly, we show how quantum statistical and many-body systems can be modeled as quantum Markov chains, and some… ▽ More Model checking has been successfully applied to verification of computer hardware and software, communication systems and even biological systems. In this paper, we further push the boundary of its applications and show that it can be adapted for applications in quantum physics. More explicitly, we show how quantum statistical and many-body systems can be modeled as quantum Markov chains, and some of their properties that interest physicists can be specified in linear-time temporal logics. Then we present an efficient algorithm to check these properties. A few case studies are given to demonstrate the use of our algorithm to actual quantum physical problems. △ Less

Submitted 8 February, 2019; originally announced February 2019.

Relational Proofs for Quantum Programs

Authors: Gilles Barthe, Justin Hsu, Mingsheng Ying, Nengkun Yu, Li Zhou

Abstract: Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantum programs. The interpretation of our logic is based on a quantum analogue of probabilistic couplings. We use our logic to verify non-trivial relational properties of quantum programs, including uniformity for samples ge… ▽ More Relational verification of quantum programs has many potential applications in quantum and post-quantum security and other domains. We propose a relational program logic for quantum programs. The interpretation of our logic is based on a quantum analogue of probabilistic couplings. We use our logic to verify non-trivial relational properties of quantum programs, including uniformity for samples generated by the quantum Bernoulli factory, reliability of quantum teleportation against noise (bit and phase flip), security of quantum one-time pad and equivalence of quantum walks. △ Less

Submitted 11 December, 2019; v1 submitted 16 January, 2019; originally announced January 2019.

Comments: 34 pages, LaTeX; v2: extend version of conference paper

Equivalence Checking of Quantum Finite-State Machines

Authors: Qisheng Wang, Junyi Liu, Mingsheng Ying

Abstract: In this paper, we introduce the model of quantum Mealy machines and study the equivalence checking and minimisation problems of them. Two efficient algorithms are developed for checking equivalence of two states in the same machine and for checking equivalence of two machines. As an application, they are used in equivalence checking of quantum circuits. Moreover, the minimisation problem is proved… ▽ More In this paper, we introduce the model of quantum Mealy machines and study the equivalence checking and minimisation problems of them. Two efficient algorithms are developed for checking equivalence of two states in the same machine and for checking equivalence of two machines. As an application, they are used in equivalence checking of quantum circuits. Moreover, the minimisation problem is proved to be in $\textbf{PSPACE}$. △ Less

Submitted 10 September, 2022; v1 submitted 8 January, 2019; originally announced January 2019.

Comments: Minor corrections. 29 pages, 2 figures, 3 tables, 2 algorithms

Journal ref: Journal of Computer and System Sciences, 116: 1-21, 2021

A Logic for Recursive Quantum Programs

Authors: Zhaowei Xu, Mingsheng Ying, Shenggang Ying

Abstract: Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of non-recursive q… ▽ More Most modern (classical) programming languages support recursion. Recursion has also been successfully applied to the design of several quantum algorithms and introduced in a couple of quantum programming languages. So, it can be expected that recursion will become one of the fundamental paradigms of quantum programming. Several program logics have been developed for verification of non-recursive quantum programs. However, there are as yet no general methods for reasoning about recursive procedures in quantum computing. We fill the gap in this paper by presenting a logic for recursive quantum programs. This logic is an extension of quantum Hoare logic for quantum While-programs. The (relative) completeness of the logic is proved, and its effectiveness is shown by a running example: fixed-point Grover's search. △ Less

Submitted 9 December, 2018; v1 submitted 2 December, 2018; originally announced December 2018.

Comments: There are errors in Section 4, i.e., the definition of quantum predicate terms should be repaired. There are also notational abuses

Quantitative Robustness Analysis of Quantum Programs (Extended Version)

Authors: Shih-Han Hung, Kesha Hietala, Shaopeng Zhu, Mingsheng Ying, Michael Hicks, Xiaodi Wu

Abstract: Quantum computation is a topic of significant recent interest, with practical advances coming from both research and industry. A major challenge in quantum programming is dealing with errors (quantum noise) during execution. Because quantum resources (e.g., qubits) are scarce, classical error correction techniques applied at the level of the architecture are currently cost-prohibitive. But while t… ▽ More 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 $ε$-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. △ Less

Submitted 1 December, 2018; v1 submitted 8 November, 2018; originally announced November 2018.

Comments: 34 pages, LaTeX; v2: fixed typos

Reasoning about Parallel Quantum Programs

Authors: Mingsheng Ying, Li Zhou, Yangjia Li

Abstract: We initiate the study of parallel quantum programming by defining the operational and denotational semantics of parallel quantum programs. The technical contributions of this paper include: (1) find a series of useful proof rules for reasoning about correctness of parallel quantum programs; (2) prove a (relative) completeness of our proof rules for partial correctness of disjoint parallel quantum… ▽ More We initiate the study of parallel quantum programming by defining the operational and denotational semantics of parallel quantum programs. The technical contributions of this paper include: (1) find a series of useful proof rules for reasoning about correctness of parallel quantum programs; (2) prove a (relative) completeness of our proof rules for partial correctness of disjoint parallel quantum programs; and (3) prove a strong soundness theorem of the proof rules showing that partial correctness is well maintained at each step of transitions in the operational semantics of a general parallel quantum program (with shared variables). This is achieved by partially overcoming the following conceptual challenges that are never present in classical parallel programming: (i) the intertwining of nondeterminism caused by quantum measurements and introduced by parallelism; (ii) entanglement between component quantum programs; and (iii) combining quantum predicates in the overlap of state Hilbert spaces of component quantum programs with shared variables. Applications of the techniques developed in this paper are illustrated by a formal verification of Bravyi-Gosset-König's parallel quantum algorithm solving a linear algebra problem, which gives for the first time an unconditional proof of a computational quantum advantage. △ Less

Submitted 1 October, 2019; v1 submitted 26 October, 2018; originally announced October 2018.

Comments: Added an application on formal verification of Bravyi-Gosset-König's algorithm

Toward Automatic Verification of Quantum Programs

Authors: Mingsheng Ying

Abstract: This paper summarises the results obtained by the author and his collaborators in a program logic approach to the verification of quantum programs, including quantum Hoare logic, invariant generation and termination analysis for quantum programs. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for futu… ▽ More This paper summarises the results obtained by the author and his collaborators in a program logic approach to the verification of quantum programs, including quantum Hoare logic, invariant generation and termination analysis for quantum programs. It also introduces the notion of proof outline and several auxiliary rules for more conveniently reasoning about quantum programs. Some problems for future research are proposed at the end of the paper. △ Less

Submitted 30 July, 2018; originally announced July 2018.

Journal ref: Formal Aspect of Computing 2018

Model Checking Quantum Systems --- A Survey

Authors: Mingsheng Ying, Yuan Feng

Abstract: This article discusses the essential difficulties in developing model-checking techniques for quantum systems that are never present in model checking classical systems. It further reviews some early researches on checking quantum communication protocols as well as a new line of researches pursued by the authors and their collaborators on checking general quantum systems, applicable to both physic… ▽ More This article discusses the essential difficulties in developing model-checking techniques for quantum systems that are never present in model checking classical systems. It further reviews some early researches on checking quantum communication protocols as well as a new line of researches pursued by the authors and their collaborators on checking general quantum systems, applicable to both physical systems and quantum programs. △ Less

Submitted 25 July, 2018; originally announced July 2018.

BoxNet: Deep Learning Based Biomedical Image Segmentation Using Boxes Only Annotation

Authors: Lin Yang, Yizhe Zhang, Zhuo Zhao, Hao Zheng, Peixian Liang, Michael T. C. Ying, Anil T. Ahuja, Danny Z. Chen

Abstract: In recent years, deep learning (DL) methods have become powerful tools for biomedical image segmentation. However, high annotation efforts and costs are commonly needed to acquire sufficient biomedical training data for DL models. To alleviate the burden of manual annotation, in this paper, we propose a new weakly supervised DL approach for biomedical image segmentation using boxes only annotation… ▽ More In recent years, deep learning (DL) methods have become powerful tools for biomedical image segmentation. However, high annotation efforts and costs are commonly needed to acquire sufficient biomedical training data for DL models. To alleviate the burden of manual annotation, in this paper, we propose a new weakly supervised DL approach for biomedical image segmentation using boxes only annotation. First, we develop a method to combine graph search (GS) and DL to generate fine object masks from box annotation, in which DL uses box annotation to compute a rough segmentation for GS and then GS is applied to locate the optimal object boundaries. During the mask generation process, we carefully utilize information from box annotation to filter out potential errors, and then use the generated masks to train an accurate DL segmentation network. Extensive experiments on gland segmentation in histology images, lymph node segmentation in ultrasound images, and fungus segmentation in electron microscopy images show that our approach attains superior performance over the best known state-of-the-art weakly supervised DL method and is able to achieve (1) nearly the same accuracy compared to fully supervised DL methods with far less annotation effort, (2) significantly better results with similar annotation time, and (3) robust performance in various applications. △ Less

Submitted 2 June, 2018; originally announced June 2018.

Quantum Büchi Automata

Authors: Qisheng Wang, Mingsheng Ying

Abstract: This paper defines a notion of quantum Büchi automaton (QBA for short) with two different acceptance conditions for ω-words: non-disturbing and disturbing. Several pumping lemmas are established for QBAs. The relationship between the ω-languages accepted by QBAs and those accepted by classical Büchi automata are clarified with the help of the pumping lemmas. The closure properties of the languages… ▽ More This paper defines a notion of quantum Büchi automaton (QBA for short) with two different acceptance conditions for ω-words: non-disturbing and disturbing. Several pumping lemmas are established for QBAs. The relationship between the ω-languages accepted by QBAs and those accepted by classical Büchi automata are clarified with the help of the pumping lemmas. The closure properties of the languages accepted by QBAs are studied in the probable, almost sure and threshold semantics. The decidability of the emptiness problem for the languages accepted by QBAs is proved using the Tarski-Seidenberg elimination. △ Less

Submitted 24 April, 2018; originally announced April 2018.

Quantum Coupling and Strassen Theorem

Authors: Li Zhou, Shenggang Ying, Nengkun Yu, Mingsheng Ying

Abstract: We introduce a quantum generalisation of the notion of coupling in probability theory. Several interesting examples and basic properties of quantum couplings are presented. In particular, we prove a quantum extension of Strassen theorem for probabilistic couplings, a fundamental theorem in probability theory that can be used to bound the probability of an event in a distribution by the probability… ▽ More We introduce a quantum generalisation of the notion of coupling in probability theory. Several interesting examples and basic properties of quantum couplings are presented. In particular, we prove a quantum extension of Strassen theorem for probabilistic couplings, a fundamental theorem in probability theory that can be used to bound the probability of an event in a distribution by the probability of an event in another distribution coupled with the first. △ Less

Submitted 27 March, 2018; originally announced March 2018.

$Q|SI\rangle$: A Quantum Programming Environment

Authors: Shusen Liu, Xin Wang, Li Zhou, Ji Guan, Yinan Li, Yang He, Runyao Duan, Mingsheng Ying

Abstract: This paper describes a quantum programming environment, named $Q|SI\rangle$. It is a platform embedded in the .Net language that supports quantum programming using a quantum extension of the $\mathbf{while}$-language. The framework of the platform includes a compiler of the quantum $\mathbf{while}$-language and a suite of tools for simulating quantum computation, optimizing quantum circuits, and a… ▽ More This paper describes a quantum programming environment, named $Q|SI\rangle$. It is a platform embedded in the .Net language that supports quantum programming using a quantum extension of the $\mathbf{while}$-language. The framework of the platform includes a compiler of the quantum $\mathbf{while}$-language and a suite of tools for simulating quantum computation, optimizing quantum circuits, and analyzing and verifying quantum programs. Throughout the paper, using $Q|SI\rangle$ to simulate quantum behaviors on classical platforms with a combination of components is demonstrated. The scalable framework allows the user to program customized functions on the platform. The compiler works as the core of $Q|SI\rangle$ bridging the gap from quantum hardware to quantum software. The built-in decomposition algorithms enable the universal quantum computation on the present quantum hardware. △ Less

Submitted 25 October, 2017; originally announced October 2017.

Comments: 30 pages, software available at http://www.qcompiler.com

Super-activating Quantum Memory with Entanglement

Authors: Ji Guan, Yuan Feng, Mingsheng Ying

Abstract: Noiseless subsystems were proved to be an efficient and faithful approach to preserve fragile information against decoherence in quantum information processing and quantum computation. They were employed to design a general (hybrid) quantum memory cell model that can store both quantum and classical information. In this paper, we find an interesting new phenomenon that the purely classical memory… ▽ More Noiseless subsystems were proved to be an efficient and faithful approach to preserve fragile information against decoherence in quantum information processing and quantum computation. They were employed to design a general (hybrid) quantum memory cell model that can store both quantum and classical information. In this paper, we find an interesting new phenomenon that the purely classical memory cell can be super-activated to preserve quantum states, whereas the null memory cell can only be super-activated to encode classical information. Furthermore, necessary and sufficient conditions for this phenomenon are discovered so that the super-activation can be easily checked by examining certain eigenvalues of the quantum memory cell without computing the noiseless subsystems explicitly. In particular, it is found that entangled and separable stationary states are responsible for the super-activation of storing quantum and classical information, respectively. △ Less

Submitted 20 November, 2018; v1 submitted 2 August, 2017; originally announced August 2017.

Quantum Privacy-Preserving Perceptron

Authors: Shenggang Ying, Mingsheng Ying, Yuan Feng

Abstract: With the extensive applications of machine learning, the issue of private or sensitive data in the training examples becomes more and more serious: during the training process, personal information or habits may be disclosed to unexpected persons or organisations, which can cause serious privacy problems or even financial loss. In this paper, we present a quantum privacy-preserving algorithm for m… ▽ More With the extensive applications of machine learning, the issue of private or sensitive data in the training examples becomes more and more serious: during the training process, personal information or habits may be disclosed to unexpected persons or organisations, which can cause serious privacy problems or even financial loss. In this paper, we present a quantum privacy-preserving algorithm for machine learning with perceptron. There are mainly two steps to protect original training examples. Firstly when checking the current classifier, quantum tests are employed to detect data user's possible dishonesty. Secondly when updating the current classifier, private random noise is used to protect the original data. The advantages of our algorithm are: (1) it protects training examples better than the known classical methods; (2) it requires no quantum database and thus is easy to implement. △ Less

Submitted 31 July, 2017; originally announced July 2017.

Comments: 30 pages,5 figures

Quantum Privacy-Preserving Data Analytics

Authors: Shenggang Ying, Mingsheng Ying, Yuan Feng

Abstract: Data analytics (such as association rule mining and decision tree mining) can discover useful statistical knowledge from a big data set. But protecting the privacy of the data provider and the data user in the process of analytics is a serious issue. Usually, the privacy of both parties cannot be fully protected simultaneously by a classical algorithm. In this paper, we present a quantum protocol… ▽ More Data analytics (such as association rule mining and decision tree mining) can discover useful statistical knowledge from a big data set. But protecting the privacy of the data provider and the data user in the process of analytics is a serious issue. Usually, the privacy of both parties cannot be fully protected simultaneously by a classical algorithm. In this paper, we present a quantum protocol for data mining that can much better protect privacy than the known classical algorithms: (1) if both the data provider and the data user are honest, the data user can know nothing about the database except the statistical results, and the data provider can get nearly no information about the results mined by the data user; (2) if the data user is dishonest and tries to disclose private information of the other, she/he will be detected with a high probability; (3) if the data provider tries to disclose the privacy of the data user, she/he cannot get any useful information since the data user hides his privacy among noises. △ Less

Submitted 14 February, 2017; originally announced February 2017.

Comments: 50 pages, 1 figure

A Theorem Prover for Quantum Hoare Logic and Its Applications

Authors: Tao Liu, Yangjia Li, Shuling Wang, Mingsheng Ying, Naijun Zhan

Abstract: Quantum Hoare Logic (QHL) was introduced in Ying's work to specify and reason about quantum programs. In this paper, we implement a theorem prover for QHL based on Isabelle/HOL. By applying the theorem prover, verifying a quantum program against a specification is transformed equivalently into an order relation between matrices. Due to the limitation of Isabelle/HOL, the calculation of the order r… ▽ More Quantum Hoare Logic (QHL) was introduced in Ying's work to specify and reason about quantum programs. In this paper, we implement a theorem prover for QHL based on Isabelle/HOL. By applying the theorem prover, verifying a quantum program against a specification is transformed equivalently into an order relation between matrices. Due to the limitation of Isabelle/HOL, the calculation of the order relation is solved by calling an outside oracle written in Python. To the best of our knowledge, this is the first theorem prover for quantum programs. To demonstrate its power, the correctness of two well-known quantum algorithms, i.e., Grover Quantum Search and Quantum Phase Estimation (the key step in Shor's quantum algorithm of factoring in polynomial time) are proved using the theorem prover. These are the first mechanized proofs for both of them. △ Less

Submitted 15 January, 2016; originally announced January 2016.