AI software – both symbolic and connectionist – pervasiveness in our societies is a fact. Its very dissemination raises important questions from the perspective of software engineering. As AI software malfunctions have dire consequences on individuals and societies, it is expected that AI software will aim for high software quality. The field of formal methods successfully transferred techniques and tools into some of the most critical industries. The goal of this course is to provide an accurate perspective of formal methods applied to AI software. Following real-world industrial examples, we will present how the use of formal methods can help AI developers assess the quality of their software, ranging from adversarial robustness to automated neural network fixing and explainable AI with guarantees.
This is the material for a course I gave at the Université Paris-Saclay AI master course for Fairness in Artificial Intelligence. Altough the course was online, interactions between students, professors and me were really interesting and sparked new questions, especially on the question of dataset quality assessment.
Since 2020, I regularly teach formal verification of machine learning programs to students of the SETI master.
Some tutorial materials I gave with my advisor Guillaume Charpiat during DigiCOSME Spring school ForMaL