SpringerLink
Log in

Maximal Robust Neural Network Specifications via Oracle-Guided Numerical Optimization

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 13881))

  • 523 Accesses

Abstract

Analyzing the robustness of neural networks is crucial for trusting them. The vast majority of existing works focus on networks’ robustness in \(\epsilon \)-ball neighborhoods, but these cannot capture complex robustness specifications. We propose MaRVeL, a system for computing maximal non-uniform robust specifications that maximize a target norm. The main idea is to employ oracle-guided numerical optimization, thereby leveraging the efficiency of a numerical optimizer as well as the accuracy of a non-differentiable robustness verifier, acting as the oracle. The optimizer iteratively submits to the verifier candidate specifications, which in turn returns the closest inputs to the decision boundaries. The optimizer then computes their gradients to guide its search in the directions the specification can expand while remaining robust. We evaluate MaRVeL on several datasets and classifiers and show that its specifications are larger by 5.1x than prior works. On a two-dimensional dataset, we show that the average diameter of its specifications is 93% of the optimal average diameter, whereas the diameter of prior works’ specifications is only 26%.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
EUR 32.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or Ebook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 64.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 84.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free ship** worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    There is an edge case where \(l_i=u_i\), in which case the gradient is zero. There are standard corrections to guarantee that the gradient is monotonically increasing. For example, for the \(L_1\) norm, which is the one currently supported in our implementation, the correction replaces the zero gradient by 1 (for \(u_i\)) or \(-1\) (for \(l_i\)).

  2. 2.

    https://github.com/ananmkabaha/MaRVeL.git.

  3. 3.

    https://github.com/eth-sri/eran.

  4. 4.

    https://github.com/liuchen11/CertifyNonuniformBounds.

References

  1. Anderson, G., Pailoor, S., Dillig, I., Chaudhuri., S.: Optimization and abstraction: a synergistic approach for analyzing neural network robustness. In: PLDI, pp. 731–744 (2019)

    Google Scholar 

  2. Balunovic, M., Vechev, M.T.: Adversarial training and provable defenses: bridging the gap. In: ICLR, pp. 1–18 (2020)

    Google Scholar 

  3. Boopathy, A., Weng, T., Chen, P., Liu, S., Dani., L.: Cnn-cert: an efficient framework for certifying robustness of convolutional neural networks. In: AAAI, pp. 3240–3247 (2019)

    Google Scholar 

  4. Carlini, N., Wagner., D.A.: Towards evaluating the robustness of neural networks. In: SP, pp. 39–57 (2017)

    Google Scholar 

  5. Chen, P., Sharma, Y., Zhang, H., Yi, J., Hsieh, C.: EAD: elastic-net attacks to deep neural networks via adversarial examples. In: AAAI (2018)

    Google Scholar 

  6. Chen, P., Zhang, H., Sharma, Y., Yi, J., Hsieh, C.: ZOO: zeroth order optimization based black-box attacks to deep neural networks without training substitute models. In: AISec Workshop, pp. 15–26 (2017)

    Google Scholar 

  7. Contagio: Contagio, pdf malware dump (2010). http://contagiodump.blogspot.de/2010/08/malicious-documents-archivefor.html

  8. Dimitrov, D.I., Singh, G., Gehr, T., Vechev, M.T.: Provably robust adversarial examples. In: ICLR (2022)

    Google Scholar 

  9. Dvijotham, K., Stanforth, R., Gowal, S., Mann, T.A., Kohli, P.: A dual approach to scalable verification of deep networks. In: UAI, p. 3 (2018)

    Google Scholar 

  10. Ehlers, R.: Formal verification of piece-wise linear feed-forward neural networks. In: D’Souza, D., Narayan Kumar, K. (eds.) ATVA 2017. LNCS, vol. 10482, pp. 269–286. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-68167-2_19

    Chapter  Google Scholar 

  11. Elboher, Y.Y., Gottschlich, J., Katz, G.: An abstraction-based framework for neural network verification. In: Lahiri, S.K., Wang, C. (eds.) CAV 2020. LNCS, vol. 12224, pp. 43–65. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-53288-8_3

    Chapter  Google Scholar 

  12. Erdemir, E., Bickford, J., Melis, L., Aydöre, S.: Adversarial robustness with non-uniform perturbations. In: NeurIPS (2021)

    Google Scholar 

  13. Gehr, T., Mirman, M., Drachsler-Cohen, D., Tsankov, P., Chaudhuri, S., Vechev, M.T.: AI2: safety and robustness certification of neural networks with abstract interpretation. In: SP, pp. 3–18 (2018)

    Google Scholar 

  14. Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: ICLR (2015)

    Google Scholar 

  15. Ilyas, A., Santurkar, S., Tsipras, D., Engstrom, L., Tran, B., Madry, A.: Adversarial examples are not bugs, they are features. In: NeurIPS (2019)

    Google Scholar 

  16. Jha, S., Gulwani, S., Seshia, S.A., Tiwari, A.: Oracle-guided component-based program synthesis. In: ICSE, pp. 215–224 (2010)

    Google Scholar 

  17. Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. Acta Informatica 54(7), 693–726 (2017). https://doi.org/10.1007/s00236-017-0294-5

    Article  MathSciNet  Google Scholar 

  18. Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kunčak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97–117. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-63387-9_5

    Chapter  Google Scholar 

  19. Katz, G., et al.: The marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019. LNCS, vol. 11561, pp. 443–452. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-25540-4_26

    Chapter  Google Scholar 

  20. Krizhevsky, A.: Learning multiple layers of features from tiny images. In: CoRR, abs/1708.07747 (2009)

    Google Scholar 

  21. Kurakin, A., Goodfellow, I.J., Bengio, S.: Adversarial examples in the physical world. In: ICLR Workshop, pp. 99–112 (2017)

    Google Scholar 

  22. Kurakin, A., Goodfellow, I.J., Bengio, S.: Adversarial machine learning at scale. In: ICLR, pp. 99–112 (2017)

    Google Scholar 

  23. Lazarus, C., Kochenderfer, M.J.: A mixed integer programming approach for verifying properties of binarized neural networks. In: IJCAI Workshop (2021)

    Google Scholar 

  24. Lecun, Y., Bottou, L., Bengio, Y., Haffner, P.: Gradient-based learning applied to document recognition. Proc. IEEE 86(11), 2278–2324 (1998)

    Article  Google Scholar 

  25. Li, C., et al.: Towards certifying the asymmetric robustness for neural networks: quantification and applications. In: TDSC (2021)

    Google Scholar 

  26. Liu, C., Tomioka, R., Cevher, V.: On certifying non-uniform bounds against adversarial attacks. In: ICML, pp. 4072–4081 (2019)

    Google Scholar 

  27. Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: ICLR (2018)

    Google Scholar 

  28. Müller, C., Serre, F., Singh, G., Püschel, M., Vechev, M.: Scaling polyhedral neural network verification on GPUs. In: MLSys (2021)

    Google Scholar 

  29. Qin, C., et al.: Verification of non-linear specifications for neural networks. In: ICLR (2019)

    Google Scholar 

  30. Raghunathan, A., Steinhardt, J., Liang, P.: Certified defenses against adversarial examples. In: ICLR (2018)

    Google Scholar 

  31. Salman, H., Yang, G., Zhang, H., Hsieh, C., Zhang, P.: A convex relaxation barrier to tight robustness verification of neural networks. In: NeurIPS (2019)

    Google Scholar 

  32. Singh, G., Ganvir, R., Püschel, M., Vechev, M.T.: Beyond the single neuron convex barrier for neural network certification. In: NeurIPS (2019)

    Google Scholar 

  33. Singh, G., Gehr, T., Püschel, M., Vechev, M.T.: An abstract domain for certifying neural networks. In: POPL, pp. 1–30 (2019)

    Google Scholar 

  34. Singh, G., Gehr, T., Püschel, M., Vechev, M.T.: Boosting robustness certification of neural networks. In: ICLR (2019)

    Google Scholar 

  35. Sinha, A., Namkoong, H., Duchi, J.C.: Certifying some distributional robustness with principled adversarial training. In: ICLR (2019)

    Google Scholar 

  36. Solar-Lezama, A., Tancau, L., Bodík, R., Seshia, S.A., Saraswat, V.A.: Combinatorial sketching for finite programs. In: ASPLOS, pp. 404–415 (2006)

    Google Scholar 

  37. Szegedy, C., et al.: Intriguing properties of neural networks. In: ICLR (2014)

    Google Scholar 

  38. Tjeng, V., **ao, K.Y., Tedrake, R.: Evaluating robustness of neural networks with mixed integer programming. In: ICLR (2019)

    Google Scholar 

  39. Tu, C., et al.: Autozoom: autoencoder-based zeroth order optimization method for attacking black-box neural networks. In: AAAI, pp. 742–749 (2019)

    Google Scholar 

  40. VirusTotal: Virustotal, a free service that analyzes suspicious files and urls and facilitates the quick detection of viruses, worms, trojans, and all kinds of malware (2004). https://www.virustotal.com/

  41. Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Efficient formal safety analysis of neural networks. In: NeurIPS (2018)

    Google Scholar 

  42. Wang, S., Pei, K., Whitehouse, J., Yang, J., Jana, S.: Formal security analysis of neural networks using symbolic intervals. In: USENIX, pp. 1599–1614 (2018)

    Google Scholar 

  43. Wang, S., et al.: Beta-crown: efficient bound propagation with per-neuron split constraints for neural network robustness verification. In: NeurIPS (2021)

    Google Scholar 

  44. **ao, H., Rasul, K., Vollgraf, R.: Fashion-mnist: a novel image dataset for benchmarking machine learning algorithms. ar**v preprint ar**v:1708.07747 (2017)

  45. **e, C., Wu, Y., van der Maaten, L., Yuille, A.L., He, K.: Feature denoising for improving adversarial robustness. In: CVPR, pp. 501–509 (2019)

    Google Scholar 

  46. Yuan, X., He, P., Zhu, Q., Li, X.: Adversarial examples: attacks and defenses for deep learning. IEEE Trans. Neural Netw. Learn. Syst. 30(9), 2805–2824 (2019)

    Article  MathSciNet  Google Scholar 

  47. Zeng, H., Zhu, C., Goldstein, T., Huang, F.: Are adversarial examples created equal? A learnable weighted minimax risk for robustness under non-uniform attacks. In: AAAI, pp. 10815–10823 (2021)

    Google Scholar 

  48. Zhang, C., Benz, P., Imtiaz, T., Kweon, I.S.: Understanding adversarial examples from the mutual influence of images and perturbations. In: CVPR, pp. 14521–14530 (2020)

    Google Scholar 

  49. Zhang, H., Weng, T., Chen, P., Hsieh, C., Daniel, L.: Efficient neural network robustness certification with general activation functions. In: NeurIPS (2018)

    Google Scholar 

Download references

Acknowledgements

We thank the reviewers for their feedback. This research was supported by the Israel Science Foundation (grant No. 2605/20).

Author information

Authors and Affiliations

  1. Technion, Haifa, Israel

    Anan Kabaha & Dana Drachsler-Cohen

Authors
  1. Anan Kabaha
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dana Drachsler-Cohen
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Anan Kabaha .

Editor information

Editors and Affiliations

  1. Inria, Amazon Web Services, Courbevoie, France

    Cezara Dragoi

  2. Amazon Web Services, Seattle, WA, USA

    Michael Emmi

  3. University of Southern California, Los Angeles, CA, USA

    **gbo Wang

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Kabaha, A., Drachsler-Cohen, D. (2023). Maximal Robust Neural Network Specifications via Oracle-Guided Numerical Optimization. In: Dragoi, C., Emmi, M., Wang, J. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2023. Lecture Notes in Computer Science, vol 13881. Springer, Cham. https://doi.org/10.1007/978-3-031-24950-1_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-24950-1_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-24949-5

  • Online ISBN: 978-3-031-24950-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation