Towards Verifying Monotonicity and Robustness Properties for Domain-Specific DRL Algorithms

Deep Reinforcement Learning (DRL) algorithms have demonstrated significant performance benefits compared to traditional heuristics in various systems and networking applications. However, concerns surrounding their explainability, generalizability, and robustness pose obstacles to their widespread deployment. In response, the research community has explored the application of formal verification techniques to ensure the safe deployment of DRL algorithms. This study focuses on DRL algorithms with discrete numerical action spaces, which are commonly utilized in systems and networking domains but have been under-explored when it comes to formal analysis. We investigate two fundamental properties: monotonicity and robustness. We employ formal methods to verify these properties beyond the confines of the training set, thereby enhancing generalization and validating robustness. To illustrate the effectiveness and tractability of the proposed verification approach, we implement a proof of concept using Gurobi and present a case study involving two systems and networking DRL algorithms.