Skip to main content
Erschienen in:
Buchtitelbild

2020 | OriginalPaper | Buchkapitel

Formal Verification of Neural Networks?

verfasst von : Martin Leucker

Erschienen in: Formal Methods: Foundations and Applications

Verlag: Springer International Publishing

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Machine learning is a popular tool for building state of the art software systems. It is more and more used also in safety critical areas. This demands for verification techniques ensuring the safety and security of machine learning based solutions. However, we argue that the popularity of machine learning comes from the fact that no formal specification exists which renders traditional verification inappropriate. Instead, validation is typically demanded, but formalization of so far informal requirements is necessary to give formal evidence that the right system is build. Moreover, we present a recent technique that allows to check certain properties for an underlying recurrent neural network and which may be uses as a tool to identify whether the system learned is right.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Fußnoten
1
“In short, Boehm (3) expressed the difference between the software verification and software validation as follows: Verification: “Are we building the product right?” Validation: “Are we building the right product?” [12].
 
3
The requirements are listed here in a very brief form. Please consult the original article for an elaborate explanation.
 
Literatur
2.
Zurück zum Zitat Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)MATH
4.
Zurück zum Zitat Deng, L., Hinton, G., Kingsbury, B.: New types of deep neural network learning for speech recognition and related applications: an overview. In: 2013 IEEE International Conference on Acoustics, Speech and Signal Processing, pp. 8599–8603 (2013) Deng, L., Hinton, G., Kingsbury, B.: New types of deep neural network learning for speech recognition and related applications: an overview. In: 2013 IEEE International Conference on Acoustics, Speech and Signal Processing, pp. 8599–8603 (2013)
5.
Zurück zum Zitat Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Boehm, B.W., Garlan, D., Kramer, J. (eds.) International Conference on Software Engineering, ICSE 1999, pp. 411–420. ACM (1999) Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in property specifications for finite-state verification. In: Boehm, B.W., Garlan, D., Kramer, J. (eds.) International Conference on Software Engineering, ICSE 1999, pp. 411–420. ACM (1999)
10.
Zurück zum Zitat Liu, J., et al.: Applications of deep learning to MRI images: a survey. Big Data Min. Anal. 1(1), 1–18 (2018)CrossRef Liu, J., et al.: Applications of deep learning to MRI images: a survey. Big Data Min. Anal. 1(1), 1–18 (2018)CrossRef
11.
Zurück zum Zitat Mahmud, M., Kaiser, M.S., Hussain, A., Vassanelli, S.: Applications of deep learning and reinforcement learning to biological data. IEEE Trans. Neural Netw. Learn. Syst. 29(6), 2063–2079 (2018)MathSciNetCrossRef Mahmud, M., Kaiser, M.S., Hussain, A., Vassanelli, S.: Applications of deep learning and reinforcement learning to biological data. IEEE Trans. Neural Netw. Learn. Syst. 29(6), 2063–2079 (2018)MathSciNetCrossRef
13.
Zurück zum Zitat Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science (FOCS 1977), Providence, Rhode Island, 31 October–2 November 1977, pp. 46–57. IEEE Computer Society Press (1977) Pnueli, A.: The temporal logic of programs. In: Proceedings of the 18th IEEE Symposium on the Foundations of Computer Science (FOCS 1977), Providence, Rhode Island, 31 October–2 November 1977, pp. 46–57. IEEE Computer Society Press (1977)
Metadaten
Titel
Formal Verification of Neural Networks?
verfasst von
Martin Leucker
Copyright-Jahr
2020
DOI
https://doi.org/10.1007/978-3-030-63882-5_1