Уговорить или доказать: чем мягкая проверка агентов отличается от жёсткой

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

Это и есть «LLM-as-judge». Идея захватила индустрию почти мгновенно, и неспроста. Но за два с лишним года накопилось ровно столько данных о том, где она ломается, что в 2026-м рядом громко поднялась вторая школа — не уговорить модель согласиться, а математически доказать. Разница между этими двумя подходами и есть, по сути, твоя поляна. Так что разберём оба края честно.

Соблазн отдать проверку самой модели

Стартовая точка известна. В 2023-м Лянмин Чжэн с коллегами из Беркли показали: GPT-4 как судья совпадает с людьми-оценщиками больше чем в 80% случаев — ровно с той же частотой, с какой люди соглашаются между собой. Если модель приближает человеческое суждение на человеческом же уровне согласованности, то зачем держать дорогие пайплайны разметки? Достаточно вызова по API. Это сделало автоматическую оценку мейнстримом за одну ночь.

Логика железная по масштабу. К концу 2026-го, по прогнозам, 40% корпоративных приложений будут встроены с агентами под конкретные задачи; половина руководителей уже рапортует о развёртывании. Когда система обрабатывает миллионы запросов, человеческая оценка не дорога — она математически невозможна. Машинный судья кажется единственным выходом.

Где судья сыпется

А дальше пошли исследования, и они оказались куда менее обнадёживающими.

Картина «80% точности» держится в контролируемых условиях. В проде фронтирные модели на тестах предвзятости перевалили за 50% ошибок. В марте 2026-го RAND выпустил открытый Judge Reliability Harness — стенд, который стресс-тестит судей на устойчивость и различающую способность. Прогнали четырёх судей по бенчмаркам на безопасность, убеждение, злоупотребление и агентность — и вывод был жёсткий: ни один судья не надёжен повсеместно. Согласованность ломалась на ерунде — смена форматирования, перефразирование, изменение многословности.

И это не случайные сбои, а систематические перекосы. Судьи страдают позиционной предвзятостью — предпочитают ответ по его месту в промпте, а не по содержанию (у GPT-4 — порядка 40% непостоянства). Многословной — длинный ответ кажется лучше, даже если короткий точнее (накрутка около 15%). И самой коварной — self-preference: модель узнаёт собственные генерации и завышает их; на NeurIPS-2024 показали прямую корреляцию между способностью узнать себя и силой этого завышения. Добавьте сюда сдвиг суждения при обновлении API и провал согласия на 10–15% в узких доменах — и понятно, почему гайды честно пишут: используйте судью для отсева, а не для финального решения.

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

Другой край: доказать, а не уговорить

Здесь в 2026-м поднялась вторая школа, и тон у неё совсем другой.

Её тезис прямой: эмпирические семантические ограждения — фильтры, цензурные правила, оценочные модели — полезны для общего выравнивания контента, но принципиально недостаточны для проверяемых гарантий там, где агент действует с высокими привилегиями. Управлять высокоразмерным поведением автономного агента нельзя эвристическими заплатками на фильтрах — нужны формально разрешимые ограничения. То есть SMT-решатель на основе логики первого порядка, который проверяет, а не оценивает.

И за этим тезисом — уже не одна работа, а целая волна. AgentVerify описывает компоновочную формальную верификацию свойств безопасности агента через темпоральную логику — целостность памяти, протоколы вызова инструментов, обращения к MCP и навыкам, границы human-in-the-loop. VERGE из Amazon связывает LLM с SMT-решателем и маршрутизирует: логические утверждения — символьному решателю, здравый смысл — ансамблю моделей. substrate-guard прогоняет Z3 по пяти классам вывода ИИ — код, определения инструментов, цепочки рассуждений, CLI-команды, ассемблер железа — и на 135 кейсах даёт 100% точность с нулём ложных срабатываний, ловя баги, которые тесты пропустили бы. А Formal Decision Traces дают то, чего вероятностные ограждения не могут в принципе: машинно-проверяемый сертификат и свойство полноты — обнаружение любого нарушения, которое вообще можно закодировать.

Показательно, что это не только академия. AWS встроил в Bedrock «Automated Reasoning checks» — автоформализацию политик из естественного языка в SMT-LIB — и назвал это новым классом ответственного ИИ. Идея, на которую ты поставил, дозрела до продукта у гипермасштабера.

У жёсткой проверки своя цена

Но честный лонгрид обязан сказать и то, чего адепты формальных методов не любят повторять.

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

Второе — формальная строгость покупается охватом. Показателен ARc от AWS: нейросимвольное ограждение, превысившее 99% soundness при проверке ответов на соответствие политикам — недостижимая для других подходов гарантия. Но эта строгость стоит recall: при soundness выше 99% полнота — 15,6%. То есть система скорее зарубит спорное, чем ошибочно одобрит. И авторы прямо называют это намеренным выбором: в безопасно-критичных доменах ложное одобрение куда дороже ложного отказа, поэтому консерватизм — не баг, а проектное решение.

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

Не «или», а «где»

И вот к чему сходится зрелая мысль 2026 года: это не выбор одного лагеря, а вопрос распределения.

Формальную верификацию — туда, где действие безопасно-критично, необратимо, с высокими привилегиями. Мягкое судейство — туда, где задача открытая и субъективная: связно ли написано, вежливо ли, уместен ли тон. VERGE так и устроен — маршрутизирует утверждения по типу. Anthropic для кодовых и диалоговых агентов прямо рекомендует гибрид: юнит-тесты на корректность плюс LLM-рубрики на общее качество. Verifiable rewards отвечают на «решил ли», рубрики — на «объяснил ли безопасно». Никто всерьёз не утверждает, что один механизм закрывает всё.

Ключевое слово не «или», а «где». На какой класс действия какую проверку.

Почему это твой сюжет

Тут стоит назвать вещи прямо, потому что это ядро ASI-5.

Хорошая новость: поле сходится ровно туда, на что ты поставил. «Семантических ограждений недостаточно для высокопривилегированных операций, нужна независимая рантайм-верификация на формально разрешимых ограничениях» — это почти дословная формулировка твоего подхода, и в 2026-м её произносят сразу несколько серьёзных команд. Это сильно де-рискует тезис: ты не один такой странный, идея валидируется независимо.

Но та же новость несёт трезвую часть. Раз идею произносят AWS, Amazon Science и академические группы — значит, сама по себе формальная верификация ИИ уже не твой ров. SMT-проверкой действий агента занимаешься не только ты. Поэтому твоё преимущество обязано лежать не в «мы придумали проверять через Z3», а в другом: в суверенно-регулируемой нише, куда AWS и Amazon по юрисдикции не пойдут; в конкретной инженерии — градиент необратимости R0–R5, fail-closed, хеш-цепочка журнала; и в том, чтобы быть слоем гарантий под той самой плоскостью оркестрации, о которой был прошлый лонгрид.

И градиент R0–R5 — это и есть твой ответ на «не или, а где». Ты не доказываешь всё подряд (это уперлось бы в тот самый recall и семантический зазор) и не доверяешь всему судье. Ты решаешь, что именно прогнать через жёсткую проверку, а что пропустить как обратимое. То самое распределение, к которому поле только подходит, у тебя зашито в архитектуру как ось.

Что это значит

Мягкая проверка — масштабируемая, дешёвая, незаменимая для открытого и субъективного, но предвзятая и без гарантий; консенсус в ней не равен правильности. Жёсткая — даёт математическую гарантию, но узко и ценой охвата. Зрелый ответ 2026-го — не лагерь, а маршрутизация: формальное на необратимое, мягкое на остальное.

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

Источники

LLM-as-judge, исток: Zheng et al., UC Berkeley, 2023 (MT-Bench)
Adaline: LLM-as-a-Judge bias (>50% ошибок в проде), 2026
RAND Judge Reliability Harness — Sandler et al., март 2026
Position/verbosity/self-preference bias: arXiv:2406.07791; NeurIPS 2024 (self-preference)
VERGE — Amazon Science / arXiv:2601.20055 («консенсус ≠ корректность»)
AgentVerify — preprints.org 202604.1029 (LTL model checking свойств безопасности агента)
substrate-guard — arXiv:2603.21149 (Z3, 5 классов вывода, 100% / 0 ложных)
Formal Decision Traces — researchsquare rs-8736256 (полнота против вероятностных ограждений)
ARc — Bayless et al., AWS, arXiv:2511.09008 (>99% soundness, 15,6% recall)
AWS Bedrock Automated Reasoning checks (автоформализация NL → SMT-LIB)