As machine learning is deployed in high-stakes , the urgency of increasing its trustworthiness is undeniable. Methods designed to enforce bounded outputs aim to keep model behavior within clearly defined limits, preventing deviations that could lead to severe consequences . A rapidly emerging field of quantum machine learning (QML) inherits these risks and expands both the attack surface and the potential consequences of failure, motivating further research in this area.
June 25, 2026
© iStock/yekorzh
In my previous post, “How secure are quantum machine learning systems?” the focus was on heuristic defenses against adversarial attacks in QML. These defense measures proved to be reliable against a variety of existing attacks, but what happens when hackers craft smarter, more advanced attacks against AI models? Is there a more general way to verify the robustness of models? Formal verification offers a rigorous alternative that aims to provide a framework to verify the robustness of an AI model under a defined general threat model, yielding either a provable robustness guarantee or a verified counterexample.
However, as with many (theoretical) formal methods, the design process is nontrivial and the approach can be computationally expensive if done naively. This blog postsummarizes the book chapter that the Quantum Computing Department at the Fraunhofer Institute for Cognitive Systems IKS wrote in collaboration with the Data Analytics and Machine Learning Group at TUM on formal verification methods of quantum AI as well as quantum-enhanced methods for verification of classical AI.
© Fraunhofer IKS
To begin,let’s look at the background on formal verification methods. Exact methods provide tight bounds (both upper and lower) and hence can reliably certify both robustness (the model is secure under a given threat model) and non‑robustness (there exist adversarial examples within this threat model). The downside is that these methods are often computationally expensive, typically requiring the solution of NP-hard optimization problems.
As a result, for neural networks of even moderate size, e.g. those with a few hundred neurons, exact verification quickly becomes intractable, limiting its practical use to relatively small models or highly constrained settings. To mitigate this cost, approximate methods relax the underlying optimization problem, usually yielding only partial guarantees, such as lower bounds / robustness-only certificates, but at substantially reduced computational effort. Complementing these are stochastic methods, which instead provide probabilistic guarantees. They certify that desired properties hold with high probability, thereby trading absolute certainty for improved scalability and efficiency.
An emerging alternative is to use quantum or quantum–classical hybrid routines to accelerate computationally expensive formal verification methods, a topic that will be discussed later. In parallel, ongoing research aims to tighten approximate bounds for a broader range of model families while keeping computational costs manageable.
Formal verification of quantum AI surveys the spectrum of methods available to certify the robustness and correctness of quantum models. Significant progress has been made in this area, notably by Fraunhofer IKS and TUM as part of Bavarian Competence Center Quantum Security and Data Science(BayQS)in which the teams are working in QC-based certification of Neural Network project, who have helped shape foundational approaches. A central theme is treating quantum noise not only as a challenge but as a potential ally: quantum systems are inherently noisy, and researchers are exploring whether controlled noise can certify or even enhance robustness.
An important notion underpinning these methods is Differential Privacy (DP), a rigorous framework for quantifying how effectively an algorithm conceals sensitive information in its input data. A key feature of DP is the introduction of randomness, which, in the quantum setting, comes essentially "for free" through intrinsic hardware noise. Although quantum noise is typically viewed as a challenge, emerging work shows it can be harnessed within a DP framework to yield provable robustness guarantees. These approaches as well as others provide a principled foundation for the rigorous verification of quantum AI applications.
Given the intractability of exact verification, it is crucial to investigate quantum computing as a means to reduce the computational burden. For example, Mixed-Integer Linear Programming (MILP) formulations for neural networks with piecewise-linear activations can provide tight, provable guarantees but are NP-hard and scale poorly. To address this, decomposition methods exploit problem structure to split large MILPs into smaller, more manageable subproblems. The Fraunhofer IKS and TUM teams have extensively studied such approaches within BayQC, and their work paired with constraints of near-term quantum hardware has given rise to hybrid quantum–classical decompositions that combine classical linear-programming solvers for the continuous parts with quantum optimizers (e.g., Quantum Approximate Optimization Algorithm, QAOA) for the binary subproblems. These methods, although they do not yet outperform classical benchmarks, lay an important foundational step toward scalable quantum-assisted verification.
Looking ahead, as hardware matures towards fault-tolerance, different algorithms such as Grover’s search and Quantum Amplitude Amplification (QAA) will become more feasible. These techniques offer provable computational speedups, and researchers worldwide (including the team at Fraunhofer IKS) are actively pursuing practical paths to deploy them as soon as possible. Beyond accelerating exact verification, they also hold promise for robustness certification via Randomized Smoothing. In randomized smoothing, a base classifier is transformed into a smoothed classifier with a certified robustness radius, but at the cost of a high number of Monte Carlo evaluations. Quantum methods such as QAA can quadratically reduce the number of queries required to estimate the probability of correct classification, significantly accelerating the certification process.
This research is supported by the Bavarian Ministry of Economic Affairs, Regional Development and Energy with funds from the Hightech Agenda Bayern.
