Developing Support for End-to-End Verification of Neural AI Agents

In this Oxford Seminar talk, Matthew Daggit presents his work on developing programming language support for end-to-end verification of neural AI agents. Explore how formal verification of neural networks has progressed over the past decade, enabling the verification of first-order, linear specifications for small-to-medium-sized networks. Learn about Vehicle, a tool developed by Daggit and collaborators that addresses the practical challenges of deploying verification algorithms in complex environments. Discover how Vehicle allows users to write high-level specifications for AI agents, use these specifications to guide training, formally verify neural network compliance, and export verified specifications to interactive theorem provers for environmental reasoning. The talk highlights innovative applications of type theory to enhance user experience, the use of real-valued logic semantics for Boolean specifications, and discusses open theoretical challenges in the field. The presentation includes information about the Vehicle project, which is available on GitHub.