#speaker #conference #it #development #opensource #holyjs #ai #logic #math #computerscience

Очередной мой доклад заанонсирован на сайте HolyJs, в этот раз шизы меньше, но гораздо больше фундамента! А вообще, меня опять сбайтил @DreamShaded , thanks man

Анонс доклада: https://holyjs.ru/talks/20011201-from-aristotle-to-runtime-formally-provable-typescript-and-ai-that-verifies-its-own-code/

Конфа будет в Санкт-Петербурге, 23–24 октября

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

О чём буду говорить? О том как начать писать с ИИ более формально-доказуемый код и всё благодаря теории Карри-Ховарда, ладно-ладно, вот текст анонса

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

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

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

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

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

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

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

Тг конфы: https://t.me/holyjsconf
Сайт конфы: https://holyjs.ru/

Всех обнял-приподнял, готовьте полисиллогизмы и энтимемы! 🤔