Research Associate

Full time - 35 hours per week

Fixed term contract - temporary

The opportunity:

The project is fully funded by the AI for Math Fund from Renaissance Philanthropy and XTX Markets. Its central goal is the development of Sketchpad, an AI-powered system that enables users to navigate semi-formal proofs (i.e., formal sketches), with Lean and Isabelle serving as the formal backends.

The PDRA will be jointly supervised by Dr Wenda Li (AI for Mathematics) and Dr Mai Luo (ML Systems), and will collaborate with team members based at the School of Informatics, University of Edinburgh, and the University of Cambridge.

The role involves: 

1) Conducting cutting-edge research on the design of semi-formal proofs that effectively interface LLMs with proof assistants; 

2) Designing and implementing an RL/agentic framework to leverage multiple forms of feedback within a theorem-proving environment. This position includes funding for international travel to attend leading conferences.

This post is advertised as full-time (35 hours per week), however, we are open to considering part-time or flexible working patterns. We are also open to considering requests for hybrid working (on a non-contractual basis) that combines a mix of remote and regular on-campus working.

Please include the following documents in your application:

• CV
• 1-page cover letter
• A maximum of 3 scientific papers and a link to a codebase that illustrate the research quality of the candidate and their affinity with the research topic

Your skills and attributes for success: 

• A PhD or near completion in PL, Formal Verification, NLP, ML, or related areas of computer science / engineering / mathematics. 
• Track record of research excellence, evidenced by e.g. preprints / publication record.
• Experience in working with large formalisation project or implementation of foundation models / LLMs, evidenced by e.g. projects on Github. 
• Willingness to explore and adapt to new tasks (both LLM and AI4Math are new fields, and so much to learn from scratch).
• Good written and communication skills.

Advert information