# Distilling Formal Logic into Neural Spaces: A Kernel Alignment Approach for Signal Temporal Logic

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

## Key facts

- No citing papers in the map yet (data through 14 Oct 2026).
- Builds on 21 of its 31 references that are in the map.
- First posted on arXiv 5 Mar 2026.

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

- [Attention Is All You Need](https://mlsanity.com/paper/1706.03762/) (2017)
- [BERT: Pre-training of Deep Bidirectional Transformers for Language Understanding](https://mlsanity.com/paper/1810.04805/) (2018)
- [A Simple Framework for Contrastive Learning of Visual Representations](https://mlsanity.com/paper/2002.05709/) (2020)
- [Distilling the Knowledge in a Neural Network](https://mlsanity.com/paper/1503.02531/) (2015)
- [Sentence-BERT: Sentence Embeddings using Siamese BERT-Networks](https://mlsanity.com/paper/1908.10084/) (2019)
- [Bootstrap your own latent: A new approach to self-supervised Learning](https://mlsanity.com/paper/2006.07733/) (2020)
- [Gaussian Error Linear Units (GELUs)](https://mlsanity.com/paper/1606.08415/) (2016)
- [SimCSE: Simple Contrastive Learning of Sentence Embeddings](https://mlsanity.com/paper/2104.08821/) (2021)
- [Barlow Twins: Self-Supervised Learning via Redundancy Reduction](https://mlsanity.com/paper/2103.03230/) (2021)
- [Understanding Contrastive Representation Learning through Alignment and Uniformity on the Hypersphere](https://mlsanity.com/paper/2005.10242/) (2020)
- [Relational Knowledge Distillation](https://mlsanity.com/paper/1904.05068/) (2019)
- [Learning to Represent Programs with Graphs](https://mlsanity.com/paper/1711.00740/) (2017)
- [Reinforcement Learning With Temporal Logic Rewards](https://mlsanity.com/paper/1612.03471/) (2016)
- [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)
- [Contrastive Learning for Image Complexity Representation](https://mlsanity.com/paper/2408.03230/) (2024)
- [On the Similarities of Embeddings in Contrastive Learning](https://mlsanity.com/paper/2506.09781/) (2025)
- [Kernel-based Translations of Convolutional Networks](https://mlsanity.com/paper/1903.08131/) (2019)
- [Bridging Logic and Learning: Decoding Temporal Logic Embeddings via Transformers](https://mlsanity.com/paper/2507.07808/) (2025)
- [Efficient Analysis of the Distilled Neural Tangent Kernel](https://mlsanity.com/paper/2602.11320/) (2026)

## Abstract (arXiv)

We introduce a framework for learning continuous neural representations of formal specifications by distilling the geometry of their semantics into a latent space. Existing approaches rely either on symbolic kernels -- which preserve behavioural semantics but are computationally prohibitive, anchor-dependent, and non-invertible -- or on syntax-based neural embeddings that fail to capture underlying structures. Our method bridges this gap: using a teacher-student setup, we distill a symbolic robustness kernel into a Transformer encoder. Unlike standard contrastive methods, we supervise the model with a continuous, kernel-weighted geometric alignment objective that penalizes errors in proportion to their semantic discrepancies. Once trained, the encoder produces embeddings in a single forward pass, effectively mimicking the kernel's logic at a fraction of its computational cost. We apply our framework to Signal Temporal Logic (STL), demonstrating that the resulting neural representations faithfully preserve the semantic similarity of STL formulae, accurately predict robustness and constraint satisfaction, and remain intrinsically invertible. Our proposed approach enables highly efficient, scalable neuro-symbolic reasoning and formula reconstruction without repeated kernel computation at runtime.