Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces

TL;DR

The paper addresses enforcing temporal logic constraints in neural learning with formal guarantees by developing a tensor-based $LTL_f$ semantics implemented and verified in Isabelle/HOL. It introduces a differentiable loss $\mathcal{L}$ and its derivative $d\mathcal{L}$ over tensors, generated automatically into executable OCaml code and integrated with PyTorch for end-to-end neurosymbolic learning. The approach is validated through trajectory planning experiments, showing that constraint-driven training can shape behavior while maintaining formal correctness. The work provides a scalable, trustworthy framework for constrained learning, bridging formal verification with practical deep learning infrastructure and enabling robust, logic-guided optimization in motion planning and similar domains.

Abstract

We present a novel formalisation of tensor semantics for linear temporal logic on finite traces (LTLf), with formal proofs of correctness carried out in the theorem prover Isabelle/HOL. We demonstrate that this formalisation can be integrated into a neurosymbolic learning process by defining and verifying a differentiable loss function for the LTLf constraints, and automatically generating an implementation that integrates with PyTorch. We show that, by using this loss, the process learns to satisfy pre-specified logical constraints. Our approach offers a fully rigorous framework for constrained training, eliminating many of the inherent risks of ad-hoc, manual implementations of logical aspects directly in an "unsafe" programming language such as Python, while retaining efficiency in implementation.

Figures (7)

• Figure 1: An example trace capturing the $x$ and $y$ coordinates of an agent.
• Figure 2: An example $5\times2\times4$ tensor representing a batch of LTL$_f$ traces, highlighting the element indexed by (2,1,0).
• Figure 3: Isabelle-PyTorch neurosymbolic pipeline.
• Figure 4: Trajectories and velocities for demonstrations with simple trajectories.
• Figure 5: Trajectories for the Unconstrained, Avoid, Patrol, Until, Compound and Loop experiments.

Theorems & Definitions (2)

• Theorem : Soundness of $\mathcal{L}$
• Theorem : Idempotence, commutativity, associativity of $\mathcal{L}$