LAIV Seminars

We are holding research meetings every Wednesday at 12.00: Room PG305.

In addition, LAIV students run a reading group every Tuesday morning, see LAIV github for more details. Currently, the reading groups cover B.Pierce’s Software Foundations, see the reading group details.

May — August 2019

Date Topics, May — September 2019
01 May A planning meeting, welcome to new members
08 MayAdversarial Examples generation (for Neural networks in Keras library):
a demo by Fraser Garrow
Pierre Le Hen: Testing DVL method of Neural network verification:
a progress report
15 May Daniel Kienitz: Generic Algorithms and Verification of Neural nets:
a progress report

Pascal Bacchus: Hardware approach to Neural net programming:
a progress report
22 MayDmitry Rozplokhas:
Title: miniKanren and its formal semantics
Abstract: miniKanren is a small logic programming language which aims to be a light-weight and purely declarative alternative to Prolog. The main field of application for miniKanren is “relational programming” — the technique of writing programs as mathematical relations rather than mathematical functions. Programs written in this way have a few interesting features, such as an ability to be “run backwards” (synthesize arguments from the result).
In the first part of the talk, I am going to give a short overview of the language. We will discuss its advantages and disadvantages, look at some simple examples of programs in miniKanren as well as state-of-the-art applications of relational programming. In the second part of the talk, I will describe the project I am currently involved in: providing formal semantics — rigorous mathematical description — to miniKanren programs and using it to prove some properties of program execution in the language.
Note the change in time and room:
the seminar will take place at 13.00 in Room 1.82
29 May Feedback session on Semester 1 MSc reports: writing about Neural Net verification.
12 June Marta Vallejo.
Title: Parkinson’s disease diagnosis using Convolutional Neural Networks and figure-copying tasks
Abstract: Parkinson’s disease (PD) is a chronic neurodegenerative disorder, which leads to a range of motor and cognitive impairments. An accurate PD diagnosis is a challenging task since its signs and symptoms are very similar to other related diseases such as normal ageing and essential tremor. This work aims to automate the PD diagnosis process by using a Convolutional Neural Network, a type of deep neural network architecture. To differentiate between healthy and PD patients, our approach focuses on discovering deviations in patient’s motor capabilities with the use of drawing tasks. Besides that, since different data representations may capture various aspects of this disease, this work explores which drawing task, cube or pentagon, is more effective in the discrimination process. The goal is to evaluate which data format is more effective in diagnosing PD.

January — April 2019

DateTopics, January — March 2019
9 JanSemester 2 Introduction.
Reading Seminar: In the next 6 sessions, we will cover
Safety Verification of Deep Neural Networks,
by Xiaowei Huang, Marta Kwiatkowska, Sen Wang and Min Wu
23 Jan

Reading Seminar: Introduction and general set-up
30 JanReading Seminar:
Background definitions, regions
6 Feb
Reading Seminar:
Verification Framework
13FebReading Seminar:
Feature Decomposition and Discovery
20 FebReading Seminar:
Feature Decomposition and Discovery
28 FebReading Seminar:
Selection of Regions and Manipulations
6 MarchReading Seminar:
Checking the verification properties in an SMT solver
18 MarchLAIV Masterclass: Survey of Deep Learning: Methods and Applications,
by Javier Garcia
21 MarchLAIV Masterclass: Convolutional Neural nets, by Mario Vasilev
27 MarchLAIV Masterclass: Keras and Adversarial example generation,
by Fraser Garrow