# Formal Verification of Noisy Quantum Reinforcement Learning Policies

arXiv: https://arxiv.org/abs/2512.01502 · HTML: https://mlsanity.com/paper/2512.01502/

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Placed in Quantum reinforcement learning, one of 15 directions in Deep reinforcement learning methods.
- Builds on 34 of its 77 references that are in the map.
- First posted on arXiv 1 Dec 2025.

## Placed in

- Deep reinforcement learning methods / [Quantum reinforcement learning](https://mlsanity.com/deeprl/quantum-reinforcement-learning/)

## Builds on (most cited first, 30 of 34)

- [Challenges and Opportunities in Quantum Machine Learning](https://mlsanity.com/paper/2303.09491/) (2023)
- [Parametrized quantum policies for reinforcement learning](https://mlsanity.com/paper/2103.05577/) (2021)
- [Better than classical? The subtle art of benchmarking quantum machine learning models](https://mlsanity.com/paper/2403.07059/) (2024)
- [Omega-Regular Objectives in Model-Free Reinforcement Learning](https://mlsanity.com/paper/1810.00950/) (2018)
- [The Probabilistic Model Checker Storm](https://mlsanity.com/paper/2002.07080/) (2020)
- [Scalar reward is not enough: A response to Silver, Singh, Precup and Sutton (2021)](https://mlsanity.com/paper/2112.15422/) (2021)
- [A Survey on Quantum Reinforcement Learning](https://mlsanity.com/paper/2211.03464/) (2022)
- [Verification of Markov Decision Processes using Learning Algorithms](https://mlsanity.com/paper/1402.2967/) (2014)
- [An Inductive Synthesis Framework for Verifiable Reinforcement Learning](https://mlsanity.com/paper/1907.07273/) (2019)
- [Quantum Data Encoding: A Comparative Analysis of Classical-to-Quantum Mapping Techniques and Their Impact on Machine Learning Accuracy](https://mlsanity.com/paper/2311.10375/) (2023)
- [COOL-MC: A Comprehensive Tool for Reinforcement Learning and Model Checking](https://mlsanity.com/paper/2209.07133/) (2022)
- [Robustness Verification of Quantum Classifiers](https://mlsanity.com/paper/2008.07230/) (2020)
- [Permissive Controller Synthesis for Probabilistic Systems](https://mlsanity.com/paper/1504.04662/) (2015)
- [Policy Gradients using Variational Quantum Circuits](https://mlsanity.com/paper/2203.10591/) (2022)
- [Statistically Model Checking PCTL Specifications on Markov Decision Processes via Reinforcement Learning](https://mlsanity.com/paper/2004.00273/) (2020)
- [Benchmarking Quantum Reinforcement Learning](https://mlsanity.com/paper/2501.15893/) (2025)
- [Safety-Oriented Pruning and Interpretation of Reinforcement Learning Policies](https://mlsanity.com/paper/2409.10218/) (2024)
- [Nav-Q: Quantum Deep Reinforcement Learning for Collision-Free Navigation of Self-Driving Cars](https://mlsanity.com/paper/2311.12875/) (2023)
- [An Introduction to Quantum Reinforcement Learning (QRL)](https://mlsanity.com/paper/2409.05846/) (2024)
- [Quantum Software Engineering: Roadmap and Challenges Ahead](https://mlsanity.com/paper/2404.06825/) (2024)
- [Targeted Adversarial Attacks on Deep Reinforcement Learning Policies via Model Checking](https://mlsanity.com/paper/2212.05337/) (2022)
- [Probabilistic Model Checking of Stochastic Reinforcement Learning Policies](https://mlsanity.com/paper/2403.18725/) (2024)
- [Trainability issues in quantum policy gradients](https://mlsanity.com/paper/2406.09614/) (2024)
- [Robustness and Generalization in Quantum Reinforcement Learning via Lipschitz Regularization](https://mlsanity.com/paper/2410.21117/) (2024)
- [Assessing the Impact of Noise on Quantum Neural Networks: An Experimental Analysis](https://mlsanity.com/paper/2311.14057/) (2023)
- [Faster and Better Quantum Software Testing through Specification Reduction and Projective Measurements](https://mlsanity.com/paper/2405.15450/) (2024)
- [Quantum Machine Learning-based Test Oracle for Autonomous Mobile Robots](https://mlsanity.com/paper/2508.02407/) (2025)
- [Quantum Circuit Mutants: Empirical Analysis and Recommendations](https://mlsanity.com/paper/2311.16913/) (2023)
- [Q-Policy: Quantum-Enhanced Policy Evaluation for Scalable Reinforcement Learning](https://mlsanity.com/paper/2505.11862/) (2025)
- [Assessing Quantum Extreme Learning Machines for Software Testing in Practice](https://mlsanity.com/paper/2410.15494/) (2024)

## Abstract (arXiv)

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.