Research Associate

Applications are invited for a Research Associate post to carry out research on Large Language Models (LLMs) for Lattice-theoretic Reasoning of Reactive Programs. The position is funded for up to 18 months.

The project aims to leverage Artificial Intelligence (AI) techniques for mathematical reasoning by developing a novel approach to proving refinement propositions using a combination of LLMs and state-of-the-art theorem provers. Developments in this area have the potential to advance software verification, with expected practical impact across a wide range of applications such as in the engineering of mobile and autonomous robots.

You will work on the synthesis of novel refinement propositions and proofs obtained via state-of-the-art theorem provers and model-checkers. There will be a need to develop novel synthesis algorithms that can scale. There will be a need to fine-tune foundational models using the produced datasets and to evaluate their performance on benchmark problems. Novel reasoning techniques integrating LLMs and state-of-the-art provers will be developed, and there will be a need to formally justify their soundness. You will liaise with academics in the project and participate in the writing of papers.

You will have the opportunity to further extend and develop your knowledge of formal methods, software engineering, and artificial intelligence whilst within the role.

Skills, Experience & Qualification needed:

You will have a PhD in formal methods, and experience on modelling and proof of algebraic refinement propositions using CSP, and their mechanisation in FDR. Experience with use of theorem proving using Isabelle, and usage of Large Language Models (LLMs), including fine-tuning, is highly desirable. You will have experience with an object-oriented and or functional programming language.

Interview date: To be confirmed

For informal enquiries: please contact Dr Pedro Ribeiro on pedro.ribeiro@york.ac.uk

The University strives to be diverse and inclusive – a place where we can ALL be ourselves. We particularly encourage applications from people who identify as Black, Asian or from a Minority Ethnic background, who are underrepresented at the University. We offer family friendly, flexible working arrangements, with forums and inclusive facilities to support our staff.