Verification of neural systems

Forthcoming autonomous systems are expected to use machine learning techniques to implement their components for perception and control functions. Such machine learning-based components are synthesised from data and can be implemented via neural networks. Although machine learning components have attractive performance, for example on image classification tasks, concerns are raised in terms of the safety of the overall system. It is known that neural networks are fragile and hard to understand. Therefore, if machine learning components are to be used in safety-critical systems, it is essential that they are verified and validated before deployment. Little work addresses the verification of closed-loop systems controlled by agents synthesised from data and implemented via neural networks. Previous work considered simple, predictable, single-agent systems with fully-observable environments resulting in linear traces. The work of the thesis aims to tackle more realistic environments where autonomous agents are typically deployed, which are more dynamic and unpredictable, with agents that cannot fully observe the environment. To overcome this, we firstly put forward a model accounting for complex, partially observable environments resulting in branching traces and produce a method to verify such systems. Secondly we introduce neural-symbolic agents equipped with a neural network-based perception unit and a symbolic controller, and we verify the outcomes of the strategic interplay of groups of such agents. All procedures are implemented in a novel toolkit called VENMAS (Verification of Neural Multi-Agent Systems). The toolkit is used to analyse a toy example % reinforcement-learning scenario called Frozen Lake, single and multi-agent variants of a complex prototype for air-traffic collision avoidance as well as the iterated prisoners dilemma scenario.Open Acces