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.

翻译：本文提出一种框架，通过将形式规范的语义几何结构蒸馏到潜在空间中，学习其连续神经表示。现有方法要么依赖符号核——该核保留行为语义但计算代价高昂、依赖锚点且不可逆，要么依赖基于语法的神经嵌入，无法捕捉底层结构。我们的方法弥合了这一差距：利用教师-学生架构，将符号鲁棒核蒸馏到Transformer编码器中。与标准对比方法不同，我们通过连续的、基于核权重的几何对齐目标监督模型，该目标根据语义差异程度按比例惩罚错误。训练后，编码器可在单次前向传播中生成嵌入，以极低的计算成本有效模拟核的逻辑性能。我们将该框架应用于信号时态逻辑（STL），证明所得神经表示忠实保留了STL公式的语义相似性，能准确预测鲁棒性和约束满足性，且保持内在可逆性。所提方法无需在运行时重复计算核，即可实现高效、可扩展的神经符号推理与公式重构。