mlsanityData to 14 Oct 2026

Neural Network Verification as Piecewise Linear Optimization: Formulations for the Composition of Staircase Functions

arXiv 2211.14706 ↗First posted 27 Nov 2022cs.LG math.OCcited by 2

Not on the map. Why?

Abstract (arXiv)

We present a technique for neural network verification using mixed-integer programming (MIP) formulations. We derive a strong formulation for each neuron in a network using piecewise linear activation functions. Additionally, as in general, these formulations may require an exponential number of inequalities, we also derive a separation procedure that runs in super-linear time in the input dimension. We first introduce and develop our technique on the class of staircase functions, which generalizes the ReLU, binarized, and quantized activation functions. We then use results for staircase activation functions to obtain a separation method for general piecewise linear activation functions. Empirically, using our strong formulation and separation technique, we can reduce the computational time in exact verification settings based on MIP and improve the false negative rate for inexact verifiers relying on the relaxation of the MIP formulation.

Key facts. Cited by 2 papers in the map (data through 14 Oct 2026). Builds on 21 of its 38 references that are in the map. First posted on arXiv 27 Nov 2022.

Builds on

21 of 38 references.

References · 21

  1. 2014Explaining and Harnessing Adversarial Examplescited by 7,364
  2. 2013Intriguing properties of neural networkscited by 5,155
  3. 2016Towards Evaluating the Robustness of Neural Networkscited by 2,998
  4. 2016XNOR-Net: ImageNet Classification Using Binary Convolutional Neural Networkscited by 849
  5. 2015The Limitations of Deep Learning in Adversarial Settingscited by 790
  6. 2014Deep Learning in Neural Networks: An Overviewcited by 770
  7. 2017Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networkscited by 744
  8. 2017Adversarial Examples for Evaluating Reading Comprehension Systemscited by 571
  9. 2016DoReFa-Net: Training Low Bitwidth Convolutional Neural Networks with Low Bitwidth Gradientscited by 569
  10. 2016Quantized Neural Networks: Training Neural Networks with Low Precision Weights and Activationscited by 426
  11. 2019Adversarial Attacks and Defenses in Images, Graphs and Text: A Reviewcited by 237
  12. 2017Towards Accurate Binary Convolutional Neural Networkcited by 149
9 more
  1. 2019Branch and Bound for Piecewise Linear Neural Network Verificationcited by 138
  2. 2018A Dual Approach to Scalable Verification of Deep Networkscited by 125
  3. 2018Strong mixed-integer programming formulations for trained neural networkscited by 115
  4. 2014Learning Activation Functions to Improve Deep Neural Networkscited by 63
  5. 2020The Convex Relaxation Barrier, Revisited: Tightened Single-Neuron Relaxations for Neural Network Verificationcited by 50
  6. 2016Adversarial Perturbations Against Deep Neural Networks for Malware Classificationcited by 42
  7. 2020Tightened Convex Relaxations for Neural Network Robustness Certificationcited by 14
  8. 2017Small and Strong Formulations for Unions of Convex Sets from the Cayley Embeddingcited by 5
  9. 2015Embedding Formulations and Complexity for Unions of Polyhedracited by 1

Built on by

Cited by year

Citing papers per year: 2023: 1; 2024: 0; 2025: 1.

2 papers.

  1. 2023When Deep Learning Meets Polyhedral Theory: A Surveycited by 39
  2. 2025Formal Verification of Markov Processes with Learned Parameterscited by 1

Similar, not cited

Close in wording, no citation either way

  1. 2026Arbitrary-Accuracy Neural Approximation with Optimal Neuron Count and Near-Optimal Bit Complexity
  2. 2024Verifying Properties of Binary Neural Networks Using Sparse Polynomial Optimization
  3. 2022A Mixed Integer Programming Approach for Verifying Properties of Binarized Neural Networks
  4. 2025On Integer Programming for the Binarized Neural Network Verification Problem
  5. 2023Efficient Symbolic Reasoning for Neural-Network Verification
  6. 2025Mathematical Programming Models for Exact and Interpretable Formulation of Neural Networks
  7. 2026Some Complexity Results for Robustness Verification for Binarized Neural Networks
  8. 2025Proof-Carrying Verification for ReLU Networks via Rational Certificates ↗