Search papers, labs, and topics across Lattice.
This paper introduces a teacher-student framework to distill the semantics of Signal Temporal Logic (STL) formulas, captured by a symbolic robustness kernel, into a Transformer encoder. The student encoder is trained using a kernel-weighted geometric alignment objective that penalizes errors based on semantic discrepancies, unlike standard contrastive methods. The resulting neural representations efficiently preserve semantic similarity, accurately predict robustness and constraint satisfaction, and enable formula reconstruction, all while avoiding repeated kernel computation.
Ditch slow symbolic kernels: this method distills their logic into a fast, invertible neural representation that understands Signal Temporal Logic.
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.
