DSAI seminar with Moa Johansson

Abstract:

The task of automatically discovery mathematical conjectures (aka theory exploration) have historically been attempted by many symbolic AI systems, with some success. However, a neuro-symbolic architecture seems like an excellent fit for this task. We can assign the generative task to a neural system without much risk, even if a few non-theorems slip through, the results are checked afterwards using a symbolic theorem prover or counter-example finder. I will talk about a small, very initial case-study using recent LLMs (GPT-3.5/4 and Llama2) for discovering conjectures for the proof assistant Isabelle/HOL (which is quite popular among people liking formal proofs).
While results are mixed, we see potential in improving on the weaknesses of purely symbolic systems. A neuro-symbolic system can for instance, add some more variation in conjectures over purely symbolic systems while not missing obvious candidates. If there is time, I would also like to discuss the difficulties in reliably evaluate and experiment with LLMs, as we know little to nothing about their training – how big a problem is this and how should we approach it? With this in mind, how should one proceed in the construction of a neuro-symbolic theory exploration system? If anyone is interested in reading a bit more, here’s a link to our recent workshop paper: https://ceur-ws.org/Vol-3432/paper5.pdf


Bio: Moa Johansson works as Associate Professor (Docent) in the DSAI division. She has many research interests, including neuro-symbolic AI, automated reasoning and synthesis of program properties/mathematical conjectures, a bit of NLP, as well as some dabbling in data science for various sports. She has a BSc degree in AI and Computer Science from the University of Edinburgh, where she also did her PhD in automated reasoning. After a post-doc in Verona in Italy, Moa has worked at Chalmers since 2011, first in the Formal Methods group and since the beginning of this year in the DSAI division.