29 sept: AI in math meeing
Alexander Shen
At 29 september we DON'T have Kolmogorov seminar meeting. But at 18 European time / 19 Moscow time (30 min later that usual seminar time) Yury Kudryashov will give a talk "What is Lean and how does it help LLMs solve mathematics?" Yury works for Harmonic, one of the companies that managed to "solve" (in some sense) 5 out of 6 problems of International Math Olympiad this year using their LLM and other tools. Here is the announcement Yury sent me.
------- In the past few years, LLMs went from generating text that only look reasonable to generating correct solutions to IMO problems and, in some cases, research problems. On the other hand, in many cases LLMs still prefer to hallucinate rather than admit failure. How one can trust LLM-produced proofs? One of the answers to this question is to make an LLM produce a proof that can be formally verified by a computer. In my talk, I will discuss the following questions: - What is Lean? How do definitions, theorem statements, and proofs look like? - How does it help LLMs solve math problems? - What other tools can an LLM use? - Can an LLM learn a new skill based on a limited amount of information?
-------
A free discussion is planned after the talk, so please think about your questions/requests for comments (including examples/demonstrations/WTF experiences etc.)
-------
Another request:
The possible application of AI in math are obviously a hot topic. The Mathematical Intelligencer is trying to collect people's observations about their personal experiences (the quotes may be published); just a few lines about these questions (some of them) would be great.
Questions:
1) What was yours most impressive ``success story'' of using AI, LLM and related tools for mathematics research/teaching?
2) What was yours most disappointing experience of this kind?
3) What would you expect to happen, say, 5 years from now in this regard?
Please send your answers to me (sasha...@gmail.com), I will forward them to M.I.
Alexander Shen
29 september, 19.00 MSK, 18:00 Paris, Zoom: https://u-bordeaux-fr.zoom.us/j/88402787361?pwd=WktCdEhBT3pXN0pLUGg4Z3RuMlpsQT09
--
Вы получили это сообщение, поскольку подписаны на группу "Kolmogorov seminar on complexity".
Чтобы отменить подписку на эту группу и больше не получать от нее сообщения, отправьте письмо на электронный адрес kolmogorov-seminar-on-...@googlegroups.com.
Чтобы посмотреть обсуждение, перейдите по ссылке https://groups.google.com/d/msgid/kolmogorov-seminar-on-complexity/8e5142cc-34b8-40dc-8bc5-29126a75a2c0%40lirmm.fr.
Alexander Shen
Reminder and some questions to think about before the talk
Few years ago we heard that LLM are advanced token predictors: the dialog stream is split into tokens and then the "most probable" next token is predicted (not just using good old statistical counting but some more advanced "machine learning" tools). Obviously what we see now goes far beyond that, and something impossible happens. But what is under the hood? More specific questions: - Are there separate stages in preparing the answer? (ChatGPT even produces some reasonably looking names for these stages) What happens during this stages? - How the search tools are involved in preparing the answer? - How the engine interacts with other programs like programming language interpreters, formal provers etc.? - What is preserved during the dialog and between the dialogs? - What amount of information needs to be learned to get some new "skill"? For example, can it learn ancient Greek or some other language where we have only a limited amount of texts in the language like people do (studying grammar textbooks, making graded exercises etc.)? Is is possible to learn some new mathematical theory just by reading the only textbook on this theory (and may be having some dialogs with experts)? - Is the technology more or less known to all the players (companies -- from Yandex to OpenAI) and the difference is just the resources and few years of development, or there are some "key secrets"? Related question: these companies hire key people for millions, presumably those people have some much needed knowledge/abilities. What are those abilities and where they come from? - Linguistic and logic seem to be in big trouble (even if they don't see it now like this): it turns out that the ``rigid'' structures like grammars and formal theories they tried to discover and develop are not something fundamental but appear from the sea of fuzzy parameters in quite mechanical (though probably not understood) way, and what looked like syntactical sugar and user-friendly interface could be much more fundamental It seems that the prover of choice is Lean - Lean and Coq are much more similar to each other than to traditional formal theories. What is the formal relation with standard theories - why large cardinals? What does it mean philosophically? May be Cantor just lead us in some non-optimal direction? Why the mathematics look the same in these theories to such an extent that people do not care? -In general, what are the current frontiers between what is easy / difficult / very difficult and expensive / hardly possible / out of reach? What is now possible locally (on a reasonable desktop) in terms of education/reeducation/dialog? And so on. After some initial talk we will have a question/answer session, so feel free to come with your questions, examples of behavior that looks strange, stories of success/failure for comments. We may also try live experiments (when we together try something)... Still if there will be a lot of people, we would have to restrict interactivity...
Чтобы посмотреть обсуждение, перейдите по ссылке https://groups.google.com/d/msgid/kolmogorov-seminar-on-complexity/381ca85d-0c26-4f8b-a51e-68f3fa3a68ed%40lirmm.fr.