Samuel Teuber
LightNews LightNews
teuber.bsky.social
Samuel Teuber
@teuber.bsky.social
150 followers 590 following 21 posts
Doctoral Researcher at KIT's Computer Science Department | Formal Methods for Software & AI (Focus on CPS and Fairness Verification)
Currently migrating from Twitter (@teuber_dev)
www.teuber.dev
Posts Replies Media Videos
teuber.bsky.social
Thank you @etapsconf.bsky.social for the great event — so many interesting talks and discussions at #etaps this year!
I also had the opportunity to present my #tacas paper on verifying behavioral equivalence of neural networks 😃
Me standing in the front of a lecture hall at McMaster University during the ETAPS conference: The slides read "Revisiting Differential Verification: Equivalence Verification with Confidence"
May 9, 2025 at 1:59 PM
teuber.bsky.social
This is really cool!
I'm obviously nitpicking here, but I think it's very meta that quite a few papers on Neural Network Verification are right around the "decision boundary" of the Adversarial Robustness cluster...
December 8, 2024 at 11:09 PM
teuber.bsky.social
Perfection
November 17, 2024 at 11:44 PM
teuber.bsky.social
We applied the overall approach to multiple case studies including Vertical Airborne Collision Avoidance (VCAS):
Here, we analyzed NNs from prior work and found numerous concrete safety problems -- but see for yourself (any plane trajectory in the red region is BAD!):
Six examples of the following: A schematic plot of two planes flying towards each other at equal vertical positions. An orange line indicates the original flight trajectory of the plane on the left, and a blue line indicates an updated trajectory that was proposed by a neural network. The latter would lead to a crash of the two planes or at the very least ot a Near Mid Air Collision.
November 17, 2024 at 6:04 PM
teuber.bsky.social
We start with a dL safety proof for an abstract control envelope. Our approach then derives an NN specification. We rigorously define the NN's semantics in dL via "nondeterministic mirrors".
Verification of the NN is then mirrored by a proof of infinite-time safety in dL.
An overview of the safety guarantee provided by our approach: We start off with a provably safe control envelope (upper right) and a neural network (lower left). Our objective is to prove the safety of a neural network control system. By encoding the neural network as a program in differential dynamic logic, we derive the program for which we would like to prove safety (lower right). However, reasoning about this program directly is infeasible due to the subsymbolic reasoning of NNs. Instead, we derive a specification for the NN in isolation based on the provably safe control envelope (upper left). By verifying this specification, we simultaneously perform a refinement proof which shows that the neural network control system is safe.
November 17, 2024 at 6:04 PM
teuber.bsky.social
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):
A schematic plot of two planes flying towards each other at equal vertical positions. An orange line indicates the original flight trajectory of the plane on the left, and a blue line indicates an updated trajectory that was proposed by a neural network. The latter would lead to a crash of the two planes.
November 17, 2024 at 6:04 PM