Bridging the embedding gap between expressive specification and efficient verification of machine learning

Job description: Formal verification of neural networks is facing a double-faceted issue. The expressiveness of specifications (as in: compact and close to human understanding) is apparently clashing with their efficient translation to state-of-the-art prover, who only support a fragment of arithmetic without quantifiers. This thesis will investigate quot;globalquot; properties. Such class of properties describe generic behaviours of neural networks, beyond the level of local samples. Such properties are currently partially specified and most of them cannot be soundly derived into standard prover queries. Using the expressive power of the WhyML specification langage, this thesis will strive to propose a common encoding for global properties and investigate their efficient compilation to prover queries thanks to automated graph editing techniques. This thesis will also investigate the comparison of provers performance, in particular drawing inspiration from portfolio approaches.