Formally Certified Reasoning in Machine Learning

The project ForML is a research project founded by the French National Research Agency.

The ForML project will investigate the use of well-known paradigms from software analysis in the context of ML reasoning. Two specific paradigms will be investigated, building on preliminary results by the research team: abstract interpretation and counterexample-guided abstraction refinement. The application of these paradigms to robustness, fairness and explainability will be investigated. Furthermore, ForML will make inroads into the problem of certifying rigorous algorithms for reasoning about ML models, thus ensuring that implementations produce results that are guaranteed to be correct.
The overarching research hypothesis is that reasoning about large, complex ML models can be achieved through the use of formal methods.
To validate the main research hypothesis, the ForML project will investigate a number of important research topics, which also serve to create research synergies between the teams participating in the project.

Open positions
In Toulouse : Funding for Master2 internships

Explanation of models derived by machine learning (ML) is crucial to help humans understand the decisions made by these models. Indeed, providing explanations with a guarantee of correctness is one of the major challenges facing the use of ML techniques in safety-critical systems. The ANR project ‘ForML’ will focus on the search for new families of explanation problems that are computationally tractable, followed by the construction of reliable explanation software. The user must have confidence in these programs, so either they will be proven correct or they will generate a certificate to justify correctness. The ultimate goal is to make publicly available efficient and reliable software. Practical information: funding is available for a postdoc, PhD and Master internships. Candidates are expected to have a background in theoretical computer science and/or mathematics, particularly in complexity theory and/or formal methods. Successful candidates will be co-supervised by Aurélie Hurault from Toulouse INP and Martin Cooper from the University of Toulouse 3. For further information, please contact: aurelie.hurault @, cooper @

In Paris : PhD Subject