Formal verification of neural agents in non-deterministic environments
Abstract
We introduce a model for agent-environment systems where the agents are implemented via feed-forward ReLU neural networks and the environment is non-deterministic. We study the verification problem of such systems against CTL properties. We show that verifying these systems against reachability properties is undecidable. We introduce a bounded fragment of CTL, show its usefulness in identifying shallow bugs in the system, and prove that the verification problem against specifications in bounded CTL is in coNExpTime and PSpace-hard. We introduce sequential and parallel algorithms for MILP-based verification of agent-environment systems, present an implementation, and report the experimental results obtained against a variant of the VerticalCAS use-case and the frozen lake scenario.
Document Details
- Document Type
- Pub Defense Publication
- Publication Date
- Nov 09, 2021
- Source ID
- 10.1007/s10458-021-09529-3
Entities
People
- Alessio Lomuscio
- Elena Botoeva
- Michael E. Akintunde
- Panagiotis Kouvaros
Organizations
- Defense Advanced Research Projects Agency
- Royal Academy of Engineering