# GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning

arXiv: https://arxiv.org/abs/2508.04438 · HTML: https://mlsanity.com/paper/2508.04438/

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Placed in Reasoning benchmarks and evaluation, one of 17 directions in LLM reasoning.
- Builds on 3 of its 23 references that are in the map.
- First posted on arXiv 6 Aug 2025.

## Placed in

- LLM reasoning / [Reasoning benchmarks and evaluation](https://mlsanity.com/lr/reasoning-benchmarks-and-evaluation/)

## Builds on (most cited first, 3 of 3)

- [BarrierNet: A Safety-Guaranteed Layer for Neural Networks](https://mlsanity.com/paper/2111.11277/) (2021)
- [TLINet: Differentiable Neural Network Temporal Logic Inference](https://mlsanity.com/paper/2405.06670/) (2024)
- [Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces](https://mlsanity.com/paper/2501.13712/) (2025)

## Built on by (most cited first, 1 of 1)

- [Quantitative Linear Logic for Neuro-Symbolic Learning and Verification](https://mlsanity.com/paper/2605.13845/) (2026)

## Abstract (arXiv)

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.