Professor Promotion Lectures: Moa Johansson and Philipp Leitner

Moa Johansson: Neuro-symbolic AI

In this talk I will introduce the field of neuro-symbolic AI which combines traditional symbolic methods from programming, logic and reasoning with modern day neural networks. 

This combination is powerful and is already making headlines in the AI for mathematics domain, for example achieving gold-medal performances in the International Mathematics Olympiad and solving Erdós problems. Here, a LLM is typically generating suggestions for proofs or proof-steps and a proof-assistant, a symbolic system for checking mathematical proofs, is used to ensure there aren’t any faulty or hallucinated steps. However, the neural part is often heavily reliant on very large language models and enormous amounts of compute. Can more sophisticated combinations of neural and symbolic methods improve on this? In particular, can such systems help us conjecture interesting and useful lemmas in the formal language of the proof assistant? 

I will also talk about other domains where the combination of neural and symbolic methods will have an impact in the future, ranging from formal methods for software verification, AI for natural science and engineering as well as cognitive science and linguistics. 

Philipp Leitner: Performance Optimization at the Intersection of Software and Systems

Performance (e.g., execution time efficiency) is an unique non-functional property of software, in that it inherently depends on the interplay of three dimensions: software (code), systems (infrastructure and platforms), and usage (workloads). We can rarely assess the efficiency of a program or software system without taking into account where it is going to run, or how it will be used.

My research in the last decade or so has circled around bridging the gap between these three dimensions. I will exemplify this based on two research threads from my past: augmenting source code with runtime performance data [ICSE'19], and software microbenchmarking [FSE'20, TSE'23].

In the second half of my talk, I will turn towards agentic coding and show how the same gap needs to be bridged yet again. I will illustrate how generative AI struggles with producing efficient code, exactly because it reasons about code in isolation, blind to the systems it runs on and the workloads it serves. Bringing in runtime data can, yet again, serve as a way forward for future agentic coding platforms.