Considerable work has been carried out in the past two decades on Verification of Multi-Agent Systems. Various methods based on binary-decision diagrams, bounded model checking, abstraction, symmetry reduction have been developed. Model checkers such as MCMAS and various extensions have been released to the community and applied to various areas including autonomous vehicles, services, robotics and beyond.
While this work has reached a level of maturity it is based on the assumption that agents can be entirely modelled symbolically, e.g. via a BDI rule system. This was entirely appropriate at the time. A new model of agents, however, is rapidly emerging in applications. In this model, agents are composed by a perception layer (vision, sound processing, etc.) which is realised via neural networks, combined with a decision making and planning layer realised via more traditional declarative methods. We call this emerging class of agents “neural-symbolic agents”.
This project concerns the development of methods and tools for the verification of neural agents composed as such. The starting point will be [1] where a neural-symbolic agent-based model is developed. Several possible objectives can be targetted, including:
* The development of efficient (ie scalable) methods for verifying neural-symbolic agent-based systems via novel compilations and data-structures,
* The development of a verification toolkit for the verification of neural-symbolic agents,
* The development of highly parallel approaches for the verification of neural-symbolic agents.
============
Requirements
Expertise with Logic, and Verification will be highly beneficial. Some knowledge of machine learning and optimisation is also advantageous.