А вот и фото с той конференции подъехали. С панельной дискуссии, правда, не с моего доклада, но тут тоже есть хорошие. Первая так прямо очень тематично выглядит. Спасибо большое организаторам во главе с Елизаветой @lizik_t!
❤22🔥13❤🔥7🤡1
Лекции во вторник продолжили обучение с подкреплением, да и закончили его.
Сначала мы обсудили одну из главных тем RL: теорему о градиенте по стратегиям. Есть много преимуществ у того, чтобы параметризовать стратегию, а не функцию значений V или Q, но задача выглядит слишком сложной. И тем не менее в итоге через пару несложных трюков всё получается, и мы рассмотрели и исторически первый алгоритм REINFORCE (Williams, 1992), представляющий собой Монте-Карло версию policy gradient, и общую схему actor-critic алгоритмов, реализующих здесь TD-обучение.
А затем дошли до самых последних новостей: разработанных в OpenAI алгоритмов policy gradient с ограничениями TRPO (Schulman et al., 2015) и PPO (Schulman et al., 2017), который стал фактически стандартом индустрии и для RLHF (да, Джон Шульман был ещё в OpenAI тогда!), и для других современных приложений, а также алгоритм GRPO (Shao et al., 2024), который DeepSeek придумал, чтобы сократить потребление памяти. Любопытно, кстати, что GPRO - это в некотором смысле возвращение к истокам, actor-critic алгоритм, который отказывается от критика и моделирует его через сэмплирование, то есть в каком-то смысле возвращается к схеме Монте-Карло.
Во второй части лекций поговорили о планировании: и базовом сэмплировании опыта (Dyna, Dyna с приоритетами), и test-time планировании, в том числе rollouts и MCTS. А потом рассказал о громких результатах глубокого обучения с подкреплением, которые было уже несложно объяснить: AlphaGo, AlphaZero и MuZero. О моделях мира (world models) поговорить всерьёз не успел, но MuZero постарался объяснить, насколько это было возможно.
На этом RL мы заканчиваем, и у меня в кои-то веки есть возможность начать deep learning немного заранее, не с осени. Это давно уже хочется делать, потому что одного семестра тут категорически мало, и сэкономленные лекции, думаю, очень помогут.
https://www.youtube.com/watch?v=A5iXUKUv4-M
Сначала мы обсудили одну из главных тем RL: теорему о градиенте по стратегиям. Есть много преимуществ у того, чтобы параметризовать стратегию, а не функцию значений V или Q, но задача выглядит слишком сложной. И тем не менее в итоге через пару несложных трюков всё получается, и мы рассмотрели и исторически первый алгоритм REINFORCE (Williams, 1992), представляющий собой Монте-Карло версию policy gradient, и общую схему actor-critic алгоритмов, реализующих здесь TD-обучение.
А затем дошли до самых последних новостей: разработанных в OpenAI алгоритмов policy gradient с ограничениями TRPO (Schulman et al., 2015) и PPO (Schulman et al., 2017), который стал фактически стандартом индустрии и для RLHF (да, Джон Шульман был ещё в OpenAI тогда!), и для других современных приложений, а также алгоритм GRPO (Shao et al., 2024), который DeepSeek придумал, чтобы сократить потребление памяти. Любопытно, кстати, что GPRO - это в некотором смысле возвращение к истокам, actor-critic алгоритм, который отказывается от критика и моделирует его через сэмплирование, то есть в каком-то смысле возвращается к схеме Монте-Карло.
Во второй части лекций поговорили о планировании: и базовом сэмплировании опыта (Dyna, Dyna с приоритетами), и test-time планировании, в том числе rollouts и MCTS. А потом рассказал о громких результатах глубокого обучения с подкреплением, которые было уже несложно объяснить: AlphaGo, AlphaZero и MuZero. О моделях мира (world models) поговорить всерьёз не успел, но MuZero постарался объяснить, насколько это было возможно.
На этом RL мы заканчиваем, и у меня в кои-то веки есть возможность начать deep learning немного заранее, не с осени. Это давно уже хочется делать, потому что одного семестра тут категорически мало, и сэкономленные лекции, думаю, очень помогут.
https://www.youtube.com/watch?v=A5iXUKUv4-M
YouTube
СПбГУ -- 2025.04.22 -- Policy gradient и actor-critic алгоритмы, планирование, MCTS и Alpha[...]
Это лекция из курса "Графические вероятностные модели", который читается на Факультете математики и компьютерных наук СПбГУ вместе с двумя другими частями курса машинного обучения -- "Основами байесовского вывода" и "Глубоким обучением". Все материалы этой…
❤14👍12🔥4
Media is too big
VIEW IN TELEGRAM
Успел-таки с пятничным постом — вот так проходят в Jamschool собственно джемы, то бишь отчётные концерты. К последней пятнице месяца каждый ансамбль (они составляются практически случайно) должен новую песенку разучить и представить.
Играть там, как правило, особо нечего (да сложное я бы и не смог / не успел), но сам процесс игры вместе с другими людьми мне нравится и кажется крутым опытом. Когда-нибудь будет что выложить на этот счёт и поинтереснее, надеюсь.)
Играть там, как правило, особо нечего (да сложное я бы и не смог / не успел), но сам процесс игры вместе с другими людьми мне нравится и кажется крутым опытом. Когда-нибудь будет что выложить на этот счёт и поинтереснее, надеюсь.)
❤19🔥17👏4🤩4🎉2😍1😎1
У меня наконец-то получилось (возможно, ценой несколько более сумбурной части про RL) закончить второй семестр раньше срока и начать лекции о глубоком обучении. Каждый год становится всё больше разных интересных вещей, которые хочется в курсе по DL обсудить, и одного семестра уже давно категорически не хватает.
Сегодня были вводные лекции, поговорил расслабленно и неспешно об истории, о мотивации, о том, как искусственные нейронные сети вообще устроены, а потом уже более конкретно о функциях активации от пороговых до ACON-C, backpropagation, градиентном спуске, в том числе стохастическом, его свойствах и вариантах: методе моментов, моментах Нестерова и адаптивных вариантах от Adagrad до Adam и AdamW.
Если вдруг вы хотели как-то "вкатиться" в тему глубокого обучения, сейчас самое время подключаться! Как ни странно, глубокое обучение практически не требует знания и понимания всего предыдущего курса: конечно, вероятностную сторону вопроса понимать всегда полезно, а чем-то (например, тем же RL) мы будем в глубоком обучении пользоваться, но в целом deep learning — это практически независимый курс, мало что требующий на входе.
https://www.youtube.com/watch?v=FyWPGgzrNOs
Сегодня были вводные лекции, поговорил расслабленно и неспешно об истории, о мотивации, о том, как искусственные нейронные сети вообще устроены, а потом уже более конкретно о функциях активации от пороговых до ACON-C, backpropagation, градиентном спуске, в том числе стохастическом, его свойствах и вариантах: методе моментов, моментах Нестерова и адаптивных вариантах от Adagrad до Adam и AdamW.
Если вдруг вы хотели как-то "вкатиться" в тему глубокого обучения, сейчас самое время подключаться! Как ни странно, глубокое обучение практически не требует знания и понимания всего предыдущего курса: конечно, вероятностную сторону вопроса понимать всегда полезно, а чем-то (например, тем же RL) мы будем в глубоком обучении пользоваться, но в целом deep learning — это практически независимый курс, мало что требующий на входе.
https://www.youtube.com/watch?v=FyWPGgzrNOs
🔥43❤4
Уф, весенний семестр в СПбГУ закончился! Мне пришлось немного ускориться и делать в апреле по две встречи в неделю, но вот уже прошло пятнадцать раз по две лекции, и курс закончен:
https://logic.pdmi.ras.ru/~sergey/teaching/mlspsu2024.html
Теперь, правда, у меня начался ещё один преподавательский проект по вечерам, но что поделать, таков путь. Рад, что успел начать обсуждать глубокое обучение. Сегодня по моему стандартному плану мы сначала рассмотрели три глобальных сюжета: дропаут, инициализацию весов и batchnorm (и другие нормализации). Все сюжеты, как мне кажется, очень вдохновляющие: идеи очень простые, почти что лежащие на поверхности, и они показывают, как много было низко висящих плодов в глубоком обучении... да, честно говоря, и сейчас ещё наверняка много осталось.
А потом отступили от стандартного плана и поговорили о рекуррентных сетях. Начинать свёрточные было бы неправильно, потому что всё равно не успел бы ничего толком, там долгий разговор, перетекающий в компьютерное зрение, лекции на четыре минимум. А вот RNN вполне можно и за одну лекцию объяснить: идея, конструкция LSTM, какие-то ещё идеи вроде GRU, да и всё. В этом плане RNN, конечно, удивительная тема: конструкцию, созданную Хохрайтером и Шмидхубером в 1997, а в окончательном виде в 2000 году, так и не смогли толком улучшить.
GRU (gated recurrent units; Cho et al., 2014) были очень популярны в обработке естественных языков в середине 2010-х, я там был и помню, но... почему-то современные "классические" RNN (т.е. не recurrent Transformers, не Mamba и т.п.) куда чаще возвращаются к тому самому LSTM. И автоматический поиск архитектур рекуррентных ячеек, который делали исследователи из Google под руководством Ильи Суцкевера (Jozefowicz et al, 2015), тоже ничего не дал. В свёрточных сетях он дал EfficientNet (Tan et al., 2019), который стал стандартом индустрии на годы. А в рекуррентных никто потом нигде получившиеся конструкции не видел. Что-то в LSTM есть особенное; если знаете, что именно (может, исследования какие), расскажите.)
https://www.youtube.com/watch?v=1sDzhWuCSY0
https://logic.pdmi.ras.ru/~sergey/teaching/mlspsu2024.html
Теперь, правда, у меня начался ещё один преподавательский проект по вечерам, но что поделать, таков путь. Рад, что успел начать обсуждать глубокое обучение. Сегодня по моему стандартному плану мы сначала рассмотрели три глобальных сюжета: дропаут, инициализацию весов и batchnorm (и другие нормализации). Все сюжеты, как мне кажется, очень вдохновляющие: идеи очень простые, почти что лежащие на поверхности, и они показывают, как много было низко висящих плодов в глубоком обучении... да, честно говоря, и сейчас ещё наверняка много осталось.
А потом отступили от стандартного плана и поговорили о рекуррентных сетях. Начинать свёрточные было бы неправильно, потому что всё равно не успел бы ничего толком, там долгий разговор, перетекающий в компьютерное зрение, лекции на четыре минимум. А вот RNN вполне можно и за одну лекцию объяснить: идея, конструкция LSTM, какие-то ещё идеи вроде GRU, да и всё. В этом плане RNN, конечно, удивительная тема: конструкцию, созданную Хохрайтером и Шмидхубером в 1997, а в окончательном виде в 2000 году, так и не смогли толком улучшить.
GRU (gated recurrent units; Cho et al., 2014) были очень популярны в обработке естественных языков в середине 2010-х, я там был и помню, но... почему-то современные "классические" RNN (т.е. не recurrent Transformers, не Mamba и т.п.) куда чаще возвращаются к тому самому LSTM. И автоматический поиск архитектур рекуррентных ячеек, который делали исследователи из Google под руководством Ильи Суцкевера (Jozefowicz et al, 2015), тоже ничего не дал. В свёрточных сетях он дал EfficientNet (Tan et al., 2019), который стал стандартом индустрии на годы. А в рекуррентных никто потом нигде получившиеся конструкции не видел. Что-то в LSTM есть особенное; если знаете, что именно (может, исследования какие), расскажите.)
https://www.youtube.com/watch?v=1sDzhWuCSY0
👍26❤10🔥8👌2🖕1
Уже больше недели назад я делал доклад на заседании Санкт-Петербургского математического общества, и вот наконец-то выкладываю. Доклад, соответственно, тематический:
AI и математика: что модели могут сейчас и куда мы идём
Математика в целом как область применения AI и компьютерных наук в целом всегда оставалась для меня загадкой: казалось бы, это самая формализованная часть человеческой деятельности. С тех самых пор, как появились компьютеры, появились и системы автоматического логического вывода (theorem provers), на первой лекции любого курса всегда рассказываю о том, что AI в некотором смысле начался с Logic Theorist Аллена Ньюэлла и Герберта Саймона. Сам Саймон, кстати, в стиле AI-оптимизма пятидесятых годов говорил об этом так: "Over Christmas, Al Newell and I invented a thinking machine... [We] invented a computer program capable of thinking non-numerically, and thereby solved the venerable mind-body problem, explaining how a system composed of matter can have the properties of mind".
И всё-таки буквально до сих пор почти ничего по-настоящему нового не получилось! Громких теорем, доказанных полностью автоматически, всё ещё нет; максимум, который я знаю – гипотеза Роббинса про булевы алгебры, которая ну очень уж близка к аксиомам. И вот кажется, что успех понемногу приходит с неожиданной стороны: не от автоматических пруверов, а от больших языковых моделей (LLM), которые как раз о формальных выводах никакого специального понятия не имеют.
Доклад был для матобщества, поэтому в детали ML я не углублялся, а наоборот, хотел дать широкую картинку того, где сейчас фронтир математических способностей AI-моделей и как быстро он движется. План такой:
– Введение, таймлайны и революции AI, трансформеры и LLM
– История AI в математике: пруверы и перебор случаев
– RL для математики: AlphaTensor, AlphaProof, гипотеза Эндрюса-Кёртиса
– LLM в математике до 2024: ToRA, FunSearch, NuminaMath
– Рассуждающие модели: от CoT к o1 и R1
– Что там на фронтире: MATH, FrontierMATH, HLE, Deep Research и обзоры, критика
– А когда original research: Google Co-Scientist, AI Scientist-v2, шкала креативности
Есть ещё связанный с этим предмет для любопытного поста, но, видимо, потом выложу. Вообще я не очень понимаю, как лучше — постить подряд всё что есть или стараться распределять, чтобы не было долгих перерывов в канале. Пока склоняюсь ко второму, но рад буду услышать мнения.
AI и математика: что модели могут сейчас и куда мы идём
Математика в целом как область применения AI и компьютерных наук в целом всегда оставалась для меня загадкой: казалось бы, это самая формализованная часть человеческой деятельности. С тех самых пор, как появились компьютеры, появились и системы автоматического логического вывода (theorem provers), на первой лекции любого курса всегда рассказываю о том, что AI в некотором смысле начался с Logic Theorist Аллена Ньюэлла и Герберта Саймона. Сам Саймон, кстати, в стиле AI-оптимизма пятидесятых годов говорил об этом так: "Over Christmas, Al Newell and I invented a thinking machine... [We] invented a computer program capable of thinking non-numerically, and thereby solved the venerable mind-body problem, explaining how a system composed of matter can have the properties of mind".
И всё-таки буквально до сих пор почти ничего по-настоящему нового не получилось! Громких теорем, доказанных полностью автоматически, всё ещё нет; максимум, который я знаю – гипотеза Роббинса про булевы алгебры, которая ну очень уж близка к аксиомам. И вот кажется, что успех понемногу приходит с неожиданной стороны: не от автоматических пруверов, а от больших языковых моделей (LLM), которые как раз о формальных выводах никакого специального понятия не имеют.
Доклад был для матобщества, поэтому в детали ML я не углублялся, а наоборот, хотел дать широкую картинку того, где сейчас фронтир математических способностей AI-моделей и как быстро он движется. План такой:
– Введение, таймлайны и революции AI, трансформеры и LLM
– История AI в математике: пруверы и перебор случаев
– RL для математики: AlphaTensor, AlphaProof, гипотеза Эндрюса-Кёртиса
– LLM в математике до 2024: ToRA, FunSearch, NuminaMath
– Рассуждающие модели: от CoT к o1 и R1
– Что там на фронтире: MATH, FrontierMATH, HLE, Deep Research и обзоры, критика
– А когда original research: Google Co-Scientist, AI Scientist-v2, шкала креативности
Есть ещё связанный с этим предмет для любопытного поста, но, видимо, потом выложу. Вообще я не очень понимаю, как лучше — постить подряд всё что есть или стараться распределять, чтобы не было долгих перерывов в канале. Пока склоняюсь ко второму, но рад буду услышать мнения.
YouTube
СПбМО -- 2025.04.22 -- AI в математике
Это запись доклада "AI и математика: что модели могут сейчас и куда мы идём" на заседании Санкт-Петербургского математического общества 22 апреля 2025 года.
Подписывайтесь на мой телеграм-канал "Sineкура":
https://t.iss.one/sinecor
Слайды доклада размещены на…
Подписывайтесь на мой телеграм-канал "Sineкура":
https://t.iss.one/sinecor
Слайды доклада размещены на…
👍27❤🔥6❤4⚡3
Пятничный пост сегодня большой, но про ровно одну игру:
The Talos Principle 2
Когда-то давным-давно я играл в The Talos Principle, и хотя обзоров не сохранилось, помню, что мне понравилось. Это игра про 3D-головоломки, похожая на Portal, но с немного другими механиками и с крутой интересной историей; если вы в неё не играли, очень рекомендую начать с неё, потому что про вторую часть без спойлеров о первой не поговоришь. Говорят, скоро ещё и ремейк сделают.
Talos Principle заканчивается тем, что всемогущий Elohim (да, кое-что тут весьма in your face) снабжает вас — AI-модель, чьё сознание проходило тестирование пазлами, — реальным физическим телом и отправляет во внешний мир. Да-да, это была пазл-игра про трансгуманистический AI: люди вымерли в результате какого-то катаклизма, но успели создать Elohim'а, который делает AI-модели, тестирует их и ищет ту самую, которую можно будет выпускать в мир создавать новое общество. В Talos Principle 2 вы — свежесделанный робот 1K (то есть №1000), которым выполняется "The Goal" легендарной основательницы Нового Иерусалима по имени Афина: достичь населения города в тысячу разумных роботов. Но оказывается, что на карте есть остров, где никто из нас-роботов не был, и теперь его надо исследовать.
Это значит, что тут теперь есть город с персонажами, с которыми можно поговорить, и с вами в экспедицию они тоже отправляются. NPC, кстати, очень живые, с характерами и забавными деталями; например, главная экзистенциальная угроза электросети города — это кот Якута (видимо, этого Якута, все роботы названы в честь разных великих людей), который очень любит всё грызть и везде писать. Есть город, есть политика, разные взгляды на жизнь этого общества, на связь нового AI-общества с погибшим человеческим, на философские взгляды человечества. Это очень круто сделано, и по всей игре пахнет LessWrong: роботы цитируют Честертона, философствуют в своей социальной сети, обсуждают падение человечества и заходят в моральную философию немного глубже, чем может заехать в шахту обычная вагонетка.
Что особенно интересно, игра не просто вываливает на вас философию, а постоянно спрашивает ваше мнение, и насколько я понял, от ваших ответов реально будет зависеть развитие сюжета и концовки (но не пазлы, конечно). В общем, это игра "с философией", которая при этом совершенно не вызывает кринжа, как большинство попыток других игр. Забавный факт: игра рассказывает про древнегреческого философа Стратона из Стагира, который собственно придумал "принцип Талоса", обильно его цитирует... и я совершенно не поставил это всё под сомнение, потом уже из обзоров узнал, что никакого Стратона не существовало (кстати, вот блог о нём, видимо, от разработчиков игры).
Пазлы, кстати, отличные. Первую часть я плохо помню, но кажется, что там был небольшой дисконнект: там были или "обычные" пазлы, которые вообще не требовали усилий, или "секретные" пазлы, которые я в основном не представлял как проходить без гайдов, иногда даже неясно было, как догадаться об их существовании. Здесь кривая сложности сделана отлично: ты идёшь дальше, раз в два-три пазла может быть нужно реально подумать (а за золотыми воротами так и почти каждый раз), но при этом ты нигде не застреваешь вплоть до самого конца. Правда, я не всё в игре собрал, возможно, там есть ещё целая коллекция секретных пазлов запредельной сложности, кто знает.
А, да, и ещё очень красиво. Огромные отлично продуманные сооружения, хорошая графика; разве что иногда бегать слишком много приходится из-за того самого гигантского масштаба. В общем, как вы уже поняли, я остался в восторге. Правда, не знаю, рекомендую ли я вам The Talos Principle 2 прямо сейчас — не исключено, что есть смысл дождаться ремейка первой части и сначала пройти её... Ой, подождите, тут прогресс как в AI-индустрии: пока я играл во вторую часть, The Talos Principle: Reawakened уже вышел! Начинать точно лучше с него хотя бы по сюжетным соображениям — но потом и вторую часть не забудьте, она гораздо больше и лучше первой.
The Talos Principle 2
Когда-то давным-давно я играл в The Talos Principle, и хотя обзоров не сохранилось, помню, что мне понравилось. Это игра про 3D-головоломки, похожая на Portal, но с немного другими механиками и с крутой интересной историей; если вы в неё не играли, очень рекомендую начать с неё, потому что про вторую часть без спойлеров о первой не поговоришь. Говорят, скоро ещё и ремейк сделают.
Talos Principle заканчивается тем, что всемогущий Elohim (да, кое-что тут весьма in your face) снабжает вас — AI-модель, чьё сознание проходило тестирование пазлами, — реальным физическим телом и отправляет во внешний мир. Да-да, это была пазл-игра про трансгуманистический AI: люди вымерли в результате какого-то катаклизма, но успели создать Elohim'а, который делает AI-модели, тестирует их и ищет ту самую, которую можно будет выпускать в мир создавать новое общество. В Talos Principle 2 вы — свежесделанный робот 1K (то есть №1000), которым выполняется "The Goal" легендарной основательницы Нового Иерусалима по имени Афина: достичь населения города в тысячу разумных роботов. Но оказывается, что на карте есть остров, где никто из нас-роботов не был, и теперь его надо исследовать.
Это значит, что тут теперь есть город с персонажами, с которыми можно поговорить, и с вами в экспедицию они тоже отправляются. NPC, кстати, очень живые, с характерами и забавными деталями; например, главная экзистенциальная угроза электросети города — это кот Якута (видимо, этого Якута, все роботы названы в честь разных великих людей), который очень любит всё грызть и везде писать. Есть город, есть политика, разные взгляды на жизнь этого общества, на связь нового AI-общества с погибшим человеческим, на философские взгляды человечества. Это очень круто сделано, и по всей игре пахнет LessWrong: роботы цитируют Честертона, философствуют в своей социальной сети, обсуждают падение человечества и заходят в моральную философию немного глубже, чем может заехать в шахту обычная вагонетка.
Что особенно интересно, игра не просто вываливает на вас философию, а постоянно спрашивает ваше мнение, и насколько я понял, от ваших ответов реально будет зависеть развитие сюжета и концовки (но не пазлы, конечно). В общем, это игра "с философией", которая при этом совершенно не вызывает кринжа, как большинство попыток других игр. Забавный факт: игра рассказывает про древнегреческого философа Стратона из Стагира, который собственно придумал "принцип Талоса", обильно его цитирует... и я совершенно не поставил это всё под сомнение, потом уже из обзоров узнал, что никакого Стратона не существовало (кстати, вот блог о нём, видимо, от разработчиков игры).
Пазлы, кстати, отличные. Первую часть я плохо помню, но кажется, что там был небольшой дисконнект: там были или "обычные" пазлы, которые вообще не требовали усилий, или "секретные" пазлы, которые я в основном не представлял как проходить без гайдов, иногда даже неясно было, как догадаться об их существовании. Здесь кривая сложности сделана отлично: ты идёшь дальше, раз в два-три пазла может быть нужно реально подумать (а за золотыми воротами так и почти каждый раз), но при этом ты нигде не застреваешь вплоть до самого конца. Правда, я не всё в игре собрал, возможно, там есть ещё целая коллекция секретных пазлов запредельной сложности, кто знает.
А, да, и ещё очень красиво. Огромные отлично продуманные сооружения, хорошая графика; разве что иногда бегать слишком много приходится из-за того самого гигантского масштаба. В общем, как вы уже поняли, я остался в восторге. Правда, не знаю, рекомендую ли я вам The Talos Principle 2 прямо сейчас — не исключено, что есть смысл дождаться ремейка первой части и сначала пройти её... Ой, подождите, тут прогресс как в AI-индустрии: пока я играл во вторую часть, The Talos Principle: Reawakened уже вышел! Начинать точно лучше с него хотя бы по сюжетным соображениям — но потом и вторую часть не забудьте, она гораздо больше и лучше первой.
❤18🔥7👍4
Сегодня — иллюстрация к AI для математики, на которую я намекал в посте про доклад. В последние полгода-год я иногда проводил простой эксперимент про способности моделей к математике: брал свежую статью с архива, которой точно не могло быть ни в какой обучающей выборке, отрезал ту часть, где доказательства, прикладывал вводную часть с постановкой задачи и просил эту задачу решить. Ничего разумного не получалось.
Но в последнее время я всё больше проникаюсь моделью o3 от OpenAI, мне кажется, она реально умнее и реально лучше отвечает на сложные запросы, чем предыдущие модели. Так что для математики я o3, конечно, тоже попробовал — и, кажется, понемногу начинает работать!
Расшаривать чаты с приложениями OpenAI до сих пор не даёт, так что я собрал наш диалог в tex-документ и выложил его:
o3 Proving a Combinatorial Identity
Делал я это 1 мая, взял, как всегда, сегодняшнюю статью с архива: "Combinatorial Identities Using the Matrix Tree Theorem". Статью взял комбинаторную про формулки, чтобы сам мог проверить результат, отрезал первые шесть страниц для контекста и сначала попросил число uprooted spanning trees посчитать, как в формуле (4.2); я прилагаю скриншот для привлечения внимания, но, конечно, удобнее будет pdf посмотреть по ссылке.
С формулой (4.2) o3 легко справилась, но это широко известный результат, о чём мне сама o3 тут же и рассказала. Поэтому мы начали двигаться дальше, к доказательству формулы (4.1), которая в статье заявлена как new identity. o3 думала почти одиннадцать минут (!) и выдала два доказательства. Proof B — это, насколько я смог понять, буквально то же доказательство счётом разных деревьев, как в статье приводится, и оно по сути правильное (можете проверить детали, я не стал).
А вот в чисто алгебраической proof A, несмотря на её простоту, я ничего не понял — когда я так говорю студенту на экзамене, это значит, что скорее всего студент в чём-то ошибается. Там был один очевидно неверный переход и один выглядящий очень сомнительно, так что я попросил саму o3 разобраться повнимательнее и переписать поподробнее. И действительно, разобралась, переписала, и в новом доказательстве я уже никаких ошибок не нашёл.
Да, конечно, это очень простая теорема для нового математического результата, и в доказательстве нет ничего особенно умного (это больше говорит, впрочем, не об LLM, а обо мне — серьёзную теорему я бы вряд ли смог легко проверить). Но дело начинает выглядеть так, как будто работа с LLM уже сейчас похожа на типичный цикл работы профессионального математика с (не самым умным пока что) аспирантом, только итерация переписывания доказательства занимает не неделю, а десять минут.
А теперь панчлайн — я в своих докладах часто рассказываю, что модели от Google очень хороши, но об этом мало кто знает, потому что у Google плохо с маркетингом. В частности, Gemini 2.5 Pro — это, пожалуй, лучшая LLM для содержательных околонаучных рассуждений прямо сейчас, в том числе для математических. И в этот раз всё это тоже блестяще подтвердилось: я сходил с тем же запросом к Gemini 2.5 Pro, и она спокойно и гораздо быстрее (точное время там не записано, но гораздо меньше десяти минут, скорее 1-2 минуты) получила то же самое прямое доказательство, сразу правильное.
И ссылку Google сделать разрешил, так что вот она:
Gemini 2.5 Pro Proving the Same Identity Much Faster
Да, и ещё замечание: заранее я этого знать не мог, но неожиданно эксперимент получился совсем чистым. Теоретически современная LLM может сходить на архив и дочитать статью до конца, но в данном случае и o3, и Gemini 2.5 выдали другое доказательство, не то, которое было в статье — так что оно уж наверняка новое.
Но в последнее время я всё больше проникаюсь моделью o3 от OpenAI, мне кажется, она реально умнее и реально лучше отвечает на сложные запросы, чем предыдущие модели. Так что для математики я o3, конечно, тоже попробовал — и, кажется, понемногу начинает работать!
Расшаривать чаты с приложениями OpenAI до сих пор не даёт, так что я собрал наш диалог в tex-документ и выложил его:
o3 Proving a Combinatorial Identity
Делал я это 1 мая, взял, как всегда, сегодняшнюю статью с архива: "Combinatorial Identities Using the Matrix Tree Theorem". Статью взял комбинаторную про формулки, чтобы сам мог проверить результат, отрезал первые шесть страниц для контекста и сначала попросил число uprooted spanning trees посчитать, как в формуле (4.2); я прилагаю скриншот для привлечения внимания, но, конечно, удобнее будет pdf посмотреть по ссылке.
С формулой (4.2) o3 легко справилась, но это широко известный результат, о чём мне сама o3 тут же и рассказала. Поэтому мы начали двигаться дальше, к доказательству формулы (4.1), которая в статье заявлена как new identity. o3 думала почти одиннадцать минут (!) и выдала два доказательства. Proof B — это, насколько я смог понять, буквально то же доказательство счётом разных деревьев, как в статье приводится, и оно по сути правильное (можете проверить детали, я не стал).
А вот в чисто алгебраической proof A, несмотря на её простоту, я ничего не понял — когда я так говорю студенту на экзамене, это значит, что скорее всего студент в чём-то ошибается. Там был один очевидно неверный переход и один выглядящий очень сомнительно, так что я попросил саму o3 разобраться повнимательнее и переписать поподробнее. И действительно, разобралась, переписала, и в новом доказательстве я уже никаких ошибок не нашёл.
Да, конечно, это очень простая теорема для нового математического результата, и в доказательстве нет ничего особенно умного (это больше говорит, впрочем, не об LLM, а обо мне — серьёзную теорему я бы вряд ли смог легко проверить). Но дело начинает выглядеть так, как будто работа с LLM уже сейчас похожа на типичный цикл работы профессионального математика с (не самым умным пока что) аспирантом, только итерация переписывания доказательства занимает не неделю, а десять минут.
А теперь панчлайн — я в своих докладах часто рассказываю, что модели от Google очень хороши, но об этом мало кто знает, потому что у Google плохо с маркетингом. В частности, Gemini 2.5 Pro — это, пожалуй, лучшая LLM для содержательных околонаучных рассуждений прямо сейчас, в том числе для математических. И в этот раз всё это тоже блестяще подтвердилось: я сходил с тем же запросом к Gemini 2.5 Pro, и она спокойно и гораздо быстрее (точное время там не записано, но гораздо меньше десяти минут, скорее 1-2 минуты) получила то же самое прямое доказательство, сразу правильное.
И ссылку Google сделать разрешил, так что вот она:
Gemini 2.5 Pro Proving the Same Identity Much Faster
Да, и ещё замечание: заранее я этого знать не мог, но неожиданно эксперимент получился совсем чистым. Теоретически современная LLM может сходить на архив и дочитать статью до конца, но в данном случае и o3, и Gemini 2.5 выдали другое доказательство, не то, которое было в статье — так что оно уж наверняка новое.
❤24🔥15❤🔥7👍7🤯1
В комменты к предыдущему посту ворвался Фёдор Петров @fedyapetrov, мой коллега с ФМКН СПбГУ, который не просто очень крутой математик, но ещё и работал над FrontierMath, тем самым датасетом, из которого ведущие модели пока очень мало решают задачек (а когда решают, иногда потом оказывается, что дело тёмное).
Фёдор сразу заметил, что тождество получилось совсем простое, по сути на геометрические прогрессии, и предложил другое похожее тождество (см. картинку), которое будет требовать именно рассуждений о графах. На этот раз я знал, где подстелить соломки, и записал промпт в TeX'е, так что могу расшарить доказательства от обеих моделей по ссылке:
Gemini 2.5 Pro (150 секунд)
OpenAI o3 (8 минут 46 секунд)
pdf-файл с обоими доказательствами (чуть менее читабельно)
Фёдор проверил доказательства: "Gemini верно, o3 нет, но легко исправить (он два раза ошибается в два раза, поэтому в итоге всё типа сходится)".
Так что и с более сложной задачкой мы опять пришли к тому же результату: модели соображают всё лучше, а Gemini 2.5 Pro сейчас лучшая LLM для таких вещей. DeepSeek-Prover я тут не считаю, потому что он специально сделан и дообучен для общения с Lean, но поэкспериментировать с ним тоже было бы интересно.
Фёдор сразу заметил, что тождество получилось совсем простое, по сути на геометрические прогрессии, и предложил другое похожее тождество (см. картинку), которое будет требовать именно рассуждений о графах. На этот раз я знал, где подстелить соломки, и записал промпт в TeX'е, так что могу расшарить доказательства от обеих моделей по ссылке:
Gemini 2.5 Pro (150 секунд)
OpenAI o3 (8 минут 46 секунд)
pdf-файл с обоими доказательствами (чуть менее читабельно)
Фёдор проверил доказательства: "Gemini верно, o3 нет, но легко исправить (он два раза ошибается в два раза, поэтому в итоге всё типа сходится)".
Так что и с более сложной задачкой мы опять пришли к тому же результату: модели соображают всё лучше, а Gemini 2.5 Pro сейчас лучшая LLM для таких вещей. DeepSeek-Prover я тут не считаю, потому что он специально сделан и дообучен для общения с Lean, но поэкспериментировать с ним тоже было бы интересно.
👍26🔥14❤6🤔2
Это, конечно, типичный пятничный пост, но нет, не дотерплю, лучше вы меня потерпите. На днях я сел почитать книжку (восклицательный знак — это бывает со мной, увы, очень редко) и встал через два часа, дочитав до конца (два восклицательных знака — такого со мной не было, пожалуй, много лет). Книжкой была "Табия тридцать два" Алексея Конакова.
Сеттинг книги — антиутопия (если не постапокалипсис) о незавидном будущем России, которая оказывается вынуждена перепридумывать (переучреждать, как говорят в книге) себя и свою культуру. Причины этого спойлерить не буду, но главный поворот Переучреждения состоял в том, что вместо признанной вредной классической литературы культуру России решили основать на шахматах — здесь и воистину великие традиции, и масса положительных сторон для развития молодёжи, и Аркадия Дворковича можно привлечь. И теперь на площади Искусств в Петербурге стоит памятник Ботвиннику, а в Камергерском переулке возле МХТ в Москве — шахматному композитору Виталию Чеховеру.
Речь героев и вся книга пронизаны шахматными аллюзиями: герои впустую теряют темпы, бюрократия движется медленно, как шатрандж, в читальном зале библиотеки герой находит местечко в углу, в уютном фианкетто; ну а секс с любимой девушкой — это просто два восклицательных знака. Если бы в книге не было больше ничего, кроме аллюзий, я бы уже получил массу удовольствия — но есть и вполне захватывающий сюжет. Я бы определил жанр как раз как "интеллектуальный детектив": хотя никаких преступлений не раскрывается, в книге идёт детективная охота за важными идеями, и за ней действительно интересно следить.
Кстати, обязательно читать всем петербуржцам и сочувствующим! Питерская топография в шахматном мире поворачивается причудливо, но узнаваемо; можете, например, догадаться, где именно подряд идут улицы Раузерская, Макагоновская, Вересовская, Полугаевская, Суэтинская и Бронштейновская. Особенно мило выходит, когда поменять достаточно только угол зрения: станция метро "Спасская" в честь чемпиона мира, Камская улица Васильевского острова (у меня там занятия в СПбГУ были! больше двадцати лет назад) в честь Гаты Камского... Я смеялся в голос, когда очень в тему оказалась вплетена идущая к Волковскому кладбищу улица Салова — в книге, конечно, Валерия Борисовича.
В общем, как вы уже поняли, очень рекомендую, десять из десяти, два восклицательных знака, не пропускайте.
Сеттинг книги — антиутопия (если не постапокалипсис) о незавидном будущем России, которая оказывается вынуждена перепридумывать (переучреждать, как говорят в книге) себя и свою культуру. Причины этого спойлерить не буду, но главный поворот Переучреждения состоял в том, что вместо признанной вредной классической литературы культуру России решили основать на шахматах — здесь и воистину великие традиции, и масса положительных сторон для развития молодёжи, и Аркадия Дворковича можно привлечь. И теперь на площади Искусств в Петербурге стоит памятник Ботвиннику, а в Камергерском переулке возле МХТ в Москве — шахматному композитору Виталию Чеховеру.
Речь героев и вся книга пронизаны шахматными аллюзиями: герои впустую теряют темпы, бюрократия движется медленно, как шатрандж, в читальном зале библиотеки герой находит местечко в углу, в уютном фианкетто; ну а секс с любимой девушкой — это просто два восклицательных знака. Если бы в книге не было больше ничего, кроме аллюзий, я бы уже получил массу удовольствия — но есть и вполне захватывающий сюжет. Я бы определил жанр как раз как "интеллектуальный детектив": хотя никаких преступлений не раскрывается, в книге идёт детективная охота за важными идеями, и за ней действительно интересно следить.
Кстати, обязательно читать всем петербуржцам и сочувствующим! Питерская топография в шахматном мире поворачивается причудливо, но узнаваемо; можете, например, догадаться, где именно подряд идут улицы Раузерская, Макагоновская, Вересовская, Полугаевская, Суэтинская и Бронштейновская. Особенно мило выходит, когда поменять достаточно только угол зрения: станция метро "Спасская" в честь чемпиона мира, Камская улица Васильевского острова (у меня там занятия в СПбГУ были! больше двадцати лет назад) в честь Гаты Камского... Я смеялся в голос, когда очень в тему оказалась вплетена идущая к Волковскому кладбищу улица Салова — в книге, конечно, Валерия Борисовича.
В общем, как вы уже поняли, очень рекомендую, десять из десяти, два восклицательных знака, не пропускайте.
❤22🔥11👍7