Pith

open record

sign in
Browse

arxiv: 2501.13712 · v1 · pith:CXEAQTRE · submitted 2025-01-23 · cs.AI · cs.LG· cs.LO

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

Mark Chevallier , Filip Smola , Richard Schmoetten , Jacques D. Fleuriot This is my paper

Reviewed by Pith T0 review T1 audit T2 compute T3 formal T4 reserved pith:CXEAQTRErecord.jsonopen to challenge →

classification cs.AI cs.LGcs.LO
keywords constraintsfiniteformalisationimplementationlearninglinearlogiclogical
0
0 comments X
read the original 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.

This paper has not been read by Pith yet.

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 3 Pith papers

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. Event-B Agent: Towards LLM Agent for Formal Model Synthesis and Repair

    cs.SE 2026-05 unverdicted novelty 7.0

    Event-B Agent is an LLM agent that synthesizes, refines, and repairs Event-B formal models from natural language requirements via iterative verification feedback loops.

  2. Quantitative Linear Logic for Neuro-Symbolic Learning and Verification

    cs.LO 2026-05 unverdicted novelty 7.0

    QLL is a novel logic for neuro-symbolic learning that uses ML-native operations (sum, log-sum-exp) on logits to embed constraints, satisfying most linear logic properties and showing stronger correlation between empir...

  3. Quantitative Linear Logic for Neuro-Symbolic Learning and Verification

    cs.LO 2026-05 unverdicted novelty 6.0

    Quantitative Linear Logic interprets logical connectives via natural ML operations on logits to embed constraints in neural training while satisfying most linear logic laws and correlating performance with independent...