Precondition Synthesis for Deep Neural Networks with Statistical Guarantees

Deep neural networks (DNNs) are increasingly being deployed in safety-critical systems. However, existing formal verification methods provide limited quantitative guarantees for their reliable specification, and emerging precondition synthesis techniques are hindered by the scalability and architectural limitations of DNNs. In this paper, we propose a select-and-solve framework, StatPre, to automatically synthesize preconditions with statistical guarantees. StatPre aims to maximally weaken the synthesized preconditions while keeping them as accurate as possible to the real preconditions through a Box-based abstraction. The framework operates in two phases: the center selection phase, which identifies potential center points using a cluster-based heuristic with potential assessment, and the expansion solution phase, which solves the problem of optimizing maximal preconditions by employing statistical model approximation, equivalent constraint transformation, and automatic iterative execution. We evaluated StatPre on 15 models with 27 properties from 6 benchmarks and compared it with 4 existing deterministic and statistical schemes. The results demonstrate that StatPre effectively synthesizes preconditions with broader coverage while accurately approximating the real preconditions in practice. Additionally, StatPre exhibits competitive performance in handling high-dimensional, non-ReLU, complex-structured neural networks.