Skip to content

Machine Learning

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

    Paper on brain tumour survival predictions accepted in Computer Methods and Programs in Biomedicine

      Our paper on the “Development of prediction models for one-year brain tumour survival using machine learning: a comparison of accuracy and interpretability” has been published in Computer Methods and Programs in Biomedicine. The work by Colleen Charlton, Michael Poon, Paul Brennan and Jacques Fleuriot looks at classification models for predicting brain tumour survival over one year, with an emphasis on interpretable/Explainable AI.  The paper can be accessed here.