Artificial Intelligence (AI), particularly with its recent advancements in Machine Learning (ML), is expected to have a wide range of applications in our society, even in critical systems like health, energy and transportation. The ML revolution has changed the way software is developed, providing performance beyond traditional explicit programming. Although there are undeniable benefits to be gained through AI, researchers have identified several shortcomings, pertaining to its reliability and explainability, that need to be addressed before AI-based systems can be widely accepted. Indeed, it is crucial to invest effort in developing tools and methods aiming at safer, more transparent AI-based systems.

Ensuring software reliability is not a new goal: several statistical and Formal Methods (FM) approaches have been developed throughout the decades to deal with these problems. The FM community has spent this time building the mathematical and logical foundation for efficient software tools that can intervene in all steps of the software lifecycle, from specification and development to deployment and monitoring. By providing tools to achieve higher safety standards, the FM community has made the world a safer place, as reflected in the growing number of standards that mandate the use of FM in the development of safety-critical software.

However, the FM approach falls short in dealing with the challenges posed by the recent advances in AI. Most of the challenges in using FM for ML-based systems stem from their stochastic and uncertain nature, large size, difficulty in specification, monolithic nature, lack of interpretability, and the profusion of different architectures that make for an ever widening field of AI.

To tackle these challenges, SAIF is organized along three objectives, articulated along three of the main steps in the traditional life-cycle of software development: specifying, designing and validating ML-based systems. Each of these objectives carries its own sub-objectives, some of which are naturally interconnected with others. These sub-objectives aim to push the current state of the art, for example in the direction of the AI artifacts that are handled (in particular complex architectures such as Graph Neural Networks and Recurrent Neural Networks), in the direction of the application domains (by extending to non-image types of data such as time series and spectrometry) and in the direction of the methods underlying the targeted trustworthiness-enhancing tools (such as tropical algebras).

ML has already shown great potential for our society, but to fully realize its positive impact, safety guarantees must be rigorously ensured. This requires a significant shift in the way we use formal methods to address the modern problems of AI. The goal of SAIF is to use the vast knowledge accumulated over decades in formal methods to rethink them and address the novel safety concerns raised with the renewal of AI. Through the synergy of a diverse consortium with complementary expertise, we aim to help society closer to a state where it can benefit from ML’s achievements without suffering its undue consequences.