Verification of RNN-Based Neural Agent-Environment Systems

  • Michael E. Akintunde Imperial College London
  • Andreea Kevorchian Imperial College London
  • Alessio Lomuscio Imperial College London
  • Edoardo Pirovano Imperial College London


We introduce agent-environment systems where the agent is stateful and executing a ReLU recurrent neural network. We define and study their verification problem by providing equivalences of recurrent and feed-forward neural networks on bounded execution traces. We give a sound and complete procedure for their verification against properties specified in a simplified version of LTL on bounded executions. We present an implementation and discuss the experimental results obtained.

AAAI Technical Track: Multiagent Systems