IDEAS home Printed from https://ideas.repec.org/a/spr/jglopt/v81y2021i1d10.1007_s10898-020-00949-1.html
   My bibliography  Save this article

Advances in verification of ReLU neural networks

Author

Listed:
  • Ansgar Rössig

    (Technische Universität Berlin)

  • Milena Petkovic

    (Zuse Institute Berlin)

Abstract

We consider the problem of verifying linear properties of neural networks. Despite their success in many classification and prediction tasks, neural networks may return unexpected results for certain inputs. This is highly problematic with respect to the application of neural networks for safety-critical tasks, e.g. in autonomous driving. We provide an overview of algorithmic approaches that aim to provide formal guarantees on the behaviour of neural networks. Moreover, we present new theoretical results with respect to the approximation of ReLU neural networks. On the other hand, we implement a solver for verification of ReLU neural networks which combines mixed integer programming with specialized branching and approximation techniques. To evaluate its performance, we conduct an extensive computational study. For that we use test instances based on the ACAS Xu system and the MNIST handwritten digit data set. The results indicate that our approach is very competitive with others, i.e. it outperforms the solvers of Bunel et al. (in: Bengio, Wallach, Larochelle, Grauman, Cesa-Bianchi, Garnett (eds) Advances in neural information processing systems (NIPS 2018), 2018) and Reluplex (Katz et al. in: Computer aided verification—29th international conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017, Proceedings, 2017). In comparison to the solvers ReluVal (Wang et al. in: 27th USENIX security symposium (USENIX Security 18), USENIX Association, Baltimore, 2018a) and Neurify (Wang et al. in: 32nd Conference on neural information processing systems (NIPS), Montreal, 2018b), the number of necessary branchings is much smaller. Our solver is publicly available and able to solve the verification problem for instances which do not have independent bounds for each input neuron.

Suggested Citation

  • Ansgar Rössig & Milena Petkovic, 2021. "Advances in verification of ReLU neural networks," Journal of Global Optimization, Springer, vol. 81(1), pages 109-152, September.
  • Handle: RePEc:spr:jglopt:v:81:y:2021:i:1:d:10.1007_s10898-020-00949-1
    DOI: 10.1007/s10898-020-00949-1
    as

    Download full text from publisher

    File URL: http://link.springer.com/10.1007/s10898-020-00949-1
    File Function: Abstract
    Download Restriction: Access to the full text of the articles in this series is restricted.

    File URL: https://libkey.io/10.1007/s10898-020-00949-1?utm_source=ideas
    LibKey link: if access is restricted and if your library uses this service, LibKey will redirect you to where you can use your library subscription to access this item
    ---><---

    As the access to this document is restricted, you may want to search for a different version of it.

    References listed on IDEAS

    as
    1. Ambros M. Gleixner & Timo Berthold & Benjamin Müller & Stefan Weltge, 2017. "Three enhancements for optimization-based bound tightening," Journal of Global Optimization, Springer, vol. 67(4), pages 731-757, April.
    Full references (including those not matched with items on IDEAS)

    Citations

    Citations are extracted by the CitEc Project, subscribe to its RSS feed for this item.
    as


    Cited by:

    1. Shengpu Wang & Mi Ding & Wang Lin & Yubo Jia, 2022. "Verification of Approximate Initial-State Opacity for Control Systems via Neural Augmented Barrier Certificates," Mathematics, MDPI, vol. 10(14), pages 1-19, July.

    Most related items

    These are the items that most often cite the same works as this one and are cited by the same works as this one.
    1. Brais González-Rodríguez & Joaquín Ossorio-Castillo & Julio González-Díaz & Ángel M. González-Rueda & David R. Penas & Diego Rodríguez-Martínez, 2023. "Computational advances in polynomial optimization: RAPOSa, a freely available global solver," Journal of Global Optimization, Springer, vol. 85(3), pages 541-568, March.
    2. Jaromił Najman & Dominik Bongartz & Alexander Mitsos, 2021. "Linearization of McCormick relaxations and hybridization with the auxiliary variable method," Journal of Global Optimization, Springer, vol. 80(4), pages 731-756, August.
    3. Huiyi Cao & Kamil A. Khan, 2023. "General convex relaxations of implicit functions and inverse functions," Journal of Global Optimization, Springer, vol. 86(3), pages 545-572, July.
    4. Artur M. Schweidtmann & Alexander Mitsos, 2019. "Deterministic Global Optimization with Artificial Neural Networks Embedded," Journal of Optimization Theory and Applications, Springer, vol. 180(3), pages 925-948, March.
    5. Victor Reyes & Ignacio Araya, 2023. "Non-Convex Optimization: Using Preconditioning Matrices for Optimally Improving Variable Bounds in Linear Relaxations," Mathematics, MDPI, vol. 11(16), pages 1-19, August.
    6. Dan Bienstock & Mauro Escobar & Claudio Gentile & Leo Liberti, 2020. "Mathematical programming formulations for the alternating current optimal power flow problem," 4OR, Springer, vol. 18(3), pages 249-292, September.
    7. G. Liuzzi & M. Locatelli & V. Piccialli & S. Rass, 2021. "Computing mixed strategies equilibria in presence of switching costs by the solution of nonconvex QP problems," Computational Optimization and Applications, Springer, vol. 79(3), pages 561-599, July.
    8. Kevin-Martin Aigner & Robert Burlacu & Frauke Liers & Alexander Martin, 2023. "Solving AC Optimal Power Flow with Discrete Decisions to Global Optimality," INFORMS Journal on Computing, INFORMS, vol. 35(2), pages 458-474, March.
    9. Pedro A. Castillo Castillo & Pedro M. Castro & Vladimir Mahalec, 2018. "Global optimization of MIQCPs with dynamic piecewise relaxations," Journal of Global Optimization, Springer, vol. 71(4), pages 691-716, August.
    10. Sass, Susanne & Mitsos, Alexander & Bongartz, Dominik & Bell, Ian H. & Nikolov, Nikolay I. & Tsoukalas, Angelos, 2024. "A branch-and-bound algorithm with growing datasets for large-scale parameter estimation," European Journal of Operational Research, Elsevier, vol. 316(1), pages 36-45.
    11. Jaromił Najman & Alexander Mitsos, 2019. "Tighter McCormick relaxations through subgradient propagation," Journal of Global Optimization, Springer, vol. 75(3), pages 565-593, November.
    12. Yifu Chen & Christos T. Maravelias, 2022. "Variable Bound Tightening and Valid Constraints for Multiperiod Blending," INFORMS Journal on Computing, INFORMS, vol. 34(4), pages 2073-2090, July.
    13. Dominic Yang & Prasanna Balaprakash & Sven Leyffer, 2022. "Modeling design and control problems involving neural network surrogates," Computational Optimization and Applications, Springer, vol. 83(3), pages 759-800, December.
    14. Daniel Bienstock & Mauro Escobar & Claudio Gentile & Leo Liberti, 2022. "Mathematical programming formulations for the alternating current optimal power flow problem," Annals of Operations Research, Springer, vol. 314(1), pages 277-315, July.

    Corrections

    All material on this site has been provided by the respective publishers and authors. You can help correct errors and omissions. When requesting a correction, please mention this item's handle: RePEc:spr:jglopt:v:81:y:2021:i:1:d:10.1007_s10898-020-00949-1. See general information about how to correct material in RePEc.

    If you have authored this item and are not yet registered with RePEc, we encourage you to do it here. This allows to link your profile to this item. It also allows you to accept potential citations to this item that we are uncertain about.

    If CitEc recognized a bibliographic reference but did not link an item in RePEc to it, you can help with this form .

    If you know of missing items citing this one, you can help us creating those links by adding the relevant references in the same way as above, for each refering item. If you are a registered author of this item, you may also want to check the "citations" tab in your RePEc Author Service profile, as there may be some citations waiting for confirmation.

    For technical questions regarding this item, or to correct its authors, title, abstract, bibliographic or download information, contact: Sonal Shukla or Springer Nature Abstracting and Indexing (email available below). General contact details of provider: http://www.springer.com .

    Please note that corrections may take a couple of weeks to filter through the various RePEc services.

    IDEAS is a RePEc service. RePEc uses bibliographic data supplied by the respective publishers.