Краткое содержание
Программа — исследовательский план института: формальная проверка действий автономных программ для регулируемых отраслей, от действующей установки до типового комплекса и стандарта.
Предмет — слой доверия над агентом: каждое необратимое действие проверяется решателем по правилу организации до исполнения, и на каждое решение остаётся квитанция.
Фазы: действующая установка MITR (работает с 24 апреля 2026 года), наблюдатели фактов и полное покрытие действий, типовой комплекс и пилотные внедрения, институт как носитель стандарта.
Риски названы по именам — регуляторный, технологический, конкурентный, репутационный — и к каждому записано, чем он снимается; коммерческая сторона изложена на странице «Инвесторам и партнёрам».
Дальше — полный текст; для первого знакомства достаточно разделов «Предмет исследования» и «Фазы программы».
Предмет исследования, рыночное окно, фазы работы
Институт реализует исследовательскую программу в области формальной верификации действий искусственного интеллекта для регулируемых отраслей. Предмет — слой доверия, надстраиваемый над автономным агентом: каждое необратимое действие транслируется в формальную спецификацию и проходит математическую проверку на соответствие заданной аксиоматике до исполнения.
Одно из определяющих свойств такой системы — верифицируемый суверенитет пользователя: действия агента доказуемо соответствуют декларированным интересам конечного пользователя и не могут быть скрытно подчинены интересам оператора платформы.
В течение ближайших 12–18 месяцев в Российской Федерации формируется регуляторно-рыночная пустота между встраиваемыми агентами крупных платформ и становящимися недоступными зарубежными моделями. В эту пустоту вытесняются профессиональные категории пользователей, для которых платформенная оптимизация несовместима с их фидуциарной, профессиональной или регуляторной ответственностью.
Программа формирует ответ на эту пустоту: типовое инженерное устройство и методологию развёртывания суверенно-пользовательских агентов внутри периметра заказчика, на открытом технологическом стеке, без платформенной привязки.
Программа сопровождается производственной референсной реализацией MITR, которая непрерывно работает с 24 апреля 2026 года. MITR обеспечивает Фазу 0 программы и служит операционной средой, в которой институт проверяет инварианты, формализует политику и измеряет поведение. Научная задача Фазы I — перевод инженерных принципов MITR из императивной реализации в формализованную, верифицируемую через SMT-аппарат.
Формальная верификация действий автономных агентов, нейросимвольный искусственный интеллект (AI), выполнимость по модулю теорий (SMT) в бескванторной линейной целочисленной арифметике (QF_UFLIA), суверенный микро-прувер, дедуктивная верификация AstraVer, локальное развёртывание в периметре заказчика, Федеральный закон № 187-ФЗ, Приказ Федеральной службы по техническому и экспортному контролю (ФСТЭК России) № 117, ГОСТ Р 56939-2024 и ГОСТ Р 57580
Элемент научной новизны
Распространённый подход к безопасности автономных систем на основе больших языковых моделей опирается на поведенческое выравнивание — обучение с подкреплением по отзывам (RLHF) и Constitutional AI. Оба подхода зависят от способности самой вероятностной модели интерпретировать и соблюдать текстовые принципы и потому не дают формальной гарантии: они остаются уязвимыми к состязательным атакам, скрытому дрейфу поведения и логическим противоречиям в политиках. Никакое увеличение объёма обучения не превращает поведенческую тенденцию в доказательство.
Институт выстраивает иной подход: управляющий слой контроля автономного агента работает как аксиоматическая нормативная среда, проверяемая формальными методами. Декларированные пользователем интересы, регуляторные требования и корпоративные политики формализуются как аксиомы; каждое действие транслируется в строго типизированную спецификацию и проходит проверку SMT-решателем до исполнения. Действия без математического доказательства допустимости отклоняются программным барьером до исполнения.
Граница гарантии формулируется со всей математической строгостью: MITR гарантирует математическую непротиворечивость (Soundness) — разрешённое действие не нарушает формализованную политику. Корректность перевода нормы в аксиоматику (семантика) остаётся за уполномоченным специалистом: ограниченная грамматикой генерация (constrained decoding) гарантирует только синтаксис, а защита от семантического сдвига достигается обратной трансляцией спецификации в естественный язык для аудита человеком до запуска решателя. MITR сохраняет окончательное решение за ответственным специалистом и даёт ему проверяемое доказательство по каждому шагу.
Принципиальное отличие от известных работ заключается в объекте и моменте проверки: формальная верификация программного кода применяет решатели к статическим артефактам — программа применяет их к динамическому потоку команд агента, до исполнения, в асинхронном режиме. Ограниченное декодирование отвечает за синтаксис вывода — программа адресует семантику и логические следствия действия. Constitutional AI выравнивает поведенческие тенденции — программа устраняет техническую возможность исполнить действие, не выводимое из аксиоматики.
Вычислительная сложность метода оценивается без приукрашивания: сильная сторона подхода состоит в проверке изолированного строго типизированного предиката вместо всего текстового контекста. Задача выполнимости в выбранной теории QF_UFLIA разрешима (проверка всегда завершается) и при этом принадлежит классу недетерминированной полиномиальной полноты (NP) — гарантии полиномиального времени нет; в худшем случае возможен экспоненциальный рост, который на узких практических спецификациях гасится эвристиками современных решателей (CDCL(T)) и сводится к миллисекундным задержкам. Промышленная масштабируемость SMT-подхода подтверждена практикой крупнейших облачных провайдеров на уровне миллиардов проверок в сутки (Amazon Zelkova).
Программа Института объединяет эти компоненты в единый типовой комплекс, пригодный для локального развёртывания внутри периметра корпоративных и государственных заказчиков по требованиям российского законодательства.
Рыночное окно
Институциональная среда Российской Федерации проходит фазу быстрого формирования собственного правового режима по использованию автономных систем на основе искусственного интеллекта. Этот процесс сопровождается одновременным действием двух факторов, которые формируют сегмент профессионального спроса на проверку действий агента внутри периметра заказчика.
Первый фактор связан с платформенной замкнутостью крупных отечественных разработчиков. Продукты на основе больших языковых моделей, развиваемые российскими технологическими гигантами, конструктивно подчинены задаче удержания заказчика внутри собственной облачной среды оператора: бизнес-модель предполагает перехват внимания и кросс-селл внутрисистемных сервисов. Для значительной части корпоративных и профессиональных сценариев этот режим работы несовместим с требованиями конфиденциальности, фидуциарной ответственности и независимости суждения.
Второй фактор — постепенное ограничение доступа к зарубежным моделям в профессиональных сценариях. Требования локализации сведений, подготавливаемое регулирование «доверенного» и «суверенного» искусственного интеллекта, ограничения для объектов критической информационной инфраструктуры и правовой режим профессиональных тайн (адвокатской, врачебной, аудиторской) делают применение внешних облачных программных интерфейсов приложений (API) в корпоративной сети юридически рискованным или прямо неприемлемым.
На пересечении этих факторов формируется сегмент профессиональных пользователей: банки и финансовые организации с фидуциарной ответственностью; медицинские организации; адвокатские и юридические образования; операторы критической информационной инфраструктуры; государственные информационные системы; корпоративные подразделения нормативного соответствия и внутреннего аудита. Программа института отвечает этому сегменту MITR, через который действие любого агента — своего или чужого — проходит до исполнения и допускается только с доказательством, внутри периметра заказчика и по его правилам.
Техническая база
Программа опирается на зрелую базу открытых решений для языкового и оркестрационного аппарата и создаёт собственное верификационное ядро — именно оно составляет защищаемый результат интеллектуальной деятельности института.
Языковой аппарат — открытые большие языковые модели локального развёртывания, в том числе компактные отечественные модели, адаптированные под русский язык; модуль заменяем, что обеспечивает независимость от поколения моделей и от одного поставщика.
Оркестрационный аппарат — лёгкие среды исполнения агентов (CrewAI, AutoGen, LangGraph). Принципиальное дополнение Института — встроенный слой формальной верификации политики, отсутствующий в существующих оркестраторах: каждый вызов инструмента транслируется в логику первого порядка и проверяется до исполнения.
Верификационное ядро выступает собственной разработкой института: на исследовательском стенде проверка ведётся решателем Z3 (Microsoft Research) как референсом метода. Целевой результат — суверенный доверенный микро-прувер: компактная реализация процедуры разрешения под разрешимой теорией QF_UFLIA в доверенной среде, без зависимости от иностранных библиотек в ядре.
Компактность кода открывает путь к дедуктивной верификации самого прувера инструментами Института системного программирования (ИСП) Российской академии наук (РАН) на платформе AstraVer и Frama-C / Why3 со спецификациями на языке формальных контрактов (ACSL) и к оценке соответствия по оценочным уровням доверия (ОУД, Приказ ФСТЭК России № 76) при разработке безопасного программного обеспечения (ПО) по ГОСТ Р 56939-2024. Протоколы переходов и состояния безопасного отказа проверяются в темпоральной логике действий (TLA, TLA+); глубокая корректность процедуры разрешения и кодогенерации — интерактивным доказательством (Rocq, бывш. Coq). Ядро решателя исполняется на стандартных серверных процессорах и не требует специализированного оборудования.
Фазы программы
Программа разворачивается по четырём последовательным фазам, и на каждой из них фиксируются материальные результаты, пригодные для институциональной и научно-технической экспертизы.
Фаза 0. Производственная референсная реализация (текущая)
Цель фазы — действующий шлюз MITR на серверах института в режиме непрерывной работы.
MITR работает непрерывно с 24 апреля 2026 года на внутреннем стенде института и проверяет действия его собственных программных агентов: кодовых агентов, служб и подключений по протоколу контекста модели (MCP). С 24 октября 2026 года все 20 контрактов проверяются решателем и работают в режиме запрета; правила хранятся как данные и применяются без переписывания программы; цепь квитанций ведётся с 16 сентября 2026 года и раз в сутки закрепляется внешним свидетелем времени.
Измерено: 6 414 автоматических тестов без отказов (ночной прогон 25.10.2026); состязательный набор из 157 случаев — пропущено атак 0, ложных отказов 0 (24.10.2026); повтор решений проверщиком для постороннего — 5 079 из 5 079 (25.10.2026). Память агентов несёт происхождение каждой записи, а журнал решений ведётся только на добавление.
Материальные результаты текущей фазы включают действующий прототип среды исполнения агентов с встроенными слоями верификации, демонстрирующий устойчивость к состязательным атакам на политику. Создана методологическая документация в формате проектных записей и выстроена нумерованная дорожная карта научно-исследовательских и опытно-конструкторских работ.
Двух вещей начальная фаза не даёт: независимого наблюдателя для каждого факта, от которого зависит правило, и замера у внешнего заказчика. Они составляют содержание Фазы I.
Фаза I. Наблюдатели фактов, полное покрытие и внешний пилот
Цель фазы — доказательная проверка на фактах, которые снимают независимые наблюдатели, для всего класса необратимых действий и первый пилот в периметре внешнего заказчика. Фаза открыта для грантовых программ институтов развития и для партнёрского финансирования.
Содержание фазы составляют пять исследовательских рубежей; каждый закрывается письменным решением или научным препринтом и тестами:
- Наблюдатели фактов: по одному детерминированному наблюдателю на каждый факт контракта; при его отсутствии факт получает статус «не измерено», и действие не допускается.
- Проверка формы запроса между выводом модели и исполнителем: запрос с искажёнными параметрами критического действия отклоняется до проверки по существу.
- Закрытие трёх пробелов правил, которые называет состязательный набор, и расширение доказательной проверки на весь класс необратимых действий с замером задержки.
- Проверка достоверности выборок из долговременной памяти агента с учётом уверенности в каждой записи и регулярный пересмотр этой уверенности с журналом изменений.
- Тридцатисуточный пилот в периметре заказчика с измеренной долей ложных остановок.
Материальные результаты первой фазы — формализованная спецификация комплекса, пригодная для передачи в экспертизу; MITR с наблюдателями фактов и модельной проверкой протоколов безопасного отказа, работающий в изолированной среде; первые технические отчёты и научные препринты; регистрация программных компонентов в реестре отечественного программного обеспечения.
Фаза II. Типовой комплекс и пилотные внедрения
Цель фазы — оформление методологии в воспроизводимый типовой комплекс, пригодный для развёртывания внутри периметра заказчика, и проведение пилотных внедрений с первыми институциональными партнёрами в профильных сегментах.
Материальные результаты второй фазы образуют типовой программный комплекс с сопроводительной документацией и инструментарием развёртывания. Пилотные внедрения у первых партнёров в сегментах, наиболее чувствительных к требованию суверенитета пользователя: профессиональная юридическая практика, медицинские организации, корпоративные подразделения нормативного соответствия. Первая редакция базы формальных аксиом для типовых отраслевых режимов (187-ФЗ, 117-ФСТЭК, ГОСТ Р 57580). Аттестация по требованиям защиты информации для конкретных объектов первых пилотов.
Начало разработки собственного компактного решателя для логики QF_UFLIA с дедуктивной проверкой его кода на инструментах Института системного программирования Российской академии наук (AstraVer) — на пути к оценке соответствия по уровням доверия ФСТЭК России.
Фаза III. Институт как носитель стандарта
Цель фазы — закрепление института как методологического и экспертного центра по построению суверенно-пользовательских агентов в российской юрисдикции.
Материальные результаты третьей фазы включают базу формальных аксиом, покрывающую основные отраслевые режимы и отраслевые стандарты, с режимом регулярного обновления. Образовательные программы дополнительного профессионального образования для корпоративных и государственных специалистов. Участие института в формировании отраслевых и национальных стандартов по устройству автономных систем с формальными гарантиями корректности.
В том числе сертификация проверяющего ядра по уровням доверия ФСТЭК России.
Коммерциализация
Коммерческую часть ведёт хозяйственное общество — оператор, которое получает лицензию на разработки института. Модель дохода, порядок входа в проект и назначение средств изложены на странице «Инвесторам и партнёрам», а первая сделка — оплачиваемый пилот у отраслевого заказчика.
Отдельное направление составляет передача знаний: программы дополнительного профессионального образования для специалистов заказчика, участие в формировании отраслевых стандартов, экспертные заключения для регуляторов. Это направление имеет самостоятельную коммерческую ценность и одновременно выступает механизмом формирования профессионального сообщества вокруг методологии института.
Риски и устойчивость
В исследовательской программе заранее выделены четыре структурные категории рисков и инженерные механизмы их последовательного снижения.
Регуляторный риск
Возможное ужесточение требований к сертификации автономных систем в Российской Федерации может усложнить процедуру лицензирования независимых разработок. Программа опирается на эту динамику как на фундамент собственного рыночного положения.
Аппарат формальной верификации по своей природе служит прямым инструментом прохождения государственной экспертизы и даёт проверяющему органу методический образец для будущих стандартов доверенного искусственного интеллекта, тогда как адвокатская и аудиторская практика научного руководителя помогает учитывать правовые нормы прямо при проектировании системы.
Технологический риск
Применение SMT-решателей к задачам неограниченной сложности теоретически сталкивается с вычислительным взрывом. В устройстве MITR этот риск структурно ограничен передачей решателю только строго типизированного изолированного предиката.
Теория QF_UFLIA разрешима (проверка завершается всегда) и NP-полна — гарантии полиномиального времени нет, но на узких практических спецификациях экспоненциальный рост гасится эвристиками решателя, и проверка занимает миллисекунды. Масштабируемость подтверждена промышленной практикой на уровне миллиардов проверок в сутки.
Конкурентный риск
Вероятность быстрого выхода крупных российских платформ в сегмент суверенно-пользовательских агентов структурно ограничена. Коммерческая модель крупных платформ держится на удержании пользовательского внимания и сборе телеметрии внутри собственной облачной среды, поэтому выпуск автономного агента, физически отключённого от внешнего оператора, противоречит их прямой выгоде и оставляет этот сегмент специализированному независимому институту.
Репутационный риск
Институт сознательно избегает публичной конкуренции с существующими платформенными игроками на их территории массовых потребительских продуктов. Позиционирование программы — инфраструктурное программное обеспечение институционального уровня, дополняющее генеративные языковые модели детерминированным проверочным барьером. Такой подход укрепляет деловую репутацию и возможность взаимодействия с регуляторами и отраслевыми ассоциациями в нейтральном статусе методологического центра.
Критерии вхождения в программу
Программа открыта для трёх категорий участников, соответствующих её текущей фазе.
Пилотные партнёры из профильных отраслей — организации, для которых требование суверенитета пользователя носит прямой операционный характер: профессиональные практики с фидуциарной ответственностью, медицинские и образовательные организации, корпоративные подразделения нормативного соответствия, государственные информационные системы. Форма взаимодействия — совместное пилотное внедрение с обоюдной готовностью к тесной рабочей коммуникации на стадии настройки комплекса.
Институциональные партнёры и инвесторы, рассматривающие программу как долгосрочный опорный актив в формирующемся сегменте. Форма взаимодействия — разговор с научным руководителем и соглашение о конфиденциальности; порядок входа описан на странице «Инвесторам и партнёрам».
Академические и отраслевые научные структуры, профильные по направлениям формальной верификации, многоагентных систем, правовых оснований автономных технологий. Форма взаимодействия — совместные исследовательские программы, экспертные советы, участие в диссертационных работах.
Заключительное положение
Программа института реализуется в форме, в которой каждый этап оставляет материальный след — действующий прототип, формальную спецификацию, публикуемые артефакты, пилотные внедрения. Это позволяет регуляторной, академической и инвестиционной экспертизе оценивать состояние программы по проверяемым материальным результатам.
Фаза 0 уже предъявлена в действующем виде, тогда как Фаза I открыта для государственной поддержки и квалифицированной экспертной оценки. Фазы II и III оформляют долгосрочный горизонт института как методологического центра по устройству автономных систем с формальными гарантиями корректности.
Обращения общего характера не рассматриваются.
Проверено по первоисточникам: 25.10.2026 — действие и реквизиты нормативных актов и стандартов, названных на странице, по первоисточникам.
Разговор о доктрине, программе и участии в работе института начинается с сообщения научному руководителю: в первом сообщении достаточно назвать тему.