Skip to content

formal verification

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.

      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

        Mark Chevallier passes his second year PhD review

          Mark successfully passed his second year PhD  review on formal verification applied to machine learning. His panel consisted of Pavlos Andreadis, Paul Jackson and Jacques Fleuriot. Congratulations to Mark!