Skip to content

news

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 formalisation of Linear Resources and Process Compositions has been published in the Archive of Formal Proof

      Abstract

      In this entry we formalise a framework for process composition based on actions that are specified by their input and output resources. We verify their correctness by translating compositions of process into deductions of intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction.

      We describe an earlier version of this formalisation in our article Linear Resources in Isabelle/HOL, which also includes a formalisation of manufacturing processes in the simulation game Factorio.

      Jiawei Zheng passes his PhD Defence!

        Congratulations to Jiawei Zheng who has passed his PhD viva with no corrections. His thesis on Process-aware Pattern Recognition and Deviation Detection Under Uncertainty was examined by Prof Juliana Bowles (St Andrews, external) and Prof David Robertson.

        Our formalisation of Lie Groups and Algebras has been published in the Archive of Formal Proof

          Abstract

          Lie Groups are formalised as locales, building on the AFP theory of Smooth Manifolds. We formalise the diffeomorphism group of a manifold, and the action of a Lie group on a manifold. The general linear group is shown to be a Lie group by proving properties of the determinant, and matrix inverses. We also develop a theory of smooth vector fields on a manifold , defined as smooth maps from the manifold to its tangent bundle . We employ a shortcut that avoids difficulties in defining the tangent bundle as a manifold, but which still leads to vector fields with the properties one would expect. We then construct the Lie algebra of a Lie group as an algebra of left-invariant smooth vector fields.

          Schmoetten R. and Fleuriot J. D. (2024). Lie Groups and Algebras. Archive of Formal Proofs. ISSN: 2150-914x.

          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},

            Our paper “Linear Resources in Isabelle/HOL” has just been published in the Journal of Automated Reasoning

              Abstract:

              We present a formal framework for process composition based on actions that are specified by their input and output resources. The correctness of these compositions is verified by translating them into deductions in intuitionistic linear logic. As part of the verification we derive simple conditions on the compositions which ensure well-formedness of the corresponding deduction when satisfied. We mechanise the whole framework, including a deep embedding of ILL, in the proof assistant Isabelle/HOL. Beyond the increased confidence in our proofs, this allows us to automatically generate executable code for our verified definitions. We demonstrate our approach by formalising part of the simulation game Factorio and modelling a manufacturing process in it. Our framework guarantees that this model is free of bottlenecks.

              Smola, F., Fleuriot, J.D. Linear Resources in Isabelle/HOL. J Autom Reasoning 68, 9 (2024). https://doi.org/10.1007/s10817-024-09698-2

              Opportunity: Fully funded PhD in predicting harm from prescribed drugs

                Fully Funded PhD in Predicting harm from prescribed drugs in people with polypharmacy, multimorbidity and frailty.

                The aim of this project is to develop and validate new models to predict who is at risk of being harmed by prescribed drugs, focusing on the outcome of acute kidney injury. More information available here.

                Fiona Smith’s exhibition “The BOX” premieres at the Edinburgh Science Festival!

                  We are proud to announce that AI Modelling Lab PhD Student Fiona Smith’s exhibition “The BOX” is running from the 6th to the 19th of April 2024 as part of the Edinburgh Science Festival. Fiona is funded by our Centre for Doctoral Traning in Biomedical AI and was selected to be the Creator in Residence at Fraunhofer MEVIS.

                  The live exhibition can be visited at Inspace, Crichton St, University of Edinburgh.

                   

                   

                  Jorge Gaete Villegas passes his PhD viva

                    Congratulations to Jorge Gatete Villegas who succesfully defended his thesis on Modelling and Predicting Medical Outcomes for Intensive Care Patients via Network Mechanisms and Machine
                    Learning                    . His examiners were Dr Areti Manataki of the University of St Andrews and Dr Sohan Seth of the University of Edinburgh.