Аннотация:
Математика как область применения AI и компьютерных наук в целом
всегда оставалась для меня загадкой: самая формализованная часть
человеческой деятельности, тем не менее, неизменно оказывалась очень
сложной для автоматизации. Громких теорем, доказанных полностью
автоматически, всё ещё нет, но кажется, что успех понемногу приходит с
неожиданной стороны: не от автоматических пруверов, а от больших
языковых моделей (LLM). В докладе мы обсудим текущее положение дел с
математическими рассуждениями у LLM, увидим, какой скачок произошёл с
появлением рассуждающих моделей и, возможно, немного помечтаем о
будущем...
