£6,000 FindAPhD Scholarship | APPLICATIONS CLOSING SOON! £6,000 FindAPhD Scholarship | APPLICATIONS CLOSING SOON!

PhD studentship in Formal Methods for Safe Artificial Intelligence


   School of Computer Science

This project is no longer listed on FindAPhD.com and may not be available.

Click here to search FindAPhD.com for PhD studentship opportunities
  Dr Mirco Giacobbe  No more applications being accepted  Funded PhD Project (Students Worldwide)

About the Project

The School of Computer Science at the University of Birmingham offers one PhD position in formal methods for safe artificial intelligence.

Safe artificial intelligence addresses the problem of automatically ensuring that learning systems satisfy correctness specifications. For deep learning systems which are based on neural networks, computer-aided formal verification is crucial; this is because (1) they often are not human interpretable, (2) they change behaviour continuously and automatically, and (3) they are being increasingly applied to safety critical domains. Exemplars are robotics and autonomous driving contexts, where deep learning systems are being embedded in decision-making components. Verifying the correctness of these systems is an open and important problem in artificial intelligence, highly relevant to industry and academia.

Computer-aided verification of deep learning systems connects formal methods, machine learning and software engineering, and builds upon symbolic verification methods such as model checking, abstract interpretation, and satisfiability modulo theories as well as novel machine learning methods for safe AI. The candidate will contribute to open problems in the area. Specific research questions include, but are not limited to, ensuring that dynamical systems controlled by neural networks are safe over infinite time [1], or ensuring that these neural networks are safe under quantisation [2]. Moreover, research at the intersection of verification and machine learning not only explores symbolic methods for the analysis of learning systems, but also investigates cutting-edge machine learning techniques for effective formal verification. Instances in this domain include machine learning for termination analysis of computer programs and stability analysis of dynamical systems [3].

Overall, the project aims at developing verification, synthesis, and machine learning methods that ensure that digital, physical, probabilistic systems interacting with deep learning and neural network are formally guaranteed to be safe.

The candidate will study and work in a stimulating environment within the school and the university and will have the opportunity to research theoretical and/or experimental aspects of formal verification of learning systems, investigate connections between theoretical computer science (e.g., logic, automata) and machine learning, and explore applications to science and engineering (e.g., control, robotics). The project spans over theory and practice of computer science and requires both

- analytical skills (strong background in models of computation, math, logics, and algorithms designin) and

- programming skills (knowledge of verification and machine learning toolchains, ability to develop software prototypes).

In short, the candidate should have a strong interest for both maths and code.

Eligibility: First or Upper Second Class Honours undergraduate degree and/or postgraduate degree with Distinction (or an international equivalent). We also consider applicants from diverse backgrounds that have provided them with equally rich relevant experience and knowledge. Full-time and part-time study modes are available. If your first language is not English and you have not studied in an English-speaking country, you will have to provide an English language qualification.

We want our PhD student cohorts to reflect our diverse society. UoB is therefore committed to widening the diversity of our PhD student cohorts. UoB studentships are open to all and we particularly welcome applications from under-represented groups, including, but not limited to BAME, disabled and neuro-diverse candidates. We also welcome applications for part-time study.


Funding Notes

The position offered is for three and a half years full-time study. The value of the award is stipend; £15,609 pa; tuition fee: £4,500. Awards are usually incremented on 1 October each year.

References

[1] E. Bacci, M. Giacobbe, D. Parker. Verifying Reinforcement Learning up to Infinity, IJCAI 2021
[2] M. Giacobbe, T. Henzinger, M. Lechner. How Many Bits Does it Take to Quantize Your Neural Network?, TACAS 2020
[3] A. Abate, D. Ahmed, M. Giacobbe, A. Peruffo. Formal Synthesis of Lyapunov Neural Networks, IEEE L-CSS 2021

How good is research at University of Birmingham in Computer Science and Informatics?


Research output data provided by the Research Excellence Framework (REF)

Click here to see the results for all UK universities
Search Suggestions
Search suggestions

Based on your current searches we recommend the following search filters.

PhD saved successfully
View saved PhDs