Repository files navigation

Vehicle is a system for embedding logical specifications into neural networks.At its heart is the Vehicle specification language, a high-level, functional language for writing mathematically-precise specifications for your networks. For example, the following simplespecification says that a network's output should be monotonically increasing with respect toits third input.

These specifications can then automatically be compiled down to loss functions to beused when training your network.After training, the same specification can be compiled down to low-level neural network verifiers such as Marabou which either prove that the specification holds or produce a counter-example. Such a proof is far better than simply testing, as you can prove thatthe specification holds forall inputs.Verified specifications can also be exported to interactive theorem provers (ITPs)such as Agda.This in turn allows for the formal verification of larger software systemsthat use neural networks as subcomponents.The generated ITP code is tightly linked to the actual deployed network, so changesto the network will result in errors when checking the larger proof.

• User manual
• Tutorial

Each of the following examples comes with an explanatory README file:

• ACAS Xu - The complete specification of the ACAS Xu collision avoidance system from theReluplex paper in a single file.

• Car controller - A neural network controller that is formally proven to always keep a simple model of a car on the road in the face of noisy sensor data and an unpredictable cross-wind.

• MNIST robustness - A classifier for the MNIST dataset that is proven to be robust around the images in the dataset.

In addition to the above, further examples of specifications can be found in thetest suiteand the corresponding output of the Vehicle compiler can be foundhere.

If you are interested in adding support for a particular format/verifier/ITPthen open an issue on theIssue Trackerto discuss it with us.

• ONNX

• IDX

• Marabou

• Agda

• Vehicle tool paper
• Vehicle's type checker (in CPP'23)
• Vehicle's compilation to verifier queries