The goal of this project is to develop new methods for assisting mathematical discovery, by leveraging recent developments in generative AI (large language models) with symbolic systems (here proof-assistants) via a neuro-symbolic architecture. This takes advantage of AI systems with different strengths: generative AI-systems provide creativity, but are potentially unreliable and may hallucinate, while classical symbolic methods are rigid but reliable and can robustly check the correctness of results. Project description Generative AI, with tools like ChatGPT, driven by Large Language Models (LLMs), have in the past year demonstrated impressive capabilities in generation of not only fluent text but also computer code. They take instructions in natural language and can perform seemingly creative tasks very well. However, LLMs can be unreliable: a well-known issue is hallucinations where seemingly sensible but incorrect answers are produced, and their reasoning capabilities are fragile. Research mathematicians are increasingly staring to use computers to assist in their research, not least in cases where proofs turn out to be so large that it is impossible to check each step manually (a amous example is Thomas Hales' proof of Kepler's conjecture). Proof-assistants are software designed for exactly this: keeping track of precise definitions and checking each step of the proof. However, using a proof assistant requires both expertise in how to program them, and libraries of foundational mathematics to already be in place. We believe that LLMs has the potential to speed up this process and even provide creative suggestions to working mathematicians. But not on their own: Proof assistants have the complementary capabilities missing for this to work. The goal of this proposal is therefore to bring LLMs and proof assistants together via a neuro-symbolic architechture. Information about the division and the department The PhD student will be supervised by Moa Johansson in the Data Science and AI division, and co-supervised Thierry Coquand in the Type Theory group in the Computing Science division. Johansson's group focuses on neuro-symbolic AI in domains ranging from natural language to cognitive science and mathematics, while the group of Coquand is famous for work in type theory and the development of the proof assistant Agda. This project is funded by WASP (https://wasp-sweden.org), and the student will be part of the WASP graduate school which offers excellent courses, study trips and networking opportunities with researchers working in AI across Sweden and abroad. Major responsibilities We are looking for a PhD student with an interest in neuro-symbolic AI (machine learning and symbolic methods) to work as a researcher on this project, which will include both implementation work and experimentation. It is an advantage to have some experience of functional programming, in addition to experience with machine learning. The PhD position is funded for five years, of which 80% is research and 20% is teaching. Read more about doctoral studies at Chalmers here. Qualifications The candidate should have (or shortly be about to finish) a MSc degree in e.g. Computer Science, AI, mathematics or other relevant fields. To qualify as a PhD student, you must have a master's level degree corresponding to at least 240 higher education credits in a relevant field. The position requires sound verbal and written communication skills in English. If Swedish is not your native language, Chalmers offers Swedish courses. Contract terms Full-time temporary employment. The position is limited to a maximum of five years. We offer Chalmers offers a cultivating and inspiring working environment in the coastal city of Gothenburg.  Read more about working at Chalmers and our benefits for employees. Chalmers aims to actively improve our gender balance. We work broadly with equality projects, for example the GENIE Initiative on gender equality for excellence. Equality and diversity are substantial foundations in all activities at Chalmers. Application procedure The application should be marked with reference number 20240250 and written in English. The application should be sent electronically and be attached as PDF-files, as below. Maximum size for each file is 40 MB. Please note that the system does not support Zip files. CV: (Please name the document: CV, Family name, reference number) • CV • Other, for example previous employments or leadership qualifications and positions of trust. • Two references that we can contact. Personal letter: (Please name the document as: Personal letter, Family name, ref.number) 1-3 pages where you: • Introduce yourself • Describe your previous experience of relevance for the position (e.g. education, thesis work and, if applicable, any other research activities) • Describe your future goals and future research focus Other documents: • Copies of bachelor and/or master’s thesis. • Attested copies and transcripts of completed education, grades and other certificates, e.g. TOEFL test results. Use the button at the foot of the page to reach the application form.  Please note: The applicant is responsible for ensuring that the application is complete. Incomplete applications and applications sent by email will not be considered. Application deadline: 2024-05-31 For questions, please contact: Associate Professor Moa Johansson [email protected]