Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

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

Sara Candussio, Gabriele Sarti, Gaia Saveri, Luca Bortolussi

TL;DR

This work introduces a framework for learning continuous neural representations of formal specifications by distilling the geometry of their semantics into a latent space by distilling a symbolic robustness kernel into a Transformer encoder using a teacher-student setup.

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.

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

TL;DR

This work introduces a framework for learning continuous neural representations of formal specifications by distilling the geometry of their semantics into a latent space by distilling a symbolic robustness kernel into a Transformer encoder using a teacher-student setup.

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.
Paper Structure (41 sections, 22 equations, 4 figures, 8 tables)

This paper contains 41 sections, 22 equations, 4 figures, 8 tables.

Table of Contents

  1. Introduction
  2. Contributions
  3. Background
  4. Signal Temporal Logic
  5. Semantic-preserving embeddings for Signal Temporal Logic
  6. Kernel embedding inversion and coverage limitations
  7. Neural encoders and pooling strategies
  8. Related works
  9. Kernel-guided neural representation learning
  10. Neural architectures and projection heads for symbolic representation
  11. Methodology
  12. Weighted geometric alignment loss
  13. Encoder module
  14. Transformer encoder
  15. Pooling
  16. ...and 26 more sections

Figures (4)

  • Figure 1: An overview of our proposed approach to distill robustness semantics from a symbolic STL kernel into a Transformer-based encoder for efficient inference.
  • Figure 2: Evolution of training (top) and validation (bottom) metrics over approximately 30,000 training steps for the three pooling strategies ([CLS], mean, and [BOS]).
  • Figure :
  • Figure :