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

arXiv: https://arxiv.org/abs/2501.13712 · HTML: https://mlsanity.com/paper/2501.13712/

## Key facts

- Cited by 3 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 23 Jan 2025.

## Built on by (most cited first, 3 of 3)

- [AI Can Learn Scientific Taste](https://mlsanity.com/paper/2603.14473/) (2026)
- [Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair](https://mlsanity.com/paper/2605.17475/) (2026)
- [GradSTL: Comprehensive Signal Temporal Logic for Neurosymbolic Reasoning and Learning](https://mlsanity.com/paper/2508.04438/) (2025)

## Abstract (arXiv)

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.