Асимметрия как методологический и инструментальный принцип тестирования моделей

Цель статьи – показать практический потенциал идеи асимметрии: она возникла как логико-риторическое правило, а сегодня стала реальным методологическим и инструментальным вектором в разработке ИИ.

Фактор логики

Отношение категорий «доказать» и «опровергнуть» имеет асимметричную логическую структуру – один точно подобранный контрпример опровергает утверждение с квантором общности, при этом любое число подтверждающих случаев его не доказывает. Иначе говоря, никаким количеством и качеством подтверждающих аргументов, тестов, экспериментов нельзя доказать общее суждение. Индуктивное умозаключение выполняет не доказательную функцию, а увеличивает степень правдоподобия вывода. Все это известно еще
со времен Аристотеля.

В среде IT эта асимметрия знакома по формуле Эдсгера Дейкстры с конца 1960-х в формулировке «тестирование способно показать наличие ошибок
и никогда не покажет их отсутствия».

О чем мы говорим конструктивно, или методологические следствия для тестирования

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

Отсюда методологические следствия:

1. Для рутинных свойств тестирование остается законным инструментом, но критерий успеха переворачивается по принципу асимметрии. Целью становится найти сбой или опровергающий случай для последующего исправления. Для этого нужны структурированные отчеты об обнаруженных ошибках, логи выполнения и атрефакты для воспроизведения сбоев. Этим объясняется сегодняшняя мода на фаззинг-тестирование и такого рода пример мы покажем в виде карты сбоев в следующей статье.

2. Для свойств, которые формальную спецификацию не допускают по своей природе, но требуют оценки количественного риска, работающим механизмом является статистическая гарантия. Правило трех и конформное предсказание покажут результат с известной уверенностью для заданного распределения входов, а сертифицированная робастность методом случайного сглаживания – для окрестности конкретного входа. Здесь плюс в том, что хотя доказательства мы и не получаем, но точно осознаем границы сделанного вывода.

3. Для критичных свойств, где высокая цена ошибки, корректным будет только формальное доказательство. Еще раз повторим, что тестировать в этом случае смысла нет, какими бы замечательными ни были инструменты, поскольку доказать подтверждающими случаями нельзя в принципе. Конечно, формально доказать можно далеко не каждое свойство, да и ресурсов может не хватить, но возвращение к 1 пункту – тоже не законный общий выход, его искать придется конкретно и, возможно, частично, а даже если и обращаться к тестированию, то результат должен формулироваться очень аккуратно. Асимметрия не требует доказывать все. Она требует не путать свидетельство с доказательством. Разница в той черте, которая отделяет корректное описание системы, совместимой с некоторым свойством, от нелегитимного перехода и приписывания ей этого свойства.

Поиск контрпримера

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

Работа Apple GSM-Simbolic показывает насколько он сильнее накопления подтверждений. На задачах школьной математики GSM8K сильные модели набирали больше 90%. Однако стоило добавить в задачу одну правдоподобную фразу, в общем-то для решения несущественную (например, что пять из собранных киви были чуть меньше обычного), и точность у всех проверенных моделей падала – у сильных моделей на 17-40 процентных пунктов, у более слабых до 65.

О дисциплине опровержения

Логически самое простое действие опровержения требует той же методологической строгости, что и доказательство.

Для опровержения логика определяет достаточность одного контрпримера. Но на практике тест работает с конъюнкцией допущений и сбой сразу не покажет какое из них ложно, нужно организовать сам тест таким образом, чтобы интерпретация результата точно могла отнести вывод к проверяемому. Иначе он о чем? О модели, о промпте, о системе оценки или лимите генерации? А может об эталонном ответе или способе разбора ответа?

Хороший пример показывает история работы Apple «The Illusion of Thinking» 2025 года. Авторы сообщили, что рассуждающие модели падают до нулевой точности на головоломках выше определенной сложности. Ответный комментарий указал, что часть заданий вообще не имеет решения, а полный список ходов для больших Ханойских башен рискует не уместиться в лимит выходных токенов, о чем и сами модели писали в ответах. Независимая повторная проверка на одной модели подтвердила довод о неразрешимых задачах, а вот провалы в Ханойской башне в довод не уложились – при пошаговом решении модель все равно сбивалась. Иначе говоря, контрпримеры отчасти оказались артефактами постановки эксперимента.

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

Что остается у бенчмарков?

На бенчмарке принцип асимметрии выглядит следующим образом. 94,3% у Gemini 3.1 Pro на GPQA Diamond – это n подтверждающих случаев, которые повышают доверие к работе модели, но ни в коем случае не доказывают, что она «рассуждает на уровне PhD». Приписывать модели понимание на основе красивой цифры – грубая логическая ошибка.

Бенчмарки не дают доказательства, но обоснованно усиливают степень правдоподобия или доверия выводу. Накопление подтверждающих случаев реально полезно, когда мы сравниваем модели или ловим регресс (например, новая версия вдруг проседает там, где раньше работала безупречно), поэтому бенчмарки имеют смысл, и это очевидно.

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

Показательный случай – та самая цифра 94%. В ней скрыты два индуктивных перехода.

Первый ведет от выборки задач к распределению, из которого она взята. Это переход статистически контролируем при условиях независимости задач, отсутствии их в обучающих данных и при истинности эталонных ответов. Здесь работает, например, «правило трех»: если на n задачах, независимо взятых из распределения, не случилось ни одного сбоя, то с уверенностью 95% частота сбоев на этом распределении меньше примерно 3/n. Тысяча задач без сбоя дает верхнюю границу около 0,3%. И это максимум того, что дает накопление подтверждающих случаев, поскольку прямо указаны граница – оценка верна только для распределения, на котором взяты задачи.

Второй переход ведет от поведения на распределении к способности модели «рассуждать на уровне PhD». Способность рассуждения здесь относится к открытому классу ситуаций, включая и те, которые не похожи на тестовые, а значит, статистика ее обосновать не может.

Асимметрия говорит о втором переходе. Грубая логическая ошибка, о которой мы говорили в начале, совершается в тот момент, когда оценка доли верных ответов начинает читаться как описание способности.

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

Проверка конкретного результата

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

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

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

Выводы в таблице

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