About the Programme
This focus programme brings together researchers and practitioners working in Formal Methods, theoretical foundations of Artificial Intelligence and their interactions. The aim is to provide students specializing in theoretical Computer Science with a gentle introduction to these subjects through a tutorial based format.
The programme is organized under the aegis of the vibrant Indo-French International Research Lab in Computer Science (ReLaX).
The programme is open to all CMI students. If you are from outside CMI and would like to participate, please contact one of the organizers.
Speakers
-
Kumar Madhukar
Indian Institute of Technology Delhi, India -
David Monniaux
VERIMAG, France -
Madhavan Mukund
Chennai Mathematical Institute, India -
Prajakta Nimbhorkar
Chennai Mathematical Institute, India
Programme Schedule
Each tutorial will have two lectures.
Lecture 1: 2:00 PM to 3:15 PM Lecture 2: 3:30 PM to 4:45 PM
- Day 1 (Feb 2): Madhavan Mukund
Introduction to Neural Networks
- Day 2 (Feb 3): Kumar Madhukar
Introduction to Neural Network Verification
Artificial neural networks are everywhere. While this has led to interesting and important developments, it is crucial to understand that neural networks are responsible for a lot of decision making, some of which can have disastrous consequences if gone wrong. Naturally, verification of neural networks has gained a lot of attention in the last several years, and is an active area of research. This tutorial aims to introduce the problem of network verification through a few early but influential papers on this topic.
- Day 3 (Feb 4): David Monniaux
Formally verified static analysis and compilation
Most compilers (e.g. gcc, clang…) or static analysis tools (Frama-C, Astrée, Polyspace…) are not proved correct. This means they may contain bugs; a correct source program may be compiled into an incorrect target program. It is very easy to design optimization passes that have incorrect “corner cases”. In most industries, the probability of bugs due to the code being compiled is far higher than those due to the compiler, thus this is not a major concern. In safety-critical industries, specific precautions may have to be taken, such as compiling with little or no optimization and checking that the assembly code follows the source code.
CompCert (www.compcert.org) and CakeML (https://cakeml.org/) are two formally verified compilers, meaning that they have a formal proof, inside a theorem prover (respectively HOL Light and Coq / Rocq). In this tutorial, I will give an overview of how CompCert is proved correct (mostly on the backend part), and discuss various issues:
- simulation arguments
- partial vs total correctness in compiler proofs
- translation validation
- abstract interpretation
- trusted computing base
- Day 4 (Feb 5): Prajakta Nimbhorkar
Fairness in resource allocation
Allocating scarce resources among individuals is a fundamental and practical problem. Presently, there is an increasing use of AI/ML tools in allocation of resources. However, bias or discrimination can inadvertently crop up in various ways while using these tools. Hence, while automating the process of resource allocation, it is necessary to ensure fairness of the outcome.
In this talk, we will focus on various notions of fairness in resource allocation. We will see some algorithms that incorporate these fairness constraints in their output.
This talk is based on results that are joint with Anand Louis, Meghana Nasre, Atasi Panda, Nada Pulath, and Govind Sankar.
- Day 5 (Feb 6): Madhavan Mukund
Introduction to Reinforcement Learning
Venue
Lecture Hall 202 (LH 202)
Chennai Mathematical Institute (CMI), Chennai, India
Organisers
Dietmar Berwanger, CNRS, France
B Srivathsan, Chennai Mathematical Institute, India
Pascal Weil CNRS, France