AISEC software


Vehicle is a system for formally proving properties of systems that include neural networks as subcomponents. Users write a neural network specification once in the high-level Vehicle specification language. This specification is then compiled down to neural network verifiers such as Marabou, and cross-compiled to a specification in an interactive theorem prover such as Agda, in which the larger system can then be formalised.

learn more

Imandra Neural Network Verification Library

A library in Imandra for representing and reasoning about neural networks as white-box functions. Includes feed-forward and convolutional neural networks, and can handle proofs of robustness, structural properties of intermediate layers and inductive proofs for networks with less than 100 nodes.

learn more

Schmitty - an Agda library for SMT integration

Schmitty is an Agda library which gives you bindings to SMT solvers, offering you is a well-typed embedding of some of the SMT-LIB language in Agda. That means as well as shouting “solve” at your problems, you can also write SMT queries yourself! Right now, Schmitty supports three theories—CoreInts, and Reals—and two backends—Z3, and CVC4. If you’re missing your favourite theory or solver, your contribution is more than welcome!

learn more

Amethyst - an Agda library for NN verification

Amethyst is an Agda library for neural network verification. Using Agda's expressive dependent type system, Amethyst is capable of specifying the desired properties of the neural network as a type. If your neural network doesn't have the right input/output behaviour, it won't even type-check! Amethyst is superseded by Vehicle in many ways.

learn more
Free Joomla! templates by Engine Templates