Reachability analysis for neural agent-environment systems

Abstract

We develop a novel model for studying agent-environment systems, where the agents are implemented via feed-forward ReLU neural networks. We provide a semantics and develop a method to verify automatically that no unwanted states are reached by the system during its evolution. We study several reachability problems for the system, ranging from one-step reachability, to fixed multi-step and arbitrary-step to study the system evolution. We also study the decision problem of whether an agent, realised via feed-forward ReLU networks will perform an action in a system run. Whenever possible, we give tight complexity bounds to decision problems intro- duced. We automate the various reachability problems stud- ied by recasting them as mixed-integer linear programming problems. We present an implementation and discuss the ex- perimental results obtained on a range of test cases.