Distilling Formal Logic into Neural Spaces: A Kernel Alignment Approach for Signal Temporal Logic
This work addresses the computational burden and limitations of symbolic kernels for neuro-symbolic reasoning, offering a more efficient and scalable approach for researchers and practitioners working with formal specifications.
This paper introduces a method to learn continuous neural representations of formal specifications, specifically Signal Temporal Logic (STL), by distilling the geometry of their semantics into a latent space. The resulting Transformer encoder produces embeddings that faithfully preserve semantic similarity, accurately predict robustness and constraint satisfaction, and are intrinsically invertible, mimicking the kernel's logic at a fraction of its computational cost.
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.