# Bridging Logic and Learning: Decoding Temporal Logic Embeddings via Transformers

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

## Key facts

- Cited by 1 papers in the map (data through 14 Oct 2026).
- Builds on 22 of its 38 references that are in the map.
- First posted on arXiv 10 Jul 2025.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [Gaussian Error Linear Units (GELUs)](https://mlsanity.com/paper/1606.08415/) (2016)
- [A Survey of Large Language Models](https://mlsanity.com/paper/2303.18223/) (2023)
- [Neurosymbolic AI: The 3rd Wave](https://mlsanity.com/paper/2012.05876/) (2020)
- [End-to-end symbolic regression with transformers](https://mlsanity.com/paper/2204.10532/) (2022)
- [Transformer-based Planning for Symbolic Regression](https://mlsanity.com/paper/2303.06833/) (2023)
- [From Statistical Relational to Neurosymbolic Artificial Intelligence: a Survey](https://mlsanity.com/paper/2108.11451/) (2021)
- [ODEFormer: Symbolic Regression of Dynamical Systems with Transformers](https://mlsanity.com/paper/2310.05573/) (2023)
- [nl2spec: Interactively Translating Unstructured Natural Language to Temporal Logics with Large Language Models](https://mlsanity.com/paper/2303.04864/) (2023)
- [Teaching Temporal Logics to Neural Networks](https://mlsanity.com/paper/2003.04218/) (2020)
- [Embedding Symbolic Knowledge into Deep Networks](https://mlsanity.com/paper/1909.01161/) (2019)
- [Formal Specifications from Natural Language](https://mlsanity.com/paper/2206.01962/) (2022)
- [DeepSTL -- From English Requirements to Signal Temporal Logic](https://mlsanity.com/paper/2109.10294/) (2021)
- [Interpretable Classification of Time-Series Data using Efficient Enumerative Techniques](https://mlsanity.com/paper/1907.10265/) (2019)
- [Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling](https://mlsanity.com/paper/1911.06904/) (2019)
- [A Robust Genetic Algorithm for Learning Temporal Specifications from Data](https://mlsanity.com/paper/1711.06202/) (2017)
- [STL2vec: Signal Temporal Logic Embeddings for Control Synthesis With Recurrent Neural Networks](https://mlsanity.com/paper/2109.04636/) (2021)
- [Learning Model Checking and the Kernel Trick for Signal Temporal Logic on Stochastic Processes](https://mlsanity.com/paper/2201.09928/) (2022)
- [Retrieval-Augmented Mining of Temporal Logic Specifications from Data](https://mlsanity.com/paper/2405.14355/) (2024)
- [stl2vec: Semantic and Interpretable Vector Representation of Temporal Logic](https://mlsanity.com/paper/2405.14389/) (2024)
- [Cause Mining and Controller Synthesis with STL](https://mlsanity.com/paper/1904.03649/) (2019)
- [Learning to Estimate System Specifications in Linear Temporal Logic using Transformers and Mamba](https://mlsanity.com/paper/2405.20917/) (2024)

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

- [Distilling Formal Logic into Neural Spaces: A Kernel Alignment Approach for Signal Temporal Logic](https://mlsanity.com/paper/2603.05198/) (2026)

## Abstract (arXiv)

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.