Technical Summary: Formal Verification of Noisy Quantum Reinforcement Learning Policies

Problem Statement

Quantum Reinforcement Learning (QRL) leverages quantum phenomena, such as superposition and entanglement, to develop sequential decision-making policies that potentially outperform classical counterparts. However, unlike classical Reinforcement Learning (RL), QRL policies are implemented via Variational Quantum Circuits (VQCs) and are inherently subject to additional uncertainties. These include stochastic outcomes from quantum measurements and hardware imperfections (noise) such as bit-flip, phase-flip, depolarizing, and amplitude damping.

These uncertainties can distort action selection, leading to unsafe agent behaviors (e.g., collisions) that standard reward functions may fail to capture. While formal verification methods like probabilistic model checking exist for classical RL and quantum communication protocols, there is a lack of systematic approaches to verify whether trained QRL policies satisfy safety requirements under specific quantum noise conditions. Furthermore, access to physical quantum hardware is prohibitively expensive, making pre-deployment verification essential for safety-critical applications.

Methodology: QVerifier

The paper introduces QVerifier, a formal verification method designed to rigorously analyze trained QRL policies against safety properties, explicitly accounting for quantum measurement uncertainty and modeled hardware noise. The approach utilizes probabilistic model checking via the Storm model checker.

The methodology proceeds in two primary stages:

1. Induced Discrete-Time Markov Chain (DTMC) Construction:

   • Given a Markov Decision Process (MDP) representing the environment and a trained memoryless stochastic policy $\pi$, QVerifier incrementally constructs a formal model of the policy-environment interaction.
   • The method expands all states reachable under the policy. For each state $s$, it considers all actions $a$ with non-zero probability.
   • Transition probabilities $P^\pi(s, s')$ are computed by marginalizing over actions: $P^\pi(s, s') = \sum_{a} \pi(a|s) \cdot Tr(s, a, s')$.
   • Noise Integration: When verifying under noise, the policy $\pi_\theta$ is replaced by a noisy policy $\pi^E_\theta$. The action probabilities are derived analytically from the final density matrix $\rho'$ after applying a quantum noise channel $E$ to the unitary evolution $U_\theta$. This allows the model to capture how gate-level noise alters the transition dynamics without relying on empirical sampling.
   • The construction terminates when all relevant states for the safety property have been visited, avoiding unnecessary expansion.

2. Probabilistic Model Checking:

   • The resulting DTMC is input into the Storm model checker.
   • Safety requirements are formalized using Probabilistic Computation Tree Logic (PCTL), supporting properties such as reachability ($P_{\sim p}(F \phi)$) and "until" properties ($P_{\sim p}(\phi U \psi)$).
   • Storm verifies whether the property is satisfied and computes the exact probability of satisfaction or violation.

Scope and Limitations: The method targets memoryless stochastic policies with discrete state and action spaces. It assumes the noise model is known; if a policy is trained on physical hardware with unknown noise characteristics, the verification constitutes an idealized approximation based on the assumed noise model.

Key Contributions

1. QVerifier Framework: The first application of probabilistic model checking to verify trained QRL policies under explicit quantum noise models (bit-flip, phase-flip, depolarizing, and amplitude damping).
2. Exact Analytical Modeling: Unlike methods relying on sampling, QVerifier computes action probabilities directly from density matrices, enabling exact transition probabilities and continuous noise-parameter sweeps.
3. Comparative Analysis: An approach for the exact comparison of QRL and classical RL performance regarding safety properties and verification overhead.
4. Pre-Deployment Safety: A method to identify safety violations and beneficial noise regimes before deploying policies on expensive quantum hardware.

Experimental Results

The authors evaluated QVerifier across three environments (Frozen Lake, Ski, and Freeway) using six policies (three QRL and three classical RL baselines).

• Performance Comparison (Noise-Free): Under ideal, noise-free conditions, classical REINFORCE policies consistently outperformed QRL policies in terms of reachability probability. QRL policies also exhibited longer verification times due to the computational overhead of simulating quantum circuits at each state.
• Impact of Quantum Noise:
  • Degradation: Bit-flip and depolarizing noise consistently degraded policy performance across all tasks. Depolarizing noise caused the most significant degradation by pushing quantum states toward maximal randomness.
  • Unexpected Improvement: The study revealed that specific noise models can improve performance. In the Ski environment, low-level amplitude-damping noise improved the QRL policy's goal-reachability probability by 27% compared to the classical RL baseline. This beneficial effect vanished as noise levels increased.
  • Phase-Flip: Showed slight performance improvements for the QRL Ski policy.
• Safety Violations: The QRL policy violated a complex "until" safety property (traversing a specific path without hitting a hazard) more frequently than the classical policy in the Frozen Lake environment.

Significance and Claims

The paper positions QVerifier as addressing a critical gap in the deployment of safety-critical quantum machine learning. By enabling rigorous, pre-deployment verification on classical hardware, it mitigates the prohibitive costs and limited availability of quantum hardware testing.

The authors claim that QVerifier targets a "sweet spot" between classical and quantum computation: it analyzes trained QRL policies that are small enough to be modeled classically for verification but are intended for execution on quantum hardware. The results demonstrate that noise is not universally detrimental; specific noise regimes can act as regularizers, improving policy performance. Consequently, QVerifier provides a tool not only to detect safety violations but also to identify optimal hardware noise characteristics for specific QRL tasks, guiding hardware selection and error budget allocation.