Formal Safety Verification and Refinement for Generative Motion Planners via Certified Local Stabilization

## Контекст Генерирующие планировщики движения (Generative Motion Planners, GMP) — это новая стратегия для планирования движения, которая использует нейронные сети для генерирования планов движения в реальном времени. Они отличаются от традиционных алгоритмов планирования движения тем, что не зависят от явного представления окружающей среды, что делает их более гибкими и эффективными. Однако, несмотря на их выгоды, генерирующие планировщики движения сталкиваются с трудностями в проверке безопасности и динамической выполнимости их планов движения. Действительно, нейронные сети, используемые в таких планировщиках, содержат миллионы параметров, что делает их проверку сложнее. Это затрудняет их использование в реальных ситуациях, где безопасность и надежность являются критичными. Наша мотивация заключается в разработке метода, который позволит проверить безопасность и динамическую выполнимость генерирующих планировщиков движения без потери их выразительности. ## Метод Мы предлагаем метод для формальной проверки безопасности и рефинеймента генерирующих планировщиков движения с помощью стабилизированных локальных управлений. Мы стабилизируем выходные данные генерирующего планировщика движения с помощью небольшого нейронного управляющего модуля, который принимает в качестве входных данных сэмплы из выходов GMP. Затем мы применяем инструменты нейронной сетевой проверки (Neural Network Verification, NNV) для закрытого цикла динамики. Это позволяет получить достижимые множества, которые могут строго подтвердить безопасность закрытого цикла. Кроме того, управляющий модуль гарантирует динамическую выполнимость. Мы также создаем библиотеку стабилизированных генерирующих планировщиков движения, которая может быть использована в реальном времени. Этот подход позволяет имитировать дистрибуцию генерирующего планировщика движения в безопасных ситуациях, улучшая безопасность без необходимости переучивания. ## Результаты Мы используем наши методы для проверки стабильности и безопасности генерирующих планировщиков движения, включая такие алгоритмы, как Diffusion Models, Flow Matching и Vision-Language Models. Мы проводим эксперименты на симуляциях (земных роботов и квадрокоптерах) и на реальном оборудовании (двухходовом роботе). Наши результаты показывают, что наш подход улучшает безопасность и отвечает высоким стандартам динамической выполнимости, не теряя выразительности генерирующих планировщиков движения. ## Значимость Наш подход имеет широкие перспективы применения в сферах, где безопасность и надежность движения роботов играют критическую