4 papers
Compiling High-Level Neural Network Specifications into VNN-LIB Queries
Matthew L. Daggitt, Wen Kokke, Robert Atkey
The formal verification of traditional software has been revolutionised by verification-orientated languages such as Dafny and F* which enable developers to write high-level specif…
Vehicle: Bridging the Embedding Gap in the Verification of Neuro-Symbolic Programs
Matthew L. Daggitt, Wen Kokke, Robert Atkey +3
Neuro-symbolic programs, i.e. programs containing both machine learning components and traditional symbolic code, are becoming increasingly widespread. Finding a general methodolog…
A Semantic Proof of Generalised Cut Elimination for Deep Inference
Robert Atkey, Wen Kokke
Multiplicative-Additive System Virtual (MAV) is a logic that extends Multiplicative-Additive Linear Logic with a self-dual non-commutative operator expressing the concept of "befor…
Marabou 2.0: A Versatile Formal Analyzer of Neural Networks
Haoze Wu, Omri Isac, Aleksandar ZeljiÄ +14
This paper serves as a comprehensive system description of version 2.0 of the Marabou framework for formal analysis of neural networks. We discuss the tool's architectural design a…