[Agda] Research internship Summer 2021 - Searching for verifiable neural network properties

[Matthew Daggitt]

*On the search for formally verifiable properties of neural
network-enhanced systems*
Summer 2021 research internship
Lab for AI Verification @ Heriott-Watt UniversityIn the last decade,
advancement in neural networks have lead to an astounding array of new
technologies, many of which use neural networks to interact with the
real-world and, in particular, humans. However, neural networks for the
most part remain black boxes and their results are hard to trust. To
address this, in the last few years a range of tools have been developed
that verify a given neural network obeys a given mathematical
specification. The Lab for AI Verification <http://laiv.uk/> at Heriot-Watt
in Edinburgh has recently won a joint grant with Prof. Guy Katz
<https://www.katz-lab.com/> from the Hebrew University of Jerusalem, author
of Marabou <https://github.com/NeuralNetworkVerification/Marabou>, a
cutting-edge tool for the verification of neural networks. Prof Katz will
be visiting the robotics departments at Scottish Universities looking for
systems which use neural networks and that have clear mathematical
specifications that the neural network component should obey.We are looking
for someone to collaborate with Prof Katz in creating a library of such
properties, formally specified in an (yet undetermined) Interactive Theorem
Prover such as Agda/Coq/Isabelle. The actual verification of these
properties is not necessarily required as part of the internship. The ideal
candidate will have prior experience of using an interactive theorem prover
and know the basics about the operation of neural networks. We are looking
for applicants with a range of experience from undergraduate/masters
students/PhDs and RAs. Compensation will be dependent on experience. The
internship will be between 2 and 3 months in Summer 2021 and we are
flexible with respect to whether it is a full-time or part-time position
and whether it is in-person or remote. Accommodation can be arranged at
Heriot-Watt Univerisity, but will not be included as part of the
compensation. If the applicant is interested, the position will also
include fully-paid entry fees to SPLV 2021
<http://www.macs.hw.ac.uk/splv/>.Please
send enquiries to Prof. Ekaterina Komendantskya and Dr Matthew Daggitt at
ek19 at hw.ac.uk and md2006 at hw.ac.uk
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20210429/4b3cfed3/attachment.html>