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.
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, pp. 1-1.
View/Download from: Publisher's site
Le, TP 2025, 'The limits of quantum correlations', Nature Physics, vol. 21, no. 4, pp. 501-502.
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
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.
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.
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'.