Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Удаление одного навыка из малой нейросети при сохранении другого научились подтверждать формальным доказательством для целой области входов, а не набором тестов. Работа AIUB охватила примерно в 9 раз больше измерений возмущения, чем мог обработать точный решатель, но препринт не рецензирован, а результаты получили сами авторы. Для продуктовых команд это пока не готовая проверка больших LLM, а схема более строгого контроля правок модели.
Метод проверяет поведение после механистического редактирования: отключения нейронов, изменения весов или сдвига активаций. Для заданной области входов система доказывает два утверждения: удалённый навык нигде не проявляется, а выбранный полезный навык продолжает работать. Сети с кусочно-линейными операциями кодируют как логическую задачу и передают точному решателю; для трансформера с softmax и LayerNorm используют распространение гарантированных границ, которое даёт надёжную, хотя не всегда точную оценку.
Конечный детерминированный тест через API такой гарантии дать не может. В построенном примере правка прошла сетку из 40 401 точки, однако навык сохранился в полосе шириной 0,0006 между соседними точками, расположенными с шагом 0,002. Формальный решатель нашёл этот участок, потому что проверял всю непрерывную область, а не отдельные запросы.
Способ правки тоже повлиял на результат. Отключение нейронов и изменение весов позволяли удалить один навык без доказуемого ущерба для другого, если их цепи были разделены. Сдвиг активаций постепенно сокращал область, где сохранялся полезный навык; в опыте с трансформером подходящей величины сдвига, которая одновременно выполняла оба условия, не нашлось.
Проверки охватывают небольшие сети: от игрушечных ReLU-моделей до стандартного трансформера с softmax и LayerNorm. Навыки задавали вычислимыми правилами, поэтому результат можно было однозначно признать правильным или ошибочным. Гарантия действует для последовательностей токенов и непрерывных областей в пространстве эмбеддингов, но не переносится автоматически на опасные способности реальных LLM, для которых сначала нужно формально определить само запрещённое поведение.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.



