Bridging Logic and Learning: Decoding Temporal Logic Embeddings via Transformers

TL;DR

This paper presents a Transformer-based model that inverts semantic embeddings of Signal Temporal Logic formulae, enabling the generation of valid, simplified formulas from embeddings for applications like requirement mining.

Contribution

The authors introduce a novel Transformer decoder approach to invert STL embeddings, allowing for accurate and semantically consistent formula generation from continuous representations.

Findings

Model generates valid formulas after 1 epoch

Generalizes to new semantics in about 10 epochs

Decodes embeddings into simpler, semantically close formulas

Abstract

Continuous representations of logic formulae allow us to integrate symbolic knowledge into data-driven learning algorithms. If such embeddings are semantically consistent, i.e. if similar specifications are mapped into nearby vectors, they enable continuous learning and optimization directly in the semantic space of formulae. However, to translate the optimal continuous representation into a concrete requirement, such embeddings must be invertible. We tackle this issue by training a Transformer-based decoder-only model to invert semantic embeddings of Signal Temporal Logic (STL) formulae. STL is a powerful formalism that allows us to describe properties of signals varying over time in an expressive yet concise way. By constructing a small vocabulary from STL syntax, we demonstrate that our proposed model is able to generate valid formulae after only 1 epoch and to generalize to the semantics of the logic in about 10 epochs. Additionally, the model is able to decode a given embedding into formulae that are often simpler in terms of length and nesting while remaining semantically close (or equivalent) to gold references. We show the effectiveness of our methodology across various levels of training formulae complexity to assess the impact of training data on the model's ability to effectively capture the semantic information contained in the embeddings and generalize out-of-distribution. Finally, we deploy our model for solving a requirement mining task, i.e. inferring STL specifications that solve a classification task on trajectories, performing the optimization directly in the semantic space.