I'm interested in neuro-symbolic AI: the combination between neural networks and symbolic methods from logic and programming. The research of my group covers a wide range of applications ranging from language models for analyzing natural language for social science research, to formal methods and AI for mathematics and reasoning, and cognitive modeling.
How do you know that a mathematical proof is correct? And how do we find a nice elegant proof in the first place? Can computers help us with this? Solving mathematical problems was in fact one of the tasks adressed by the earliest AI systems developed already in the 1950’s. In this talk I will give a brief history of computer mathematics and how it connects to the development of early functional programming languages like Standard ML. I will also talk about some of my current research in how we can get computers to act creatively in the domain of mathematics; not only reason about given facts, as historically has been the case, but also invent and prove new interesting facts. To achieve this, we use tools like Haskell’s QuickCheck to allow our system, Hipster, to explore and test its way towards promising conjectures.
Slides