Workshop, Large Language Models for Mathematics and Programming

Today, large language models are used in a range of areas. In this workshop we will focus on their use in mathematics and programming. In particular, LLMs can augment proof assistants, helping users to go from mathematics described informally in English to representations that can be checked by the proof assistant (autoformalisation).

Proofs in proof assistants resemble programs, so generating proof-scripts is not too dissimilar from program synthesis, which is also a topic of this workshop. Here, we might not only want to synthesise programs in a given language, but perhaps even augment the language with new constructs, abstractions and functions.  
 
As this is quite a recent direction of research, we have an exciting lineup of young researchers presenting their work in these areas.

Schedule

9.00 - 9.10 Intro and Welcome
9.10 - 9.50: Emily First - Machine Learning for Theorem Proving Using Trial-And-Error
9.50 - 10.30: Gabriel Poesia - Learning Formal Mathematics From Intrinsic Motivation

10.30 - 11.00 Coffe break

11.00 - 11.40: Atharva Sehgal - Neurosymbolic Programming for Scientific Discovery
11.40 - 12.20: Theo X Olausson - TBC

12.20 -13.20: Lunch

13.20 - 14.00: Siddhartha Gadgil - Autoformalization and Friends: Interactive Theorem Provers and Artificial Intelligence
14.00 - 14.40: Wenda Li - Autoformalisation: Bridging the Gap between Informal and Formal Proofs

14.40 - 15.10: Coffe break

15.10 - 15.50: Alex Gu - TBC

.