The course aims to provide students with foundational knowledge and applied skills to analyze, design and verify AI systems with safety guarantees.
Knowledge and understanding: understand core risks in AI systems and formal techniques used to verify them.
Applying knowledge and understanding: be able to model properties (e.g. robustness, reachability) and verify them on specific ML systems using dedicated tools.
Making judgments: evaluate the safety of AI pipelines and propose verification-based mitigation strategies.
Communication skills: effectively present formal arguments and system limitations during analysis or development reviews.
Learning skills: autonomously explore advanced methods and tools in Safe AI and formal methods.

Basic understanding of Deep NN and RL. Familiarity with linear algebra, and Python programming is recommended.

The course provides a theoretical and practical introduction to the safety and verification of Artificial Intelligence systems, with a focus on safety-critical applications and formal methods. Topics include: Risks and failures in AI systems, Safety-critical AI domains (e.g., automotive, healthcare, robotics), Formal verification of neural networks, Adversarial robustness and certified defenses, Runtime verification and monitoring with temporal specifications, Safe reinforcement learning and Markov decision processes.

Not yet a proper book for the topic. Part of the course background will be cover by the Principles of Model Checking – C. Baier, J.-P. Katoen.
Materials prepared for the students in the form of notebooks and slides, paper reference and documentation for the tools will be provided during the course.

Introduction to AI Safety: Case studies of failures in autonomous systems (Tesla, Boeing MCAS, etc.), Taxonomy of risks in AI systems (adversarial attacks, out-of-distribution behavior, hallucinations, systemic errors).
Foundations of Formal Methods: propositional logic and temporal logics (LTL, CTL), transition systems, automata, safety and liveness properties; Practical exercises on formal specifications and automatic verification Formal Verification of Neural Networks: verifiable properties (local robustness, monotonicity, fairness); verification workflows for neural networks: modeling specifications, choosing appropriate verification strategies, and interpreting formal outcomes in safety-critical contexts
Adversarial Robustness in AI Systems: definitions of adversarial attacks, threat models, and their implications on the reliability and safety of neural networks; defenses against adversarial attacks with provable guarantees: formal robustness certification and strategies for bounding model behavior under perturbations Runtime Verification and Monitoring: monitorable temporal logics and automatic monitor synthesis; runtime monitors for neural networks and sequential agents; specification and verification of safety properties during execution, exercise on design and implementation of a monitor for a safety-critical task
Safe Reinforcement Learning: MDPs, policies, reward functions: formalization and symbolic models; safety notions: reachability, safe sets, shielding; probabilistic model checking: PRISM, Storm, guided simulations: verification of safe policies for robot navigation.
Safe Autonomy in AI-Based Systems; formal modeling of autonomous systems operating in physical environments; hybrid system representations: integrating discrete AI decision-making with continuous dynamics; safety properties for autonomous agents: collision avoidance, invariant regions, bounded behavior; verification techniques for control and planning modules in AI-augmented systems; examples from autonomous vehicles, drones, and robotic platforms.
Integration in the AI Development Lifecycle: specification and traceability of formal safety requirements; systematic testing of AI components using structured input generation, fault injection, and behavioral analysis; building a safety case: structured collection of safety evidence

Lectures include theoretical background and hands-on sessions. Students will experiment with model checkers, verification tools, and simple AI components. Non-compulsory assignments will be proposed for practice.

Slides and additional materials (code, datasets, papers) will be made available after each class.

The exam will consist of a practical project of specifying and analyzing an AI component (e.g., NN or policy) using one of the various techniques seen in class (e.g., runtime monitoring or adversarial attack). followed by its presentation in class.
The oral presentation should concisely communicate the system's design principles, methodologies employed, functionalities, strengths, potential areas of improvement, and any challenges encountered during the developmental phase.
Evaluation criteria: soundness of formal specification, correctness and reproducibility of the analysis, clarity of the presentation, and ability to answer conceptual questions.
Evaluation criteria will emphasize the system's efficiency, accuracy, user-friendliness, and reproducibility of the analysis. In addition, the clarity and consistency of the oral presentation and the ability to answer conceptual questions will also be under scrutiny.
During the presentation general questions related to the course will be asked.
The minimum grade to pass the exam is 18 and the maximum grade is 30.
Honours may only be awarded in exceptional cases if the student(s) has (have) extended the work with original contributions.

In any type of content produced by the student for admission to or participation in an exam (projects, reports, exercises, tests), the use of Large Language Model tools (such as ChatGPT and the like) must be explicitly declared. This requirement must be met even in the case of partial use.

This course explores topics closely related to one or more goals of the United Nations 2030 Agenda for Sustainable Development (SDGs)