stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic

TL;DR

This paper introduces a method to create finite-dimensional, interpretable vector embeddings of Signal Temporal Logic formulae that faithfully reflect their semantics, enabling continuous learning and integration with neural models.

Contribution

It provides a principled, semantics-preserving embedding technique for STL formulae that does not require training, facilitating symbolic and neural integration in AI.

Findings

Effective in predicting satisfaction probabilities in stochastic processes.

Enables neural models to generate outputs compliant with logical specifications.

Demonstrates improved interpretability and semantic fidelity of logic embeddings.

Abstract

Integrating symbolic knowledge and data-driven learning algorithms is a longstanding challenge in Artificial Intelligence. Despite the recognized importance of this task, a notable gap exists due to the discreteness of symbolic representations and the continuous nature of machine-learning computations. One of the desired bridges between these two worlds would be to define semantically grounded vector representation (feature embedding) of logic formulae, thus enabling to perform continuous learning and optimization in the semantic space of formulae. We tackle this goal for knowledge expressed in Signal Temporal Logic (STL) and devise a method to compute continuous embeddings of formulae with several desirable properties: the embedding (i) is finite-dimensional, (ii) faithfully reflects the semantics of the formulae, (iii) does not require any learning but instead is defined from basic principles, (iv) is interpretable. Another significant contribution lies in demonstrating the efficacy of the approach in two tasks: learning model checking, where we predict the probability of requirements being satisfied in stochastic processes; and integrating the embeddings into a neuro-symbolic framework, to constrain the output of a deep-learning generative model to comply to a given logical specification.