Publications

Lin, Y, Guan, J, Fang, W, Ying, M & Su, Z 2025, 'A obustness fication Tool for  uantum Machine Learning Models' in Lecture Notes in Computer Science, Springer Nature Switzerland, pp. 403-421.
View/Download from: Publisher's site
View description>>

AbstractAdversarial noise attacks present a significant threat to quantum machine learning (QML) models, similar to their classical counterparts. This is especially true in the current Noisy Intermediate-Scale Quantum era, where noise is unavoidable. Therefore, it is essential to ensure the robustness of QML models before their deployment. To address this challenge, we introduce VeriQR, the first tool designed specifically for formally verifying and improving the robustness of QML models, to the best of our knowledge. This tool mimics real-world quantum hardware’s noisy impacts by incorporating random noise to formally validate a QML model’s robustness. VeriQR supports exact (sound and complete) algorithms for both local and global robustness verification. For enhanced efficiency, it implements an under-approximate (complete) algorithm and a tensor network-based algorithm to verify local and global robustness, respectively. As a formal verification tool, VeriQR can detect adversarial examples and utilize them for further analysis and to enhance the local robustness through adversarial training, as demonstrated by experiments on real-world quantum machine learning models. Moreover, it permits users to incorporate customized noise. Based on this feature, we assess VeriQR using various real-world examples, and experimental outcomes confirm that the addition of specific quantum noise can enhance the global robustness of QML models. These processes are made accessible through a user-friendly graphical interface provided by VeriQR, catering to general users without requiring a deep understanding of the counter-intuitive probabilistic nature of quantum computing.

Berta, M, Lami, L & Tomamichel, M 2025, 'Continuity of Entropies via Integral Representations', IEEE Transactions on Information Theory, vol. 71, no. 3, pp. 1896-1908.
View/Download from: Publisher's site

Cervero-Martí­n, E & Tomamichel, M 2025, 'Device independent security of quantum key distribution from monogamy-of-entanglement games', Quantum, vol. 9, pp. 1652-1652.
View/Download from: Publisher's site
View description>>

We analyse two party non-local games whose predicate requires Alice and Bob to generate matching bits, and their three party extensions where a third player receives all inputs and is required to output a bit that matches that of the original players. We propose a general device independent quantum key distribution protocol for the subset of such non-local games that satisfy a monogamy-of-entanglement property characterised by a gap in the maximum winning probability between the bipartite and tripartite versions of the game. This gap is due to the optimal strategy for two players requiring entanglement, which due to its monogamy property cannot be shared with any additional players. Based solely on the monogamy-of-entanglement property, we provide a simple proof of information theoretic security of our protocol. Lastly, we numerically optimize the finite and asymptotic secret key rates of our protocol using the magic square game as an example, for which we provide a numerical bound on the maximal tripartite quantum winning probability which closely matches the bipartite classical winning probability. Further, we show that our protocol is robust for depolarizing noise up to about 2.88%, providing the first such bound for general attacks for magic square based quantum key distribution.

Ene, A, Lee, T, Micek, P & Sachdeva, S 2025, 'Introduction: ACM-SIAM Symposium on Discrete Algorithms (SODA) 2021 Special Issue', ACM Transactions on Algorithms, vol. 21, no. 3, pp. 1-2.
View/Download from: Publisher's site

Gao, L & Yu, N 2025, 'Optimal Tomography of Quantum Markov Chains via Continuity of Petz Recovery States', IEEE Transactions on Information Theory, pp. 1-1.
View/Download from: Publisher's site

Huang, Q, Zhou, L, Fang, W, Zhao, M & Ying, M 2025, 'Efficient Formal Verification of Quantum Error Correcting Programs', Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI, pp. 1068-1093.
View/Download from: Publisher's site
View description>>

Quantum error correction (QEC) is fundamental for suppressing noise in quantum hardware and enabling fault-tolerant quantum computation. In this paper, we propose an efficient verification framework for QEC programs. We define an assertion logic and a program logic specifically crafted for QEC programs and establish a sound proof system. We then develop an efficient method for handling verification conditions (VCs) of QEC programs: for Pauli errors, the VCs are reduced to classical assertions that can be solved by SMT solvers, and for non-Pauli errors, we provide a heuristic algorithm. We formalize the proposed program logic in Coq proof assistant, making it a verified QEC verifier. Additionally, we implement an automated QEC verifier, Veri-QEC, for verifying various fault-tolerant scenarios. We demonstrate the efficiency and broad functionality of the framework by performing different verification tasks across various scenarios. Finally, we present a benchmark of 14 verified stabilizer codes.

Huang, Y, Gao, D, Ying, S & Li, S 2025, 'DasAtom: A Divide-and-Shuttle Atom Approach to Quantum Circuit Transformation', IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, vol. 44, no. 8, pp. 2966-2978.
View/Download from: Publisher's site

Li, S, Zhou, X & Feng, Y 2025, 'Benchmarking Quantum Circuit Transformation With QKNOB Circuits', IEEE Transactions on Quantum Engineering, vol. 6, pp. 1-15.
View/Download from: Publisher's site

Mann, RL, Elman, SJ, Wood, DR & Chapman, A 2025, 'A graph-theoretic framework for free-parafermion solvability', Proceedings of the Royal Society A: Mathematical, Physical and Engineering Sciences, vol. 481, no. 2312.
View/Download from: Publisher's site
View description>>

We present a graph-theoretic characterization of when a quantum spin model admits an exact solution via a mapping to free parafermions. Our characterization is based on the concept of a frustration graph, which represents the commutation relations between Weyl operators of a Hamiltonian. We show that a quantum spin system has an exact free-parafermion solution if its frustration graph is an oriented indifference graph. Furthermore, we show that if the frustration graph of a model can be dipath oriented via switching operations, then the model is integrable in the sense that there is a family of commuting independent set charges. Additionally, we establish an efficient algorithm for deciding whether this is possible. Our characterization extends that given for free-fermion solvability. Finally, we apply our results to solve three qudit spin models.

Mohanty, N, Behera, BK, Ferrie, C & Dash, P 2025, 'A quantum approach to synthetic minority oversampling technique (SMOTE)', Quantum Machine Intelligence, vol. 7, no. 1.
View/Download from: Publisher's site
View description>>

Abstract The paper proposes the Quantum-SMOTE method, a novel solution that uses quantum computing techniques to solve the prevalent problem of class imbalance in machine learning datasets. Quantum-SMOTE, inspired by the Synthetic Minority Oversampling Technique (SMOTE), generates synthetic data points using quantum processes such as swap tests and quantum rotation. The process varies from the conventional SMOTE algorithm’s usage of K-Nearest Neighbors (KNN) and Euclidean distances, enabling synthetic instances to be generated from minority class data points without relying on neighbor proximity. The algorithm asserts greater control over the synthetic data generation process by introducing hyperparameters such as rotation angle, minority percentage, and splitting factor, which allow for customization to specific dataset requirements. Due to the use of a compact swap test, the algorithm can accommodate a large number of features. Furthermore, the approach is tested on a public dataset of TelecomChurn and evaluated alongside two prominent classification algorithms, Random Forest and Logistic Regression, to determine its impact along with varying proportions of synthetic data.

Morales, MES, Costa, PCS, Pantaleoni, G, Burgarth, DK, Sanders, YR & Berry, DW 2025, 'Selection and Improvement of Product Formulae for Best Performance of Quantum Simulation', Quantum Information & Computation, vol. 25, no. 1, pp. 1-35.
View/Download from: Publisher's site
View description>>

Abstract Quantum algorithms for simulation of Hamiltonian evolution are often based on product formulae. The fractal methods give a systematic way to find arbitrarily high-order product formulae, but result in a large number of exponentials. On the other hand, product formulae with fewer exponentials can be found by numerical solution of simultaneous non-linear equations. It is also possible to reduce the cost of long-time simulations by processing, where a kernel is repeated and a processor need only be applied at the beginning and end of the simulation. In this work, we found thousands of new product formulae, and numerically tested these formulae, together with many formulae from prior literature. We provide methods to fairly compare product formulae of different lengths and different orders. For the case of 8th order, we have found new product formulae with exceptional performance, about two orders of magnitude better accuracy than prior work, both in the processed and non-processed cases. The processed product formula provides the best performance due to being shorter than the non-processed product formula. It outperforms all other tested product formulae over a range of many orders of magnitude in system parameters T (time) and ε (allowable error). That includes reasonable combinations of parameters to be used in quantum algorithms, where the size of the simulation is large enough to be classically intractable, but not so large it takes an impractically long time on a quantum computer.

Verhagen, F, Tomamichel, M & Haapasalo, E 2025, 'Matrix Majorization in Large Samples with Varying Support Restrictions', IEEE Transactions on Information Theory, pp. 1-1.
View/Download from: Publisher's site

Wang, Z, Shi, X, Ji, Z & Yin, X 2025, 'Quantum Network Optimization: From Optimal Routing to Fair Resource Allocation', ACM SIGMETRICS Performance Evaluation Review, vol. 53, no. 1, pp. 142-144.
View/Download from: Publisher's site
View description>>

Quantum networks are essential infrastructure for enabling large-scale and long-distance quantum communications but face significant challenges in routing optimization and resource allocation due to their probabilistic nature and quantum resource limitations. Existing approaches typically tackle these problems in isolation, often by simply applying classical routing algorithms, maximizing the overall profit to allocate resources without considering fairness, or improving fairness in an ad-hoc way without a rigorous model. This paper proposes a general framework to systematically address these challenges. First, we conduct a thorough analysis of quantum network metrics using routing algebra as the mathematical foundation, and design provably optimal routing algorithms to tackle the unique challenges arising from their probabilistic characteristics. Second, we formulate an optimization model that simultaneously considers fairness among concurrent requests while respecting various quantum resource constraints, and design efficient near-optimal heuristics to solve it. The proposed framework provides both theoretical insights and practical solutions for the design and management of future quantum networks.

Wang, Z, Shi, X, Ji, Z & Yin, X 2025, 'Quantum Network Optimization: From Optimal Routing to Fair Resource Allocation', Proceedings of the ACM on Measurement and Analysis of Computing Systems, vol. 9, no. 2, pp. 1-26.
View/Download from: Publisher's site
View description>>

Quantum networks are essential infrastructure for enabling large-scale and long-distance quantum communications but face significant challenges in routing optimization and resource allocation due to their probabilistic nature and quantum resource limitations. Existing approaches typically tackle these problems in isolation, often by simply applying classical routing algorithms, maximizing the overall profit to allocate resources without considering fairness, or improving fairness in an ad-hoc way without a rigorous model. This paper proposes a general framework to systematically address these challenges. First, we conduct a thorough analysis of quantum network metrics using routing algebra as the mathematical foundation, and design provably optimal routing algorithms to tackle the unique challenges arising from their probabilistic characteristics. Second, we formulate an optimization model that simultaneously considers fairness among concurrent requests while respecting various quantum resource constraints, and design efficient near-optimal heuristics to solve it. The proposed framework provides both theoretical insights and practical solutions for the design and management of future quantum networks.

Yu, N 2025, 'The Quantum Repeater Network Saturates the Entanglement Distribution Asymptotically', IEEE Transactions on Information Theory, vol. 71, no. 8, pp. 6155-6164.
View/Download from: Publisher's site

Zhang, K, Li, R & Ying, M 2025, 'A Divide-And-Conquer Pebbling Strategy for Oracle Synthesis in Quantum Computing', IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, pp. 1-1.
View/Download from: Publisher's site

Zhang, Z & Ying, M 2025, 'Quantum Register Machine: Efficient Implementation of Quantum Recursive Programs', Proceedings of the ACM on Programming Languages, vol. 9, no. PLDI, pp. 822-847.
View/Download from: Publisher's site
View description>>

Quantum recursive programming has been recently introduced for describing sophisticated and complicated quantum algorithms in a compact and elegant way. However, implementation of quantum recursion involves intricate interplay between quantum control flow and recursive procedure calls. In this paper, we aim at resolving this fundamental challenge and develop a series of techniques to efficiently implement quantum recursive programs. Our main contributions include: 1. We propose a notion of quantum register machine, the first quantum architecture (including an instruction set) that provides instruction-level support for quantum control flow and recursive procedure calls at the same time. 2. Based on quantum register machine, we describe the first comprehensive implementation process of quantum recursive programs, including the compilation, the partial evaluation of quantum control flow, and the execution on the quantum register machine. 3. As a bonus, our efficient implementation of quantum recursive programs also offers automatic parallelisation of quantum algorithms. For implementing certain quantum algorithmic subroutine, like the widely used quantum multiplexor, we can even obtain exponential parallel speed-up (over the straightforward implementation) from this automatic parallelisation. This demonstrates that quantum recursive programming can be win-win for both modularity of programs and efficiency of their implementation.

Acharya, J, Dharmavarapu, A, Liu, Y & Yu, N 1970, 'Pauli Measurements Are Not Optimal for Single-Copy Tomography', Proceedings of the 57th Annual ACM Symposium on Theory of Computing, STOC '25: 57th Annual ACM Symposium on Theory of Computing, ACM, pp. 718-729.
View/Download from: Publisher's site

Grochow, JA & Qiao, Y 1970, 'On the Complexity of Isomorphism Problems for Tensors, Groups, and Polynomials IV: Linear-Length Reductions and Their Applications', Proceedings of the 57th Annual ACM Symposium on Theory of Computing, STOC '25: 57th Annual ACM Symposium on Theory of Computing, ACM, pp. 766-776.
View/Download from: Publisher's site

Grochow, JA, Qiao, Y, Stange, KE & Sun, X 1970, 'On the Complexity of Isomorphism Problems for Tensors, Groups, and Polynomials V: Over Commutative Rings', Proceedings of the 57th Annual ACM Symposium on Theory of Computing, STOC '25: 57th Annual ACM Symposium on Theory of Computing, ACM, pp. 777-784.
View/Download from: Publisher's site

Hong, X, Gao, D, Li, S, Ying, S & Ying, M 1970, 'Image Computation for Quantum Transition Systems', 2025 Design, Automation & Test in Europe Conference (DATE), 2025 Design, Automation & Test in Europe Conference (DATE), IEEE, pp. 1-7.
View/Download from: Publisher's site

Lin, H, Deng, R, Yao, CZ, Ji, Z & Ying, M 1970, 'Control Flow Adaption: An Efficient Simulation Method for Noisy Quantum Networks', Proceedings IEEE INFOCOM.
View/Download from: Publisher's site
View description>>

Quantum network research at both the software stack and hardware implementation level has become an exciting area of quantum information science. Although demonstrations of small-scale quantum networks have emerged in the past decade, quantum communication and computation hardware remain scarce resources today. As a result, the evaluation and validation of quantum network protocols primarily rely on classical simulators rather than real quantum networks. This paper introduces a novel quantum network simulation method called control flow adaptation, which enhances standard tensor network simulations. This method enables accurate and efficient simulations of many important quantum network protocols by carefully leveraging the control flow structures of them. Furthermore, we have developed a prototype quantum network simulator, qns-3, as a module for ns-3. This new module implements the control flow adaptation technique and applies it to a wide range of protocols. All related code is open-source [1]. We believe the development of the control flow adaptation method and the qns-3 simulator represents a step forward in quantum network research, offering a versatile and scalable platform for testing and verifying quantum network protocols on classical computers.

Lin, Y, Guan, J, Fang, W, Ying, M & Su, Z 1970, 'VeriQR: A Robustness Verification Tool for Quantum Machine Learning Models', Lecture Notes in Computer Science Including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics, pp. 403-421.
View/Download from: Publisher's site
View description>>

Adversarial noise attacks present a significant threat to quantum machine learning (QML) models, similar to their classical counterparts. This is especially true in the current Noisy Intermediate-Scale Quantum era, where noise is unavoidable. Therefore, it is essential to ensure the robustness of QML models before their deployment. To address this challenge, we introduce VeriQR, the first tool designed specifically for formally verifying and improving the robustness of QML models, to the best of our knowledge. This tool mimics real-world quantum hardware’s noisy impacts by incorporating random noise to formally validate a QML model’s robustness. VeriQR supports exact (sound and complete) algorithms for both local and global robustness verification. For enhanced efficiency, it implements an under-approximate (complete) algorithm and a tensor network-based algorithm to verify local and global robustness, respectively. As a formal verification tool, VeriQR can detect adversarial examples and utilize them for further analysis and to enhance the local robustness through adversarial training, as demonstrated by experiments on real-world quantum machine learning models. Moreover, it permits users to incorporate customized noise. Based on this feature, we assess VeriQR using various real-world examples, and experimental outcomes confirm that the addition of specific quantum noise can enhance the global robustness of QML models. These processes are made accessible through a user-friendly graphical interface provided by VeriQR, catering to general users without requiring a deep understanding of the counter-intuitive probabilistic nature of quantum computing.

Nair, SR, Southwell, B & Ferrie, C 1970, 'Short-time quantum Fourier transform processing', ICASSP 2025 - 2025 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), ICASSP 2025 - 2025 IEEE International Conference on Acoustics, Speech and Signal Processing (ICASSP), IEEE, pp. 1-5.
View/Download from: Publisher's site
View description>>

Algorithms for processing data in short-time batches are critical for both online and offline processing of streamed and large data respectively due to the quadratic relation between signal length and computational cost of convolution-based processing schemes. Whilst quantum analogs to some digital signal processing algorithms have been discovered, including the quantum Fourier transform (QFT), there has been no development of short-time processing techniques in the quantum domain. In this manuscript, we introduce the short-time QFT (STQFT) processing technique to bridge this gap in research. We develop a novel overlap-add reconstruction technique in the quantum domain using a permutation gate to combine subsequent windows. With this in mind, we discuss convolution under our novel STQFT processing scheme. We demonstrate filtering in the quantum Fourier domain with a filter stored in a quantum register as well as in a block encoded unitary gate. Throughout the paper, we elaborate upon implementation details such as applying DC offsets to input signals, skipping input data frames whenever necessary, the use of overlap-save as a reconstruction technique and mitigating time-varying scaling due to normalization of the windowed input data and filters.

Tiwari, A, Sundaram, RG, Gupta, H, Ramakrishnan, CR & Yu, N 1970, 'Uncomputing Ancilla Qubits in Quantum Circuits', 2025 International Conference on Quantum Communications, Networking, and Computing (QCNC), 2025 International Conference on Quantum Communications, Networking, and Computing (QCNC), IEEE, pp. 379-387.
View/Download from: Publisher's site

Wang, Z, Shi, X, Ji, Z & Yin, X 1970, 'Quantum Network Optimization: From Optimal Routing to Fair Resource Allocation', Abstracts of the 2025 ACM SIGMETRICS International Conference on Measurement and Modeling of Computer Systems, SIGMETRICS '25: ACM SIGMETRICS International Conference on Measurement and Modeling of Computer Systems, ACM, pp. 142-144.
View/Download from: Publisher's site

Beigi, S, Hirche, C & Tomamichel, M 2025, 'Some properties and applications of the new quantum $f$-divergences'.

George, I & Tomamichel, M 2025, 'A Unified Approach to Quantum Contraction and Correlation Coefficients'.

Girardi, F, Oufkir, A, Regula, B, Tomamichel, M, Berta, M & Lami, L 2025, 'Quantum umlaut information'.

Girardi, F, Oufkir, A, Regula, B, Tomamichel, M, Berta, M & Lami, L 2025, 'Umlaut information'.

Seyfried, J, Sen, S & Tomamichel, M 2025, 'Testing (Conditional) Mutual Information'.

Weng, C-X, Qin, M, Hu, Y & Tomamichel, M 2025, 'A tight consecutive measurement theorem and its applications'.