stl2vec: Semantic and Interpretable Vector Representation of
Temporal Logic

D 2024

stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic

SAVERI, Gaia; Laura NENZI; Luca BORTOLUSSI a Jan KŘETÍNSKÝ

Základní údaje

Originální název

stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic

Autoři

SAVERI, Gaia; Laura NENZI; Luca BORTOLUSSI a Jan KŘETÍNSKÝ

Vydání

Santiago de Compostela, Spain, ECAI 2024, 27th European Conference on Artificial Intelligence, od s. 1381-1388, 8 s. 2024

Nakladatel

IOS Press

Další údaje

Jazyk

angličtina

Typ výsledku

Stať ve sborníku

Obor

10201 Computer sciences, information science, bioinformatics

Stát vydavatele

Nizozemské království

Utajení

není předmětem státního či obchodního tajemství

Forma vydání

elektronická verze "online"

Kód RIV

RIV/00216224:14330/24:00139091

Organizační jednotka

Fakulta informatiky

ISBN

978-1-64368-548-9

ISSN

DOI

https://doi.org/10.3233/FAIA240638

EID Scopus

2-s2.0-85213343344

Klíčová slova anglicky

Vector Representation of Temporal Logic; Temporal Logic

Štítky

core_A, firank_A

Příznaky

Mezinárodní význam, Recenzováno

Změněno: 31. 3. 2025 17:44, RNDr. Pavel Šmerk, Ph.D.

Anotace

V originále

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.

Návaznosti

MUNI/I/1757/2021, interní kód MU

Název: MUNI Award in Science and Humanities (Akronym: Křetínský)

Investor: Masarykova univerzita, MUNI Award in Science and Humanities, MASH - MUNI Award in Science and Humanities

Citovat

SAVERI, Gaia; Laura NENZI; Luca BORTOLUSSI a Jan KŘETÍNSKÝ. stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic. Online. In ECAI 2024, 27th European Conference on Artificial Intelligence. Santiago de Compostela, Spain: IOS Press, 2024, s. 1381-1388. ISBN 978-1-64368-548-9. Dostupné z: https://doi.org/10.3233/FAIA240638.

@inproceedings{2484764,
   author = {Saveri, Gaia and Nenzi, Laura and Bortolussi, Luca and Křetínský, Jan},
   address = {Santiago de Compostela, Spain},
   booktitle = {ECAI 2024, 27th European Conference on Artificial Intelligence},
   doi = {https://doi.org/10.3233/FAIA240638},
   keywords = {Vector Representation of Temporal Logic; Temporal Logic},
   howpublished = {elektronická verze "online"},
   language = {eng},
   location = {Santiago de Compostela, Spain},
   isbn = {978-1-64368-548-9},
   pages = {1381-1388},
   publisher = {IOS Press},
   title = {stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic},
   year = {2024}
}

TY  - CONF
ID  - 2484764
AU  - Saveri, Gaia - Nenzi, Laura - Bortolussi, Luca - Křetínský, Jan
PY  - 2024
TI  - stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic
PB  - IOS Press
CY  - Santiago de Compostela, Spain
SN  - 9781643685489
KW  - Vector Representation of Temporal Logic
KW  - Temporal Logic
N2  - 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.
ER  -

SAVERI, Gaia; Laura NENZI; Luca BORTOLUSSI a Jan KŘETÍNSKÝ. stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic. Online. In \textit{ECAI 2024, 27th European Conference on Artificial Intelligence}. Santiago de Compostela, Spain: IOS Press, 2024, s.~1381-1388. ISBN~978-1-64368-548-9. Dostupné z: https://doi.org/10.3233/FAIA240638.

Přehled o publikaci