From Compositional to Relational Verification of AI-based Systems
Talk by Samuel Teuber
Abstract: Formally specifying, let alone verifying, properties of systems that combine heterogeneous subsystems is inherently challenging. In the first part of this talk, I will introduce Heterogeneous Dynamic Logic (HDL) as a framework for combining reasoning principles from distinct (dynamic) program logics in a modular and compositional way. HDL mirrors the architecture of satisfiability modulo theories (SMT): Individual dynamic logics, along with their calculi, are treated as dynamic theories that can be combined to reason about heterogeneous systems whose components are verified using distinct proof infrastructures.
The second part of this talk discusses the application of HDL to neural network control systems. Logic-based verification enables us to leverage control theoretic safety proofs for cyber-physical systems for verifying the safety of neural network controllers all the way down to the fixed-point arithmetic level of an FPGA (an FMCAD'25 result that HDL now lets us justify much more directly). The final part of my talk will broaden the scope and investigate the safety of AI-based systems which lack a comprehensive system model. I will argue that relational verification can provide meaningful best-effort guarantees in this setting and present an abstract interpretation-based approach for the relational verification of neural networks that has applications to neural network equivalence and global robustness.
Bio: Samuel Teuber is a PhD Candidate at Karlsruhe Institute of Technology (KIT) in Germany advised by Bernhard Beckert at the Application-oriented Formal Verification group. His research develops logical foundations and practical tools for the verification of AI-based heterogeneous systems, that is, systems combining software, AI, and physical components. Concrete applications include the formal verification of neural network control systems, the verification of algorithmic fairness, and the derivation of global relational guarantees for neural networks via differential verification. He holds an M.Sc. degree in Computer Science from KIT and completed his Master’s Thesis in the Logical Systems Lab at Carnegie Mellon University under the supervision of André Platzer. During his bachelor studies he spent a year abroad at ENSIMAG (Grenoble, France) and participated in the CERN Openlab Summer Student Program (Geneva, Switzerland).
