Материал подготовлен автоматически по первоисточникам: ссылки на них — в конце статьи.
Автоматический проверяющий модуль для самообновляющейся системы нельзя сделать одновременно безошибочным и открытым для любого полезного обновления. В работе DFKI и RPTU Kaiserslautern-Landau показано, что ограничение сохраняется даже после замены проверки поиском подходящего варианта, хотя препринт не рецензирован и результаты получены самими авторами. Для продуктовой архитектуры вывод прямой: строгие гарантии появляются только после явного ограничения времени проверки и числа кандидатов.
Систему представили как программу, которая предлагает изменить собственный код, модель, подсказку или правила работы с инструментами. Проверяющий модуль должен завершить работу и принять либо отклонить обновление, тогда как его реальная польза может зависеть от сколь угодно долгого поведения программы.
В доказательстве кандидат учитывает решение проверяющего модуля. Если его принимают, он ведёт себя не лучше исходной версии; если отклоняют — становится улучшением. Любое решение поэтому нарушает одно из требований: модуль либо пропускает бесполезное изменение, либо блокирует полезное.
Замена проверки поиском не решает проблему. Даже если процедура должна лишь выбрать один полезный вариант из списка, механизм предложений может сформировать кандидат, поведение которого зависит от результата поиска. Случайный выбор с ограниченной вероятностью ошибки также не даёт универсальной гарантии.
Гарантии возвращаются в режиме, который ближе к реальным контурам разработки: проверка ограничена по времени, а число предложений заранее конечно. Тогда все варианты можно последовательно выполнить и выбрать улучшение относительно измеряемого показателя. Но этот показатель остаётся заменой настоящей цели: в построенной авторами цепочке каждое принятое обновление повышает ограниченную оценку, а реальное качество на каждом шаге падает.
Работа рассматривает произвольные исполняемые артефакты и семантическую оценку их поведения, а не конкретные LLM или бенчмарки. Поэтому доказательство задаёт предел для универсальных гарантий, тогда как практическая надёжность зависит от выбранных лимитов, тестов и того, насколько измеряемый показатель соответствует цели продукта. Основные теоремы дополнительно формализованы в Lean 4.
Источники
Похоже на вашу задачу?
Расскажите, что собираете. За полчаса разложим на этапы и назовём сроки — это бесплатно и ни к чему не обязывает.
