Abstract: In this talk, we explore the transformative potential of custom reinforcement learning (RL) algorithms in accelerating solutions to complex, research-level mathematical challenges. We begin by illustrating how these algorithms have achieved a 10X improvement in areas where previous advances of the same magnitude required many decades. A comparative analysis of different network architectures is presented to highlight their performance in this context. We then delve into the application of RL algorithms to exceptionally demanding tasks, such as those posed by the Millennium Prize problems and the smooth Poincaré conjecture in four dimensions. Drawing on our experiences, we discuss the prerequisites for developing new RL algorithms and architectures that are tailored to these high-level challenges. This talk is largely based on recent work with A.Shehper, A.Medina-Mardones, L.Fagan, B.Lewandowski, A.Gruen, Y.Qiu, P.Kucharski, and Z.Wang.

Bio: After receiving his PhD from Princeton University, Sergei Gukov spent five years at Harvard University as a research fellow of the Clay Mathematics Institute and two years at the school of mathematics at the Institute for Advanced Studies. His passion is building new bridges between different areas of mathematical physics and pure mathematics, such as quantum topology, mirror symmetry, and gauge theory. His more recent interests involve new connections between mathematics and machine learning.

The Generative AI Laboratory (GAIL) at the University of Edinburgh is a centre for excellence dedicated to researching all aspects of generative artificial intelligence (AI) in society. Uniting the diverse research expertise across the University with generative AI at its core, GAIL taps into a thriving AI landscape with recognised strengths in natural language processing, machine learning, and data-driven innovation.

This interdisciplinary initiative focuses on advancing generative AI techniques in the key areas of future health and care, climate and sustainability, and economic growth, and is committed to innovating in generative AI through partnerships with global stakeholders, driving new collaborations and dynamic projects across government, industry, and the public sector.

To learn more about GAIL, see here: https://gail.ed.ac.uk/

Abstract: AI for Mathematics (AI4Math) is not only intriguing intellectually but also crucial for AI-driven discovery in science, engineering, and beyond. In the recent past, there have been many efforts on AI4Math that mirror techniques in NLP, in particular, by training large language models on textual math datasets. As a complementary yet less explored avenue, formal mathematical reasoning is grounded in formal systems such as proof assistants, which can verify the correctness of reasoning and provide automatic feedback. In this talk, we advocate for formal mathematical reasoning as a task for LLMs and argue that it is indispensable for advancing AI4Math to the next level. In recent years, we have seen steady progress in using AI to perform formal reasoning, including core tasks such as theorem proving and autoformalization, as well as emerging applications such as verifiable generation of code and hardware designs. However, significant challenges remain to be solved for AI to truly master mathematics and achieve broader impact. We summarize existing progress, discuss open challenges, and envision critical milestones to measure future success. We end by calling on the research community to come together to drive transformative advancements in this field.

Bio: Swarat Chaudhuri is a Professor of Computer Science and the director of the Trishul laboratory at UT Austin, as well as a Visiting Researcher at Google Deepmind, London. His research lies at the interface of machine learning, programming languages, and formal methods. Through a synthesis of ideas from these areas, he seeks to develop a new generation of intelligent systems that are reliable, transparent, and secure by construction and can solve mathematical reasoning, scientific discovery, and system engineering tasks beyond the scope of contemporary AI. Dr. Chaudhuri has received the NSF CAREER award, the ACM SIGPLAN John Reynolds Dissertation award, Meta and Google Research awards, and several ACM SIGPLAN and SIGSOFT distinguished paper awards. He also served as a Program Chair for CAV 2016 and ICLR 2024.

Further Venue details: https://museum.rcsed.ac.uk/

Prior registration for the dinner is essential.

To learn more about Euro Proof Net, its events and working groups, see here: https://europroofnet.github.io/

This panel session will provide an opportunity for community building, and free-format discussion of the current trends in the area, as well as its future directions.

Panel members:

•  Swarat Chaudhuri (UT Austin and Google Deepmind)
•  Sergei Gukov (Caltech & Dublin Inst. Adv. Studies)
•  Josef Urban (CIIRC/CVUT)
• Andrew Gordon (Cogna and University of Edinburgh)
• Wenda Li (Edinburgh University) 

Possible drinks and meal at Mariott Hotel: https://www.marriott.com/en-us/hotels/edihw-courtyard-edinburgh-west/overview/?scid=f2ae0541-1279-4f24-b197-a979c79310b0