This work introduces a verification framework that provides both sound and complete guarantees for data poisoning attacks during neural network training. We formulate adversarial data manipulation, model training, and test-time evaluation in a single mixed-integer quadratic programming (MIQCP) problem. Finding the global optimum of the proposed formulation provably yields worst-case poisoning attacks, while simultaneously bounding the effectiveness of all possible attacks on the given training pipeline. Our framework encodes both the gradient-based training dynamics and model evaluation at test time, enabling the first exact certification of training-time robustness. Experimental evaluation on small models confirms that our approach delivers a complete characterization of robustness against data poisoning.
Figures & tables
Figure 1: Comparison of formulation tightness and optimization progress for the Iris dataset under an unbounded attack model ( n=8 ). Left: Tightness of the test-data Big-M constants, defined as ∣U(i,test)−L(i,test)∣ . Right: Objective value (dashed) and dual bound (dotted) progress over time.
Figure 2: Optimal denial of service attack on the Diabetes dataset with n=50,ϵ=0,ν=0.5 . The red squares depict the points poisoned by the adversary. The rightmost figure depicts the training loss for the poisoned (green) vs original (blue) datasets.
Figure 3: Right: Label flipping attacks and certificates for the Halfmoons dataset. Left: Example optimal attack for n=5 label flips.