Bridging Logic and Learning: Decoding Temporal Logic Embeddings via Transformers
This work addresses the need for invertible embeddings to integrate symbolic knowledge into data-driven learning, particularly for requirement mining in temporal logic, though it is incremental as it builds on existing embedding methods.
The paper tackles the problem of inverting semantic embeddings of Signal Temporal Logic (STL) formulae to translate continuous representations back into concrete logic specifications, using a Transformer-based decoder-only model that generates valid formulae quickly and simplifies them while maintaining semantic accuracy.
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.