Семантический diff для политик от LLM: из 18 «изменённых» строк видно 2 бага

Ревью кода начинается с diff. Две файла по три тысячи строк на глаз никто не сравнивает. С формальными политиками всё хуже: текстовый diff подсвечивает синтаксис, который смысл не меняет. Поменяли местами два условия, развернули аргументы равенства, заменили предикат на эквивалентный, и половина файла выглядит изменённой. А настоящий баг, например Or там, где в требовании стоит «и», в этом шуме легко теряется.

AWS Machine Learning Blog описывает открытый движок, который решает эту задачу через антиунификацию. Это классическая идея Плоткина 1970 года: для двух выражений находим самый конкретный общий шаблон.

Зачем это нужно, если политики пишет LLM

Главный сценарий здесь автоформализация. Вы берёте требования на естественном языке и просите модель превратить их в SMT-LIB для Z3 или cvc5, в политики Cedar или Dogwood, в YAML-правила песочницы OpenShell или в выражения CEL. Модель пишет артефакт, а в сравнении она не участвует. Эталона при этом нет. Запустите модель дважды, и получите две разные формализации, а какая верная, неизвестно.

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

Это родственник семантической энтропии из работы Farquhar и коллег в Nature (2024). Там много ответов кластеризуют и получают одно число. Антиунификация сохраняет больше информации: она показывает общую структуру и каждое расхождение, а не только оценку.

Как это работает на примере

Движок работает поверх e-графа, структуры, которая хранит выражения, заведомо равные друг другу. Равенства вы объявляете сами. Операторам And и Or задаёте ассоциативность, коммутативность и идемпотентность. Предметные факты, скажем «external равно не internal», записываете как rewrite-правило. Всё остальное движок считает различием.

Результат выглядит как один терм. Общее показано один раз, а каждое расхождение лежит в узле Variants с обеими версиями. Если выбрать первый вариант во всех узлах, получится политика A, если второй, то B. Слияние получается без потерь.

В разобранном примере есть требование к межрегиональной репликации в S3: версионирование, одобренный регион назначения, для confidential-объектов тот же аккаунт и шифрование ключом клиента, а для больших объектов multipart-копирование. Две формализации различаются в пяти местах. Три различия косметические: порядок условий, перевёрнутый Eq и approvedRegion, раскрытый в us-east-1 и eu-west-1. Два меняют смысл. В одной версии условие для confidential-объектов требует аккаунт и шифрование, а в другой хватает одного из двух (And превратился в Or). Порог размера в одной версии Lte, в другой Lt.

Обычный unified diff помечает 18 из 28 строк и не говорит, какие из изменений важны. Семантический diff убирает перестановки и сводит результат к узлам, которые и надо читать. Для таких случаев есть метрика cr, степень сжатия. Ноль означает полное согласие при объявленных равенствах, а единица означает, что общего нет вовсе. В примере cr равен 0,5862 при размере результата 42.

Ограничения и что делать

Есть несколько оговорок. Движок не импортирует нативные политики Cedar, Dogwood, OpenShell или CEL. Нужные конструкции вы кодируете как термы вручную и вручную объявляете равенства. Если правил не хватает или поиск неполон, оставшееся различие может оказаться эквивалентностью, которую движок не нашёл. Низкий cr тоже не доказывает правильность: два кандидата могут одинаково ошибаться. Кроме того, по умолчанию поиск идёт методом Монте-Карло, и поле :completion покажет budget вместо exact, если лимит исчерпан до перебора всех вариантов.

Практический вывод для тех, кто собирает пайплайны «требования → формальная политика»: не доверяйте единственному выходу модели. Сгенерируйте несколько кандидатов, сведите их через семантический diff и отдайте человеку или SMT-солверу только узлы Variants. Солвер может найти контрпример, то есть конкретное присваивание, при котором одна формула верна, а другая нет, а антиунификатор покажет, где искать. Попробовать можно за пять минут: репозиторий yaspar-org/semi-persistent, сборка через cargo build --release и пример 12-first-au.egg.