GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866916884055588864 |
|---|---|
| author | Chevallier, Mark Smola, Filip Schmoetten, Richard Fleuriot, Jacques D. |
| author_facet | Chevallier, Mark Smola, Filip Schmoetten, Richard Fleuriot, Jacques D. |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2508_04438 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning Chevallier, Mark Smola, Filip Schmoetten, Richard Fleuriot, Jacques D. Logic in Computer Science 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. |
| title | GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning |
| topic | Logic in Computer Science |
| url | https://arxiv.org/abs/2508.04438 |