Verification of Sigmoid-Like Neural Networks via Symbolic Relaxation

Formal robustness verification is essential for providing rigorous guarantees that a neural network's predictions remain unchanged with perturbations. For networks with sigmoid-like activations, a central challenge is to construct relaxations that faithfully capture their transcendental relations while remaining amenable to efficient verification. We propose a symbolically derived family of rational function relaxations, parametric in a relaxation order $k$. The relaxations are sound and convergent, and they yield a $k$-complete verification procedure, meaning that robust instances with a strictly positive margin can be certified with a finite relaxation order. Building on this family, we develop a scalable robustness verification method. Experiments on image classification benchmarks show that our method often outperforms the representative linear-relaxation baselines with tighter certified bounds on the robustness margin and improves certified robustness accuracy. Together, these results highlight the potential of rational relaxations beyond conventional linear bounds and suggest a new direction for certified robustness.