IsaGrad paper accepted at LogicNN 2026
Our paper “IsaGrad: Verified Automatic Differentiation over Computational Graphs in Imperative HOL” has been accepted and will be presented at LogicNN, FLOC 2026.
neurosymbolic
Our paper on differentiable Signal Temporal Logic for neurosymbolic AI has been published by LIPIcs
GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning
Authors
Part of: Volume: 32nd International Symposium on Temporal Representation and Reasoning (TIME 2025)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Symposium on Temporal Representation and Reasoning (TIME)
Our pre-print on differentiable Signal Temporal Logic for neural learning is out on arXiv
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, a neurosymbolic process 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.
Paper: https://www.arxiv.org/abs/2508.04438
This work has been accepted as a long paper at TIME 2025 and will be presented at the conference at the end of August 2025.