English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Verification of neural networks is currently a hot topic in automated theoremproving. Progress has been rapid and there are now a wide range of toolsavailable that can verify properties of networks with hundreds of thousands ofnodes. In theory this opens the door to the verification of larger controlsystems that make use of neural network components. However, although work hasmanaged to incorporate the results of these verifiers to prove largerproperties of individual systems, there is currently no general methodology forbridging the gap between verifiers and interactive theorem provers (ITPs).  In this paper we present Vehicle, our solution to this problem. Vehicle isequipped with an expressive domain specific language for stating neural networkspecifications which can be compiled to both verifiers and ITPs. It overcomesprevious issues with maintainability and scalability in similar ITPformalisations by using a standard ONNX file as the single canonicalrepresentation of the network. We demonstrate its utility by using it toconnect the neural network verifier Marabou to Agda and then formally verifyingthat a car steered by a neural network never leaves the road, even in the faceof an unpredictable cross wind and imperfect sensors. The network has over20,000 nodes, and therefore this proof represents an improvement of 3 orders ofmagnitude over prior proofs about neural network enhanced systems in ITPs.

Vehicle: Interfacing Neural Network Verifiers with Interactive Theorem Provers