Программа

Предмет исследования, рыночное окно, фазы работы и критерии вхождения в программу

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

В течение ближайших 12–18 месяцев в Российской Федерации формируется регуляторно-рыночная пустота между экосистемными агентами крупных платформ и становящимися недоступными зарубежными моделями. В эту пустоту вытесняются профессиональные категории пользователей, для которых платформенная оптимизация несовместима с их фидуциарной, профессиональной или регуляторной ответственностью. Программа формирует ответ на эту пустоту: референс-архитектуру и методологию развёртывания суверенно-пользовательских агентов внутри периметра заказчика, на открытом технологическом стеке, без платформенной привязки.

User-Sovereign Agents · SMT · Z3 · Neurosymbolic AI · Compliance by Design · On-Premise · 187-ФЗ · 117-ФСТЭК · ГОСТ Р 57580

Элемент научной новизны

Доминирующая парадигма обеспечения безопасности автономных систем на основе больших языковых моделей базируется на поведенческом выравнивании — обучении с подкреплением на основе отзывов (RLHF) и архитектуре Constitutional AI. Оба подхода опираются на способность модели самостоятельно интерпретировать и соблюдать набор текстовых принципов.

В научной литературе последних двух лет эта парадигма признана фундаментально ограниченной. Задача семантической самоверификации — способности системы достоверно оценивать корректность собственной интерпретации директив — формализована и доказана как NP-полная. Это означает, что никакое увеличение вычислительной мощности или объёма обучения не устраняет структурной уязвимости вероятностного выравнивания к состязательным атакам, скрытому дрейфу поведения и логическим противоречиям в политиках.

Институт разрабатывает альтернативу: управляющий контур автономного агента как аксиоматическую нормативную среду, верифицируемую формальными методами. Декларированные пользователем интересы, регуляторные требования и корпоративные политики формализуются как набор аксиом в логике первого порядка. Каждое действие агента — вызов инструмента, обращение к внешней системе, принятие решения — транслируется в формальную спецификацию и проходит проверку промышленным SMT-решателем (Satisfiability Modulo Theories) до исполнения. Действия, не получившие доказательства корректности, блокируются архитектурно, не поведенчески.

Принципиальное отличие от известных работ. Исследования в области формальной верификации программного кода применяют SMT-решатели к статическим артефактам; программа применяет их к динамическому управляющему контуру агента в реальном времени. Методы ограниченного декодирования (constrained decoding) обеспечивают синтаксическую корректность вывода языковой модели, не затрагивая семантической безопасности действия; программа верифицирует именно семантику и логические следствия. Работы по Constitutional AI выравнивают поведенческие тенденции модели; программа устраняет саму техническую возможность отклонения от аксиоматики. Работы по агентным политикам в многоагентных системах, как правило, описывают поведенческие ограничения, не выводимые из формального доказательства; программа формирует среду, в которой любое действие имеет исчислимое основание.

Отдельные компоненты этой архитектуры проходят экспериментальную проверку в мировой исследовательской среде: зафиксировано эмерджентное обращение автономных AI-экосистем к SMT-решателям для обеспечения собственной безопасности (SUBSTRATE S3, 2026); продемонстрирована работа специализированных языков политики с проверкой Z3 за время менее одной миллисекунды на изолированную проверку и нулевой показатель обхода политик при состязательных атаках (CSL-Core, Chimera Specification Language); масштабируемость SMT-подхода подтверждена на уровне миллиардов запросов в день в промышленной эксплуатации (Amazon Zelkova). Программа института впервые в российской научно-инженерной практике объединяет эти компоненты в единую референс-архитектуру, пригодную для локального развёртывания внутри периметра корпоративных и государственных заказчиков под требования российского регуляторного контура.

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

Рыночное окно

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

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

Второй фактор — постепенное ограничение доступа к зарубежным моделям в профессиональных сценариях. Требования локализации данных, подготавливаемое регулирование «доверенного» и «суверенного» искусственного интеллекта, ограничения для объектов критической информационной инфраструктуры и правовой режим профессиональных тайн (адвокатской, врачебной, аудиторской) делают применение внешних облачных API в корпоративном контуре юридически рискованным или прямо неприемлемым.

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

Техническая база

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

Вычислительный аппарат — промышленный SMT-решатель Z3, разработанный Microsoft Research и применяющийся в глобальной практике формальной верификации на уровне миллиардов запросов в сутки. Решатель исполняется на стандартных серверных процессорах и не требует специализированного вычислительного оборудования.

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

Оркестрационный аппарат — лёгкие агентные рантаймы класса CrewAI, AutoGen, LangGraph, демонстрирующие зрелость инженерной базы для построения многоагентных систем. Принципиальное дополнение программы — встроенный слой формальной верификации политики агента, отсутствующий в существующих оркестраторах: каждый вызов инструмента или внешней системы проходит трансляцию в логику первого порядка и проверку SMT-решателем до исполнения. Это превращает потребительский оркестратор в инструмент корпоративного уровня с архитектурной невозможностью отклонения от декларированной политики.

Фазы программы

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

Фаза I. Прототип и формализация методологии

Цель фазы — построение рабочего прототипа агента с интегрированным слоем формальной верификации и формализация методологии в научно-технической и публикационной форме.

Материальные результаты фазы. Действующий прототип агентного рантайма с встроенным SMT-слоем верификации политики, функционирующий в изолированной среде и демонстрирующий устойчивость к состязательным атакам на политику агента. Формализованная референс-спецификация архитектуры, пригодная для передачи в экспертизу. Первые публикации института в формате технических отчётов и программных записок.

Фаза II. Референс-архитектура и пилотные внедрения

Цель фазы — упаковка методологии в воспроизводимую референс-архитектуру, пригодную для развёртывания внутри периметра заказчика, и проведение пилотных внедрений с первыми институциональными партнёрами в профильных сегментах.

Материальные результаты фазы. Референс-архитектура с сопроводительной документацией и инструментарием развёртывания. Пилотные внедрения у первых партнёров в сегментах, наиболее чувствительных к требованию суверенитета пользователя: профессиональная юридическая практика, медицинские организации, корпоративные подразделения комплаенса. Первая редакция базы формальных аксиом для типовых регуляторных контуров (187-ФЗ, 117-ФСТЭК, ГОСТ Р 57580). Регистрация программных компонентов в реестре отечественного программного обеспечения.

Фаза III. Институт как носитель стандарта

Цель фазы — закрепление института как методологического и экспертного центра по архитектуре суверенно-пользовательских агентов в российской юрисдикции.

Материальные результаты фазы. База формальных аксиом, покрывающая основные регуляторные контуры и отраслевые стандарты, с режимом регулярного обновления. Образовательные программы дополнительного профессионального образования для корпоративных и государственных специалистов (ОКВЭД 85.42). Участие института в формировании отраслевых и национальных стандартов по архитектуре автономных систем с формальными гарантиями корректности.

Коммерциализация

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

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

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

Риски и устойчивость

Институт явно фиксирует четыре категории рисков и подходы к их минимизации.

Регуляторный риск

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

Технологический риск

Применение SMT-решателей на задачах неограниченной сложности теоретически сталкивается с проблемой вычислительного взрыва. В архитектуре программы этот риск структурно ограничен. Решатель не анализирует весь смысловой контекст действия агента: в него передаются строго типизированные параметры вызова инструмента в виде формальной спецификации. Проверка таких изолированных ограничений занимает субмиллисекундное время и не создаёт задержек в реальной эксплуатации. Масштабируемость подхода подтверждена промышленной практикой глобальных эксплуатантов SMT-решателей на уровне миллиардов запросов в сутки.

Конкурентный риск

Вероятность быстрого выхода крупных российских платформ в сегмент суверенно-пользовательских агентов структурно ограничена. Бизнес-модель экосистемных игроков построена на монетизации пользовательского внимания и данных внутри собственного контура; развёртывание агента, физически отключённого от экосистемы оператора и не пополняющего корпоративные массивы данных, противоречит их экономическим интересам. Институт формирует нишу, в которую крупные платформы не войдут по конструктивным основаниям, а не по недостатку ресурсов.

Репутационный риск

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

Критерии вхождения в программу

Институт не работает с массовым рынком и не принимает обращения общего характера. Программа открыта для трёх категорий контрагентов, соответствующих её текущей фазе.

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

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

Академические и отраслевые научные структуры, профильные по направлениям формальной верификации, многоагентных систем, правовых оснований автономных технологий. Форма взаимодействия — совместные исследовательские программы, экспертные советы, участие в диссертационных работах.