Skip to main content

Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis

Author(s): Zhang, Hongce; Shinn, Maxwell; Gupta, Aarti; Gurfinkel, Arie; Le, Nham; et al

To refer to this page use:
Abstract: Recurrent Neural Networks (RNNs) are one of the most successful neural network architectures that deal with temporal sequences, e.g., speech and text recognition. Recently, RNNs have been shown to be useful in cognitive neuroscience as a model of decision-making. RNNs can be trained to solve the same behavioral tasks performed by humans and other animals in decision-making experiments, allowing for a direct comparison between networks and experimental subjects. Analysis of RNNs is expected to be a simpler problem than the analysis of neural activity. However, in practice, reasoning about an RNN’s behaviour is a challenging problem. In this work, we take an approach based on formal verification for the analysis of RNNs. We make two main contributions. First, we consider the cognitive domain and formally define a set of useful properties to analyse for a popular experimental task. Second, we employ and adapt wellknown verification techniques for reachability analysis to our focus domain, i.e., polytope propagation, invariant detection, and counter-example-guided abstraction refinement. Our experiments show that our techniques can effectively solve classes of benchmark problems that are challenging for state-of-the-art verification tools.
Publication Date: 2020
Citation: Zhang, Hongce, Maxwell Shinn, Aarti Gupta, Arie Gurfinkel, Nham Le, and Nina Narodytska. "Verification of Recurrent Neural Networks for Cognitive Tasks via Reachability Analysis." 24th European Conference on Artificial Intelligence (2020): pp. 1690 - 1697. doi:10.3233/FAIA200281
DOI: 10.3233/FAIA200281
ISSN: 0922-6389
Pages: 1690 - 1697
Type of Material: Conference Article
Series/Report no.: Frontiers in Artificial Intelligence and Applications;
Journal/Proceeding Title: 24th European Conference on Artificial Intelligence
Version: Final published version. This is an open access article.

Items in OAR@Princeton are protected by copyright, with all rights reserved, unless otherwise indicated.