Телеграм канал «Metaprogramming»

Контуры фронтира ИИ-математики

Пояснение к иллюстрации выше.

Утверждение самой гипотезы Эрдёша (левая надводная часть) требует лишь чуть более чем базового знания школьной геометрии. Мол расставим данное число точек по плоскости так, чтобы максимальное число пар находилось на расстоянии 1. Гипотеза утверждает, что этот максимум растёт лишь чуть быстрее, чем n.

Правая надводная часть – хорошо оформленные определения и теория, на которые опирается сгенерированное доказательство. Есть небольшое число людей, которые в сумме владеют полным пониманием этих элементов алгебраической теории чисел.

Подводная часть – ИИ-слоп, проверенный машинкой на зависимых типах (языком программирования Lean). Важно отметить, что связь подводной части с надводной односторонняя: определения сверху никак не зависят от слопа снизу.

Исходя из такой картинки можно конкретизировать, чем будет заниматься AI<->Human mathematics:

1. Искать утверждения, которые имеют простые формулировки, но потенциально глубокое скрытое содержание. Утверждения, хорошо понятные людям и компоненты которых формализованы в отрецензированных математических библиотеках.
2. Увеличивать надводную часть путём:
а) формализации существующей математики в коде;
б) расширения границ математического знания за счёт творческих усилий человека.
3. Повышать эффективность подводной части путём ИИ-инженерии: тренировке моделей, подключению инструментов и баз знаний, разработке харнесов и всего такого.
4. Заниматься рыбалкой: сидя на углу надводной части пытаться подцепить и выловить кусочек слопа, который можно после надлежащей доработки напильником сделать элементом надводной части.

Первая картинка из доклада Терренса Тао "Математика 2.0". Судя по слайдам доклад невнятный. Как бы ИИ это зло, мешает нам работать. С другой стороны доказательства теорем (самая рутинная часть) больше не проблема и это вроде как хорошо. С третьей стороны вот нужна интерпретируемость, может у ИИ идеи какие-то новые будут и т.п.

Вторая картинка – схематичное изображение опровержения гипотезы Эрдёша, сделанное недавно OpenAI.

Суть формальной (дедуктивной) верификации

Так сложилось, что параллельно с очередной серией роста способностей ИИ я начал заниматься формальной верификацией. Так как математики не умеют программировать, программисты не любят математику, а операторы LLM не понимают сути деятельности ни тех, ни других, у меня появился уникальный взгляд на ключевой аспект формальной верификации (о котором наверняка уже кто-то либо написал, либо скоро напишет в мейнстриме).

Некоторое время назад большую часть времени в работе с пруф-ассистентами (языками программирования, позволяющими доказывать математические теоремы и корректность работы программ) занимали, собственно, пруфы – доказательства теорем. Примерно полгода назад бастион был взят и, также как в обычном программировании, модельки стали справляться с написанием кода пруфов лучше лучших людей.

При этом код пруфов имеет гораздо меньшее значение, чем какой-то рутинный код в обычных программах – компилятор сам проверит что доказательство соответствует постулируемой теореме (да, остаются соображения скорости компиляции, поддерживаемости, устойчивости к изменениям и т.п. – но они второстепенны). То есть смотреть надо на сами формулировки теорем.

А какие должны быть формулировки? Должны быть короткие и ёмкие – короче, выразительные.

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

Самый элементарный пример, который пришёл мне в голову, следующий – допустим мы пишем программу, умножающую каждый элемент массива на два:
xs := [1, 2, ...]
for i := 1 to len(A):
xs[i] := xs[i] * 2

При внешней простоте в этом коде чудовищное количество умолчаний. Мы более-менее ясно представляем, что хотим иметь вот какие свойства этой программы:

1. Длина результирующего массива совпадает с длиной исходного
2. Собственно, каждый элемент конечного равен элементу исходного с тем же индексом, умноженному на два

Однако как бы краем ума подразумеваем, что вообще-то:

1. Исполнение на конкатенации двух массивов равно конкатенации исполнений на каждом из массивов
2. Если пройтись по элементам задом наперёд (или вообще в произвольном порядке), а потом в том же порядке интерпретировать результирующий массив, то ничего не поменяется
3. Если последовательно выполнить два цикла с разными операциями, то будет тоже самое, что в одном цикле с каждым элементом выполнить две операции

Причём это не какие-то произвольные свойства – их наличие позволяет реализовать chaining, lazy-исполнение, параллелизм.

Но на самом деле это одна идея. Идея о map.

Другими словами – о действии на морфизмах функтора List, имеющем особые свойства из-за моноидальной структуры списков и естественности преобразования перестановками.

Думаю в будущем математика в целом будет, по ряду причин, всё в большей мере синонимом "формализации интуиции разработчиков систем". Разработчики систем будут мыслить всё ближе к математическим конструкциям, а математические конструкции всё проще описывать системные особенности.

Learning-driven development

На фоне триллионных вложений последних лет в искусственных интеллект стала крайне популярной тема формальной верификации. Мол, пусть слоп-машина генерирует стохастически что хочет, а мы на неё формальные ограничения повесим, так что строго математически будет доказано что она отработала в желаемых рамках.

Выяснилось, однако, что за ~20 лет научных работ в этой области сделали лишь парочку каких-то полуработающих прототипов, которые через раз падают от утечки памяти на больших программах; то ли поддерживают, то ли нет многопоточность; не понятно как моделируют ввод-вывод (сами понимаете, класс программ, который не имеют ни ввода, ни вывода, весьма малочисленный).

В самих языках с зависимыми типами (именно на них можно формализовать доказательства математических теорем и верифицировать императивный код), оказывается, множество открытых теоретических вопросов, связанных, например, с понятием эквивалентности/равенства или бесконечно длящихся процессов. Математическая теория, которая должна эти вопросы решать, фрагментарно разбросана по статьям и диссертациям и фундаментально неполна.

Никакое вливание токенов причём тут, судя по всему, не поможет. Как разбирались в этом хозяйстве пять человек во всём мире так до сих пор те же люди и разбираются. Эмуляция привычной математики на Lean – позволившая вагонами доказывать незакрытые теоремы – или генеративная верификация софта на Rocq – с помощью которой можно проверить корректность (кстати, что это слово означает?) работы всех существующих сишных программ – кажется нисколько не приближает решение.

Одновременно на фоне очевидных успехов фронтирных моделей в программировании (никто больше не пишет код руками, разве что для развлечения) отчётливо проявляется новый тренд: серьёзные проекты закрывают кран для трубы слоп-машины. Прежде чем отправить PR в Linux, LLVM, GCC и пр. требуется лично подписаться под тем, что сгенерировала слоп-машина. Если у рецензента возникнут вопросы и сомнения требуется их снова лично (то есть, без ИИ) прояснить и развеять. Подозрения в том, что разработчик играет роль прокладки между репликами рецензента и "клодом" приведут к закрытию PR со стандартным комментарием.

Программисты решают проблему слопа, переходя на spec-driven development: пусть моделька не за один заход исполняет всё от начала до конца на своё усмотрение, а сначала вместе с разработчиком сформулирует задачу. После того как техническое задание будет утверждено – отправляем его на исполнение. И в такой манере далее – сложный многошаговый конвейер проверок и возвратов (на каждом шаге с участием человека-рецензента), по сути воспроизводящий обычную работу хорошо организованной софтверной компании.

Узким местом здесь становится не написание кода, как раньше – моделька сама его и напишет, и даже проверит – а рецензирование спецификаций.

Очевидно, что для его преодоления надо воздействовать на ключевую инфраструктуру напрямую – на рецензента. Модели уже несколько месяцев как доказали радикальное интеллектуальное превосходство (с оговорками) не просто над средним человеком, а над лучшими представителями человечества (ну, как-то даже бессмысленно сравнивать скорость езды автомобиля и скорость бега человека). При этом некоторые технические и существенные организационные ограничения заставляют продолжать держать людей в качестве контролёров на ключевых этапах разработки программ.

Так пусть ИИ обучает человека, тем самым упрощая и ускоряя его работу.

Очевидно, что как в начале, так и в конце конвейера spec-driven development должны быть шаги по созданию буквально обучающего материала, объясняющего человеку ключевые концепции, которые ему не знакомы, конкретные механизмы их применения и реализации в коде и, в идеале, дающие опциональный набор упражнений для ручного прорешивания для желающих держать свой интеллект в тонусе.

Так как скорость принятия решений людьми-рецензентами становится главным узким местом всего конвейера разработки подобный подход можно отдельно назвать learning-driven development.

https://www.youtube.com/watch?v=3TNpOD6bov8 – весёлое видео про внедрение ИИ в разработку (сделанное, разумеется, суно и клодом)

Ренесанс командной строки

Современные интерфейсы веб-сайтов и приложений, стараниями продуктовых менеджеров, дошли до какой-то совсем уж невероятной степени издевательства над пользователем.

Я просто хочу заплатить деньги и получить услугу, почему я должен продираться сквозь заросли очень полезных функций, ценных рекомендаций похожих услуг (в каком сценарии предлагать одновременно с заказом такси купить наушники будет релевантной рекомендацией?) и вульгарных поп-апов, которые вроде начали считаться неприличными уже двадцать лет назад?

К счастью, похоже всему этому наступает конец.

Интерфейс будущего – как и интерфейс прошлого – это командная строка. В этот раз, конечно, командная строка к ИИ.

Интересно пофантазировать о некоторых деталях реализации. Понятно, что разработчики фронтирных моделей мечтают, чтобы запрос в командную строку, вместе со всеми персональными данными с устройства, уходил в их облака. Тот же самый ChatGPT, который просто умеет звонить (имея доступ к телефонной книге) и отправлять сообщения в WhatsApp.

Однако, вероятно, это будет не единственная опция.

Массовому рядовому пользователю редко когда требуется, не привлекая внимания санитаров, доказывать теоремы, над которыми математики бились сотню лет, переписывать операционную систему с нуля на Rust или делать бесплатный Photoshop на основе открытых спецификаций. Замечательно, что всё это теперь может сделать даже школьник, но на фоне блицкрига в сингулярность остался длинный хвост не решённых задач.

Забронировать столик в ресторане, оплатить такси, спланировать поездку с билетами и отелем, напомнить о приёме, оформить документы, организовать замену счётчика и т.д. – всё это уже сейчас решается с телефона в пять кликов. Это на пять кликов больше, чем необходимо. Останется командная строка (с опциональным голосовым вводом-выводом) и локальная модель, которая на основе коротких команд сама всё организует, свяжется, напомнит и будет поддерживать.

Кажется, что технический уровень уже сейчас позволяет такие модели делать.

Выбросить из нейросеток общие сведения о мире (локальный архив википедии + лента официальных новостей + API сервисов дадут всю необходимую информацию), сделать акцент на вызове сторонних инструментов и скиллов (возможно не только через промпт но и в стиле LoRA – модульного специализированного "затачивания" сетки), научить беспощадной целеустремлённости, организовать "песочницу" для безопасного исполнения – и окажется, что для запуска модели не требуется два шкафа с видеокартами и компактная электростанция, восьми энергоэффективных ядер ARM процессора вполне хватает.

Взглянуть здраво на повседневную рутинную ерунду, которой приходится заниматься – так для её решения не требуется, чтобы нейронка сохраняла когерентность на протяжении недели непрерывной работы. Ну, полчасика если сможет не сбиваясь исполнять задачу, то уже достаточно. Добавить к этому внешний календарь и вызовы по расписанию и вопрос решён.

Если захочется посмотреть на едущую по карте машинку – вообще говоря, а зачем? текста "через 5 минут приедет жёлтая номер 123" достаточно – то можно будет вечером на ПК запустить по облачной подписке задачу создать соответствующий виджет по индивидуальному заказу и на следующее утро закинуть его на телефон. Без рекламы наушников, празднования дня рождения компании, ленты интересных событий в городе, уникальных скидок и таргетированных предложений от премиум менеджеров.

Ранее обсуждали:

– Бедность простоты (27.03.2025)
– Театр экономики (13.06.2026)

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