Meta is seeking a PhD Student to join its Fundamental AI Research (FAIR) team in London. We are committed to advancing the field of artificial intelligence by making fundamental advances in scientific methods and technologies to help interact with and understand our world. For this position we are looking for an individual to work at the intersection of formal verification and machine learning. Our research interest include, for example, proof assistants (e.g., Lean), automatic code analysis (e.g., abstract interpretation), code synthesis, reinforcement learning, and large language models. The remit of the PhD will be to conduct research on a problem, or problems, in these areas which is beyond what current techniques can do. PhD positions are 4-year fixed-term for PhD students in London who will work in collaboration with the UCL Centre for Artificial Intelligence, jointly supervised by academics at this lab and research scientists at FAIR. In the spirit of FAIR’s general mission, we expect the work to come out of the PhD, both at Meta and the academic partner, to be open science and open source.