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

TL;DR

This paper presents a novel method for learning neural representations of formal specifications, specifically Signal Temporal Logic, by distilling the semantics into a continuous space using a kernel alignment approach, enabling efficient reasoning.

Contribution

The authors introduce a kernel alignment-based distillation framework that creates invertible neural embeddings of STL formulas, combining symbolic robustness kernels with Transformer encoders for scalable reasoning.

Findings

Embeddings preserve semantic similarity of STL formulas.

Accurately predict robustness and constraint satisfaction.

Achieve efficient, scalable neuro-symbolic reasoning.

Abstract

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.