Verification of RNN-Based Neural Agent-Environment Systems
Authors: Michael E. Akintunde, Andreea Kevorchian, Alessio Lomuscio, Edoardo Pirovano6006-6013
AAAI 2019 | Conference PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Experimental | We present an implementation and discuss the experimental results obtained. 6 Implementation and Evaluation We implemented the methods described in the previous sections into an experimental toolkit, called RNSVERIFY (RNSVerify 2018), thereby automating the unrolling procedures described in Section 4 as well as the verification procedure described in Algorithm 1. ... In order to evaluate our implementation and its scalability, we consider the Open AI task Pendulum-v0 (Open AI 2018). |
| Researcher Affiliation | Academia | Michael E. Akintunde, Andreea Kevorchian, Alessio Lomuscio, Edoardo Pirovano Department of Computing, Imperial College London, UK |
| Pseudocode | Yes | Algorithm 1 Verification Procedure Input: RNN-AES; formula φ Output: True/False 1: C CI 2: switch φ do 3: case Xk C 4: for n 0 until k do 5: C C[ x, xn] Co[ x, xn][ o, on] 6: C C CRn Ct[ x, xn][ a, an][ y, x] 7: end for 8: return SAT({ C} C) 9: case C1U k C2 10: for n 0 until k do 11: C C { C2} 12: if SAT(C) then 13: return True 14: end if 15: if SAT({ C1} C) then 16: return False 17: end if 18: C C[ x, xn] Co[ x, xn][ o, on] 19: C C CRn Ct[ x, xn][ a, an][ y, x] 20: end for 21: return False |
| Open Source Code | Yes | We implemented the methods described in the previous sections into an experimental toolkit, called RNSVERIFY (RNSVerify 2018), thereby automating the unrolling procedures described in Section 4 as well as the verification procedure described in Algorithm 1. ... RNSVerify. 2018. Recurrent Neural System Verify, http://vas.doc.ic.ac.uk/software/ also available as supplementary material. |
| Open Datasets | Yes | In order to evaluate our implementation and its scalability, we consider the Open AI task Pendulum-v0 (Open AI 2018). ... Open AI. 2018. Pendulum-v0. https://gym.openai.com/envs/Pendulum-v0/. |
| Dataset Splits | No | The paper describes the initial states for the environment in experiments ('We fix a set of initial states with 0 θi π/64 and 0 θi 0.3'), but it does not specify explicit training, validation, or test dataset splits in terms of percentages or sample counts, nor does it refer to predefined splits for a dataset. |
| Hardware Specification | Yes | on a machine running Linux kernel 3.16 on an Intel Core i5-3320M CPU with 4GB of RAM. |
| Software Dependencies | Yes | RNSVERIFY is written in Python and uses Gurobi ver. 7.5.2 (Gu, Rothberg, and Bixby 2016) as its underlying MILP solver. ... For the agent, we used QLearning (Watkins and Dayan 1992) to train a Re LU-RNN with 16 hidden units using the open source deep learning toolkit Keras ver. 2.2.2 (Chollet 2015). |
| Experiment Setup | Yes | For the agent, we used QLearning (Watkins and Dayan 1992) to train a Re LU-RNN with 16 hidden units using the open source deep learning toolkit Keras ver. 2.2.2 (Chollet 2015). The weights of the RNN were initialised as described in (Le, Jaitly, and Hinton 2015). In order to utilise a Q-Learning approach, we discretised the action space of the agent such that it may only produce forces contained in the set { 1, 1}, i.e., only a positive or negative force of equal magnitude. ... We checked the property φ = Xn(θf > ε) for different positive values of ε and a variable number of steps n. |