Когда ИИ переходит от безобидных советов к автономным действиям — бронированию билетов, оплате счетов или развертыванию кода — индустрия упирается в кризис доверия. Классические методы безопасности вроде электронных подписей здесь бесполезны: они подтверждают автора сообщения, но ничего не говорят о том, безопасно ли само действие. В свежем препринте Мердок Дж. Габбай из Университета Хериота-Уатта предлагает сменить парадигму: перейти от доверия к источнику к доверию на основе математических улик — криптографических сертификатов валидности.
От логических предикатов к полиномиальным ограничениям
Техническое изящество подхода Габбая заключается в «арифметизации» безопасности. Условия политики сначала формулируются как логические предикаты первого порядка, а затем компилируются в систему полиномиальных ограничений. Это позволяет агенту генерировать лаконичное криптографическое свидетельство — если нужно, с использованием доказательств с нулевым разглашением (ZKP). В итоге система доказывает, что намерение соответствует правилам, не раскрывая при этом ни веса модели, ни архитектуру, ни чувствительные данные.
«Не верьте действию из-за его происхождения; верьте ему, потому что оно несет криптографически проверяемые доказательства корректности».
Этот метод работает как продвинутый аналог концепции доказательного кода (proof-carrying code). Для верификатора выгода очевидна: ему больше не нужно слепо доверять вендору или «пересчитывать» логику выводов нейросети, тратя огромные ресурсы. Благодаря компактности ZK-доказательств проверка остается быстрой, даже если логика под капотом перегружена нюансами. Это та самая золотая середина между невозможным полным аудитом кода «черного ящика» и наивной верой в корпоративные лозунги о безопасности.
Мост между формальными методами и управлением агентами
Архитектура Габбая универсальна и не привязана к конкретному софту. Хотя сейчас основной запрос идет от разработчиков агентского ИИ, трансляция спецификаций в криптографические сертификаты применима везде, где одна сторона должна доказать свою честность другой. По оценке автора, такой подход превращает комплаенс из посмертного анализа логов в обязательное условие для выполнения любого действия. Проще говоря: нет доказательства — нет доступа к API.
Главным барьером остается вычислительная сложность генерации таких доказательств и, что более важно, проблема формализации. Перевести абстрактные этические нормы или размытые бизнес-правила на жесткий язык логических предикатов — задача не из легких. Мы вступаем в эпоху, где стоимость верификации станет ключевым проектным ограничением.
Будущее корпоративного ИИ теперь напрямую зависит от того, научатся ли системы доказывать свою лояльность математически. Пока теоретики прокладывают путь к автономной безопасности, практикам придется осваивать роль переводчиков с человеческого «не навреди» на язык полиномов. В мире, где агенты распоряжаются деньгами и инфраструктурой, вера в «добрую волю» разработчика становится непозволительной роскошью.