Unifying speaker Thomas A. Henzinger
Tom Henzinger is the President of the Institute of Science and Technology Austria (ISTA). He holds a Ph.D. from Stanford University and Dr.h.c. degrees from Fourier University in Grenoble and from Masaryk University in Brno. He was Assistant Professor at Cornell University and Professor at the University of California, Berkeley. He was also Director at the Max-Planck Institute for Computer Science in Saarbrücken and Professor at EPFL in Lausanne. His research focuses on the theory of software systems, especially models, algorithms, and tools for the design and verification of reliable software systems. His HyTech tool was the first model checker for mixed discrete-continuous systems. He is a member of the US National Academy of Sciences, the American Academy of Arts and Sciences, Academia Europaea, the German Academy of Sciences (Leopoldina), and the Austrian Academy of Sciences. He is also a Fellow of the AAAS, the ACM, and the IEEE. He has received the Robin Milner Award of the Royal Society, the EATCS Award of the European Association for Theoretical Computer Science, the Wittgenstein Award of the Austrian Science Fund, and two Advanced Grants of the European Research Council.
Talk
A Learner-Verifier Framework for Neural Network Controllers and Certificates of Stochastic Systems
Monday, 9:00
Room: Auditorium
Reinforcement learning has received much attention for learning controllers of deterministic systems. We present a learner-verifier framework for stochastic control systems. Our method formally guarantees conjunctions of reachability and safety properties. Given a property and a lower bound on the probability of the property being satisfied, our framework jointly learns a control policy and a formal certificate for the probabilistic property. Both the control policy and the formal certificate are continuous functions from states to reals, which are learned as parameterized neural networks. While in the deterministic case, the certificates are invariant and barrier functions for safety, or Lyapunov and ranking functions for liveness, in the stochastic case the certificates are supermartingales. For certificate verification, we use interval arithmetic abstract interpretation to bound the expected values of neural network functions.
This is joint work with Krishnendu Chatterjee, Mathias Lechner, and Djordje Zikelic. The talk unifies and summarizes
results from the following two papers:
[1] Mathias Lechner, Djordje Zikelic, Krishnendu Chatterjee, Thomas A. Henzinger: Stability Verification in Stochastic
Control Systems via Neural Network Supermartingales. AAAI 2022.
[2] Djordje Zikelic, Mathias Lechner, Thomas A. Henzinger, Krishnendu Chatterjee: Learning Control Policies for
Stochastic Systems with Reach-avoid Guarantees. AAAI 2023.