Предмет исследования, рыночное окно, фазы работы
Институт реализует исследовательскую программу в области формальной верификации действий искусственного интеллекта для регулируемых отраслей. Предмет — слой доверия, надстраиваемый над автономным агентом: каждое необратимое действие транслируется в формальную спецификацию и проходит математическую проверку на соответствие заданной аксиоматике до исполнения. Одно из ключевых свойств такого контура — верифицируемый суверенитет пользователя: действия агента доказуемо соответствуют декларированным интересам конечного пользователя и не могут быть скрытно подчинены интересам оператора платформы.
В течение ближайших 12–18 месяцев в Российской Федерации формируется регуляторно-рыночная пустота между экосистемными агентами крупных платформ и становящимися недоступными зарубежными моделями. В эту пустоту вытесняются профессиональные категории пользователей, для которых платформенная оптимизация несовместима с их фидуциарной, профессиональной или регуляторной ответственностью. Программа формирует ответ на эту пустоту: референс-архитектуру и методологию развёртывания суверенно-пользовательских агентов внутри периметра заказчика, на открытом технологическом стеке, без платформенной привязки.
Программа сопровождается производственной референсной реализацией MITR — мультиагентной системой в непрерывной эксплуатации с 24 апреля 2026 года. MITR обеспечивает Фазу 0 программы и служит операционной средой, в которой институт проверяет инварианты, формализует политику и измеряет поведение. Научная задача Фазы I — перевод архитектурных принципов MITR из императивной реализации в формализованную, верифицируемую через SMT-аппарат.
Верификация действий ИИ · Neurosymbolic AI · SMT · QF_UFLIA · Суверенный микро-прувер · AstraVer · On-Premise · 187-ФЗ · 117-ФСТЭК · ГОСТ Р 56939-2024 · ГОСТ Р 57580
Элемент научной новизны
Доминирующая парадигма безопасности автономных систем на основе больших языковых моделей опирается на поведенческое выравнивание — обучение с подкреплением по отзывам (RLHF) и Constitutional AI. Оба подхода зависят от способности самой вероятностной модели интерпретировать и соблюдать текстовые принципы и потому не дают формальной гарантии: они остаются уязвимыми к состязательным атакам, скрытому дрейфу поведения и логическим противоречиям в политиках. Никакое увеличение объёма обучения не превращает поведенческую тенденцию в доказательство.
Институт разрабатывает альтернативу: управляющий контур автономного агента как аксиоматическую нормативную среду, проверяемую формальными методами. Декларированные пользователем интересы, регуляторные требования и корпоративные политики формализуются как аксиомы; каждое действие транслируется в строго типизированную спецификацию и проходит проверку SMT-решателем до исполнения. Действия без доказательства корректности блокируются архитектурно, а не поведенчески.
Граница гарантии формулируется честно. Контур обеспечивает Soundness — разрешённое действие не нарушает формализованную политику. Корректность перевода нормы в аксиоматику (семантика) остаётся за уполномоченным специалистом: ограниченная грамматикой генерация (constrained decoding) гарантирует только синтаксис, а защита от семантического сдвига достигается обратной трансляцией спецификации в естественный язык для аудита человеком до запуска решателя. Контур вооружает человека-в-контуре проверяемым основанием, а не заменяет его.
Принципиальное отличие от известных работ. Формальная верификация программного кода применяет решатели к статическим артефактам — программа применяет их к динамическому управляющему контуру агента, до исполнения, в асинхронном режиме. Ограниченное декодирование отвечает за синтаксис вывода — программа адресует семантику и логические следствия действия. Constitutional AI выравнивает поведенческие тенденции — программа устраняет техническую возможность исполнить действие, не выводимое из аксиоматики.
О вычислительной сложности — без приукрашивания. Сильная сторона подхода в том, что проверке подвергается не весь смысловой контекст, а изолированный строго типизированный предикат. Задача выполнимости в выбранной теории QF_UFLIA разрешима (проверка всегда завершается) и при этом NP-полна — гарантии полиномиального времени нет; в худшем случае возможен экспоненциальный рост, который на узких практических спецификациях гасится эвристиками современных решателей (CDCL(T)) и сводится к миллисекундным задержкам. Промышленная масштабируемость SMT-подхода подтверждена практикой глобальных эксплуатантов на уровне миллиардов проверок в сутки (Amazon Zelkova).
Программа Института впервые в российской научно-инженерной практике объединяет эти компоненты в единую референс-архитектуру, пригодную для локального развёртывания внутри периметра корпоративных и государственных заказчиков под требования российского регуляторного контура.
Рыночное окно
Институциональная среда Российской Федерации проходит фазу быстрого формирования собственного регуляторного контура по использованию автономных систем на основе искусственного интеллекта. Этот процесс сопровождается одновременным действием двух факторов, формирующих устойчивый сегмент профессионального спроса, который не обслуживается ни одним из существующих классов решений.
Первый фактор — экосистемная оптимизация крупных отечественных платформ. Продукты на основе больших языковых моделей, развиваемые российскими технологическими гигантами, конструктивно подчинены логике удержания пользователя внутри экосистемы оператора: бизнес-модель предполагает перехват внимания и кросс-селл внутрисистемных сервисов. Для значительной части корпоративных и профессиональных сценариев этот режим работы несовместим с требованиями конфиденциальности, фидуциарной ответственности и независимости суждения.
Второй фактор — постепенное ограничение доступа к зарубежным моделям в профессиональных сценариях. Требования локализации данных, подготавливаемое регулирование «доверенного» и «суверенного» искусственного интеллекта, ограничения для объектов критической информационной инфраструктуры и правовой режим профессиональных тайн (адвокатской, врачебной, аудиторской) делают применение внешних облачных API в корпоративном контуре юридически рискованным или прямо неприемлемым.
На пересечении этих факторов формируется сегмент профессиональных пользователей, не обслуживаемых ни одним из существующих классов решений: банки и финансовые организации с фидуциарной ответственностью; медицинские организации; адвокатские и юридические образования; операторы критической информационной инфраструктуры; государственные информационные системы; корпоративные подразделения комплаенса и внутреннего аудита. Программа института формирует ответ на этот сегмент — класс агентов, совместимых одновременно с требованиями российской регуляторной рамки и с интересами конечного пользователя.
Техническая база
Программа опирается на зрелую базу открытых решений для языкового и оркестрационного аппарата и создаёт собственное верификационное ядро — именно оно является результатом интеллектуальной деятельности Института.
Языковой аппарат — открытые большие языковые модели локального развёртывания, в том числе компактные отечественные модели, адаптированные под русский язык; модуль заменяем, что обеспечивает независимость от поколения моделей и от одного поставщика.
Оркестрационный аппарат — лёгкие агентные рантаймы (CrewAI, AutoGen, LangGraph). Принципиальное дополнение Института — встроенный слой формальной верификации политики, отсутствующий в существующих оркестраторах: каждый вызов инструмента транслируется в логику первого порядка и проверяется до исполнения.
Верификационное ядро (собственная разработка). На исследовательском стенде проверка ведётся решателем Z3 (Microsoft Research) как референсом метода. Целевой результат — суверенный доверенный микро-прувер: компактная реализация процедуры разрешения под разрешимой теорией QF_UFLIA в доверенной среде, без зависимости от иностранных библиотек в ядре. Компактность кода открывает путь к дедуктивной верификации самого прувера инструментами ИСП РАН (AstraVer, платформа Frama-C / Why3, спецификации ACSL) и к оценке соответствия по уровням доверия ФСТЭК (ОУД, Приказ ФСТЭК России № 76) с разработкой безопасного ПО по ГОСТ Р 56939-2024. Протоколы переходов и состояния безопасного отказа специфицируются и проверяются модельно (TLA+); глубокая корректность процедуры разрешения и кодогенерации — интерактивным доказательством (Rocq, бывш. Coq). Ядро решателя исполняется на стандартных серверных процессорах и не требует специализированного оборудования.
Фазы программы
Программа разворачивается по четырём фазам. На каждой фазе фиксируются материальные результаты, пригодные для институциональной и научно-технической экспертизы.
Фаза 0. Производственная референсная реализация (текущая)
Цель фазы — рабочая мультиагентная система, реализующая архитектурные принципы программы на императивном уровне в режиме непрерывной эксплуатации.
Состояние фазы. Система MITR в производственной эксплуатации с 24 апреля 2026 года, режим непрерывный. Обслуживает фидуциарные задачи оператора в закрытом периметре: работа с почтовыми очередями, управление календарём, сопровождение юридических дел, ведение рабочих заметок, обработка голосового ввода. Реализованы четыре независимых слоя верификации действий, многослойная память с провенансом, audit trail в формате 117-го приказа ФСТЭК, тестовая база свыше ста сорока модульных тестов.
Материальные результаты фазы. Действующий прототип агентного рантайма с встроенными слоями верификации, демонстрирующий устойчивость к состязательным атакам на политику. Методологическая документация в формате архитектурных решений (ADR). Нумерованная дорожная карта научно-исследовательских и опытно-конструкторских работ.
Данная фаза обеспечивает операционную устойчивость в рамках одного оператора, но не предоставляет математической гарантии корректности, необходимой для регулируемых профессиональных сред. Эта задача составляет содержание Фазы I.
Фаза I. Формализация архитектуры и научная программа
Цель фазы — формализация архитектурных принципов MITR через формальные методы; превращение императивных гарантий в доказуемые. Фаза реализуется как научная программа под государственную поддержку.
Содержание фазы. Пять исследовательских milestone-ов, каждый сопровождается письменным артефактом (ADR / научный препринт) и тестовым покрытием:
- Schema-validation слой между LLM-выводом и executor’ом. Закрывает класс ошибок, связанных с malformed-параметрами критических действий.
- Внешняя политика как редактируемый артефакт. Формат, версионирование, hot-reload, hash-attestation.
- Расширение SMT-верификации с пилотного класса на полное покрытие класса деструктивных действий. Формализация политик, бенчмарк latency, состязательные кейсы.
- Активация эпистемического контура на slice-выборках долгосрочной памяти. Confidence-aware retrieval, метрики качества выборки.
- Challenge pass MVP. Автоматический пересмотр уверенности записей памяти на еженедельной основе. Audit-журналирование изменений уверенности.
Материальные результаты фазы. Формализованная референс-спецификация архитектуры, пригодная для передачи в экспертизу. Действующий прототип с расширенным SMT-слоем верификации политики, (референс — Z3) с модельной проверкой протоколов безопасности и безопасного отказа в TLA+ , функционирующий в изолированной среде. Первые публикации института в формате технических отчётов и научных препринтов. Регистрация программных компонентов в реестре отечественного программного обеспечения.
Фаза II. Референс-архитектура и пилотные внедрения
Цель фазы — упаковка методологии в воспроизводимую референс-архитектуру, пригодную для развёртывания внутри периметра заказчика, и проведение пилотных внедрений с первыми институциональными партнёрами в профильных сегментах.
Материальные результаты фазы. Референс-архитектура с сопроводительной документацией и инструментарием развёртывания. Пилотные внедрения у первых партнёров в сегментах, наиболее чувствительных к требованию суверенитета пользователя: профессиональная юридическая практика, медицинские организации, корпоративные подразделения комплаенса. Первая редакция базы формальных аксиом для типовых регуляторных контуров (187-ФЗ, 117-ФСТЭК, ГОСТ Р 57580). Аттестация по требованиям защиты информации для конкретных объектов первых пилотов.
Начало разработки суверенного микро-прувера под QF_UFLIA и его дедуктивной верификации (AstraVer, Frama-C / Why3) на пути к оценке соответствия по уровням доверия ФСТЭК.
Фаза III. Институт как носитель стандарта
Цель фазы — закрепление института как методологического и экспертного центра по архитектуре суверенно-пользовательских агентов в российской юрисдикции.
Материальные результаты фазы. База формальных аксиом, покрывающая основные регуляторные контуры и отраслевые стандарты, с режимом регулярного обновления. Образовательные программы дополнительного профессионального образования для корпоративных и государственных специалистов. Участие института в формировании отраслевых и национальных стандартов по архитектуре автономных систем с формальными гарантиями корректности.
В том числе сертификация верификационного ядра по уровням доверия ФСТЭК (ОУД)
Коммерциализация
Результаты исследовательской программы институт переводит в коммерциализуемую форму по трём направлениям, юридически закреплённым в уставной деятельности. Эта структура совпадает со структурой трёх контуров деятельности института и обеспечивает его операционную устойчивость за счёт диверсификации источников выручки.
Первое направление — лицензирование референс-архитектуры и методологии суверенно-пользовательских агентов корпоративным и государственным заказчикам для развёртывания внутри их периметра.
Второе направление — инженерное сопровождение внедрений: адаптация архитектуры под конкретные отраслевые контексты заказчика, разработка специализированных компонентов политики, интеграция с существующей информационной инфраструктурой.
Третье направление — подписочное обновление базы формальных аксиом, сопровождающее изменения в регуляторном контуре и отраслевых стандартах; эта модель формирует устойчивый источник рекуррентной выручки и одновременно обеспечивает заказчику непрерывное соответствие меняющимся требованиям регулятора.
Дополнительным направлением является передача знания: программы дополнительного профессионального образования для специалистов заказчика, участие в формировании отраслевых стандартов, экспертные заключения для регуляторов. Это направление имеет самостоятельную коммерческую ценность и одновременно выступает механизмом формирования профессионального сообщества вокруг методологии института.
Риски и устойчивость
Институт явно фиксирует четыре категории рисков и подходы к их минимизации.
Регуляторный риск
Возможное ужесточение требований к сертификации автономных систем в Российской Федерации может усложнить процедуру лицензирования независимых разработок. Программа рассматривает эту динамику не как угрозу, а как основание собственного позиционирования. Архитектура формальной верификации по своей природе является инструментом прохождения регуляторной экспертизы: институт не конфликтует с регулятором, а предоставляет ему методологический эталон для формирования будущих стандартов доверенного искусственного интеллекта. Адвокатская и аудиторская экспертиза научного руководителя обеспечивает прямое взаимодействие с правовым контуром на стадии проектирования архитектуры.
Технологический риск
Применение SMT-решателей к задачам неограниченной сложности теоретически сталкивается с вычислительным взрывом. В архитектуре программы риск структурно ограничен: решателю передаётся не весь смысловой контекст, а строго типизированный изолированный предикат. Теория QF_UFLIA разрешима (проверка завершается всегда) и NP-полна — гарантии полиномиального времени нет, но на узких практических спецификациях экспоненциальный рост гасится эвристиками решателя, и проверка занимает миллисекунды. Масштабируемость подтверждена промышленной практикой на уровне миллиардов проверок в сутки.
Конкурентный риск
Вероятность быстрого выхода крупных российских платформ в сегмент суверенно-пользовательских агентов структурно ограничена. Бизнес-модель экосистемных игроков построена на монетизации пользовательского внимания и данных внутри собственного контура; развёртывание агента, физически отключённого от экосистемы оператора и не пополняющего корпоративные массивы данных, противоречит их экономическим интересам. Институт формирует нишу, в которую крупные платформы не войдут по конструктивным основаниям, а не по недостатку ресурсов.
Репутационный риск
Институт сознательно избегает публичной конкуренции с существующими платформенными игроками на их территории массовых потребительских продуктов. Позиционирование программы — инфраструктурное программное обеспечение институционального уровня, работающее в симбиозе, а не в конкуренции с генеративными моделями. Это обеспечивает устойчивость репутационного контура и возможность взаимодействия с регуляторами и отраслевыми ассоциациями в нейтральном статусе методологического центра.
Критерии вхождения в программу
Институт не работает с массовым рынком и не принимает обращения общего характера. Программа открыта для трёх категорий контрагентов, соответствующих её текущей фазе.
Пилотные партнёры из профильных отраслей — организации, для которых требование суверенитета пользователя является не декларативным, а операционным: профессиональные практики с фидуциарной ответственностью, медицинские и образовательные организации, корпоративные подразделения комплаенса, государственные информационные системы. Форма взаимодействия — совместное пилотное внедрение с обоюдной готовностью к тесной рабочей коммуникации на стадии адаптации архитектуры.
Институциональные партнёры и инвесторы, рассматривающие программу как долгосрочную стратегическую позицию в формирующемся сегменте. Форма взаимодействия — партнёрские и инвестиционные переговоры по закрытому контуру, с раскрытием материалов по мере продвижения.
Академические и отраслевые научные структуры, профильные по направлениям формальной верификации, многоагентных систем, правовых оснований автономных технологий. Форма взаимодействия — совместные исследовательские программы, экспертные советы, участие в диссертационных работах.
Заключительное положение
Программа института реализуется в форме, в которой каждый этап оставляет материальный след — действующий прототип, формальную спецификацию, публикуемые артефакты, пилотные внедрения. Это позволяет регуляторной, академической и инвестиционной экспертизе оценивать состояние программы по проверяемым результатам, а не по декларативным намерениям.
Фаза 0 предъявлена в работающем виде. Фаза I открыта для государственной поддержки и квалифицированной экспертной оценки. Фазы II и III оформляют долгосрочный горизонт института как методологического центра по архитектуре автономных систем с формальными гарантиями корректности.
Обращения общего характера не рассматриваются.
Telegram-канал
Системный синтез
Искусственный интеллект на пересечении технической и юридической реальности.