От Аристотеля до runtime: формально доказуемый TypeScript и код, который ИИ проверяет сам

LLM умеет писать код, который выглядит убедительно даже тогда, когда не работает. Мы отвечаем на это новыми промптами, увеличиваем контекст, подключаем RAG — и все равно получаем программу, уверенно объясняющую собственную ошибку. А что, если проблема не в качестве генерации, а в том, что у модели нет возможности проверить результат так же, как это сделал бы инженер?

В докладе пройдем путь от силлогизмов Аристотеля и энтимем через булеву алгебру, множества и группы к теории категорий. Разберемся, как из этой, на первый взгляд, академической экскурсии получить практический язык для описания программ: объекты, преобразования, композиции и функторы.

Я покажу созданное мной надмножество над TypeScript, в котором разработчик описывает утилиту через ее типы, допустимые преобразования и отношения между ними. Такая спецификация сужает пространство решений для ИИ и позволяет генерировать не просто синтаксически правдоподобный, а формально проверяемый код. Здесь же поговорим о числах Чёрча, неизменяемых структурах данных, логических парадоксах и о том, почему универсальное множество способно испортить не только вечер математику, но и модель предметной области программисту.

Но статических ограничений недостаточно. Поэтому во второй части я разберу архитектуру самописного контура runtime-самопроверки. ИИ сначала генерирует черновик программы. Отдельный инструмент инструментирует код: оборачивает выполняемые выражения и собирает типы, значения, переходы состояния и ошибки. Черновик запускается в изолированном окружении, трасса возвращается модели, и та исправляет программу до того, как результат увидит пользователь.

Покажу, как в этот цикл встраиваются научный метод и prompting-практики: zero-shot и few-shot, RCTF, ReAct, Tree of Thoughts, RAG и STAR. Главное здесь не коллекция аббревиатур, а переход от «попросить модель написать код» к циклу «гипотеза — эксперимент — наблюдение — исправление».

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

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