В октябре 2025 у Дарио Амодеи вышел текст “Machines of Loving Grace“, о позитивной стороне развития AI. И вот его новое эссе "The Adolescence of Technology" посвящено тому, как развитие AI может оказаться опасным.
Сегодня разбираю этот текст, с чем-то не соглашаюсь, но в основном спорить, конечно, не с чем. Пост по ссылке, здесь краткие выжимки:
Переходный возраст машин любви и благодати
AI Safety и роль Anthropic
Здесь Амодеи заслуженно горд достижениями Anthropic; эту область действительно в основном Anthropic и двигает в последнее время. [...]
Правы ли AI-думеры?
Амодеи проходится по классическим "думерским" аргументам вроде instrumental convergence. [...] Конечно, это не математические теоремы. [...] Лучше говорить не "ASI с вероятностью 99.9% уничтожит человечество", а "ASI с заметной вероятностью, более 10%, уничтожит человечество".
Но следствия из этого "более мягкого" утверждения будут всё равно ровно те же самые: этого никак нельзя допустить, и если мы не знаем как этого избежать, значит, не надо строить ASI. [...]
А на какую долю риска лично вы были бы согласны в таком мысленном эксперименте?
Интересные примеры
Дальше Дарио описывает некоторые из экспериментов Anthropic, показывая всякие плохие и просто интересные эффекты, а также о прогрессе в интерпретируемости. [...] Очень интересная тема!
Буквально один пример: [...]
Риски от плохих людей
Переходя к возможным рискам, Амодеи пишет о том, что “a superintelligent genius in your pocket” будет доступен не только хорошим людям, но и плохим. [...]
В этом разделе для меня самым интересным примером была история с mirror life. [...]
Добавлю ещё один источник, который на меня произвёл большое впечатление: книга “Nine Lives“, которую я, конечно же, не читал, а читал подробный обзор на Astralcodexten. Смысл, если кратко, в том, что у настоящих террористических организаций не так уж плохо с деньгами, доступом к ресурсам и т.п. Главное, чего им не хватает, — мозгов. То есть умных людей, потому что умных людей трудно привлечь к работе в террористических организациях. То есть кого-нибудь умного, не обязательно именно человека... [...]
Что же делать? Дарио Амодеи ратует за подход Anthropic, известный как Constitutional AI. [...]
Промышленная революция AI-моделей
После экзистенциальных рисков Амодеи переходит к рискам для рынков труда. Сначала он описывает классическую промышленную революцию... парадокс Джевонса... [...]
А потом Дарио объясняет, почему с AI вряд ли получится так же. [...]
И ничего с этим не поделаешь даже в самых оптимистичных сценариях:
Лавкрафт был оптимистом
Последний раздел эссе, "Black seas of infinity", посвящён unknown unknowns. [...]
Название раздела взято из "Call of Cthulhu", и если Дарио Амодеи может предполагать знакомство с источником, то для русскоязычной аудитории лучше привести цитату. Давайте на ней и закончим (пер. С. Лихачёвой):
#ai #longreads
Сегодня разбираю этот текст, с чем-то не соглашаюсь, но в основном спорить, конечно, не с чем. Пост по ссылке, здесь краткие выжимки:
Переходный возраст машин любви и благодати
AI Safety и роль Anthropic
Здесь Амодеи заслуженно горд достижениями Anthropic; эту область действительно в основном Anthropic и двигает в последнее время. [...]
Правы ли AI-думеры?
Амодеи проходится по классическим "думерским" аргументам вроде instrumental convergence. [...] Конечно, это не математические теоремы. [...] Лучше говорить не "ASI с вероятностью 99.9% уничтожит человечество", а "ASI с заметной вероятностью, более 10%, уничтожит человечество".
Но следствия из этого "более мягкого" утверждения будут всё равно ровно те же самые: этого никак нельзя допустить, и если мы не знаем как этого избежать, значит, не надо строить ASI. [...]
А на какую долю риска лично вы были бы согласны в таком мысленном эксперименте?
Интересные примеры
Дальше Дарио описывает некоторые из экспериментов Anthropic, показывая всякие плохие и просто интересные эффекты, а также о прогрессе в интерпретируемости. [...] Очень интересная тема!
Буквально один пример: [...]
Риски от плохих людей
Переходя к возможным рискам, Амодеи пишет о том, что “a superintelligent genius in your pocket” будет доступен не только хорошим людям, но и плохим. [...]
В этом разделе для меня самым интересным примером была история с mirror life. [...]
Добавлю ещё один источник, который на меня произвёл большое впечатление: книга “Nine Lives“, которую я, конечно же, не читал, а читал подробный обзор на Astralcodexten. Смысл, если кратко, в том, что у настоящих террористических организаций не так уж плохо с деньгами, доступом к ресурсам и т.п. Главное, чего им не хватает, — мозгов. То есть умных людей, потому что умных людей трудно привлечь к работе в террористических организациях. То есть кого-нибудь умного, не обязательно именно человека... [...]
Что же делать? Дарио Амодеи ратует за подход Anthropic, известный как Constitutional AI. [...]
Промышленная революция AI-моделей
После экзистенциальных рисков Амодеи переходит к рискам для рынков труда. Сначала он описывает классическую промышленную революцию... парадокс Джевонса... [...]
А потом Дарио объясняет, почему с AI вряд ли получится так же. [...]
И ничего с этим не поделаешь даже в самых оптимистичных сценариях:
Ultimately, I think of all of the above interventions as ways to buy time. In the end AI will be able to do everything, and we need to grapple with that.
Лавкрафт был оптимистом
Последний раздел эссе, "Black seas of infinity", посвящён unknown unknowns. [...]
Название раздела взято из "Call of Cthulhu", и если Дарио Амодеи может предполагать знакомство с источником, то для русскоязычной аудитории лучше привести цитату. Давайте на ней и закончим (пер. С. Лихачёвой):
Мы живем на безмятежном островке неведения посреди черных морей бесконечности, и дальние плавания нам заказаны. Науки, трудясь каждая в своем направлении, до сих пор особого вреда нам не причиняли. Но в один прекрасный день разобщенные познания будут сведены воедино, и перед нами откроются такие ужасающие горизонты реальности, равно как и наше собственное страшное положение, что мы либо сойдем с ума от этого откровения, либо бежим от смертоносного света в мир и покой нового темного средневековья.
#ai #longreads
👍19❤12🔥5🤔4😱2
Длинный пост про эссе Дарио Амодеи что-то не зашёл. Попробую короткий, про свежую статью на мою любимую тему "AI и математика". Выложил на сайт, но по ссылке можно не ходить, тут почти всё поместилось:
130K строк топологических доказательств за две недели: автоформализация для всех?
Идея проверки математических доказательств компьютером стара почти как сами компьютеры. Ещё в 1962 году Джон Маккарти писал, что это "потенциально одно из самых интересных и полезных применений вычислительных машин". Фактически первой AI-системой был Logic Theorist (1956), о котором я всё время рассказываю на лекциях (в третьей лекции, например) и в докладах о математике (например).
С тех пор появилось много систем автоматического доказательства и верификации: Mizar в 70-х, Isabelle/Isar в 2000-х, а сейчас самый популярный прувер — Lean, появившийся в 2013 году. Но все они требовали, чтобы человек вручную переводил математику на формальный язык, а это очень трудно.
Роль личности: кто такой Урбан
Йозеф Урбан — один из пионеров идеи автоматической формализации с помощью машинного обучения. В 2004 году, когда это казалось безумием, он уже начал это пропагандировать. В 2014 Урбан представил программу исследований и сделал несколько публичных ставок. Например: через 25 лет 50% утверждений из учебников уровня магистратуры будут автоматически парситься с корректной формальной семантикой. Урбан тогда добавил: "возможно, это произойдёт быстрее, чем я ожидал".
Прошло чуть больше десяти лет, и похоже, что он был прав насчёт "быстрее".
Что произошло
Математические доказательства — это текст на естественном языке, который читают и проверяют другие математики. Но люди ошибаются, и история знает случаи, когда "доказанные" теоремы оказывались неверными спустя годы. Формализация — это перевод доказательств на язык формальной логики, где каждый шаг проверяется компьютером. Если верификатор принял доказательство — оно гарантированно корректно.
В препринте Урбан запустил простой цикл: большая языковая модель (в основном ChatGPT 5.2) пишет формальные доказательства, верификатор проверяет, модель получает обратную связь и исправляет ошибки, и так далее.
За две недели система произвела около 130 тысяч строк формализованной топологии по учебнику Манкреса. Полностью доказаны серьёзные теоремы: лемма Урысона (3K строк), теорема метризации Урысона (2K), теорема Титце о продолжении (более 10K). Последняя даже потребовала от системы самостоятельно восполнить пробел в учебнике; GPT думал долго, но в итоге справился.
Что здесь удивительного?
Во-первых, цена: $100 на LLM-подписки и всё.
Во-вторых, система доказательств: Урбан использовал не Lean, с которым LLM работают давно, а Megalodon — малоизвестный верификатор на основе логики высших порядков. И это ничему не помешало.
В-третьих, степень автономности. Вот очень милая цитата про workflow Урбана:
Куда всё это катится?
Урбан осторожно предполагает, что в 2026 году мы можем увидеть автоформализацию большинства стандартных учебников. Или не увидеть — возможно, система упрётся в какие-то пределы. Но сам факт, что это теперь "дёшево и доступно каждому", меняет многое.
Будущее предсказать всегда трудно, но опять кажется, что движемся мы туда быстрее, чем ожидали.
#ai #longreads
130K строк топологических доказательств за две недели: автоформализация для всех?
Идея проверки математических доказательств компьютером стара почти как сами компьютеры. Ещё в 1962 году Джон Маккарти писал, что это "потенциально одно из самых интересных и полезных применений вычислительных машин". Фактически первой AI-системой был Logic Theorist (1956), о котором я всё время рассказываю на лекциях (в третьей лекции, например) и в докладах о математике (например).
С тех пор появилось много систем автоматического доказательства и верификации: Mizar в 70-х, Isabelle/Isar в 2000-х, а сейчас самый популярный прувер — Lean, появившийся в 2013 году. Но все они требовали, чтобы человек вручную переводил математику на формальный язык, а это очень трудно.
Роль личности: кто такой Урбан
Йозеф Урбан — один из пионеров идеи автоматической формализации с помощью машинного обучения. В 2004 году, когда это казалось безумием, он уже начал это пропагандировать. В 2014 Урбан представил программу исследований и сделал несколько публичных ставок. Например: через 25 лет 50% утверждений из учебников уровня магистратуры будут автоматически парситься с корректной формальной семантикой. Урбан тогда добавил: "возможно, это произойдёт быстрее, чем я ожидал".
Прошло чуть больше десяти лет, и похоже, что он был прав насчёт "быстрее".
Что произошло
Математические доказательства — это текст на естественном языке, который читают и проверяют другие математики. Но люди ошибаются, и история знает случаи, когда "доказанные" теоремы оказывались неверными спустя годы. Формализация — это перевод доказательств на язык формальной логики, где каждый шаг проверяется компьютером. Если верификатор принял доказательство — оно гарантированно корректно.
В препринте Урбан запустил простой цикл: большая языковая модель (в основном ChatGPT 5.2) пишет формальные доказательства, верификатор проверяет, модель получает обратную связь и исправляет ошибки, и так далее.
За две недели система произвела около 130 тысяч строк формализованной топологии по учебнику Манкреса. Полностью доказаны серьёзные теоремы: лемма Урысона (3K строк), теорема метризации Урысона (2K), теорема Титце о продолжении (более 10K). Последняя даже потребовала от системы самостоятельно восполнить пробел в учебнике; GPT думал долго, но в итоге справился.
Что здесь удивительного?
Во-первых, цена: $100 на LLM-подписки и всё.
Во-вторых, система доказательств: Урбан использовал не Lean, с которым LLM работают давно, а Megalodon — малоизвестный верификатор на основе логики высших порядков. И это ничему не помешало.
В-третьих, степень автономности. Вот очень милая цитата про workflow Урбана:
Before December 22, I was "babysitting" the command-line interface, i.e., looking every now and then... This was manageable, because my early $20/month LLM subnoscriptions would quickly run out of credits anyway... With the $200/month ChatGPT Pro subnoscription the limits on usage got much higher and automating the prompting became necessary. I have implemented it by writing the following noscript that watches the tmux session and feeds it the prompt followed by "Enter" whenever there has not been any change in the session for 60 seconds
Куда всё это катится?
Урбан осторожно предполагает, что в 2026 году мы можем увидеть автоформализацию большинства стандартных учебников. Или не увидеть — возможно, система упрётся в какие-то пределы. Но сам факт, что это теперь "дёшево и доступно каждому", меняет многое.
Будущее предсказать всегда трудно, но опять кажется, что движемся мы туда быстрее, чем ожидали.
#ai #longreads
1🔥24❤5👍5
В Бангкоке я наконец-то распробовал Claude Code. Великая вещь, лично для меня это скачок вперёд в полезности, сравнимый с рассуждающими моделями. Если ещё не пробовали, очень рекомендую.
Но сейчас не буду подробно о Claude Code. Хотел просто вспомнить в связи с этим цитату из прошлого поста, из статьи Йозефа Урбана:
У меня всё вертелось на языке, что мне это напоминает, и вот вспомнил. Разумеется, The Simpsons Did It, как же иначе!
В эпизоде "King-Size Homer" (из тех, давних, хороших "Симпсонов") Гомеру разрешают работать из дома из-за ожирения. Работа его состоит в том, чтобы на запросы отвечать Yes или No. Сначала он догадывается, что можно просто нажимать "Y" ("I just tripled my productivity!"), а потом устанавливает пьющую птичку, чтобы она нажимала "Y" за него (рис. 2-3).
Как вы помните, Гомер Симпсон — security officer на АЭС, и это дело ничем хорошим не заканчивается.
Разумеется, очевидно, что у задачи автоформализации учебника топологии (пока) не может быть серьёзных последствий, и пьющая птичка Йозефа Урбана вполне подходящий инструмент.
Но сам вопрос интересный. На новогодних праздниках многие распробовали Claude Code, и многие начали доверять ему всё больше и больше — доверять вполне заслуженно, он и правда крутой. Но не безгрешный. В итоге некоторые уже перешли в "Ratatouille mode", как на рис. 4; отличный термин, кстати!
А какая у вас позиция? Что вы готовы доверить AI-агенту (тому же Claude Code) прямо сейчас? И есть ли что-то, что сейчас готовы, а полгода назад готовы не были? Год назад? (а раньше и агентов-то доступных не было)
#ai
Но сейчас не буду подробно о Claude Code. Хотел просто вспомнить в связи с этим цитату из прошлого поста, из статьи Йозефа Урбана:
With the $200/month ChatGPT Pro subnoscription... automating the prompting became necessary. I have implemented it by writing the following noscript that watches the tmux session and feeds it the prompt followed by "Enter" whenever there has not been any change in the session for 60 seconds
У меня всё вертелось на языке, что мне это напоминает, и вот вспомнил. Разумеется, The Simpsons Did It, как же иначе!
В эпизоде "King-Size Homer" (из тех, давних, хороших "Симпсонов") Гомеру разрешают работать из дома из-за ожирения. Работа его состоит в том, чтобы на запросы отвечать Yes или No. Сначала он догадывается, что можно просто нажимать "Y" ("I just tripled my productivity!"), а потом устанавливает пьющую птичку, чтобы она нажимала "Y" за него (рис. 2-3).
Как вы помните, Гомер Симпсон — security officer на АЭС, и это дело ничем хорошим не заканчивается.
Разумеется, очевидно, что у задачи автоформализации учебника топологии (пока) не может быть серьёзных последствий, и пьющая птичка Йозефа Урбана вполне подходящий инструмент.
Но сам вопрос интересный. На новогодних праздниках многие распробовали Claude Code, и многие начали доверять ему всё больше и больше — доверять вполне заслуженно, он и правда крутой. Но не безгрешный. В итоге некоторые уже перешли в "Ratatouille mode", как на рис. 4; отличный термин, кстати!
А какая у вас позиция? Что вы готовы доверить AI-агенту (тому же Claude Code) прямо сейчас? И есть ли что-то, что сейчас готовы, а полгода назад готовы не были? Год назад? (а раньше и агентов-то доступных не было)
#ai
🔥9👍5❤4🤔1
В ближайшее время, наверное, мало буду играть, как-то не до того, да и настроения нету. Так что ещё поразгребаю свои списки маленьких игр, и обзоры будут короче обычного. Но это и есть самые ценные рекомендации, как мне кажется: зачем мне вам рекомендовать Baldur’s Gate 3 или Expedition 33…
Сегодня вот мини-серия из двух коротких игр.
Strange Horticulture и Strange Antiquities
Bad Viking — это британская инди-студия, состоящая буквально из двух братьев: Роб Донкин занимается программированием, Джон — артом. Братья начинали ещё во времена Flash-игр, а в 2022 году выстрелили со Strange Horticulture — игра попала в топы года и разошлась тиражом около полумиллиона копий. Для инди-пазла про магазин растений это очень, очень круто.
И вот недавно (осенью 2025 года) вышел сиквел — Strange Antiquities.
Strange Horticulture: магазинчик ужасов без ужасов
В Strange Horticulture вы управляете магазином растений в маленьком викторианском городке, окружённом туманными холмами и лесами с ведьмами.
К вам приходят посетители и просят что-нибудь — скажем, “растение, которое поможет моему другу забыть о прошлом” или “траву для защиты от кошмаров”. Ваша задача — найти нужное растение на полках.
Как это работает? Вы листаете энциклопедию, сопоставляете описания с тем, что клиент рассказал, смотрите на внешний вид растений, и в итоге выдаёте нужное. [...]
Звучит очень стандартно, но затягивает. Хорошая атмосфера: мерцающие свечи, дождь за окном, кот на прилавке (которого можно гладить), медитативная музыка и такой же медитативный геймплей.
Правда, геймплей довольно однообразный. Весь цикл — это “прочитай описание в книге, найди подходящее растение, отдай клиенту”. Повторить 50 раз. Загадки на карте более разнообразны, но их и не так чтобы много.
Но для своей продолжительности (три часа) Strange Horticulture работает прекрасно: сел, погрузился, порешал загадки, вынырнул уже с пройденной игрой. Усталость от однообразия накопиться не успевает.
Strange Antiquities: те же щи, но погуще (простите)
В Strange Antiquities вы уже не ботаник, а ученик тауматурга — управляете магазином оккультных древностей.
Клиенты всё так же приходят с запросами (“мне нужно что-то от проклятия”, “хочу артефакт для защиты в путешествии”), и вы снова сопоставляете описания с предметами на полках.
Базовая механика та же. Но разработчики явно сделали шаг вперёд и добавили разнообразия.
Во-первых, сама система идентификации стала глубже. [...] Во-вторых, появились дополнительные справочники: книга символов, книга драгоценных камней, книга проклятий. [...] В-третьих, загадки на карте стали разнообразнее. Как минимум, карт теперь несколько. [...]
В общем, геймплейный цикл по сути всё тот же, но с гораздо большим числом переменных, и это прекрасно. Strange Antiquities — игра уже не на три, а на пять часов, и она это время вполне заслуживает.
Заключение
Обе игры — милые, атмосферные головоломки для медитативного и недолгого прохождения, на 1-2 вечера. Strange Antiquities объективно лучше во всём: разнообразнее головоломки, глубже система идентификации, интереснее загадки. Если выбирать одну игру из двух — берите эту. Но и Strange Horticulture тоже хороша. Да ещё и котиков уважают.
Лично я обе игры прошёл с удовольствием и определённо попробую и следующую часть серии, когда братья Донкины её выпустят. Что это будет — Strange Concoctions? Strange Taxidermy? Strange Eldritch Horrors? Время покажет.
#tgif #games
Сегодня вот мини-серия из двух коротких игр.
Strange Horticulture и Strange Antiquities
Bad Viking — это британская инди-студия, состоящая буквально из двух братьев: Роб Донкин занимается программированием, Джон — артом. Братья начинали ещё во времена Flash-игр, а в 2022 году выстрелили со Strange Horticulture — игра попала в топы года и разошлась тиражом около полумиллиона копий. Для инди-пазла про магазин растений это очень, очень круто.
И вот недавно (осенью 2025 года) вышел сиквел — Strange Antiquities.
Strange Horticulture: магазинчик ужасов без ужасов
В Strange Horticulture вы управляете магазином растений в маленьком викторианском городке, окружённом туманными холмами и лесами с ведьмами.
К вам приходят посетители и просят что-нибудь — скажем, “растение, которое поможет моему другу забыть о прошлом” или “траву для защиты от кошмаров”. Ваша задача — найти нужное растение на полках.
Как это работает? Вы листаете энциклопедию, сопоставляете описания с тем, что клиент рассказал, смотрите на внешний вид растений, и в итоге выдаёте нужное. [...]
Звучит очень стандартно, но затягивает. Хорошая атмосфера: мерцающие свечи, дождь за окном, кот на прилавке (которого можно гладить), медитативная музыка и такой же медитативный геймплей.
Правда, геймплей довольно однообразный. Весь цикл — это “прочитай описание в книге, найди подходящее растение, отдай клиенту”. Повторить 50 раз. Загадки на карте более разнообразны, но их и не так чтобы много.
Но для своей продолжительности (три часа) Strange Horticulture работает прекрасно: сел, погрузился, порешал загадки, вынырнул уже с пройденной игрой. Усталость от однообразия накопиться не успевает.
Strange Antiquities: те же щи, но погуще (простите)
В Strange Antiquities вы уже не ботаник, а ученик тауматурга — управляете магазином оккультных древностей.
Клиенты всё так же приходят с запросами (“мне нужно что-то от проклятия”, “хочу артефакт для защиты в путешествии”), и вы снова сопоставляете описания с предметами на полках.
Базовая механика та же. Но разработчики явно сделали шаг вперёд и добавили разнообразия.
Во-первых, сама система идентификации стала глубже. [...] Во-вторых, появились дополнительные справочники: книга символов, книга драгоценных камней, книга проклятий. [...] В-третьих, загадки на карте стали разнообразнее. Как минимум, карт теперь несколько. [...]
В общем, геймплейный цикл по сути всё тот же, но с гораздо большим числом переменных, и это прекрасно. Strange Antiquities — игра уже не на три, а на пять часов, и она это время вполне заслуживает.
Заключение
Обе игры — милые, атмосферные головоломки для медитативного и недолгого прохождения, на 1-2 вечера. Strange Antiquities объективно лучше во всём: разнообразнее головоломки, глубже система идентификации, интереснее загадки. Если выбирать одну игру из двух — берите эту. Но и Strange Horticulture тоже хороша. Да ещё и котиков уважают.
Лично я обе игры прошёл с удовольствием и определённо попробую и следующую часть серии, когда братья Донкины её выпустят. Что это будет — Strange Concoctions? Strange Taxidermy? Strange Eldritch Horrors? Время покажет.
#tgif #games
1👍6❤1👎1🔥1