Formal Safety Verification of Stochastic Systems under Diffusion-Induced Uncertainty

Formal safety verification of autonomous systems in open environments is challenged by interaction-induced stochasticity. Existing methods typically assume pre-specified stochastic models or handcrafted disturbance distributions, limiting their ability to capture complex disturbance patterns encountered in real-world operation. In this paper, we leverage expressive diffusion models to learn data-driven stochastic behaviors from observed trajectories and adapts it to the evolving system state. By exploiting their intrinsic score-based reverse stochastic dynamics, we analytically propagate the learned uncertainty into an explicit verification-oriented stochastic differential equation (SDE), enabling rigorous probabilistic safety verification via stochastic barrier certificates. Experimental results on representative benchmarks demonstrate the effectiveness of our proposed approach.