Verification of RNN-Based Neural Agent-Environment Systems

Abstract

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.

Cite

Text

Akintunde et al. "Verification of RNN-Based Neural Agent-Environment Systems." AAAI Conference on Artificial Intelligence, 2019. doi:10.1609/AAAI.V33I01.33016006

Markdown

[Akintunde et al. "Verification of RNN-Based Neural Agent-Environment Systems." AAAI Conference on Artificial Intelligence, 2019.](https://mlanthology.org/aaai/2019/akintunde2019aaai-verification/) doi:10.1609/AAAI.V33I01.33016006

BibTeX

@inproceedings{akintunde2019aaai-verification,
  title     = {{Verification of RNN-Based Neural Agent-Environment Systems}},
  author    = {Akintunde, Michael E. and Kevorchian, Andreea and Lomuscio, Alessio and Pirovano, Edoardo},
  booktitle = {AAAI Conference on Artificial Intelligence},
  year      = {2019},
  pages     = {6006-6013},
  doi       = {10.1609/AAAI.V33I01.33016006},
  url       = {https://mlanthology.org/aaai/2019/akintunde2019aaai-verification/}
}