Exporting a specification to an ITP
The end goal for most Vehicle projects is to verify that the neural network obeys the specification. However, in some projects it is also desirable to use the specification to prove that some larger development that uses the neural network is also functionally correct.
Take the car example in the list of example Vehicle projects. Here the end goal is to prove that the car being steered by the neural network never leaves the road. This safety property is not just a property of the neural network, but is instead a temporal property about the model of the entire system, e.g. the car, the road, the physics of the system. The problem is that Vehicle is not designed for modelling or reasoning about anything except neural networks.
To get around this, Vehicle is capable of exporting a verified specification to Interactive Theorem Provers (ITPs), which are much more general purpose systems that are capable of formalising and reasoning about arbitrary code and models.
This can be done using the vehicle export
command:
vehicle export \
--target Agda \
--cache examples/windController/windController.vcl-cache \
--output examples/windController/agdaProof/WindControllerSpec.agda
Command-line options
The table below contains the full list of command line arguments available
for the export
command.
- --target, -t
Set which ITP to export the specification to. At the moment the only supported option is
Agda
.
- --cache, -c
Provide Vehicle the location of the verification cache from which the exported specification should be generated. If not provided then all
@property
declarations will be converted intopostulates
.
- --output, -o
Set the name and location of the generated output file.
- --modulePrefix, -m
Set the prefix for the generated module. For example, setting to
Baz.agda
with a prefix ofFoo.Bar
will result in the Agda module with the name Foo.Bar.Baz.”
Supported backends
Currently only the Agda interactive theorem prover is supported, but adding support for new ones should be relatively simple, assuming that they have the ability to call out to external solvers. Please get in touch if you are interested in adding support for a new ITP.
Agda
The Agda backend generates a new Agda module with the functions in the
specification lifted to the Agda type Set
. The proofs of the
properties are provided by a macro called checkSpecification
.
This macro calls vehicle validate
on the verification cache, which
then checks the status of the specification. Consequently no
expensive reverification occurs when you try to type-check the Agda
module.
The generated Agda module provides a full interface which can then be used to build and prove properties about a model of the larger system. See the car example project for a demonstration of this.
Limitations
Postulated resources
When exporting a specification, the parameters are inserted into the Agda version of the specification but at the moment the networks and datasets are left as postulates. This allows them to be used and programmed with abstractly but not to be evaluated or inspected.
This is a not a fundemental limitation, as it would be possible to gain the ability to evaluate them by implementing an Agda tactic that martialed the arguments, and then unmartialed results. This would however be a significant undertaking.
Poor interaction with Agda’s caching mechanism
Due to its caching machinary, currently Agda only calls the
checkSpecification
macro when first type-checking the
generated module or its contents changes. This means that it won’t
automatically detect changes to the backing network within a single
Agda session. See issues #73
for an upstream link to the proposed fix on Agda’s end to guarantee
the macro gets called every time the generated module is type-checked.