Release of Version 2.0 of VNN-LIB standard

[Matthew Daggitt]

Dear all,

 We are very pleased to announce the release of v2.0 of the VNN-LIB standard. I have attached the final document here, and the website has also been updated.

 

Features in the document include:

1. A formal grammar for the VNN-LIB query language. Their is additional support for more complex queries involving:

• Multiple networks
• Multiple inputs and outputs
• Hidden layers
• Explicit type annotations for networks

2. A formal semantics for the VNN-LIB query language, which includes mathematically rigorous descriptions of:

• The dependency of the VNN-LIB standard on the ONNX standard.
• Queries over floating-point ONNX data types over various precisions.
• Queries over approximate real-number semantics.

4. A set of SMT-LIB-style logics and theories that describe subsets of the query language that may be supported by different verifiers.
   
   
5. A standardised command-line interface to invoke verifiers and for verifiers to report their capabilities.

In addition the team has developed the following libraries that can be dropped into your project to allow easy parsing and type-checking VNN-LIB queries:

1. C++ library
2. Python package (available on Pip)
3. Julia package (not yet available on the Julia package manager but soon will be).
4. Agda library (also contains a full mechanisation of the semantics of the query language).

On benchmarking we have found the parsers to be between 2x and 1000x faster then the parsers implemented by some existing solvers.

The hope is that the standard will help to increase the expressiveness and rigour of neural network solvers, and at the same time help make it easier to develop higher-level tools that make use of those solvers.

The process of updating a solver to use VNN-LIB 2.0 should hopefully be relatively painless:

   1. add the relevant library above to your project.

   2. update the code that traverses the property.

   3. add support for the new command line format. 

If you would like some help to upgrade a solver then please do get in touch. I plan to get a team of students at the start of next year to go around offering to upgrade some of the existing solvers. Equally feel free to get in touch if you would like to see more features added to the standard.

Best,

Matthew