Partition-based formulations for mixed-integer optimization of trained ReLU neural networks | Proceedings of the 35th International Conference on Neural Information Processing Systems (2024)

Supplemental Material

1. Tobias Achterberg and Roland Wunderling. Mixed integer programming: Analyzing 12 years of progress. In Facets of Combinatorial Optimization, pages 449–481. Springer, 2013.Google Scholar
2. Michael Akintunde, Alessio Lomuscio, Lalit Maganti, and Edoardo Pirovano. Reachability analysis for neural agent-environment systems. In International Conference on Principles of Knowledge Representation and Reasoning., pages 184–193, 2018.Google Scholar
3. Ross Anderson, Joey Huchette, Will Ma, Christian Tjandraatmadja, and Juan Pablo Vielma. Strong mixed-integer programming formulations for trained neural networks. Mathematical Programming, pages 1–37, 2020.Google Scholar
4. Egon Balas. Disjunctive Programming. Springer International Publishing, 2018. .Google ScholarCross Ref
5. Elena Botoeva, Panagiotis Kouvaros, Jan Kronqvist, Alessio Lomuscio, and Ruth Misener. Efficient verification of ReLU-based neural networks via dependency analysis. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 34, pages 3291–3299, 2020.Google ScholarCross Ref
6. Rudy Bunel, Ilker Turkaslan, Philip HS Torr, Pushmeet Kohli, and M Pawan Kumar. A unified view of piecewise linear neural network verification. arXiv preprint arXiv:1711.00455, 2017.Google Scholar
7. Rudy Bunel, Alessandro De Palma, Alban Desmaison, Krishnamurthy Dvijotham, Pushmeet Kohli, Philip Torr, and M Pawan Kumar. Lagrangian decomposition for neural network verification. In Conference on Uncertainty in Artificial Intelligence, pages 370–379. PMLR, 2020.Google Scholar
8. Pin-Yu Chen, Yash Sharma, Huan Zhang, Jinfeng Yi, and Cho-Jui Hsieh. Ead: elastic-net attacks to deep neural networks via adversarial examples. In Proceedings of the AAAI Conference on Artificial Intelligence, volume 32, 2018.Google ScholarCross Ref
9. Chih-Hong Cheng, Georg Nührenberg, and Harald Ruess. Maximum resilience of artificial neural networks. In International Symposium on Automated Technology for Verification and Analysis, pages 251–268. Springer, 2017.Google Scholar
10. Michele Conforti, Gérard Cornuéjols, and Giacomo Zambelli. Integer Programming, volume 271 of Graduate Texts in Mathematics, 2014.Google ScholarCross Ref
11. Francesco Croce and Matthias Hein. Minimally distorted adversarial examples with a fast adaptive boundary attack. In International Conference on Machine Learning, pages 2196–2205. PMLR, 2020.Google Scholar
12. Sumanth Dathathri, Krishnamurthy Dvijotham, Alexey Kurakin, Aditi Raghunathan, Jonathan Uesato, Rudy Bunel, Shreya Shankar, Jacob Steinhardt, Ian Goodfellow, Percy Liang, et al. Enabling certification of verification-agnostic networks via memory-efficient semidefinite programming. arXiv preprint arXiv:2010.11645, 2020.Google Scholar
13. Alessandro De Palma, Harkirat Singh Behl, Rudy Bunel, Philip HS Torr, and M Pawan Kumar. Scaling the convex barrier with sparse dual algorithms. In International Conference on Learning Representations, 2021.Google Scholar
14. Souradeep Dutta, Susmit Jha, Sriram Sankaranarayanan, and Ashish Tiwari. Output range analysis for deep feedforward neural networks. In NASA Formal Methods Symposium, pages 121–138. Springer, 2018.Google Scholar
15. Krishnamurthy Dvijotham, Robert Stanforth, Sven Gowal, Timothy A Mann, and Pushmeet Kohli. A dual approach to scalable verification of deep networks. In UAI, volume 1, page 3, 2018.Google Scholar
16. Ruediger Ehlers. Formal verification of piece-wise linear feed-forward neural networks. In International Symposium on Automated Technology for Verification and Analysis, pages 269–286. Springer, 2017.Google Scholar
17. Matteo Fischetti and Jason Jo. Deep neural networks and mixed integer linear optimization. Constraints, 23(3):296–309, 2018.Google ScholarDigital Library
18. Bjarne Grimstad and Henrik Andersson. ReLU networks as surrogate models in mixed-integer linear programs. Computers & Chemical Engineering, 131:106580, 2019.Google ScholarCross Ref
19. Gurobi Optimization, LLC. Gurobi optimizer reference manual, 2020. URL http://www.gurobi.com.Google Scholar
20. Alex Krizhevsky. Learning multiple layers of features from tiny images. Master's thesis, The University of Toronto, 2009.Google Scholar
21. Jan Kronqvist, Ruth Misener, and Calvin Tsay. Between steps: Intermediate relaxations between big-M and convex hull formulations. In International Conference on Integration of Constraint Programming, Artificial Intelligence, and Operations Research, pages 299–314. Springer, 2021.Google Scholar
22. Yann LeCun, Corinna Cortes, and CJ Burges. MNIST handwritten digit database. ATT Labs [Online]. Available: http://yann.lecun.com/exdb/mnist, 2, 2010.Google Scholar
23. Alessio Lomuscio and Lalit Maganti. An approach to reachability analysis for feed-forward ReLU neural networks. arXiv preprint arXiv:1706.07351, 2017.Google Scholar
24. Adam Paszke, Sam Gross, Francisco Massa, Adam Lerer, James Bradbury, Gregory Chanan, Trevor Killeen, Zeming Lin, Natalia Gimelshein, Luca Antiga, Alban Desmaison, Andreas Kopf, Edward Yang, Zachary DeVito, Martin Raison, Alykhan Tejani, Sasank Chilamkurthy, Benoit Steiner, Lu Fang, Junjie Bai, and Soumith Chintala. Pytorch: An imperative style, high-performance deep learning library. In Advances in Neural Information Processing Systems, pages 8024–8035. 2019.Google Scholar
25. Aditi Raghunathan, Jacob Steinhardt, and Percy S Liang. Semidefinite relaxations for certifying robustness to adversarial examples. In Advances in Neural Information Processing Systems, volume 31, pages 10877–10887, 2018.Google Scholar
26. Ted Ralphs, Yuji Shinano, Timo Berthold, and Thorsten Koch. Parallel solvers for mixed integer linear optimization. In Handbook of Parallel Constraint Reasoning, pages 283–336. Springer, 2018.Google Scholar
27. Thiago Serra, Christian Tjandraatmadja, and Srikumar Ramalingam. Bounding and counting linear regions of deep neural networks. In International Conference on Machine Learning, pages 4558–4566. PMLR, 2018.Google Scholar
28. Thiago Serra, Abhinav Kumar, and Srikumar Ramalingam. Lossless compression of deep neural networks. In Integration of Constraint Programming, Artificial Intelligence, and Operations Research, pages 417–430. Springer, 2020.Google Scholar
29. Gagandeep Singh, Rupanshu Ganvir, Markus Püschel, and Martin Vechev. Beyond the single neuron convex barrier for neural network certification. In Advances in Neural Information Processing Systems, pages 15098–15109, 2019.Google Scholar
30. Gagandeep Singh, Timon Gehr, Markus Püschel, and Martin T Vechev. Boosting robustness certification of neural networks. In International Conference on Learning Representations, 2019.Google Scholar
31. Christian Tjandraatmadja, Ross Anderson, Joey Huchette, Will Ma, KRUNAL KISHOR PATEL, and Juan Pablo Vielma. The convex relaxation barrier, revisited: Tightened single-neuron relaxations for neural network verification. In H. Larochelle, M. Ranzato, R. Hadsell, M. F. Balcan, and H. Lin, editors, Advances in Neural Information Processing Systems, volume 33, pages 21675–21686, 2020.Google Scholar
32. Vincent Tjeng, Kai Xiao, and Russ Tedrake. Evaluating robustness of neural networks with mixed integer programming. arXiv preprint arXiv:1711.07356, 2017.Google Scholar
33. Michael Volpp, Lukas P Fröhlich, Kirsten Fischer, Andreas Doerr, Stefan Falkner, Frank Hutter, and Christian Daniel. Meta-learning acquisition functions for transfer learning in bayesian optimization. In International Conference on Learning Representations, 2019.Google Scholar
34. Lily Weng, Huan Zhang, Hongge Chen, Zhao Song, Cho-Jui Hsieh, Luca Daniel, Duane Boning, and Inderjit Dhillon. Towards fast computation of certified robustness for ReLU networks. In International Conference on Machine Learning, pages 5276–5285. PMLR, 2018.Google Scholar
35. Eric Wong and Zico Kolter. Provable defenses against adversarial examples via the convex outer adversarial polytope. In International Conference on Machine Learning, pages 5286–5295. PMLR, 2018.Google Scholar
36. Ga Wu, Buser Say, and Scott Sanner. Scalable planning with deep neural network learned transition models. Journal of Artificial Intelligence Research, 68:571–606, 2020.Google ScholarCross Ref

• Compact mixed-integer programming formulations in quadratic optimization

  Abstract

  We present a technique for producing valid dual bounds for nonconvex quadratic optimization problems. The approach leverages an elegant piecewise linear approximation for univariate quadratic functions due to Yarotsky (Neural Netw 94:103–114, 2017)...

  Read More

• Strong Mixed-Integer Programming Formulations for Trained Neural Networks

  Integer Programming and Combinatorial Optimization

  Abstract

  We present an ideal mixed-integer programming (MIP) formulation for a rectified linear unit (ReLU) appearing in a trained neural network. Our formulation requires a single binary variable and no additional continuous variables beyond the input and ...

  Read More

• Solving Mixed Integer Bilinear Problems Using MILP Formulations

  In this paper, we examine a mixed integer linear programming reformulation for mixedinteger bilinear problems where each bilinearterm involves the product of a nonnegativeinteger variable and a nonnegative continuous variable. This reformulation is ...

  Read More