Formal Verification of Noisy Quantum Reinforcement Learning Policies

TL;DR

This paper introduces QVerifier, a formal verification method using probabilistic model checking to ensure the safety of quantum reinforcement learning policies under various noise conditions, addressing a critical gap in pre-deployment safety assurance.

Contribution

QVerifier is the first systematic approach to verify the safety of trained QRL policies considering quantum noise, combining probabilistic modeling with formal safety checks.

Findings

QVerifier accurately assesses safety under different noise models.

Noise can both degrade and unexpectedly improve policy safety.

Pre-deployment verification is crucial for quantum reinforcement learning applications.

Abstract

Quantum reinforcement learning (QRL) aims to use quantum effects to create sequential decision-making policies that achieve tasks more effectively than their classical counterparts. However, QRL policies face uncertainty from quantum measurements and hardware noise, such as bit-flip, phase-flip, and depolarizing errors, which can lead to unsafe behavior. Existing work offers no systematic way to verify whether trained QRL policies meet safety requirements under specific noise conditions. We introduce QVerifier, a formal verification method that applies probabilistic model checking to analyze trained QRL policies with and without modeled quantum noise. QVerifier builds a complete model of the policy-environment interaction, incorporates quantum uncertainty directly into the transition probabilities, and then checks safety properties using the Storm model checker. Experiments across multiple QRL environments show that QVerifier precisely measures how different noise models influence safety, revealing both performance degradation and cases where noise can help. By enabling rigorous safety verification before deployment, QVerifier addresses a critical need: because access to quantum hardware is expensive, pre-deployment verification is essential for any safety-critical use of QRL. QVerifier targets a potential sweet spot between classical and quantum computation, where trained QRL policies could still be modeled classically for probabilistic model checking. When the policy was trained under matching noise conditions, this formal model is exact; when trained on physical hardware, it constitutes an idealized approximation, as unknown hardware noise prevents exact policy modeling.