Past seminars

Title: Categories of abstract and noncommutative measurable spaces

Abstract: In quantum probability, the category of $$C^$$-algebras and completely positive unital (cpu) maps is a well-established setting. However, its classical side, given by commutative $$C^$$-algebras, does not contain all regular conditional probabilities, a central concept in classical probability. This shortcoming is due to the inherent topological nature of $$C^*$$-algebras, which ties them to continuous rather than measurable structures. To address this, we investigate what noncommutative (or quantum) measurable spaces should be, by establishing adjunctions and equivalences between special classes of $$C^*$$-algebras and cpu maps and categories of measurable spaces and Markov kernels. On the classical side, these can be equivalently described by Boolean σ-algebras (also known as abstract measurable spaces). Moreover, our operator-algebraic analysis equips these structures with a generalized notion of Markov kernels, realized as POVMs. Ultimately, we obtain a categorical framework in which both classical and quantum probability coexist, and the classical side has regular conditional probabilities. Read more

Title: Formal Verification of Noisy Quantum Reinforcement Learning Policies

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 classical–quantum sweet spot: trained QRL policies that execute efficiently on quantum hardware, yet remain tractable for classical probabilistic model checking despite being too slow for real-time classical deployment.