Skip to content

Papers

Our preprint on formally verified neurosymbolic trajectory learning is out on arXiv

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

    Astract:

    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.

    Paper: https://arxiv.org/abs/2501.13712

    Our survey paper on Neurosymbolic AI for reasoning over knowledge graphs has just been published in TNNLS

      Abstract:

      Neurosymbolic artificial intelligence (AI) is an increasingly active area of research that combines symbolic reasoning methods with deep learning to leverage their complementary benefits. As knowledge graphs (KGs) are becoming a popular way to represent heterogeneous and multirelational data, methods for reasoning on graph structures have attempted to follow this neurosymbolic paradigm. Traditionally, such approaches have utilized either rule-based inference or generated representative numerical embeddings from which patterns could be extracted. However, several recent studies have attempted to bridge this dichotomy to generate models that facilitate interpretability, maintain competitive performance, and integrate expert knowledge. Therefore, we survey methods that perform neurosymbolic reasoning tasks on KGs and propose a novel taxonomy by which we can classify them. Specifically, we propose three major categories: 1) logically informed embedding approaches; 2) embedding approaches with logical constraints; and 3) rule-learning approaches. Alongside the taxonomy, we provide a tabular overview of the approaches and links to their source code, if available, for more direct comparison. Finally, we discuss the unique characteristics and limitations of these methods and then propose several prospective directions toward which this field of research could evolve.

      L. N. DeLong, R. F. Mir and J. D. Fleuriot, “Neurosymbolic AI for Reasoning Over Knowledge Graphs: A Survey,” in IEEE Transactions on Neural Networks and Learning Systems, doi: 10.1109/TNNLS.2024.3420218.

      keywords: {Cognition;Artificial intelligence;Artificial neural networks;Surveys;Taxonomy;Knowledge graphs;Semantics;Graph neural networks (GNNs);hybrid artificial intelligence (AI);knowledge graphs (KGs);neurosymbolic AI;representation learning},