Synergistic Verification of Neural Network Controlled Systems via Adversarially Guided Refinement

Neural network controlled systems (NNCSs) are increasingly deployed in safety-critical applications, making the safety property verification a fundamental challenge. Static reachability-based analysis offers formal safety guarantees but often suffers from overapproximation errors, leading to conservative or “Unknown” results, while dynamic falsification methods can efficiently discover counterexamples but provide no guarantees in their absence. In this paper, we propose a novel synergistic verification framework via adversarially guided refinement, which integrates dynamic falsification with static verification in a unified loop. The core idea is to integrate backward reachability analysis with projected gradient descent (PGD) based adversarial testing to efficiently explore safe behaviors, along with exploiting adversarial trajectories to guide targeted branch-and-bound refinement over critical time steps and neurons. Experimental results demonstrate our approach significantly enhances verification effectiveness, achieving up to 85% speedups, while producing tighter reachable set approximations and more conclusive verification outcomes for complex NNCSs.