Краткое содержание

arXiv:2511.14435v1 Тип объявления: кросс Аннотация: Обеспечение безопасности и надежности автономных систем особенно сложно при использовании компонентов с обучением и открытых сред. Формальные методы обеспечивают строгие гарантии, но зависят от полных моделей и статических предположений. Верификация во время выполнения (runtime verification, RV) дополняет их путем мониторинга исполнения в реальном времени и, в своих прогнозирующих вариантах, за счет предсказания потенциальных нарушений. Большие языковые модели (large language models, LLM), тем временем, отлично справляются с переводом естественного языка в формальные артефакты и распознаванием закономерностей в данных, однако они остаются склонными к ошибкам и не имеют формальных гарантий. Данная концептуальная статья аргументирует необходимость симбиотической интеграции методов runtime verification и больших языковых моделей. Методы RV могут служить ограничителем для автономии на основе LLM, тогда как сами LLM способны расширить возможности RV, помогая захватывать спецификации, поддерживать предиктивное рассуждение и справляться с неопределенностью. Мы описываем, каким образом это взаимное усиление отличается от существующих обзоров и дорожных карт, обсуждаем вызовы