Certified Guidance for Planning with Deep Generative Models

Deep generative models, such as generative adversarial networks (GANs) and score-based 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 1. We focus on Signal Temporal Logic (STL) specifications, which are rich enough to describe non-trivial planning tasks. Our approach leverages neural network verification techniques to systematically explore the generative models' latent spaces, identifying latent regions that are certifiably correct w.r.t. 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 (non-certified) guidance methods.