Panagiotis Kouvaros awarded prestigious IJCAI Early Career Spotlight Award

Panagiotis Kouvaros, a Research Associate in the SAIL (formerly VAS) Group, has been awarded an Early Career Spotlight Award to be presented at the 32nd International Joint Conference on Artificial Intelligence (IJCAI 2023). This award is highly prestigious: Early career researchers in AI are first nominated and the program committee then makes a selection among the nominees. People selected need to have an outstanding track record in AI. There is a special track, called “Early Career Spotlight Track” at the conference where the awardees present their work and a report detailing the work of each awardee is published in the conference proceedings:

P. Kouvaros. Towards Formal Verification of Neuro-symbolic Multi-agent Systems. Proceedings of the 32nd International Joint Conference on Artificial Intelligence (IJCAI2023). Macao, S.A.R.

Panagiotis explained the details of his work and the main contributions that he made during a short interview:

What are your main contributions and what do you think was the most important paper that you contributed?

My main contributions in safe AI have been twofold.

Firstly, we pioneered formal verification methods for unbounded multi-agent systems, i.e. multi-agent systems that are composed of an arbitrary number of homogeneous agents, as in robot swarms, multi-party negotiation protocols and auctions. The methods that we put forward enabled for the first time the verification of properties of unbounded multi-agent systems irrespective of the number of agents composing the systems. In doing so the methods bypassed the state space explosion problem of traditional verification whereby only systems with very few constituents can be analysed. The most important paper in the area that I contributed is “Parameterised Verification for Multi-agents” (AIJ) which first introduced said methods.

Secondly, we introduced novel methods for improving the efficiency of neural network verification. These methods are based on the concept of ReLU dependencies whereby ReLU nodes are in a dependency relation if their operational states for a set of inputs are 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. Further improvements have been made possible via the exploitation of dependency-based branching heuristics in branch-and-bound procedures that we introduced. The most important paper in this area that I contributed is “Efficient verification of neural networks via dependency analysis” (AAAI 20) which first introduced the notion of dependencies.

Exciting! Is this also used as part of any practical applications in industry?

To enable the analysis of industrial models, we have developed the neural network verifier Venus, which in the span of four years progressed from analysing networks of a few thousands of nodes to examining networks of millions of nodes. Venus has been used to analyse several models with the industry, including models developed with Audi and Boeing. All analyses were drawn with respect to robustness to input perturbations pertaining to white noise and photometric adjustments. The model we analysed with Audi concerned a variant of VGG16 that forms a key component of the Multi-View 3D Detector, a high-accuracy 3D object detection network for autonomous driving. The models trained by Boeing concerned neural network-based systems in the aircraft domain, including object detection and landing assistance systems, and semantic segmentation models for pose estimation. A common finding in the analyses is the potential brittleness of the models with respect to minor, imperceptible perturbations of the inputs. These may pose significant safety risks during operation, thus strengthening the need for the principled analysis of AI before deployment.

Relevant publications with Audi and Boeing