Formal Methods for AI Safety

The rapid progress in artificial intelligence and machine learning has lead to the deployment of AI-based systems in a number of areas of modern life, such as manufacturing, transportation, and healthcare. However, serious concerns about the safety and trustworthiness of such systems still remain, due to the lack of assurance regarding their behavior. To address this problem, significant efforts in the area of formal methods in recent years have been dedicated to the development of rigorous techniques for the design of safe AI-based systems. 

In this seminar, we will read and discuss research papers that present the latest results in this area. We will cover a range of topics, including the formal specification and verification of correctness properties of AI components of autonomous systems, and the design of reinforcement learning agents that respect safety constraints.

Each participant will give a presentation of an assigned paper, followed by a group discussion. All students are expected to read each paper carefully and to actively participate in the discussions. 

 

Logistics

Time: Thursday, 8:15-9:45

Venue: All meetings will be virtual, via Zoom (Disclaimer).

               The link to the recurring meeting has been communicated by email.

Participation in all meetings is mandatory (exceptions require an official document, such as a doctor's certificate).

 

Important dates

5 November, 8:15 Kick-off meeting (participation is strictly required)

8 November, 23:59 Deadline for paper preference registration

9 November, 18:00 Release of paper assignment

5 March 2021, 18:00 Deadline for submission of seminar report

 

Paper Assignment and Schedule

Date	Presenter	Paper	Short Reviews
19.11	Saif Ali Khan	Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks	Sukrut Rao, Maurice Vincon
26.11	no meeting
03.12	Sukrut Rao	Verification of Deep Convolutional Neural Networks Using ImageStars	Md Jonybul Islam,   Muhammad Hassan Rashid, Rati Devidze
10.12	Ashish Khullar	Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness	Muhammad Hassan Rashid,  Markus Bever, Maurice Vincon
17.12	Maksim Moor	Requirements-driven Test Generation for Autonomous Vehicles with Machine Learning Components	Md Jonybul Islam
07.01	Markus Bever	Verisig: verifying safety properties of hybrid systems with neural network controllers	Sukrut Rao,   Saif Ali Khan, Muhammad Hassan Rashid
14.01	Maurice Vincon	Cautious Reinforcement Learning with Logical Constraints	Rati Devidze, Maksim Moor
21.01	Rati Devidze	A Composable Specification Language for Reinforcement Learning Tasks	Md Jonybul Islam, Maurice Vincon
28.01	Muhammad Hassan Rashid	Abduction-Based Explanations for Machine Learning Models	Sukrut Rao, Ashish Khullar
04.02	Md Jonybul Islam	Synthesizing Action Sequences for Modifying Model Decisions	Saif Ali Khan, Ashish Khullar, Maksim Moor, Markus Bever, Rati Devidze
11.02	not presented	FairSquare: Probabilistic Verification of Program Fairness	Markus Bever,   Maksim Moor, Ashish Khullar, Saif Ali Khan

Deliverables

• 3 short reviews: For 3 of the papers that will be discussed during the seminar (different from the paper that you will present) you will write a short (maximum 1 page) review that addresses the following questions:

1. What is the problem addressed by the paper?
2. What was done before, and how does the paper improve on previous work?
3. What are the strengths and the limitations of the techniques in the paper?
4. What part of the paper was difficult to understand?
5. What are possible improvements or extensions of the techniques in the paper?

Each review is to be submitted before the meeting at which the paper will be presented and discussed.

Each of the three reviews contributes 10% of your final grade.

• Presentation: You will prepare and deliver a 45 min presentation of the paper assigned to you. You will have the possibility to get feedback on your slides before the presentation.

The slides and presentation make up 40% of the final grade.

• Summary: After your presentation you will write a summary of the paper that you have presented, including a general overview of the topic and reflecting the group discussion.

The summary will make up 30% of the final grade.

Papers

Verification of Neural Networks

• Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks  (CAV 2017)    

• Optimization and Abstraction: A Synergistic Approach for Analyzing Neural Network Robustness (PLDI 2019)

• An Abstraction-Based Framework for Neural Network Verification (CAV 2020)

• Verification of Deep Convolutional Neural Networks Using ImageStars (CAV 2020)

Cyber-Physical Systems with ML Components

• Compositional Falsification of Cyber-Physical Systems with Machine Learning Components (Journal of Automated Reasoning 2019)

• Requirements-driven Test Generation for Autonomous Vehicles with Machine Learning Components (EEE Transactions on Intelligent Vehicles 2020)

• Verisig: verifying safety properties of hybrid systems with neural network controllers (HSCC 2019)

• Formal verification of neural network controlled autonomous systems (HSCC 2019)

• Safety Verification of Cyber-Physical Systems with Reinforcement Learning Control (EMSOFT 2019)

Safe Reinforcement Learning

• Safe Reinforcement Learning via Shielding (AAAI 2018)

• An Inductive Synthesis Framework for Verifiable Reinforcement Learning (PLDI 2019)

• End-to-End Safe Reinforcement Learning through Barrier Functions for Safety-Critical Continuous Control Tasks (AAAI 2019)

• Cautious Reinforcement Learning with Logical Constraints (AAMAS 2020)

• A Composable Specification Language for Reinforcement Learning Tasks (NeurIPS 2019)

Interpretability

• Abduction-Based Explanations for Machine Learning Models (AAAI 2019)

• Extracting Automata from Recurrent Neural Networks Using Queries and Counterexamples (ICML 2018)

• Imitation-Projected Programmatic Reinforcement Learning (NeurIPS 2019)

• Synthesizing Action Sequences for Modifying Model Decisions (AAAI 2020)

Verification of Fairness Properties

• FairSquare: Probabilistic Verification of Program Fairness (OOPSLA 2017)

• Probabilistic Verification of Fairness Properties via Concentration (OOPSLA 2019)