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

TL;DR

This paper introduces a rigorous tensor-based formalization of linear temporal logic on finite traces, enabling safe, differentiable constraint integration into neural network training with verified correctness.

Contribution

It presents a novel tensor semantics for LTLf with formal proofs, and integrates this into neurosymbolic learning via a differentiable loss function in PyTorch.

Findings

Successfully formalized LTLf semantics with Isabelle/HOL

Developed a differentiable loss for LTLf constraints

Enabled constraint satisfaction in neural network training

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.