IsaGrad paper accepted at LogicNN 2026
Our paper “IsaGrad: Verified Automatic Differentiation over Computational Graphs in Imperative HOL” has been accepted and will be presented at LogicNN, FLOC 2026.
theorem proving
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 accepted at CICM 2022
Our paper, “Re-imagining the Isabelle Archive of Formal Proofs” (MacKenzie, Huch, Vaughan and Fleuriot), has been accepted at the 15th Conference on Intelligent Computer Mathematics (CICM 2022).
New Archive of Formal Proof Website
A project involving Carlin MacKenzie, James Vaughan and Jacques Fleuriot has resulted in a re-design and re-implementation of the Archive of Formal Proofs, which is a collection of proof libraries, examples, and larger scientific developments, mechanically checked in the theorem prover Isabelle. The revamped website (https://www.isa-afp.org) is now live and will serve the Isabelle community across the world. The Edinburgh team worked with Fabian Huch of TU Munich to integrate their work into the AFP infrastructure.
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!