Autonomous robotics are desirable in hazardous environments such as nuclear decommissioning and space exploration. But before we can deploy autonomous robots, we need a fundamental change to the way that these autonomous systems are specified, verified and assessed. This change includes support for specification and verification of new and advanced forms of Artificial Intelligence (AI) that will be used to drive autonomous decision-making in critical robotic systems. AI can be broadly segregated into two approaches: Symbolic AI (knowledge-driven, e.g. rule-based systems, logical deduction) and Sub-Symbolic AI (data-driven, e.g. neural networks, machine learning, generative AI). Just using one variety can lead to significant problems. For example, while Sub-Symbolic AI is both fast and flexible, it is very poor when it comes to transparency and explainability. Consequently, at least in robots operating in safety-critical or mission-critical areas, Symbolic AI is often used for the key, decision-making components. Though slower, these components can be verified and can explain exactly why they chose to do something, and what they aim to do next and why. The combination of these into the Neuro-Symbolic (NeSy) AI paradigm seeks to merge the best of both worlds [1,4], ideally enabling verifiable, transparent, and efficient autonomous systems [2,3].
Methodology: In this project, we first identify the different combinations of Symbolic and Sub-Symbolic AI for Neuro-Symbolic reasoning that are relevant for fully autonomous robotic systems to be deployed in critical scenarios. We then provide a systematic analysis and a formal approach to extract the requirements of these systems and transform them into Neuro-Symbolic Reasoning specification patterns. Domain-specific contracts are then derived from the specification patterns, which are then verified using a suitable approach for that type of contract. This project will focus on the following research questions and objectives:
RQ1: What are useful degrees of NeSy AI in autonomous robotic systems that are deployed in critical domains?
RQ2: What kinds of properties do we want/need to verify of robotic systems using NeSy AI components?
Answering these research questions leads us to the following objectives:
O1: Develop taxonomies of NeSy designs (e.g., neural-dominant with symbolic checks, symbolic-first with neural augmentation) and document which combinations are most effective for robotics. This will involve analysing the trade-offs between different NeSy combinations (e.g., safety vs. efficiency, interpretability vs. speed).
O2: Define reusable specification patterns that encode safety constraints. Encode these as templates in the Formal Requirements Elicitation Tool (FRET). This may involve a tool extension to FRET.
O3: Design and demonstrate (via example use cases) a verification strategy for each NeSy specification pattern.
O4: Develop prototype tool support for the verification strategies. This will use FRET as a base tool.
Outcomes: (1) A catalogue of combinations of NeSy AI in robotic systems. (2) A set of reusable specification patterns for NeSy AI in robotics. (3) Tool-supported specification and verification strategies by extending the Formal Requirements Elicitation Tool (FRET), and an associated collection of verified NeSy AI robotic components. (4) A series of high-quality publications at suitable top-tier venues including conferences (PMLR, AAAI, ICSE, TACAS, FM, ICRA) and journals (TSE, TOSEM, RAS). (5) Through collaboration on exemplar NeSy AI combinations and case studies, we will strengthen existing collaborations with NASA, Amentum, Satellite Applications Catapult, and Airbus. We will explore new collaborations with SLB, Renault, and Space Solar. This will help the student with networking, internships (if desired) and future career planning.
Eligibility
Applicants should have, or expect to achieve, at least a 2.1 honours degree or a master’s (or international equivalent) in a relevant science or engineering related discipline.
Before you apply
We strongly recommend that you contact the supervisors for this project before you apply. Please include details of your current level of study, academic background and any relevant experience and include a paragraph about your motivation to study this PhD project.
How to apply
Apply online through our website: https://uom.link/pgr-apply-2425
When applying, you’ll need to specify the full name of this project, the name of your supervisor, if you already having funding or if you wish to be considered for available funding through the university, details of your previous study, and names and contact details of two referees.
Your application will not be processed without all of the required documents submitted at the time of application, and we cannot accept responsibility for late or missed deadlines. Incomplete applications will not be considered.
After you have applied you will be asked to upload the following supporting documents:
If you have any questions about making an application, please contact our admissions team by emailing FSE.doctoralacademy.admissions@manchester.ac.uk.
Equality, diversity and inclusion is fundamental to the success of The University of Manchester, and is at the heart of all of our activities. We know that diversity strengthens our research community, leading to enhanced research creativity, productivity and quality, and societal and economic impact.
We actively encourage applicants from diverse career paths and backgrounds and from all sections of the community, regardless of age, disability, ethnicity, gender, gender expression, sexual orientation and transgender status.
We also support applications from those returning from a career break or other roles. We consider offering flexible study arrangements (including part-time: 50%, 60% or 80%, depending on the project/funder).
uom_cs_artificial_intelligence uom_cs_theory_foundations