Certified Guidance for Planning with Deep Generative Models
Francesco Giacomarra, Mehran Hosseini, Nicola Paoletti, Francesca Cairoli
TL;DR
Certified guidance addresses the lack of guarantees in planning with deep generative models by enforcing ST L specifications through latent-space restriction. It constructs a phi-satisfying latent region as a union of hyper-rectangles and defines a truncated latent distribution p_φ(z) to guarantee satisfaction with probability $1$, while preserving relative likelihoods from the original latent space. The method leverages neural network verification (e.g., Auto-LiRPA with CROWN) to certify latent regions and uses differentiable STL robustness as a reward to guide pivot discovery, enabling gradient-based expansion of certified regions. Experiments on GANs and diffusion models across four planning benchmarks demonstrate robust STL satisfaction and competitive sample quality, though diffusion models face notable scalability challenges in verification. Overall, the work provides a principled path toward certification-backed planning with DGMs and suggests directions for extending to VAEs and improving conditioning generalization.
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.