Home

Awesome

PyPI GitHub tag (latest by date) GitHub Workflow Status readthedocs status pre-commit.ci status

Vehicle

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 simple specification says that a network's output should be monotonically increasing with respect to its third input.

<!-- This must be a direct link, because the same README is used on PyPI -->

Example specification

These specifications can then automatically be compiled down to loss functions to be used 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 that the specification holds for all 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 systems that use neural networks as subcomponents. The generated ITP code is tightly linked to the actual deployed network, so changes to the network will result in errors when checking the larger proof.

Documentation

Examples

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

In addition to the above, further examples of specifications can be found in the test suite and the corresponding output of the Vehicle compiler can be found here.

Support

If you are interested in adding support for a particular format/verifier/ITP then open an issue on the Issue Tracker to discuss it with us.

Neural network formats

Dataset formats

Verifier backends

Interactive Theorem Prover backends

Related papers