The aim of this report is to present the outcome of the collaboration between the European Union Aviation Safety Agency (EASA) and Collins Aerospace on an Innovation Partnership Contract (IPC) that investigated the use of formal methods (FM) as part of the learning assurance building block of the EASA Artificial Intelligence (AI) Roadmap. The project focused on emphasising opportunities for the adoption of formal methods (FM) techniques in the design assurance process of machine-learning (ML)-enabled systems.
Applicability
The considerations summarised in the report apply to machine learning (ML) in general, but particular emphasis has been placed on specific challenges related to neural networks. The discussion of formal methods (FM) applications is purposefully kept generic.
This report does not recommend specific methods or tools but is rather intended to motivate opportunities from a theoretical perspective. Where applicable, a reference is made to concrete methods and tools.
Key achievements
- Formal methods (FM) can be applied to assess machine-learning (ML) model stability, robustness, and compliance with intended behaviours for a set of key certification objectives from the EASA Artificial Intelligence Concept Paper Issue 2
— Guidance for Level 1 & 2 machine-learning applications. - Practical demonstration of the use of formal methods (FM) on an industrial use case of a deep learning (DL)-based estimator for the remaining useful life of mechanical bearings in airborne equipment: The output of the estimator is used for on-ground maintenance applications. Demonstrations provided concrete evidence of how FM and supporting statistical techniques can be used as part of the verification activities to deal with data quality assessment, machine-learning (ML) stability, robustness, and intended behaviour verification.
- Detailed discussion of relevant formal methods (FM) technologies and supporting statistical methods, and their possible role in the development, as well as validation and verification (V&V) of machine learning (ML)-enabled systems: Emphasis has been placed on innovative formal methods (FM) applications, specific to the robustness assessment of machine-learning (ML) models.
Challenges
Scalability and applicability of formal methods (FM) tools need further development, to be used on machine-learning (ML) applications.
Future work
Further research activities are needed, to enhance formal methods (FM) scalability and address high-dimensional machine-learning (ML) models: The ForMuLA IPC will serve as an important concrete input to Task 3 of the Horizon Europe Research Project Machine Learning Applications Approval (MLEAP), launched by EASA in May 2022 with a consortium of Airbus Protect, LNE, and Numalis.
Quoting this report
EASA and Collins Aerospace, Formal Methods use for Learning Assurance (ForMuLA), April 2023
