Towards Formal Verification of Neuro-symbolic Multi-agent Systems

1 Introduction

Recent advances in Artificial Intelligence (AI) enabled the automation of challenging tasks, such as computer vision, that have been traditionally difficult to tackle for decades. This accelerated the incorporation of AI components in diverse applications, including ones situated within domains, such as healthcare and transportation, where the impact to society can be significant. While however AI has the potential of revolutionising society, its inherent fragility and opacity hinders its adoption in safety-critical applications. The associated risks are compounded in an increasingly inter-connected world, where systems of multiple interacting intelligent agents, or multi-agent systems (MAS), constitute a paradigm shift from object-oriented to interaction-oriented design standards.

In response to these concerns the area of formal verification of AI has grown rapidly over the past few years to provide methods to automatically verify that AI systems robustly behave as intended. One of the key techniques that has emerged in the area is that of model checking [Clarke et al., 1999]. Model checking provides automated solutions to the problem of establishing whether a model MS representing a system S satisfies a logical formula ϕP encoding a specification P. In the case of MAS, the formula φ does not simply express temporal properties of systems, as in reactive systems, but it may also be accounting for high-level attitudes of agency, such as knowledge and strategies, which can be described in temporal-epistemic logic [Fagin et al., 1995a] and alternating-time logic [Alur et al., 1998].

Whilst methods such as binary binary decision diagrams [Gammie and van der Meyden, 2004] and bounded model checking [Penczek and Lomuscio, 2003] enabled the model checking of systems of large state spaces, a main drawback of the approach remains the state-space explosion problem, whereby the state-space grows exponentially in the number of variables encoding the agents.

Notwithstanding that in practice this limits model checking to the verification of systems with only few constituents, the analysis of systems with arbitrarily many participants, such as robot swarms and applications in the Internet of Things, raises a principal barrier to its application. Indeed, verifying systems of this kind, henceforth unbounded multi-agent systems (UMAS), requires checking whether any system for any number of agents satisfies the specification in question. This renders model checking intractable when enumerating and analysing all individual systems.

Another key limitation of model checking is the requirement that the systems are given in traditional, agentbased programming languages, thereby not accounting for agents endowed with neural network components. Systems of this kind, henceforth neuro-symbolic multi-agent systems (NMAS), constitute important forthcoming applications, such as autonomous vehicles, where the neural components are responsible for automating complex tasks such as perception and control.

Even though neural networks exhibit remarkable performance on these tasks, their fragility to adversarial attacks [Szegedy et al., 2014] and their lack of interpretability [Doshi-Velez and Kim, 2017] raise additional concerns regarding the overall system safety, thereby strengthening the need for the principled analysis of NMAS before deployment.

This paper gives an overview of the methods that we developed within the Verification of Autonomous Systems Research Group, Imperial College London, towards the formal verification of UMAS and NMAS. Our pioneering work in the verification of UMAS, discussed in Section 2, overcomes the model checking barrier with the development of methods that enable the derivation of the number of agents that is sufficient to consider when evaluating a specification. Our studies in the analysis of NMAS, outlined in Section 3, include efficient methods for the verification of neural networks and mixed-integer linear programming (MILP) formulations for checking system-level specifications. The paper concludes in Section 4 with directions for future work.

2 UnboundedMulti-agent Systems

Interpreted systems are a standard semantics for describing multi-agent systems [Fagin et al., 1995b]. They provide a natural setup to interpret specifications in a variety of languages including temporal-epistemic logic and alternating temporal logic [Fagin et al., 1995a; Lomuscio and Raimondi, 2006]. Parameterised Interpreted Systems (PIS) is a parametric extension of interpreted systems that we put forward to reason about the temporal-epistemic properties of UMAS in both synchronous [Kouvaros and Lomuscio, 2015b] and asynchronous [Kouvaros and Lomuscio, 2016c] settings. The parameter in PIS denotes the number of agents in the system, each homogeneously constructed from an agent template.

The verification problem for PIS is to check whether any system for any value of the parameter satisfies a given specification. This is in general undecidable [Apt and Kozen, 1986]. Solutions to the problem can thus be given only in the form of incomplete techniques, which can decide the problem only some of the times. Alternatively, decidable fragments of the problem can be curved through the imposition of restrictions on the systems and/or the specifications.

In either case, a key concept that enables the verification of UMAS is that of a cutoff. A cutoff is a natural number that expresses the number of agents that is sufficient to consider when evaluating a given specification. In other words, if a cutoff can be identified, then the verification problem can be solved by checking all systems whose number of agents is below the cutoff value.

Whilst we've shown that cutoffs do not always exist [Kouvaros and Lomuscio, 2013b], strong empirical evidence supports their existence for real-world systems [Emerson and Kahlon, 2000; Emerson and Namjoshi, 1995; Aminof et al., 2014]. Moreover, for the cases where they do not exist, theoretical analyses that we conducted show that these often concern systems with impractical cyclic behaviours, which adhere to the peculiarity that their number of possible repetitions depends on the exact number of agents in the system [Kouvaros and Lomuscio, 2013b].

In the light of these observations we have analysed various sufficient conditions for the identification of cutoffs. The conditions were drawn with respect to different synchronisation primitives endowing the agents. In the fully synchronous setting, we have shown that cutoffs can always be identified and gave a procedure for their computation [Kouvaros and Lomuscio, 2015b]. In the asynchronous case, where agents communicate via broadcast actions, we have similarly given a sound and complete technique for their derivation [Kouvaros and Lomuscio, 2013a]. When the agents can additionally participate in pairwise communication with their environment, we have shown that if

• (i) the environment can never block pairwise synchronisations for the system of one agent only, and
• (ii) each synchronisation can happen in unique configurations for the environment,

then cutoffs can be computed in an efficient procedure that runs in linear time in the size of the agent template [Kouvaros and Lomuscio, 2013b]. Following this, we have shown that the second restriction can be lifted in a cutoff procedure that runs in exponential time [Kouvaros and Lomuscio, 2015a].

While these results were drawn with respect to homogeneous UMAS, where every agent is instantiated from a unique agent template, we have also provided extensions that account for heterogeneous UMAS, where agents can assume different roles and responsibilities, e.g., heterogeneous robot swarms [Kouvaros and Lomuscio, 2016c]. The heterogeneous semantics that we introduced allow for broadcast actions that may either concern all agents of all templates or regard only all agents following a certain template. They additionally enable pairwise interactions between agents of different roles, thereby far surpassing the expressive power of the homogeneous model.

Further gains in the expressivity of the protocols that can be verified have been obtained from our studies on UMAS programmed using variables with infinite domains [Kouvaros and Lomuscio, 2017a]. Our resulting verification method combines predicate abstraction [Lomuscio and Michaliszyn, 2015] with parameterised verification, the former addressing the unboundedness of the state-space of the agents and the latter tackling the unboundedness of their number.

Still other expressivity advances facilitated the verification of strategic properties of UMAS expressed in a parameterised variant of alternating-time temporal logic that we introduced [Kouvaros and Lomuscio, 2016b].

We have released the open-source parameterised verification toolkit MCMAS-P implementing these procedures. MCMAS-P enabled for the first time the verification of aggregation and foraging algorithms for robot swarms irrespective of the number of robots composing the swarm [Kouvaros and Lomuscio, 2015b; Kouvaros and Lomuscio, 2016c].

Further applications included the analysis of the security of an unbounded number of concurrent sessions of cryptographic protocols, for which we provided a mapping from a Dolev-Yao threat model to PIS [Boureanu et al., 2016].

Others concerned the verification of UMAS composed of data-aware agents, i.e., agents that are endowed with possibly infinite domains and that interact with an environment composed of (semi)-structured data. Having used simulationbased abstractions to deal with the infinity of the agents, we have then presented a translation to PIS to solve their verification problem [Belardinelli et al., 2017]. Analogous translations to PIS have enabled us to give verification procedures for open MAS, where countably many agents can join and leave the system at runtime [Kouvaros et al., 2019].

Yet other applications included adaptations of the underlying parameterised verification methods that enabled us to derive techniques for the verification of opinion formation protocols in swarms. These were used to give formal guarantees on the outcome of consensus protocols [Kouvaros and Lomuscio, 2016a].

Finally, complementary to protocol correctness, which the aforementioned methods can formally ascertain, the evaluation of protocols also requires analyses of the extent to which they are are resilient to adverse functioning behaviours for some of the agents in the system. For instance, when evaluating a robot swarm search-and-rescue scenario, it is not sufficient to establish that the swarm will collectively cover the search area, but it is also crucial to determine that local faults, e..g, hardware malfunctions, will be tolerated by the swarm, as opposed to being propagated through agent interactions with the result of dis-coordinating the search. To address this concern we have put forward an automated procedure to establish the robustness of UMAS against a given ratio of faulty to non-faulty agents in the system [Kouvaros and Lomuscio, 2017b], which we followed by a symbolic method to automatically synthesise the maximum ratio of faulty to non-faulty agents the system can tolerate [Kouvaros et al., 2018].

3 Neuro-symbolic Multi-agent Systems

To reason about the properties of NMAS, we have introduced neural interpreted systems (NIS), a novel formalisation of MAS based on interpreted systems. In a nutshell, an agent in NIS comprises a perception mechanism implement via neural networks and coupled with a symbolic action mechanism.

The neural network components, which endow the agents with infinite domains, pose significant challenges to the verification problem. In particular, differently from traditional verification for symbolic systems, where atomic formulae are evaluated in constant time at symbolic states of the system, the evaluation of atomic formulae in NIS includes the computation of the output regions of the neural networks for a (potentially infinite) set of inputs. This is an NP-complete problem [Katz et al., 2017]. Increasingly sophisticated solutions to the problem have been put forward in the past few years with a focus on the analysis of neural network robustness against adversarial attacks [Singh et al., 2019; Kouvaros and Lomuscio, 2021; Wang et al., 2021].

We first discuss our work on the verification of standalone neural networks which forms the backbone of our studies on the analysis of NMAS later outlined.

3.1 Neural Network Verification

The neural network verification problem is to determine whether the output of a given network is as expected for a potentially infinite set of inputs.

One of its most common instantiations is the local adversarial robustness problem whereby the set of inputs denotes imperceptible perturbations on a fixed input and the set of outputs encodes classification equivalence for all perturbations. While significant progress has been made in push-down engines to solve the problem [Brix et al., 2023], scalability to industrial-size models found in complex tasks such as computer vision remains a key difficulty in the area.

Advances are driven by complete and incomplete methods. Complete methods can in principle return a definite answer as to the whether the verification problem is satisfied, whereas incomplete methods may be unable to decide the one way or the other. Complete methods are based on exact MILP/SMT formulations [Bastani et al., 2016; Katz et al., 2017] and dedicated branch-and-bound procedures that tackle optimisation mappings of the problem [Bunel et al., 2018]. Incomplete methods rely on linear/semi-definite relaxations of the ReLU non-linearities [Wong and Kolter, 2018; Raghunathan et al., 2018] thereby displaying better scalability over complete ones. In the cases where the induced overapproximations do not allow for solutions to be given, network properties such as operational bounds computed by the methods can be used to strengthen the formulations used in complete verification [Botoeva et al., 2020].

Our efforts in the area included methods towards improving scalability in complete verification and techniques in the direction of strengthening precision in incomplete verification. Concerning complete verification, we have introduced the novel concept of ReLU dependencies whereby ReLU nodes are in a dependency relation if their operational states for a set of inputs is connected by logical implication. We have devised methods for the computation of these dependencies, which we have translated into MILP cuts, thereby improving the efficacy of MILP formulations of the verification problem [Botoeva et al., 2020]. Further improvements have been made possible via the exploitation of dependencybased branching heuristics in branch-and-bound procedures that we introduced [Kouvaros and Lomuscio, 2021].

Regarding incomplete verification, we have devised abstraction methods that strengthened the previously considered linear relaxations of the ReLU non-linearities. The methods accomplished this by additionally accounting for intralayer dependencies, instead of simply relying on local overapproximation areas, when choosing a relaxation. This enabled us to give proofs of adversarial robustness for computer vision models whose verification problem could not be previously resolved [Hashemi et al., 2021]. To a similar effect we have strengthened the semidefinite approximations of the ReLU functions through the construction of layer-wise relaxations and the incorporation of linear cuts into their formulation [Batten et al., 2021].

We have released the open-source neural network verification toolkit VENUS implementing these methods. In the span of four years, VENUS has progressed from analysing networks of few thousands of nodes to examining networks of millions of nodes. Among the latter are neural network-based systems in the aircraft domain developed by Boeing. These include object detection and landing assistance systems [Kouvaros et al., 2021], and semantic segmentation models for pose estimation [Kouvaros et al., 2023].

3.2 NMAS Verification

The scalability hurdle previously discussed is even more prevalent when analysing closed-loop systems with neural components such as NMAS. In particular, we have shown their verification problem to be undecidable for plain reachability properties [Akintunde et al., 2022].

In the light of this, we have isolated bounded fragments of computation tree logic and alternating-time logic, where formulae can be evaluated in a bounded number of execution steps. This enabled us to analyse properties concerning, for instance, whether the agents can bring about a state of affairs or reach a safe configuration within a bounded number of steps. We have shown that verification with respect to these fragments is in coNEXPTIME and solved the resulting verification problems via MILP formulations [Akintunde et al., 2020a; Akintunde et al., 2020b]. At the core of the formulations are adaptations of the neural network verification procedures earlier described which facilitate tight encodings of satisfaction checks for atomic formulae.

Finally, to further alleviate the difficulty of verification, we have developed compositional MILP encodings. Inspired by bounded model checking [Clarke et al., 2001], these can be used to check for the occurrence of bugs in parallel over the execution paths. Consequently, as we have experimentally shown, the encodings often enable the identification of bugs in shallow execution depths [Akintunde et al., 2020a].

4 Conclusions and FutureWork

As argued in the Introduction, with the development of autonomous agents and multi-agent systems in diverse applications, there is an urgent need to study principled methods for their verification before deployment. This paper gave an overview of some of the key methods that we put forward towards the verification of key classes of systems, including standalone neural networks, unbounded multi-agent systems, and neuro-symbolic multi-agent systems.

While significant progress has been made, scalability remains the main challenge to overcome in order to address the systems embedded in forthcoming applications such as autonomous vehicles. Formal reasoning for such systems needs to also account for specifications beyond the ones discussed in this paper, including robustness to semantic perturbations.

In future work we will focus on conquering the scalability of formal verification, extending the specification languages, and expanding the formal models to account for richer classes of systems, including unbounded systems of neuro-symbolic agents.

Acknowledgments

I am grateful to the Verification of Autonomous Systems Research Group, Imperial College London, for the mentoring and support in conducting the research presented in this paper. I acknowledge the financial support of the DARPA Assured Autonomy Programme (FA8750-18-C-0095), and the EPSRC Research Projects Trusted Autonomous Systems (EP/I00520X/1) and Secure AI Assistants (EP/T026731/1). Finally, I thank the IJCAI 2023 program committee for the invitation to deliver a spotlight talk in the Early Career Spotlight Track.