Formal Verification of Machine Learning with the Industry: the Journey so Far, and the Future Ahead

Abstract

Since the third AI revolution in 2012, industry displayed a keen interest in the newfound capabilities of machine learning. However, in the field of critical systems, existing regulations and practices require some degree of formal specification (and verification). Furthermore, machine learning specification is implicitly defined by hyperparameters that are impossible to formalise (the dataset, the architecture, the objective function, the intended goal). To address those newfound challenges and fulfill its mission to support industrial actors, the French Atomic Energy Commission develop and maintain several tools for the specification and verification of machine learning systems. For seven years, those tools were applied in industrial settings, in national and international projects. Through this presentation mixing science and technical retrospective, we present the successes, the limitations and potential future paths for formal verification informed by the needs of the French industry.