Certifying Almost-Sure Reachability in Unknown MDPs

arXiv:2610.18119v1 Announce Type: cross Abstract: {em Specification-Guided Reinforcement Learning (RL)} has largely concerned itself with learning an optimal policy against a formal specification in an unknown {em Markov Decision Process (MDP)}. We take up the dual question. Given a policy already in hand, can one verify that it is correct against a formal specification in an unknown MDP, using sampling access alone? Such a question arises naturally in safety-critical systems. We investigate it for the {em almost-sure reachability property}, whose correctness is witnessed by a {em ranking supermartingale (RSM)} certificate. Our first finding is negative. In the absence of any further information about the MDP, one can neither learn such a certificate nor verify a candidate one with probabilistic guarantees. On the positive side, we show that, under a mild restriction, a known lower bound p_{min} on nonzero transition probabilities, a correct certificate can be learned with PAC-style guarantees. To the best of our knowledge, this is the first study of learning and verifying certificates for almost-sure reachability in unknown MDPs from sampling access alone. Finally, our experiments show that the p_{min}-based sufficient condition, while sound, is conservative: the learned certificate often remains valid on the true MDP even when the condition fails.

Related

• Offline Reinforcement Learning for Hemodynamic Management of Sepsis in the ICU: a MIMIC-IV Study with Dual Off-Policy Evaluation
• Visually-Guided Policy Optimization for Multimodal Reasoning
• EDGE: Experience-Distillation for Guided Exploration in Agentic Reinforcement Learning
• CoRe-MARL: Cooperative Redistribution Under Unknown Dynamics Using Recurrent Multi-Agent Reinforcement Learning

Source: arXiv cs.AI | 2026-10-15