In the frame of its Artificial Intelligence Roadmap, the European Union Aviation Safety Agency (EASA) and Collins Aerospace Applied Research & Technology completed an Innovation Partnership Contract (IPC) with the publication of a report that addresses the concrete challenges of the use of Formal methods techniques to address objectives of the Learning Assurance framework on learning algorithm and trained model stability that was developed in the EASA AI Concept Paper Issue 01 and refined in the Proposed Issue 02.
This scope of work led to select the name ForMuLA for this IPC, standing for ‘Formal Methods Use for Leaning Assurance’.
A public Version of the ForMULA report is available under the link below.
The goal of this project was to explore the challenges and possible use of Formal methods techniques for machine learning application. Trustworthiness of machine learning enabled systems is an open challenge, and barriers to their certification still exist. To overcome those, new assurance methods and processes need to be developed and adopted in the aviation industry. To make a step towards this goal, the ForMuLA project covered:
• an overview of state-of-the-art of ML-specific formal methods technologies and their limitations
• efficient ways of applying promising Formal Methods for Machine Learning development and Validation/Verification activities with a specific focus on the stability and robustness of machine learning models
• an identification of a subset of formal methods approaches as efficient means of compliance for certification objectives from the EASA AI concept paper.
The conclusions of this report resonate with Task 3 of the major Horizon Europe research project MLEAP (Machine Learning Applications Approval) launched by EASA in May 2022 with a consortium Airbus Protect, LNE and Numalis. The ForMuLA IPC will serve as an important concrete input to this project.
