Fwd: Change in venue and time: {AI for Maths lecture} @ Faculty Hall: 26 February: 'AlphaGeometry and friends: AI for Mathematics'.

[Siddhartha Gadgil]

---------- Forwarded message ---------
From: Office KIAC <offic...@iisc.ac.in>
Date: Wed, 21 Feb 2024 at 11:52
Subject: Change in venue and time: {AI for Maths lecture} @ Faculty Hall: 26 February: 'AlphaGeometry and friends: AI for Mathematics'.
To: Math Seminar Mailing List <maths...@iisc.ac.in>
Cc: Siddhartha Gadgil <gad...@iisc.ac.in>

Dear All,

The Kotak IISc AI-ML Centre cordially invites you for a talk by Professor Siddhartha Gadgil on ‘AlphaGeometry and friends: AI for Mathematics’. Please find the details below.

Kotak IISc AI-ML talk: AlphaGeometry and friends: AI for Mathematics

Speaker: Siddhartha Gadgil, Professor, Department of Mathematics, Indian Institute of Science, Bengaluru.

Date: 26 February 2024

Time: 4:30 to 5:30 PM

Venue: Faculty Hall, IISc

Abstract:

Recently researchers at Google developed a system AlphaGeometry that 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, evaluate results, etc. 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, Professor Siddhartha Gadgil will begin by discussing AlphaGeometry. He will then discuss 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 will also discuss the design of possible systems for going beyond the present systems, and discuss 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.

https://math.iisc.ac.in/~gadgil/

All are welcome!

No knowledge of AI or machine learning will be assumed.

[Siddhartha Gadgil]

Thanks to the organizers, this will be live streamed: https://www.youtube.com/live/QufkZoo-Kns?si=XnlTj-3BQ4VkaL0-

regards,

Siddhartha

[Tarun Gupta]

Thanks for the very interesting and energetic talk! I learned a lot. 

Some preliminary thoughts:

In AlphaGeometry, there are 71 possible auxiliary constructions. It uses a deduction engine to verify the auxiliary constructions outputted by the language model. Hence, AlphaGeometry is essentially a chess engine for Euclidean geometry. There are 71 possible moves (auxiliary constructions) and rules for when those moves can be used (deduction engine). Similar to how chess engines are trained by playing "synthetic" chess games by themselves, AlphaGeometry learns by generating and solving "synthetic" problems by itself. As the search space is quite constrained, AlphaGeometry is able to achieve IMO gold-medalist performance, similar to how chess engines achieve super-human performance. So saying AlphaGeometry (or the language model used by it) has human-like-intuition has as much truth to it as saying chess engines has human-like-intuition. A similar argument holds for other models like FunSearch.

While using existing auxiliary constructions to prove something is certainly very useful and clever, what is even more suggestive of human-like-intuition is coming up with entirely new auxiliary constructions; something outside the system (e.g., something outside the list of 71 possible auxiliary constructions in AlphaGeometry). Some of the very seminal works in mathematics and logic have come from inventing new auxiliary constructions which no one ever thought of in their fields. For example, a "diagonalization" auxiliary construction, which no one had used before, was used by Georg Cantor to show that the (infinite) set of real numbers is larger than the (infinite) set of integers. A similar diagonalization construction was used by Gödel in his celebrated incompleteness theorem and also by Turing in his Halting problem proof. Hence, an interesting line of research could be on developing models that can conjecture new auxiliary constructions for a given system of mathematics, not just use existing ones in constrained search problems. The conjectures could be wrong; that's not the problem, as humans also conjecture things that are refuted all the time, but the important thing is humans can conjecture new things at all.

Thanks!

Tarun

[Siddhartha Gadgil]

Thanks.

One point I should make here: there is a difference between "human like intuition/creativity" and "all time great mathematician (of at least fields medal level) intuition/creativity". Sure, no AI system has come close to Godel/Poincare/Cantot/Gromov/Terry Tao. But almost no humans, not even professional mathematicians, come close to that.

Second, a logical point. It is true that AlphaGeometry used a restricted logic so there are things "outside the system" which AlphaGeometry could not come up with. But in principle a system could use first-order logic or something like Lean Prover, so there is nothing "outside the system". So claiming true creativity is outside the system no longer makes sense (strictly speaking they will be people in logic/foundations who may do so, but that is a small corner in mathematics).

best,

Siddhartha

--
You received this message because you are subscribed to the Google Groups "Automated Mathematics India" group.
To unsubscribe from this group and stop receiving emails from it, send an email to automated-mathemati...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/automated-mathematics-india/02e538d3-7fe9-43eb-ac1c-2b22a2b1d068n%40googlegroups.com.

[Tarun Gupta]

👍

Tarun Gupta reacted via Gmail

[Tarun Gupta]

>  But in principle a system could use first-order logic or something like Lean Prover, so there is nothing "outside the system". So claiming true creativity is outside the system no longer makes sense

Certainly, true creativity would reside within such a system. If the human brain (essentially a computer) can do creativity, then according to computational universality principle (setting aside memory constraints), computer programs can also achieve it. However, I am slightly skeptical that such a "computer program" would resemble an auto-regressive LLM conducting a beam search over millions of options. But who knows!

Thank you!

Tarun

[Siddhartha Gadgil]

To clarify, only one component of AlphaGeometry is an LLM conducting a beam search. The other is a deduction engine. Furthermore, the LLM is trained by the equivalent of solving a huge number of problems deductively and remembering interesting ideas.

On a larger scale, what one can hope is that LLMs can learn from mathematics and, when also presented relevant mathematics in the context, make plausible suggestions. Many of these plausible suggestions will be wrong, and many others useless. But a large enough fraction have to be useful to allow deduction based on these.

To view this discussion on the web visit https://groups.google.com/d/msgid/automated-mathematics-india/644e7881-2f8a-49c6-96fb-2e6f0937a70dn%40googlegroups.com.

[Tarun Gupta]

Thanks for the replies and clarifications.

> "To clarify, only one component of AlphaGeometry is an LLM conducting a beam search. The other is a deduction engine."

Yes, LLM + beam search + deduction engine. They essentially reduced Euclidean geometry problems to chess problems, which at first seemed quite bizarre and genius to me.

> "But in principle a system could use first-order logic or something like Lean Prover, so there is nothing "outside the system""

LLM + beam-search + deduction-engine for formal mathematics essentially offers a more clever and faster approach than simply checking through all possible strings in alphabetical order until one of them proves a theorem. In principle, AlphaGeometry could be replaced by "searching all possible strings." However, even then, a system using "first-order logic or Lean Prover" might not possess the capability for creativity or "thinking outside the system." Thanks to Gödel's incompleteness theorem, there isn't a fixed mechanical way for testing whether a mathematical theorem is true. An LLM trained on an axiomatic system cannot prove every statement within that axiomatic system; it requires something more (creativity or "thinking outside the system") to conjecture that a mathematical proposition is true even if it can't be proved (e.g., (A∧B)→A).

> On a larger scale, what one can hope is that LLMs can learn from mathematics and, when also presented relevant mathematics in the context, make plausible suggestions. Many of these plausible suggestions will be wrong, and many others useless. But a large enough fraction have to be useful to allow deduction based on these.

Certainly, I believe it will definitely assist in making plausible suggestions in mathematics. LLMs are already highly useful for software development. One can hope that LLMs can streamline the 99% perspiration phase, leaving humans to focus only on the 1% inspiration phase (EdisonQuoteRef, DeutschQuoteRef). However, I doubt LLMs can replace the 1% inspiration phase; that would require a better computer program to achieve.

Thanks,
Tarun

[Siddhartha Gadgil]

There are two separate issues.

* If the system is Lean or ZFC in First-order logic, then "thinking out of the system" is a tiny corner of mathematics and most mathematicians (even most fields medalists) do not so it. If an AI system cannot do this it says very little in practice.

* The 1% inspiration part is an empirical question: the only real proof that AI can generate new mathematics is generating new mathematics, which as of now has not happened. But I have been immersed among people doing mathematics (even guided them) and in my view this is much less magical than it may seem. A bunch of heuristics, analogical reasoning, deduction etc cover mathematics done by most mathematicians. 

To view this discussion on the web visit https://groups.google.com/d/msgid/automated-mathematics-india/a99aa356-3dca-4234-9c8f-08fa1e857c9en%40googlegroups.com.

[Tarun Gupta]

Certainly, I largely agree with both your points; "in practice" it doesn't matter much in current Generative AI field if it cannot (or can) go outside the system. "In principle", it makes a very interesting philosophical & scientific question for debate.

Thanks for your time and the detailed explanations!

Regards,

-Tarun