Пятничный пост сегодня большой, но про ровно одну игру:

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 уже вышел! Начинать точно лучше с него хотя бы по сюжетным соображениям — но потом и вторую часть не забудьте, она гораздо больше и лучше первой.

Сегодня — иллюстрация к 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 выдали другое доказательство, не то, которое было в статье — так что оно уж наверняка новое.

Это, конечно, типичный пятничный пост, но нет, не дотерплю, лучше вы меня потерпите. На днях я сел почитать книжку (восклицательный знак — это бывает со мной, увы, очень редко) и встал через два часа, дочитав до конца (два восклицательных знака — такого со мной не было, пожалуй, много лет). Книжкой была "Табия тридцать два" Алексея Конакова.

Сеттинг книги — антиутопия (если не постапокалипсис) о незавидном будущем России, которая оказывается вынуждена перепридумывать (переучреждать, как говорят в книге) себя и свою культуру. Причины этого спойлерить не буду, но главный поворот Переучреждения состоял в том, что вместо признанной вредной классической литературы культуру России решили основать на шахматах — здесь и воистину великие традиции, и масса положительных сторон для развития молодёжи, и Аркадия Дворковича можно привлечь. И теперь на площади Искусств в Петербурге стоит памятник Ботвиннику, а в Камергерском переулке возле МХТ в Москве — шахматному композитору Виталию Чеховеру.

Речь героев и вся книга пронизаны шахматными аллюзиями: герои впустую теряют темпы, бюрократия движется медленно, как шатрандж, в читальном зале библиотеки герой находит местечко в углу, в уютном фианкетто; ну а секс с любимой девушкой — это просто два восклицательных знака. Если бы в книге не было больше ничего, кроме аллюзий, я бы уже получил массу удовольствия — но есть и вполне захватывающий сюжет. Я бы определил жанр как раз как "интеллектуальный детектив": хотя никаких преступлений не раскрывается, в книге идёт детективная охота за важными идеями, и за ней действительно интересно следить.

Кстати, обязательно читать всем петербуржцам и сочувствующим! Питерская топография в шахматном мире поворачивается причудливо, но узнаваемо; можете, например, догадаться, где именно подряд идут улицы Раузерская, Макагоновская, Вересовская, Полугаевская, Суэтинская и Бронштейновская. Особенно мило выходит, когда поменять достаточно только угол зрения: станция метро "Спасская" в честь чемпиона мира, Камская улица Васильевского острова (у меня там занятия в СПбГУ были! больше двадцати лет назад) в честь Гаты Камского... Я смеялся в голос, когда очень в тему оказалась вплетена идущая к Волковскому кладбищу улица Салова — в книге, конечно, Валерия Борисовича.

В общем, как вы уже поняли, очень рекомендую, десять из десяти, два восклицательных знака, не пропускайте.

Сегодня целый день записывал видеокурс для Центра искусственного интеллекта СПбГУ — по-взрослому, в студии, с настоящим светом, гримом, редакторами и так далее.

Изначально мы договорились, что у меня будет три так называемых модуля. Когда я их уже распланировал, выяснилось, что модуль — это не полноценная полуторачасовая лекция, а скорее один час суммарного видео. Такого я стерпеть не мог, поэтому слегка поругался и выбил себе право записывать модули на полтора часа.

В итоге за сегодня, примерно с 9 до 18, три модуля и записали. Первый где-то на два часа, второй тоже, а третий на два с половиной.) Конечно, монтаж их чуток ужмёт, но на самом деле не сильно. И вообще процесс был отлично организован и шёл очень гладко, что-то перезаписывать приходилось в единичных случаях.

Большое спасибо организаторам и исполнителям, это было круто!