Martingale-based Methods for Formal Verification and Certified Control of Stochastic Systems

This talk will advocate for the use of martingale-based methods towards the formal verification of infinite state stochastic systems. Stochasticity is commonly used to model and quantify uncertainty in a system, and martingale-based methods present a promising approach to the formal verification of stochastic systems with applications in PL and AI. The key advantage of martingale-based methods is that they provide formal soundness and even certain level of theoretical completeness guarantees, while allowing for fully automated verification algorithms for stochastic system verification. In this talk, we present martingale-based methods for static analysis of probabilistic programs as well as for learning stabilizing control policies in stochastic systems with formal guarantees on stabilization. First, we show that martingale-based methods can be used to design sound and fully automated algorithms for the verification of termination and safety properties in probabilistic programs. Second, we present a recent method that utilizes martingales in order to either learn or formally verify a stabilizing policy for a stochastic system. Stability is one of the most important safety properties of control systems which requires the agent to eventually reach and stabilize within some specified region with probability 1. Our method learns a control policy together with a martingale-based certificate that formally certifies almost-sure stability of the learned policy, both parametrized as neural networks.

Bio
Djordje is a PhD student in computer science at IST Austria, under the supervision of Krishnendu Chatterjee and Petr Novotný. His research focuses on developing algorithms for formally verifying correctness of software and combine ideas from formal verification, programming languages and machine learning in order to design mathematically rigorous yet fully automated methods for providing formal guarantees about programs, systems with learned components and safe learning. Prior to joining IST Austria, he completed his bachelor's and master's degrees in mathematics at the University of Cambridge.