Verification of Autonomous Agents in Uncertain Environments

With the widespread deployment of autonomous agents, such as autonomous cars and robots and the increasing focus on AI safety [24], this project aims to investigate the safety of neuro-symbolic agents. The field of neuro-symbolic systems is an exciting area of research that combines the power of machine learning with the rigour of symbolic reasoning. Neural systems have shown great promise in a wide range of applications, from robotics and autonomous systems to natural language processing and decision-making. However, verifying the correctness of these systems remains a significant challenge. While neural networks are excellent at learning patterns in data, they can be difficult to interpret and analyse. On the other hand, symbolic reasoning is highly transparent and understandable, but it can be challenging to scale up to complex non-linear and high-dimensional systems.

In this project, we are interested in the analysis of multi-agent neuro-symbolic systems (NSS), which are systems comprising multiple agents interacting with each other and with the environment. The behaviour of such agents is determined by a combination of physical dynamics, such as laws of motion, and machine learning components, which are used, for instance, for perception and control. This kind of system is relevant in many applications, such as multi-agent (deep) reinforcement learning [1], swarm robotics, and traffic management.

We aim to develop verification algorithms for multi-agent NSSs, to provide formal guarantees about the satisfaction of some requirements of interest (reach-avoid, multi-stage tasks, or other kinds of temporal properties). Formal reasoning about these systems is, however, computationally challenging, owing to the presence of (complex) neural network models, multiple agents, uncertain (non-deterministic or probabilistic) environments, and sequential decision-making over multiple time steps.

Considerable progress has been made in the verification of one-step reachability for neural networks (i.e., input-output specifications), including probabilistic deep models, using techniques like bound propagation [2,3], and constraint solving [4,5]. These techniques have been recently extended to the verification of single-agent sequential decision-making [6-8]. However, the multi-agent case remains a largely unexplored research area, except [9-11].

This project will focus on developing new methods to verify the behaviour of multi-agent NSSs under uncertain environments, where uncertainty can be reasoned about in a probabilistic or non-deterministic fashion. We envision that the solution methods will build on and improve existing verification techniques for single-agent systems, possibly investigating suitable abstractions for dimensionality reduction as well as the combination with data-driven methods like [12-14] to obtain probabilistic guarantees in the most complex cases where purely symbolic approaches fail.

The methods will be evaluated in standard multi-agent RL benchmarks like [15,16] and different real-world scenarios coming from the REXASI-PRO EU project [17], which will focus on safe navigation of autonomous wheelchairs in crowded environments for people with reduced mobility.

This research project will contribute to the development of trustworthy and reliable multi-agent systems, which can have a significant impact on many applications. The developed techniques will further contribute to improving the scalability of current verification (aka certification) techniques for neural networks.

[1] Hernandez-Leal, Pablo, Bilal Kartal, and Matthew E. Taylor. “A survey and critique of multiagent deep reinforcement learning.” Autonomous Agents and Multi-Agent Systems 33, no. 6 (2019): 750-797.

[2] Wang, Shiqi, Kexin Pei, Justin Whitehouse, Junfeng Yang, and Suman Jana. “Efficient formal safety analysis of neural networks.” Advances in neural information processing systems 31 (2018).

[3] Wicker, Matthew, Luca Laurenti, Andrea Patane, and Marta Kwiatkowska. “Probabilistic safety for bayesian neural networks.” In Conference on uncertainty in artificial intelligence, pp. 1198-1207. PMLR, 2020.

[4] Katz, Guy, Derek A. Huang, Duligur Ibeling, Kyle Julian, Christopher Lazarus, Rachel Lim, Parth Shah et al. “The marabou framework for verification and analysis of deep neural networks.” In CAV 2019, pp. 443-452.

[5] Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., & Misener, R. (2020, April). Efficient verification of relu-based neural networks via dependency analysis. In the AAAI Conference on Artificial Intelligence, AAAI.

[6] Tran, H. D., Yang, X., Manzanas Lopez, D., Musau, P., Nguyen, L. V., Xiang, W., Bak, S., & Johnson, T. T. (2020). NNV: the neural network verification tool for deep neural networks and learning-enabled cyber-physical systems. In Computer Aided Verification, CAV.

[7] Wicker, M., Laurenti, L., Patane, A., Paoletti, N., Abate, A., & Kwiatkowska, M. (2021). Certification of iterative predictions in Bayesian neural networks. In Uncertainty in Artificial Intelligence, UAI.

[8] Hosseini, M. & Lomuscio, M., (2023) Bounded and Unbounded Verification of RNN-based Agents in Non-deterministic Environments. In The International Conference on Autonomous Agents and Multiagent Systems, AAMAS.

[9] Akintunde, Michael E., Elena Botoeva, Panagiotis Kouvaros, and Alessio Lomuscio. “Verifying strategic abilities of neural-symbolic multi-agent systems.” In Proceedings of the International Conference on Principles of Knowledge Representation and Reasoning, vol. 17, no. 1, pp. 22-32. 2020.

[10] Mqirmi, P. E., Belardinelli, F., & León, B. G. (2021). An Abstraction-based Method to Check Multi-Agent Deep Reinforcement-Learning Behaviors. In The International Conference on Autonomous Agents and Multiagent Systems, AAMAS.

[11] Riley, J., Calinescu, R., Paterson, C., Kudenko, D., & Banks, A.: Reinforcement Learning with Quantitative Verification for Assured Multi-Agent Policies. In International Conference on Agents and Artificial Intelligence, ICAART.

[12] Cubuktepe, Murat, Nils Jansen, Sebastian Junges, Joost-Pieter Katoen, and Ufuk Topcu. “Scenario-based verification of uncertain mdps.” In TACAS 2020, pp. 287-305.

[13] Bortolussi, Luca, Francesca Cairoli, and Nicola Paoletti. “Conformal Quantitative Predictive Monitoring of STL Requirements for Stochastic Processes.” In 26th ACM International Conference on Hybrid Systems: Computation and Control. 2023.

[14] Dixit, Anushri, Lars Lindemann, Skylar Wei, Matthew Cleaveland, George J. Pappas, and Joel W. Burdick. “Adaptive Conformal Prediction for Motion Planning among Dynamic Agents.” arXiv preprint arXiv:2212.00278 (2022).

[15] Mordatch, Igor, and Pieter Abbeel. “Emergence of grounded compositional language in multi-agent populations.” In Proceedings of the AAAI conference on artificial intelligence, vol. 32, no. 1. 2018.

[16] Lanctot, M., Lockhart, E., Lespiau, J.B., Zambaldi, V., Upadhyay, S., Pérolat, J., Srinivasan, S., Timbers, F., Tuyls, K., Omidshafiei, S. and Hennes, D., 2019. OpenSpiel: A framework for reinforcement learning in games. arXiv preprint arXiv:1908.09453.

[17] REliable & eXplAinable Swarm Intelligence for People with Reduced mObility (REXASI-PRO),

Project ID