Формальная модель нашла дефект агента до запуска дорогих тестов
Описание процессов pause и resume выявило дефект еще до симуляции терминала и прогонов на настоящих агентах
Автор предлагает брать самый слабый формализм, который уже ловит реальные ошибки: LTL, STN, SMT, Datalog, PDDL или TLA+
Полезность подхода предлагают мерить долей невалидных планов, ценой перепланирования и частотой ошибок формализации
Почему важно
Проверка структуры плана до исполнения может перенести часть надежности агентов из дорогих прогонов в более дешевый анализ моделей