This research theme is an expansion of a previous one focusing on Large Language Models in mathematics and programming. This time, we want to expand the scope, to think more broadly about not only how language modelling can be applied, but also how insights from cognitive science can inspire and motivate new architectures and methodologies.
Research questions related to the theme include:
Formalisation and autoformalisation of mathematics: What are good foundations of mathematics? Formalisation and the use of proof assistants is becoming increasingly important in mathematics. Can Large Language Models (LLMs) and related techniques help to automatically assist in turning mathematical definitions and proofs into formal statements which can be checked for correctness by a proof assistant (a software system for interactively developing and checking mathematical proofs)?
Neuro-symbolic methods: How can neural (LLMs) and symbolic (proof assistants, automated theorem provers) work together to complement each other’s strengths? For instance, suggest and prove suitable lemmas or hints in a new theory development/formalisation effort.
Reinforcement Learning (RL) with feedback from provers: Related to the above, how can feedback from the proof assistant or automated theorem prover instruct a reinforcement learning loop to improve e.g. proof and/or lemmas construction?
Cognitive aspects: A central theme in recent RL is the use of intrinsic motivation which stems originally from cognitive science and psychological literature to describe how children learn. How can this concept be integrated in a AI system for mathematics? This concept is very relevant to how human mathematicians work. Even if a statement or conjecture has been formulated, the choice of key intermediate abstractions is not given a priori by the rules of the game of mathematics. AI methods can also help model human cognition, to for instance better understand how our number systems, underpinning all modern mathematics, have evolved and been shaped. This requires considering how collaboration between agents and/or humans shape communication.
