CS620: New Trends in IT (Formal Methods in Machine Learning)
Spring 2021

Pre-requisites

Course project

• The course project carries 20% marks.
• The ideal size for a project team is 2 students. If you want to do a course project alone, please contact the instructor by Apr 8, 2021
• Each group must choose a tool, say T from among the topics studied in this course and do the following.
  • Choose a machine-learning model, such as a deep neural network N, for a specific task. Examples are ACAS-Xu networks, MNIST networks, etc.
  • Decide on a property P you'd like to verify/analyze for the network.
  • Train the network using publicly available datasets for the task you'd like to verify properties of.
  • Use the tool T to verify/analyze property P of ML model N
• Submit a report of the exercise by Sat, May 8, 2021
• Important dates
  • Apr 17, 2021: Meeting (online) with instructor to discuss your project plan
  • May 8 May 14, 2021: Demo and presentation of your project

Readings for paper critique

• Each student is required to read one of the papers from the list below, and present a short critique consisting of
  • Problem being solved in the paper
  • Positive points/strengths of the technique
  • Weaknesses of the technique
  • Points skipped, missed, ignored that could've been taken into account to make a better paper.
• This exercise has to be done by each student individually. It is ok for multiple students to choose the same paper to critique.
• Each student is required to prepare a 7-10 slide presentation of her/his critique. The set of slides is to be submitted via moodle for evaluation. Students who can make a presentation are encouraged to make a presentation to the instructor
• The deadline for submission of the paper critique writeup/presentation is Sat, May 8 Fri, May 14, 2021. If you want to schedule a presentation earlier, please let the instructor know.

• Abduction-based explanations for machine learning models by Alexey Ignatiev, Nina Narodytska, and Joao Marques-Silva.
• A SAT-based approach to learn explainable decision sets by Alexey Ignatiev, Filipe Pereira, Nina Narodytska, and João Marques-Silva.
• Learning Optimal Decision Trees with SAT by Nina Narodytska, Alexey Ignatiev, Filipe Pereira, Joao Marques-Silva
• Explaining AI Decisions using Efficient Methods for Learning Sparse Boolean Formulae by Susmit Jha, Tuhin Sahai, Vasumathi Raman, Alessandro Pinto, Michael Francis
• Scalable Quantitative Verification for Deep Neural Networks Teodora Baluta, Zheng Leong Chua, Kuldeep S. Meel and Prateek Saxena
• SAT-based Decision Tree Learning for Large Data Sets by Andre Schidler and Stefan Szeider

Reading References

Required Reading List

Quizes and Exams

Lectures and interactions