Title: GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning
Speakers: Mark Chevallier
Abstract:

We present GradSTL, the first fully comprehensive implementation of signal temporal logic (STL) suitable for integration with neurosymbolic learning. In particular, GradSTL can successfully evaluate any STL constraint over any signal, regardless of how it is sampled. Our formally verified approach specifies smooth STL semantics over tensors, with formal proofs of soundness and of correctness of its derivative function. Our implementation is generated automatically from this formalisation, without manual coding, guaranteeing correctness by construction. We show via a case study that using our implementation, an optimiser learns to satisfy a pre-specified STL constraint. Our approach offers a highly rigorous foundation for integrating signal temporal logic and learning by gradient descent. During the presentation, we will discuss why STL is important for learning functions of continuous time and its limitations. We will also discuss the verification and code generation methods we use to ensure the correctness of the implementation.