Flagged as work that qualifies or bounds the uncontainability case.
This paper introduces a model for agent-environment systems where the agents are implemented via feed-forward ReLU (rectified linear unit) neural networks, i.e. fully-connected networks whose hidden layers apply the activation function max(0, x), and the environment is non-deterministic. The verification problem of such systems against CTL (computation tree logic, a branching-time temporal logic) properties is studied. Verifying these systems against reachability properties, i.e. whether a target set of states is eventually reached, is undecidable. A bounded fragment of CTL, i.e. a language expressing temporal properties realisable in a limited number of execution steps, is introduced; its usefulness in identifying shallow bugs, i.e. malfunctions that are realised within a few steps from the system's initialisation, is shown, and the verification problem against specifications in bounded CTL is in coNExpTime (the complement class of nondeterministic exponential time) and PSpace-hard (at least as hard as every problem solvable in polynomial space). Sequential and parallel algorithms for MILP-based (mixed-integer linear programming based) verification of agent-environment systems are introduced, an implementation is presented, and experimental results obtained against a variant of the VerticalCAS use-case, an aircraft collision avoidance system that issues vertical climbrate advisories to the pilot to avoid near mid-air collisions, and the frozen lake scenario, a gridworld in which an agent must reach a goal tile while avoiding holes in the ice, with slippery tiles making its resulting movement direction uncertain, are reported. Since forthcoming autonomous systems will make greater use of machine learning methods, there is an urgent need to develop techniques aimed at providing guarantees on the resulting behaviour of such systems, and formal verification methods — long adopted in safety-critical and industrial-scale software — should be extended to systems driven by neural networks, where few such efforts currently exist.
Extend the framework for verifying closed-loop neural systems, i.e. neural agents coupled to an environment in a feedback loop of observations and actions, whose non-deterministic dynamics make the system's temporal evolutions branch into many possible futures rather than a single linear trace, to multiple agents operating in an environment.