Где ставить проверку работы ИИ-агентаГраница агрегата и теорема Райса

Коротко: что проверяет человек, а что делает агент

Три зоны работы с агентом: где он свободен, где стоит проверка и где решает человек.

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

На границе агрегата стоит проверка. Здесь записано, какие команды агрегат принимает, какие события отдаёт соседям и какие правила верны всегда. Эту границу проверяет машина. Модель на Quint — это запись правил системы на специальном языке, по которой программа перебирает все возможные порядки команд и ищет тот, где правило нарушится. Ограничения в базе данных — правила, которые база проверяет при каждой записи и не даёт сохранить запрещённое. Человек смотрит только правки самой границы.

Границу контекста держит человек. Какие агрегаты живут вместе и где меняется смысл слов, по коду не вычислить: это зависит от будущих изменений. Поэтому эту рамку ставит человек и сдвигает её по истории правок и планам, подробно об этом в разделе «Первая рамка».

Почему нельзя проверить весь код агента: теорема Райса

Суть. Какой бы умной ни была проверка кода агента, найдётся код, на котором она ошибётся. Это доказал Генри Гордон Райс в 1951 году.

• Что нельзя проверить: поведение программы, то есть что она делает при запуске. Например, «никогда не списывает деньги без заказа».
• Условие теоремы: свойство есть у одних программ и нет у других. Если оно есть у всех или ни у одной, ответ известен заранее.
• Подробно с доказательством: статья «Теорема Райса простыми словами».

Два вида вопросов о программе. Вопрос с ответом «да» или «нет» математики называют предикатом. Теорема запрещает точный ответ только на второй вид.

Практический приём: переписать код так, чтобы важное правило стало вопросом первого вида.

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

Код один и тот же. Вопрос о записи решается чтением конечного текста, вопрос о поведении требует перебрать все запуски.

Почему на вопрос о поведении нельзя ответить для любой программы, видно из одного построения. Возьмём любую программу $P$ и любые входные данные $w$ для неё; запись $P(w)$ значит «программа $P$, запущенная на данных $w$». Соберём новую программу $Q$: сначала она запускает $P(w)$, а когда та закончится, делает шаг $B$, который нарушает правило, например списывает деньги без заказа. Если $P(w)$ никогда не заканчивается, до шага $B$ дело не доходит и правило не нарушено. Значит, проверка правила для $Q$ должна знать, закончится ли $P(w)$. Схема ниже показывает это построение, формулы и вывод — сразу под ней.

Доказательство в одну схему: проверка правила для $Q$ отвечала бы, остановится ли $P(w)$.

Шаг $B(x)$ правило нарушает, а программа, которая работает вечно, его не нарушает. Значит, $Q$ доходит до нарушения только если $P(w)$ когда-нибудь закончится:

Если бы существовала проверка правила для любой программы, она, получив $Q$, ответила бы и на вопрос, остановится ли $P(w)$. А этот вопрос, проблема остановки, не решается никакой программой: это доказал Алан Тьюринг.

Три способа сделать проверку конечной

Раз точной проверки для любой программы нет, проверку ограничивают так, чтобы она касалась не любой программы. Ограничить можно тремя способами: уменьшить мир, в котором проверяют, сузить язык, на котором пишут, или разрешить проверке честно отвечать «не знаю». На схеме все три способа рядом.

Слева перебор маленького мира, в центре один путь записи в базу, справа три ответа проверки, где третий уходит человеку.

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

Подробнее, с доказательством того, почему каждый способ снимает запрет, — в статье «Теорема Райса простыми словами».

Как это выглядит на деле: одно правило, три проверки

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

Сузить мир: модель на Quint. Правило и действия системы записывают коротким описанием, без настоящего кода. Состояние — снимок данных в какой-то момент: какие брони есть, у какой комнаты, с какого по какое время. Действия — «забронировать» и «отменить». Правило записывается одной строкой: для любых двух броней одной комнаты одна заканчивается раньше, чем начинается другая.

Правило в модели на Quint

val noOverlap = bookings.forall(a => bookings.forall(b =>
  a == b or a.room != b.room or a.end <= b.start or b.end <= a.start))

Дальше программа сама перебирает все последовательности действий для маленького мира: 3 комнаты, до 5 броней. Если правило где-то нарушается, она выдаёт цепочку шагов. Например: два клиента одновременно бронируют комнату 2 на 10:00–11:00, обе проверки «свободно ли» проходят раньше обеих записей, и в базе оказываются две брони на одно время. Эта цепочка и есть находка: ошибка в замысле видна до того, как агент написал код. Маленького мира хватает, потому что такие ошибки проявляются уже на двух-трёх бронях.

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

Ограничение в PostgreSQL

CREATE EXTENSION IF NOT EXISTS btree_gist;
ALTER TABLE bookings ADD CONSTRAINT no_overlap
  EXCLUDE USING gist (room_id WITH =, tstzrange(starts_at, ends_at) WITH &&);

Вторая половина — один писатель: записывать в таблицу броней может только один модуль. Это проверяется поиском по тексту кода при каждой правке агента. Команда ниже ищет все файлы, где есть запись в таблицу броней, кроме разрешённого; пустой результат значит «обхода нет».

Проверка «один писатель» поиском по коду

grep -rl "INSERT INTO bookings" src | grep -v src/booking/repository.ts

Вопрос «может ли код агента создать пересекающиеся брони» превратился в два вопроса о тексте: есть ли ограничение в схеме базы и нет ли записи в обход. На оба ответ точный.

Разрешить «не знаю»: три вердикта на правку агента. Проверка правки агента собирается из предыдущих двух и выдаёт один из трёх ответов. «Доказано»: модель на Quint прошла, ограничение в базе на месте, поиск не нашёл записей в обход. «Нарушено»: поиск нашёл, что агент добавил запись в таблицу броней из модуля отчётов. «Не уверена»: агент собирает запрос к базе из строк на лету, и поиск по тексту не может понять, в какую таблицу он пишет. Тогда правка получает пометку «нужен человек», и её смотрит разработчик. Человек тратит время только на третий случай.

Каждый из трёх ответов точен только в своих пределах. Перебор доказывает, что правило держится в модели с 3 комнатами и 5 бронями, но не в боевой базе с тысячами броней. Поиск доказывает, что в коде нет записи в обход, но не то, что само ограничение в базе написано верно. Ответ «соблюдено» точен, но часть правок всё равно уходит человеку. Поэтому способы используют вместе: модель проверяет замысел до кода, ограничение и поиск проверяют сам код, а человек смотрит то, что осталось с меткой.

Есть и четвёртый вариант, который на практике встречается чаще всего: отвечать всегда, но иногда ошибаться. Так работают тесты на примерах и ревью кода другой моделью. Это тоже допустимый выбор, но осознанный: он годится там, где ошибка дешёвая, и не годится для денег и доступов. Похожую развилку знают по теореме CAP о распределённых системах: при разрыве связи сервер либо ждёт, либо отвечает по устаревшей копии. Общее у них одно — пока событие не произошло, нельзя понять, случится ли оно позже или не случится никогда, сколько бы ни ждать, — а причины разные; подробно в статье «Теорема Райса простыми словами».

Агрегат как пост проверки: что даёт event storming

Event storming — формат совместной работы, на котором команда раскладывает предметную область на события. После него у каждого агрегата есть четыре вещи: команды, которые его меняют, события, которые он отправляет, модели чтения, через которые на него смотрят, и инварианты — правила, которые верны в каждом состоянии.

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

Пост проверки стоит на входе команд и выходе событий. Внутри границы агент свободен.

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

Как выбрать размер ограниченного контекста: по проверяемости

Переход от предметной области к ограниченным контекстам — самое трудное место в DDD. Обычные признаки границы: одно слово начинает значить разное, меняется команда, правила перестают быть обязаны выполняться одновременно.

Как применить критерий к своему проекту. Берут часть системы, которую считают кандидатом в контекст, например «бронирование», и проверяют её за пять шагов.

1. Выписать правила и действия. Правила — то, что должно быть верно всегда: «брони одной комнаты не пересекаются». Действия — команды, которые меняют данные: «забронировать», «отменить».
2. Записать их моделью на Quint. Состояние — какие брони есть; действия — как они меняют состояние; правила — проверки после каждого шага. Это десятки строк, без настоящего кода.
3. Выбрать малые числа. По 2–3 объекта каждого вида: 3 комнаты, 5 броней, 2 клиента. Обычно этого достаточно, чтобы встретились типичные неприятные сочетания: две брони одной комнаты, два клиента в одну минуту. Гарантии нет: ошибка, которой нужно больше объектов, пройдёт мимо.
4. Запустить перебор с пределом времени, например 10 минут.
5. Прочитать результат по таблице ниже. Перебор закончился без нарушений — размер подходит. Закончился и показал нарушение — размер подходит, но в правилах или действиях ошибка, её чинят. Не закончился за предел — состояний слишком много, кандидата режут.

Запуск перебора для модели бронирования

quint verify booking.qnt --invariant=noOverlap --max-steps=10

Как резать, если перебор не закончился. Выписать для каждого правила, каких данных оно касается. Правила, у которых нет общих данных, разводят по разным частям: «брони не пересекаются» касается только броней, «счёт не оплачивается дважды» — только счетов. Между частями оставляют события, например «БроньСоздана». Потом каждую часть проверяют теми же пятью шагами.

Если модель контекста отвечает «не уверена», контекст режут, и между частями остаются только события.

Как пользоваться этим признаком: записать правила контекста моделью на Quint, задать маленькие числа и запустить перебор. Результат прогона попадает в одну из строк таблицы, а в последнем столбце сказано, что делать дальше.

Первая рамка: почему она ошибётся и как сделать её дешёвой

Рамку провели вокруг броней и комнат. Если дальше придёт правка про брони и комнаты, рамка подойдёт. Если придёт правка про брони и счета, она пересечёт границу, и рамку придётся сдвигать. Какая из них придёт, сейчас не узнать — это и есть открытый вопрос.

Что предстоит выяснить:

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

Выбрать рамку мешает другой запрет, чем в теореме Райса. Проверке кода сведений хватает, весь код перед ней, но ответ из него нельзя вычислить. Рамке не хватает самих сведений. Хорошая рамка — та, внутри которой будут жить будущие изменения, а о будущем нет данных ни в коде, ни где-либо ещё. Это ровно положение сервера из теоремы CAP: он не знает, что происходит у соседа за оборванной связью, а здесь неизвестно, какие правки придут через месяц.

Поэтому и выходы те же, что в CAP. Ждать, пока будущее станет известно, нельзя: работа идёт сейчас. Остаётся ответить сейчас по тому, что есть, и быть готовым ошибиться. «То, что есть» — два приближения будущего: история прошлых правок, где видно, что обычно меняется вместе, и планы, которые знаете только вы. А третий выход из CAP — ограничить время — здесь превращается в короткие циклы agile: ставить рамку на две недели, смотреть, как в ней живут правки, и сдвигать. Раз рамка всё равно будет ошибаться, важно, чтобы её было дёшево сдвинуть.

Теорема Райса в этом разделе всё же участвует, но в другой роли. Она не помогает угадать будущее, зато даёт проверку уже выбранной рамки: если модель правил части перебирается на Quint до конца, часть достаточно мала, а если не перебирается — её стоит разрезать. Об этом признаке шла речь в разделе о размере контекста.

Откуда взять первые части

Знать части заранее не нужно: первую нарезку даёт то, что уже есть, а человеку остаётся дать частям имена и поправить спорные места.

Как работает склейка по правилам. Выписать правила о данных, например «в закрытом эпике нет открытого репорта», «токен видит только свои проекты». Если правило упоминает две таблицы, они в одной части. Получившиеся группы и есть первая нарезка.

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

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

При чём тут Гёдель: только аналогия

Связь теоремы Гёделя о неполноте с этой темой — моё предположение, источников, которые бы её проводили, я не нашёл. Повод для него: и у Гёделя, и у Райса доказательство держится на одном приёме, программе или формуле, которая говорит о самой себе. Но первая теорема Гёделя относится к формальным системам, в которых можно вести элементарную арифметику, и о границах предметной области ничего не говорит. Для довода о проверке агента точный результат — теорема Райса.

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

Частые вопросы