Research map / Adversarial robustness and security / Certified and empirical robustness

Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization

ICLR 2025 · Adversarial robustness and security › Certified and empirical robustness · approach: Neural network robustness verification · 0 citations (OpenAlex)

Read the paperCheck your idea against 108,967 papers

AI-extracted summary. Written by AI from the paper's full text. Numbers and claims can be wrong or missing context, so check the paper before you cite or build on it.

Verifies robustness of binary neural networks by encoding sign activations as a polynomial optimization problem and solving tightened first-order sparse SDP relaxations, compared against LP and MILP solvers.

Problem

Robustness verification of Binary Neural Networks under continuous input perturbations (l-infinity and l2); existing SAT/MILP exact methods scale poorly and suffer floating-point issues, while LP relaxations are coarse.

Approach

Encode BNN sign activations as semi-algebraic quadratic constraints forming a polynomial optimization problem, add redundant tautological quadratic constraints to enlarge the first-order quadratic module, and solve the resulting correlatively sparse first-order SDP relaxation to get certified lower bounds.

Key results

• On BNN_1 with l-infinity delta 0.25, the tightened first-order sparse SDP certifies 91 of 100 instances vs 83 for LP, and the paper reports on average 15.75% (BNN_1) and 25.67% (BNN_2) less conservative than LP.
• For l2 attacks, the SDP method certifies nearly the same number of instances as Soft-MINP at severe perturbations while being 11.4 times faster on average.
• On randomly generated networks, the tightened bound is consistently better than the LP bound, e.g. -24.71 vs -78.83 on [300,100,100] dense.

Measured effects reported in the paper

Surprising findings

• The first-order SDP relaxation without tautologies can be no tighter than the LP relaxation; the paper shows the LP bound can be strictly better than the first-order relaxation of the plain encoding.

Limitations

• Relies on interior-point SDP solvers, inheriting their scalability limits.
• Higher-order relaxations are computationally intractable for high-dimensional problems.
• Tested only on small MNIST/CIFAR-10 BNNs with fully connected layers.

Experimental setup

Datasets: MNIST CIFAR-10

Benchmarks: MNIST robustness verification (first 100 test images) CIFAR-10 l-infinity verification random BNN verification instances

Metrics: number of certified instances verification time (s) bound value

Baselines: LP relaxation Soft-MILP Soft-MINP

Builds on: Lasserre hierarchy correlative sparsity SDP relaxations TSSOS Larq

Closest papers by meaning

• Efficient Exact Verification of Binarized Neural Networks (NeurIPS 2020 · similarity 0.90)
• A Convex Relaxation Barrier to Tight Robustness Verification of Neural Networks (NeurIPS 2019 · similarity 0.89)
• Evaluating Robustness of Neural Networks with Mixed Integer Programming (ICLR 2019 · similarity 0.89)
• DeepBern-Nets: Taming the Complexity of Certifying Neural Networks Using Bernstein Polynomial Activations and Precise Bound Propagation (AAAI 2024 · similarity 0.87)
• VNN: Verification-Friendly Neural Networks with Hard Robustness Guarantees (ICML 2024 · similarity 0.87)
• Certified but Private: Scalable Zero-Knowledge Proofs for the Formal Verification of Neural Networks (NeurIPS 2026 · similarity 0.86)