FRAIME

The widespread adoption of AI in many fields of society calls for techniques making AI safer and more trustworthy. Systems based on AI show impressive performance but their opacity makes them unreliable for industrial applications, since they do not offer any guarantee. In contrast, Formal Methods excel at logical reasoning, can prove properties of programs or detect bugs, but are often limited in their scalability.

In the FRAIME Défi between Inria and MERCE, we propose to explore on the one hand how Formal Methods can provide guarantees on AI systems, and on the other hand how AI can help Formal Methods to be more efficient and easier to use by practitioners. The vision is to intertwine Formal Methods and AI to efficiently design safe systems.