Treffer: Enhancing Deep Reinforcement Learning with Executable Specifications.

Deep reinforcement learning (DRL) has become a dominant paradigm for using deep learning to carry out tasks where complex policies are learned for reactive systems. However, these policies are "black-boxes", e.g., opaque to humans and known to be susceptible to bugs. For example, it is hard --- if not impossible --- to guarantee that the trained DRL agent adheres to specific safety and fairness properties that may be required. This doctoral dissertation's first and primary contribution is a novel approach to developing DRL agents, which will improve the DRL training process by pushing the learned policy toward high performance on its main task and compliance with such safety and fairness properties, guaranteeing a high probability of compliance while not compromising the performance of the resulting agent. The approach is realized by incorporating domain-specific knowledge captured as key properties defined by domain experts directly into the DRL optimization process while leveraging behavioral languages that are natural to the domain experts. We have validated the proposed approach by extending the AI-Gym Python framework [1] for training DRL agents and integrating it with the BP-Py framework [2] for specifying scenario-based models [3] in a way that allows scenario objects to affect the training process through reward and cost functions, demonstrating dramatic improvement in the safety and performance of the agent. In addition, we have validated the resulting DRL agents using the Marabou verifier [4], confirming that the resulting agents indeed comply (in full) with the required safety and fairness properties. We have applied the approach, training DRL agents for use cases from network communication and robotic navigation domains, exhibiting strong results. A second contribution of this doctoral dissertation is to develop and leverage probabilistic verification methods for deep neural networks to overcome the current scalability limitations of neural network verification technology, limiting the applicability of verification to practical DRL agents. We carried out an initial validation of the concept in the domain of image classification, showing promising results. [ABSTRACT FROM AUTHOR]

Copyright of ICSE: International Conference on Software Engineering is the property of Association for Computing Machinery and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.)