Certified Guidance for Planning with Deep Generative Models

TL;DR

This paper introduces a method called certified guidance that modifies deep generative models to guarantee satisfaction of planning specifications, specifically Signal Temporal Logic, without retraining, ensuring correctness in autonomous planning tasks.

Contribution

The paper presents a novel certification approach that guarantees generative models satisfy planning specifications with probability one, using neural network verification techniques without retraining.

Findings

Certified guidance guarantees correctness of generated outputs.

Method is effective across multiple planning benchmarks.

Ensures models always satisfy specified planning objectives.

Abstract

Deep generative models, such as generative adversarial networks and diffusion models, have recently emerged as powerful tools for planning tasks and behavior synthesis in autonomous systems. Various guidance strategies have been introduced to steer the generative process toward outputs that are more likely to satisfy the planning objectives. These strategies avoid the need for model retraining but do not provide any guarantee that the generated outputs will satisfy the desired planning objectives. To address this limitation, we introduce certified guidance, an approach that modifies a generative model, without retraining it, into a new model guaranteed to satisfy a given specification with probability one. We focus on Signal Temporal Logic specifications, which are rich enough to describe nontrivial planning tasks. Our approach leverages neural network verification techniques to systematically explore the latent spaces of the generative models, identifying latent regions that are certifiably correct with respect to the STL property of interest. We evaluate the effectiveness of our method on four planning benchmarks using GANs and diffusion models. Our results confirm that certified guidance produces generative models that are always correct, unlike existing guidance methods that are not certified.