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

Sara Candussio; Gabriele Sarti; Gaia Saveri; Luca Bortolussi

cs.CLMar 5, 2026

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

Authors: Sara Candussio, Gabriele Sarti, Gaia Saveri, Luca Bortolussi

Organizations: AILab, MIGe, University of Trieste, IT · Khoury College of Computing Sciences, Northeastern University, Boston, MA, USA

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.

Figures & tables

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] ).

Metric	Equivalent	Non-equivalent	Lexically Sim.
Neural similarity	0.966	0.182	0.308
Kernel similarity	0.997	0.170	0.225
MAE (semantic gap)	0.034	0.072	0.112
Relative neural distance	0.137	0.833	0.770
Relative kernel distance	0.105	0.830	0.775

Table 1: Semantic agreement evaluation for [CLS] pooling.

Metric	Kernel						Transformer
Metric	$N=500$	$1000$	$2000$	$4000$	$8000$	$16000$	loaded	full
Time (s)	2.18	3.03	4.77	8.36	17.08	48.86	2.17	3.56
RAM (GB)	4.91	8.74	16.46	31.70	62.38	123.38	1.54	1.71

Table 2: Embedding efficiency comparison (

B=2000

) on a NVIDIA A100 80GB GPU. loaded : inference time for a pre-loaded model; full also includes model loading.

Appendix figures & tables9 assets

Supplementary material from the paper’s appendix.

Appendix

Rule	$P(\cdot)$	Mathematical Transformation
Not -injection	0.1%	$\varphi\to\neg\neg\varphi\quad(\text{if parent}\neq\neg)$
De Morgan rewriting	9.9%	$(A\wedge B)\to\neg(\neg A\vee\neg B)\quad(\text{and dual})$
Time partitioning	35.0%	$\text{op}_{I}\varphi\to\text{op}_{I_{1}}(\text{op}_{I_{2}}\varphi),\quad\text{op}\in\{\Box,\diamondsuit\}$
Until nesting	25.0%	$\varphi\to(\varphi\,\mathcal{U}\,\psi)\quad\text{or}\quad(\psi\,\mathcal{U}\,\varphi)$
Temporal identity	5.0%	$\varphi\to\text{op}_{[0,0]}\varphi,\quad\text{op}\in\{\Box,\diamondsuit\}$
Distributivity	15.0%	$\Box_{I}(A\wedge B)\to\Box_{I}A\wedge\Box_{I}B\quad(\text{or dual})$

Appendix

Table 3: Semantic-preserving augmentation rules. Notation:

\Box

(always),

\diamondsuit

(eventually),

\mathcal{U}

(until).

$\mathcal{U}(Z)$	geometrically	interpretation
$0.0$	complete collapse	zero discriminative power; all formulae are isomorphic
$-1.0$	dense clustering	poor resolution; distinct logics occupy overlapping regions
$-2.5$	reasonable distribution	reliable separation of standard temporal properties
$-3.0$	good sparsity	maximum entropy; preserves fine-grained semantic nuances.
$-4.0$	asymptotic limit	theoretical maximum spread for $d\to\infty$ with $t=2$

Appendix

Table 6

$B$	$N$	STL Kernel		Transformer
		$T_{\mathrm{Emb}}$	Mem	$T_{\mathrm{Emb}}$ (Loaded)	Mem (Loaded)	$T_{\mathrm{Emb}}$ (Full)	Mem (Full)
500	500	0.61	2059	0.62	2136	2.06	2914
500	1000	0.83	3061	0.62	2128	1.98	2916
500	2000	1.25	5051	0.62	2128	2.05	2918
500	4000	2.21	8955	0.63	2134	2.02	2918
500	8000	4.53	16995	0.62	2127	1.98	2918

Appendix

Table 4: Embedding times (s) and total memory usage (MB) for STL kernel and Transformer. Total memory = RAM + VRAM. “Loaded” refers to Transformer with model already initialized; “Full pipeline” includes model loading.

$B$	$N$	STL Kernel		Transformer (Loaded)		Transformer (Full)
		$T_{\mathrm{Sim}}$	Mem	$T_{\mathrm{Sim}}$	Mem	$T_{\mathrm{Sim}}$	Mem
500	500	1.58	2059	0.73	2136	2.04	2914
500	1000	2.50	3061	0.73	2128	1.99	2916
500	2000	4.38	5051	0.73	2128	2.02	2918
500	4000	8.21	8955	0.73	2134	2.02	2918
500	8000	16.81	16995	0.73	2127	1.99	2918

Appendix

Table 5: Pairwise similarity computation times (s) and total memory usage (MB) for STL kernel and Transformer. Total memory = RAM + VRAM. “Loaded” refers to Transformer with model already initialized; “Full pipeline” includes model loading. Kernel hits OOM for large

N

Metric	Equivalent	Non-equivalent	Syntactically similar
Neural similarity	0.966	0.182	0.308
Kernel similarity	0.997	0.170	0.225
MAE (semantic gap)	0.034	0.072	0.112
Relative neural distance	0.137	0.833	0.770
Relative kernel distance	0.105	0.830	0.775

Appendix

Table 6: Semantic understanding evaluation for [CLS] pooling (reference).

Metric	Equivalent	Non-equivalent	Syntactically similar
Neural similarity	0.954	0.201	0.332
Kernel similarity	0.997	0.163	0.221
MAE (semantic gap)	0.044	0.066	0.143
Relative neural distance	0.169	0.833	0.749
Relative kernel distance	0.100	0.837	0.779

Appendix

Table 7: Semantic understanding evaluation for mean pooling.

Metric	Equivalent	Non-equivalent	Syntactically similar
Neural similarity	0.946	0.171	0.280
Kernel similarity	0.997	0.152	0.182
MAE (semantic gap)	0.052	0.070	0.133
Relative neural distance	0.186	0.834	0.794
Relative kernel distance	0.111	0.848	0.818

Appendix

Table 8: Semantic understanding evaluation for [BOS] pooling.

Explore similar work

NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic
May 20, 2026Paapa Kwesi Quansah, Ernest BonnahFormal Verification Neuro-Symbolic AI
Baylor University, Waco TX 76706, USA
ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning
May 7, 2026Bowen Ye, Zhijian Li, Junyue Huang +2Signal Temporal Logic LLM Tool Use
Shanghai Jiao Tong University · Alibaba Group, Hangzhou, China
Time to Reason: Scalable Neurosymbolic Learning for LTLf via Fuzzy Semantics
Aug 17, 2026Riccardo Andreoni, Andrei Buliga, Alessandro Daniele +4Neuro-Symbolic Reasoning Neurosymbolic Learning
Fondazione Bruno Kessler, Via Sommarive, 18, Trento, 38123, Italy · Free University of Bozen-Bolzano, Via Bruno Buozzi, 1, Bolzano, 39100, Italy · Università di Bologna, Via Mura Anteo Zamboni 7, Bologna, 40126, Italy

May 20, 2026J/K move · Enter open · S save

NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic

Paapa Kwesi Quansah, Ernest Bonnah

Baylor University, Waco TX 76706, USA

Formal Verification Neuro-Symbolic AI Linear Temporal Logic

Open paper AskPDF arXiv

Effectively translating between natural language (NL) and formal logics like Linear Temporal Logic (LTL) requires expertise that limits formal verification's reach in safety-critical development. Template-based approaches sacrifice expressiveness for reliability; neural methods achieve fluency but provide no correctness guarantees. We present NeuroNL2LTL, a neurosymbolic architecture unifying learned translation with formal verification. NeuroNL2LTL routes translation through an intermediate representation whose mapping to LTL is structure-preserving by construction. Generated specifications undergo satisfiability and non-triviality checking; a minimal-edit repair mechanism corrects near-miss outputs before they reach downstream tools. The central innovation is verifier-in-the-loop training: verification outcomes serve as reward signals for reinforcement learning, producing neural components that optimize directly for formal correctness. On 200,000+ requirements spanning aerospace, robotics, autonomous vehicles, and ten additional domains, NeuroNL2LTL achieves 28% semantic equivalence with reference specifications while ensuring 86% of outputs are verified satisfiable. The system also generates contextually grounded explanations from LTL, enabling domain experts to validate specifications without specialized training. This work demonstrates that formal verification can function as both training objective and runtime filter for neural specification systems, allowing us to build neural-based tools whose reliability derives from logical guarantees rather than statistical confidence.

Abstract

Explore similar work

NeuroNL2LTL: A Neurosymbolic Framework for Natural Language Translation of Linear Temporal Logic

ReasonSTL: Bridging Natural Language and Signal Temporal Logic via Tool-Augmented Process-Rewarded Learning

Time to Reason: Scalable Neurosymbolic Learning for LTLf via Fuzzy Semantics