Formally Verified Neurosymbolic Trajectory Learning via Tensor-based Linear Temporal Logic on Finite Traces
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.
Code (0)
등록된 구현이 없습니다.
Similar Papers 제목 키워드 기반
Neurosymbolic Reinforcement Learning with Formally Verified Exploration
We present Revel, a partially neural reinforcement learning (RL) framework for provably safe exploration in continuous state and action spaces. A key challenge for provably safe deep RL is that repeatedly verifying neura…
reinforcement-learningReinforcement LearningReinforcement Learning (RL)Safe ExplorationCTSketch: Compositional Tensor Sketching for Scalable Neurosymbolic Learning
Many computational tasks benefit from being formulated as the composition of neural networks followed by a discrete symbolic program. The goal of neurosymbolic learning is to train the neural networks using only end-to-e…
A Fast Convoluted Story: Scaling Probabilistic Inference for Integer Arithmetic
As illustrated by the success of integer linear programming, linear integer arithmetic is a powerful tool for modelling combinatorial problems. Furthermore, the probabilistic extension of linear programming has been used…
Agentic Neurosymbolic Collaboration for Mathematical Discovery: A Case Study in Combinatorial Design
We study mathematical discovery through the lens of neurosymbolic reasoning, where an AI agent powered by a large language model (LLM), coupled with symbolic computation tools, and human strategic direction, jointly prod…
Neurosymbolic Methods for Dynamic Knowledge Graphs
Knowledge graphs (KGs) have recently been used for many tools and applications, making them rich resources in structured format. However, in the real world, KGs grow due to the additions of new knowledge in the form of e…
Entity AlignmentKnowledge Graphs