Siddhartha Gadgil, Professor, Department of Mathematics, IISc
– 26 February 2024
Talk summary: Recently, researchers at Google developed a system, AlphaGeometry, which can solve geometry problems from the International Mathematical Olympiad (IMO) at close to Gold Medal level. This was based on algorithmic (i.e., rule based) deduction together with a language model (Generative AI) to generate auxiliary constructions. To train the language model, ‘synthetic data’ was generated.
This work follows what are becoming common patterns for the use of artificial intelligence in mathematics, in particular using Generative AI to obtain useful candidates paired with deductive systems, including interactive theorem provers (ITPs), to check correctness, complete proofs, and evaluate results. Essentially, Generative AI is used for ‘intuitive’ aspects of reasoning and algorithms/symbolic AI/ITPs are used for the ‘logical’ aspects of reasoning.
In this talk, Siddhartha Gadgil began by discussing AlphaGeometry. He then discussed a few other systems for AI for mathematics, including ‘FunSearch’ which proved a result giving an improved bound for the so-called CapSet problem. He also discussed the design of possible systems for going beyond the present systems and experiments with GPT-4 showing its powers and its limitations relevant to this quest.
Speaker bio: Siddhartha Gadgil is a Professor of Mathematics at the Indian Institute of Science, Bengaluru. He has a PhD from California Institute of Technology and a BStat degree from the Indian Statistical Institute, Calcutta. Before joining IISc, he was a postdoctoral fellow at Stony Brook University and on the faculty of the Indian Statistical Institute, Bengaluru.
Siddhartha began his research career in topology and has worked for many years in this and related fields such as geometric group theory and Riemannian geometry. In recent years the main focus of his work has been automated theorem proving, i.e., mathematics generated by computers.
[Talk organised in collaboration with the Department of Computer Science and Automation]