<div dir="ltr"><span style="background-color:rgb(255,255,255)"><span style="color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures"><u>On the search for formally verifiable properties of neural network-enhanced systems</u></span><br style="box-sizing:inherit;color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures"><span style="color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">Summer 2021 research internship</span><br style="box-sizing:inherit;color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures"><span style="color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">Lab for AI Verification @ Heriott-Watt University</span></span><span class="gmail-c-mrkdwn__br" style="box-sizing:inherit;display:block;height:8px;color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures"></span><span style="background-color:rgb(255,255,255)"><span style="color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">In 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 </span><a target="_blank" class="gmail-c-link" href="http://laiv.uk/" rel="noopener noreferrer" style="box-sizing:inherit;text-decoration-line:none;font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">Lab for AI Verification</a><span style="color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures"> at Heriot-Watt in Edinburgh has recently won a joint grant with </span><a target="_blank" class="gmail-c-link" href="https://www.katz-lab.com/" rel="noopener noreferrer" style="box-sizing:inherit;text-decoration-line:none;font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">Prof. Guy Katz</a><span style="color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures"> from the Hebrew University of Jerusalem, author of </span><a target="_blank" class="gmail-c-link" href="https://github.com/NeuralNetworkVerification/Marabou" rel="noopener noreferrer" style="box-sizing:inherit;text-decoration-line:none;font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">Marabou</a><span style="color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">, 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.</span></span><span class="gmail-c-mrkdwn__br" style="box-sizing:inherit;display:block;height:8px;color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures"></span><span style="background-color:rgb(255,255,255)"><span style="color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">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 </span><a target="_blank" class="gmail-c-link" href="http://www.macs.hw.ac.uk/splv/" rel="noopener noreferrer" style="box-sizing:inherit;text-decoration-line:none;font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">SPLV 2021</a><span style="color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">.</span></span><span class="gmail-c-mrkdwn__br" style="box-sizing:inherit;display:block;height:8px;color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures"></span><span style="background-color:rgb(255,255,255)"><span style="color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">Please send enquiries to Prof. Ekaterina Komendantskya and Dr Matthew Daggitt at </span><a target="_blank" class="gmail-c-link" href="mailto:ek19@hw.ac.uk" rel="noopener noreferrer" style="box-sizing:inherit;text-decoration-line:none;font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">ek19@hw.ac.uk<span style="box-sizing:inherit"></span></a><span style="color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures"> and </span><a target="_blank" class="gmail-c-link" href="mailto:md2006@hw.ac.uk" rel="noopener noreferrer" style="box-sizing:inherit;text-decoration-line:none;font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures">md2006@hw.ac.uk<span style="box-sizing:inherit"></span></a><span style="color:rgb(29,28,29);font-family:Slack-Lato,appleLogo,sans-serif;font-size:15px;font-variant-ligatures:common-ligatures"> </span></span><br></div>