Standards Development

Scope

This document provides methodology on the use of formal methods to assess robustness properties of neural networks. The document focuses on how to manage and put in place formal methods to prove robustness properties.

Purpose

Robustness is the ability of an AI system to maintain its level of performance under any conditions. However, unlike others techniques in the AI domain, neural networks pose specific challenges in term of robustness. For example, they are known to have adversarial examples which constitute serious vulnerabilities. For some very small and specific variations on their inputs the neural network can drastically change its behavior. Also they do not have a steady ability to generalize correctly over their domain of use. Meaning that the performance observed on some inputs are not necessarily representative of the performance on some other one, making the any experimental validation process complex and uncertain. Ideally it would be optimal to test each input however this solution is not tractable due to either the very large number of inputs possible or the fact that the domain of use of the neural network is open and is difficult to confine.

All of these issues can have an important impact on the trustworthiness of the system and in return its acceptability by the public or the industry. To assess the robustness of neural networks several formal method techniques are available, each one presents a tradeoff between advantages and inconveniences that is to be accounted for. While statistical and empirical methods can help construct a first validation framework for neural networks validation, formal methods are useful to determine strong properties that are proven true on whole domains and not just isolated inputs.

Some robustness metrics are described in the technical report 24029-1, they allow to build properties needed for neural network. For example, the uncertainty of an interpolator or the maximum stable space are important to assess robustness properties. Their use in a process of validation of neural networks raise some questions and require some guidelines in order to prove robustness properties that are useful to bring trust in the neural network behavior.

For example, it is essential for any engineer assessing formally robustness properties of a neural network to ask himself:

• Which property is desired on the system and how to translate it in terms that formal methods can prove?

• How to express at a higher level the robustness properties checked using formal methods?

• Which formal method to use depending on the kind of property that is needed on the system?

In order to have a trusted process of assessing the robustness of neural networks, some methodologies are needed, which is the purpose of this deliverable.