nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Towards Logical Specification of Statistical Machine Learning

verfasst von : Yusuke Kawamoto

Erschienen in: Software Engineering and Formal Methods

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

We introduce a logical approach to formalizing statistical properties of machine learning. Specifically, we propose a formal model for statistical classification based on a Kripke model, and formalize various notions of classification performance, robustness, and fairness of classifiers by using epistemic logic. Then we show some relationships among properties of classifiers and those between classification performance and robustness, which suggests robustness-related properties that have not been formalized in the literature as far as we know. To formalize fairness properties, we define a notion of counterfactual knowledge and show techniques to formalize conditional indistinguishability by using counterfactual epistemic operators. As far as we know, this is the first work that uses logical formulas to express statistical properties of machine learning, and that provides epistemic (resp. counterfactually epistemic) views on robustness (resp. fairness) of classifiers.

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!

Jetzt informieren

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!

Jetzt informieren

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!

Jetzt informieren

Vorheriges Kapitel Isabelle/DOF: Design and Implementation

Nächstes Kapitel Efficient Formal Verification for the Linux Kernel

Nur mit Berechtigung zugänglich

Our definition of counterfactual knowledge is limited to the condition of having an observation different from the actual one. More general notions of counterfactual knowledge can be found in previous work (e.g., [38]).

This usage of modality relies on the fact that the value of the measurement variable x can be different in different possible worlds.

For instance, fairness through awareness [13] requires that protected attributes (e.g., race, religion, or gender) are not explicitly used in the prediction process. However, StatEL may not be suited to formalizing such a property in treatment.

Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181–185 (1985). https://doi.org/10.1016/0020-0190(85)90056-0MathSciNetCrossRefMATH

Athalye, A., Engstrom, L., Ilyas, A., Kwok, K.: Synthesizing robust adversarial examples. In: Proceedings of the ICML, pp. 284–293 (2018)

Balliu, M., Dam, M., Guernic, G.L.: Epistemic temporal logic for information flow security. In: Proceedings of PLAS, p. 6 (2011). https://doi.org/10.1145/2166956.2166962

Bana, G.: Models of objective chance: an analysis through examples. In: Hofer-Szabó, G., Wroński, L. (eds.) Making it Formally Explicit. ESPS, vol. 6, pp. 43–60. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-55486-0_3CrossRef

Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18–36 (1990). https://doi.org/10.1145/77648.77649CrossRefMATH

Carlini, N., Wagner, D.A.: Towards evaluating the robustness of neural networks. In: Proceedings Security and Privacy, pp. 39–57 (2017). https://doi.org/10.1109/SP.2017.49

Chadha, R., Delaune, S., Kremer, S.: Epistemic logic for the applied pi calculus. In: Proceedings of FMOODS/FORTE, pp. 182–197 (2009).https://doi.org/10.1007/978-3-642-02138-1_12CrossRef

Chakraborty, A., Alam, M., Dey, V., Chattopadhyay, A., Mukhopadhyay, D.: Adversarial attacks and defences: a survey. CoRR abs/1810.00069 (2018). http://arxiv.org/abs/1810.00069

Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: Proceedings of CSF, pp. 51–65. IEEE (2008). https://doi.org/10.1109/CSF.2008.7

10.

Dechesne, F., Mousavi, M., Orzan, S.: Operational and epistemic approaches to protocol analysis: bridging the gap. In: Proceedings of LPAR, pp. 226–241 (2007)

11.

Dreossi, T., Ghosh, S., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: A formalization of robustness for deep neural networks. In: Proceedings of VNN (2019)

12.

Dwork, C.: Differential privacy. In: Proceedings of ICALP, pp. 1–12 (2006)

13.

Dwork, C., Hardt, M., Pitassi, T., Reingold, O., Zemel, R.S.: Fairness through awareness. In: Proceedings of ITCS, pp. 214–226. ACM (2012)

14.

Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning About Knowledge. The MIT Press, Cambridge (1995)MATH

15.

French, T., Gozzard, A., Reynolds, M.: Dynamic aleatoric reasoning in games of bluffing and chance. In: Proceedings of AAMAS, pp. 1964–1966 (2019)

16.

Gajane, P.: On formalizing fairness in prediction with machine learning. CoRR abs/1710.03184 (2017). http://arxiv.org/abs/1710.03184

17.

Garcia, F.D., Hasuo, I., Pieters, W., van Rossum, P.: Provable anonymity. In: Proceedings of FMSE, pp. 63–72 (2005). https://doi.org/10.1145/1103576.1103585

18.

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

19.

Halpern, J.Y.: Reasoning About Uncertainty. The MIT press, Cambridge (2003)MATH

20.

Halpern, J.Y., O’Neill, K.R.: Anonymity and information hiding in multiagent systems. J. Comput. Secur. 13(3), 483–512 (2005)CrossRef

21.

Hardt, M., Price, E., Srebro, N.: Equality of opportunity in supervised learning. In: proceedings of NIPS, pp. 3315–3323 (2016)

22.

Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Proceedings of CAV, pp. 3–29 (2017). https://doi.org/10.1007/978-3-319-63387-9_1CrossRef

23.

Hughes, D., Shmatikov, V.: Information hiding, anonymity and privacy: a modular approach. J. Comput. Secur. 12(1), 3–36 (2004)CrossRef

24.

Jonker, H.L., Pieters, W.: Receipt-freeness as a special case of anonymity in epistemic logic. In: Proceedings of Workshop On Trustworthy Elections (WOTE 2006), June 2006

25.

Katz, G., Barrett, C.W., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Proceedings of CAV, pp. 97–117 (2017). https://doi.org/10.1007/978-3-319-63387-9_5CrossRef

26.

Kawamoto, Y.: Statistical epsitemic logic. CoRR abs/1412.4451 (2019). https://arxiv.org/pdf/1907.05995.pdf

27.

Kawamoto, Y., Mano, K., Sakurada, H., Hagiya, M.: Partial knowledge of functions and verification of anonymity. Trans. Japan Soc. Ind. Appl. Math. 17(4), 559–576 (2007). https://doi.org/10.11540/jsiamt.17.4_559CrossRef

28.

Kripke, S.A.: Semantical analysis of modal logic i normal modal propositional calculi. Math. Logic Q. 9(5–6), 67–96 (1963)MathSciNetCrossRef

29.

Lewis, D.: A subjectivist’s guide to objective chance. In: Studies in Inductive Logic and Probability, Vol. II, pp. 263–293. University of California Press, Berkeley (1980)

30.

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

31.

Moosavi-Dezfooli, S., Fawzi, A., Frossard, P.: Deepfool: A simple and accurate method to fool deep neural networks. In: Proceedings of CVPR, pp. 2574–2582 (2016). https://doi.org/10.1109/CVPR.2016.282

32.

Pardo, R., Schneider, G.: A formal privacy policy framework for social networks. In: Proceedings of SEFM, pp. 378–392 (2014). https://doi.org/10.1007/978-3-319-10431-7_30CrossRef

33.

Pei, K., Cao, Y., Yang, J., Jana, S.: Deepxplore: automated whitebox testing of deep learning systems. In: Proceedings of SOSP, pp. 1–18 (2017). https://doi.org/10.1145/3132747.3132785

34.

Seshia, S.A., et al.: Formal specification for deep neural networks. In: Lahiri, S.K., Wang, C. (eds.) ATVA 2018. LNCS, vol. 11138, pp. 20–34. Springer, Cham (2018). https://doi.org/10.1007/978-3-030-01090-4_2CrossRef

35.

Syverson, P.F., Stubblebine, S.G.: Group principals and the formalization of anonymity. In: Wing, J.M., Woodcock, J., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 814–833. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48119-2_45CrossRef

36.

Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I.J., Fergus, R.: Intriguing properties of neural networks. In: Proceedings of ICLR (2014)

37.

Tian, Y., Pei, K., Jana, S., Ray, B.: Deeptest: automated testing of deep-neural-network-driven autonomous cars. In: Proceedings of ICSE, pp. 303–314 (2018). https://doi.org/10.1145/3180155.3180220

38.

Williamson, T.: Philosophical knowledge and knowledge of counterfactuals. Grazer Philosophische Studien 74, 89 (2007)CrossRef

39.

von Wright, G.H.: An Essay in Modal Logic. North-Holland Pub. Co., Amsterdam (1951)MATH

40.

Zafar, M.B., Valera, I., Gomez-Rodriguez, M., Gummadi, K.P.: Fairness beyond disparate treatment and disparate impact: Learning classification without disparate mistreatment. In: Proceedings of WWW, pp. 1171–1180 (2017). https://doi.org/10.1145/3038912.3052660

Titel: Towards Logical Specification of Statistical Machine Learning
verfasst von: Yusuke Kawamoto
Verlag: Springer International Publishing
Buch: Software Engineering and Formal Methods
Print ISBN: 978-3-030-30445-4

Electronic ISBN: 978-3-030-30446-1

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-030-30446-1_16

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner