ForML

The ongoing advances in machine learning (ML) foretell an ever-increasing range of practical uses of ML models. However, in domains deemed high-risk at the EU level, but also in safety-critical domains, the deployment of complex ML models should be underpinned by reasoning tools that are rigorous and efficient, and which are thus capable of identifying possible limitations of such ML models. Concrete examples include whether the ML model is adequately robust, whether it does not exhibit bias, but also whether its actions can be explained so as to be understood by a human decision maker or automatically validated. The ForML project proposes to make fundamental inroads in advancing the state of the art in rigorous approaches for reasoning about ML models. The ForML project proposes to exploit well-known hallmarks from software analysis, including abstract interpretation and counterexample-guided abstraction refinement, to promote a new generation of tools for rigorous ML reasoning, in explainability, fairness and robustness, which are both automated and efficient. Furthermore, the ForML project will also pioneer the certification of such tools by exploiting proof assistants.