Samuel Teuber @ PLDI

I‘m excited to present my work on Provably Safe Neural Network Control at @horizonomega.org‘s Guaranteed Safe AI online seminar on April 9th. The talk will based on my NeurIPS‘24 paper with some updates on what I’ve been up to since :) Feel free to join if you’re interested:

You want to ensure that your neural network *never* crashes your control system? Our (now accepted 🥳) #NeurIPS paper introduces: - Reusing control theory for NN verification - Verifying *nonlinear arithmetic* specs on NNs This guarantees your NN won't behave like this (1/12):

This project was joint work with Stefan Mitsch and André Platzer. We started working on this project during my visit to CMU (SCS) and continued working on it at KIT. I'm looking forward to presenting it at #neurips2024 in Vancouver. Preprint:

You want to ensure that your neural network *never* crashes your control system? Our (now accepted 🥳) #NeurIPS paper introduces: - Reusing control theory for NN verification - Verifying *nonlinear arithmetic* specs on NNs This guarantees your NN won't behave like this (1/12):

Overall, our work proposes an alternative pathway to safe NNCS autonomy that does not rely on simulations for time-bounded guarantees. Instead, we provide stronger, infinite-time horizon guarantees, but require more apriori reasoning via deductive verification in dL.

You want to ensure that your neural network *never* crashes your control system? Our (now accepted 🥳) #NeurIPS paper introduces: - Reusing control theory for NN verification - Verifying *nonlinear arithmetic* specs on NNs This guarantees your NN won't behave like this (1/12):

We also proved safety for two VCAS scenarios. In these cases, we were able to show that (under some assumptions) the NNs' actions will guarantee safety on an infinite time horizon. "Unfortunately", safe systems make for less pretty pictures... 🥲

You want to ensure that your neural network *never* crashes your control system? Our (now accepted 🥳) #NeurIPS paper introduces: - Reusing control theory for NN verification - Verifying *nonlinear arithmetic* specs on NNs This guarantees your NN won't behave like this (1/12):

We introduce a framework that: - Supports polynomial arithmetic in a sound and complete manner - Significantly simplifies verification for specifications with complicated propositional structure Importantly, we can *lift* off-the-shelf NN verifiers to this setting!

You want to ensure that your neural network *never* crashes your control system? Our (now accepted 🥳) #NeurIPS paper introduces: - Reusing control theory for NN verification - Verifying *nonlinear arithmetic* specs on NNs This guarantees your NN won't behave like this (1/12):

Our approach comes with many advantages: - support for continuous-time control - support for infinite-time safety - no reliance on simulation which incurs approximation errors - rigorous formal foundations in dL - reuse of control theory results But is it applicable in practice?

You want to ensure that your neural network *never* crashes your control system? Our (now accepted 🥳) #NeurIPS paper introduces: - Reusing control theory for NN verification - Verifying *nonlinear arithmetic* specs on NNs This guarantees your NN won't behave like this (1/12):

I'm very excited this work is finally public as it brings together two of my favorite topics: Dynamic Logic and NN Verification. The first part of the paper explains how models of Cyber-Physical Systems in Differential Dynamic Logic (dL) can be used for NN Verification: