{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T01:43:43Z","timestamp":1768095823092,"version":"3.49.0"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2020,9,19]],"date-time":"2020-09-19T00:00:00Z","timestamp":1600473600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2020,9,19]],"date-time":"2020-09-19T00:00:00Z","timestamp":1600473600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100009024","name":"Exploratory Research for Advanced Technology","doi-asserted-by":"publisher","award":["JPMJER1603"],"award-info":[{"award-number":["JPMJER1603"]}],"id":[{"id":"10.13039\/501100009024","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001863","name":"New Energy and Industrial Technology Development Organization","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100001863","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100012950","name":"Institut national de recherche en informatique et en automatique","doi-asserted-by":"publisher","award":["project LOGIS"],"award-info":[{"award-number":["project LOGIS"]}],"id":[{"id":"10.13039\/100012950","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Softw Syst Model"],"published-print":{"date-parts":[[2021,4]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We propose an epistemic approach to formalizing statistical properties of machine learning. Specifically, we introduce a formal model for supervised learning based on a Kripke model where each possible world corresponds to a possible dataset and modal operators are interpreted as transformation and testing on datasets. Then, we formalize various notions of the classification performance, robustness, and fairness of statistical classifiers by using our extension of statistical epistemic logic. In this formalization, we show relationships among properties of classifiers, and relevance between classification performance and robustness. As far as we know, this is the first work that uses epistemic models and logical formulas to express statistical properties of machine learning, and would be a starting point to develop theories of formal specification of machine learning.<\/jats:p>","DOI":"10.1007\/s10270-020-00825-2","type":"journal-article","created":{"date-parts":[[2020,9,19]],"date-time":"2020-09-19T04:07:50Z","timestamp":1600488470000},"page":"293-310","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":5,"title":["An epistemic approach to the formal specification of statistical machine learning"],"prefix":"10.1007","volume":"20","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2151-9560","authenticated-orcid":false,"given":"Yusuke","family":"Kawamoto","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,9,19]]},"reference":[{"key":"825_CR1","doi-asserted-by":"publisher","unstructured":"Angell, R., Johnson, B., Brun, Y., Meliou, A.: Themis: automatically testing software for discrimination. In: Proceedings of ESEC\/SIGSOFT FSE, pp. 871\u2013875. ACM (2018). https:\/\/doi.org\/10.1145\/3236024.3264590","DOI":"10.1145\/3236024.3264590"},{"key":"825_CR2","unstructured":"Athalye, A., Engstrom, L., Ilyas, A., Kwok, K.: Synthesizing robust adversarial examples. In: Proceedings of ICML, pp. 284\u2013293 (2018)"},{"key":"825_CR3","doi-asserted-by":"publisher","unstructured":"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","DOI":"10.1145\/2166956.2166962"},{"key":"825_CR4","doi-asserted-by":"publisher","unstructured":"Bana, G.: Models of objective chance: an analysis through examples. In: Making it Formally Explicit. Springer, pp. 43\u201360 (2017). https:\/\/doi.org\/10.1007\/978-3-319-55486-0_3","DOI":"10.1007\/978-3-319-55486-0_3"},{"key":"825_CR5","unstructured":"Barocas, S., Hardt, M., Narayanan, A.: Fairness and machine learning. http:\/\/www.fairmlbook.org (2019)"},{"key":"825_CR6","doi-asserted-by":"publisher","DOI":"10.1177\/0049124118782533","author":"R Berk","year":"2018","unstructured":"Berk, R., Heidari, H., Jabbari, S., Kearns, M., Roth, A.: Fairness in criminal justice risk assessments: the state of the art. Sociol. Methods Res. (2018). https:\/\/doi.org\/10.1177\/0049124118782533","journal-title":"Sociol. Methods Res."},{"key":"825_CR7","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic. Cambridge Tracts in Theoretical Computer Science","author":"P Blackburn","year":"2001","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2001). https:\/\/doi.org\/10.1017\/CBO9781107050884"},{"issue":"1","key":"825_CR8","doi-asserted-by":"publisher","first-page":"18","DOI":"10.1145\/77648.77649","volume":"8","author":"M Burrows","year":"1990","unstructured":"Burrows, M., Abadi, M., Needham, R.M.: A logic of authentication. ACM Trans. Comput. Syst. 8(1), 18\u201336 (1990). https:\/\/doi.org\/10.1145\/77648.77649","journal-title":"ACM Trans. Comput. Syst."},{"issue":"2","key":"825_CR9","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1007\/s10618-010-0190-x","volume":"21","author":"T Calders","year":"2010","unstructured":"Calders, T., Verwer, S.: Three naive bayes approaches for discrimination-free classification. Data Min. Knowl. Discov. 21(2), 277\u2013292 (2010). https:\/\/doi.org\/10.1007\/s10618-010-0190-x","journal-title":"Data Min. Knowl. Discov."},{"key":"825_CR10","doi-asserted-by":"publisher","unstructured":"Carlini, N., Wagner, D.A.: Towards evaluating the robustness of neural networks. In: Proceedings of S&P, pp. 39\u201357 (2017). https:\/\/doi.org\/10.1109\/SP.2017.49","DOI":"10.1109\/SP.2017.49"},{"key":"825_CR11","doi-asserted-by":"publisher","unstructured":"Chadha, R., Delaune, S., Kremer, S.: Epistemic logic for the applied pi calculus. In: Proceedings of FMOODS\/FORTE, pp. 182\u2013197 (2009). https:\/\/doi.org\/10.1007\/978-3-642-02138-1_12","DOI":"10.1007\/978-3-642-02138-1_12"},{"key":"825_CR12","unstructured":"Chakraborty, A., Alam, M., Dey, V., Chattopadhyay, A., Mukhopadhyay, D.: Adversarial attacks and defences: a survey (2018). CoRR arXiv:1810.00069"},{"key":"825_CR13","unstructured":"Dreossi, T., Ghosh, S., Sangiovanni-Vincentelli, A.L., Seshia, S.A.: A formalization of robustness for deep neural networks. In: Proceedings of VNN (2019)"},{"key":"825_CR14","doi-asserted-by":"crossref","unstructured":"Dwork, C.: Differential privacy. In: Proceedings of ICALP, pp. 1\u201312 (2006)","DOI":"10.1007\/11787006_1"},{"key":"825_CR15","doi-asserted-by":"crossref","unstructured":"Dwork, C., Hardt, M., Pitassi, T., Reingold, O., Zemel, R.S.: Fairness through awareness. In: Proceedings of ITCS, pp. 214\u2013226. ACM (2012)","DOI":"10.1145\/2090236.2090255"},{"key":"825_CR16","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning About Knowledge","author":"R Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning About Knowledge. The MIT Press, Cambridge (1995)"},{"key":"825_CR17","unstructured":"Gajane, P.: On formalizing fairness in prediction with machine learning (2017). CoRR arXiv:1710.03184"},{"key":"825_CR18","doi-asserted-by":"publisher","unstructured":"Galhotra, S., Brun, Y., Meliou, A.: Fairness testing: testing software for discrimination. In: Proceedings of ESEC\/FSE, pp. 498\u2013510. ACM (2017). https:\/\/doi.org\/10.1145\/3106237.3106277","DOI":"10.1145\/3106237.3106277"},{"key":"825_CR19","doi-asserted-by":"publisher","unstructured":"Garcia, F.D., Hasuo, I., Pieters, W., van Rossum, P.: Provable anonymity. In: Proceedings of FMSE, pp. 63\u201372 (2005). https:\/\/doi.org\/10.1145\/1103576.1103585","DOI":"10.1145\/1103576.1103585"},{"key":"825_CR20","unstructured":"Goodfellow, I.J., Shlens, J., Szegedy, C.: Explaining and harnessing adversarial examples. In: Proceedings of ICLR (2015)"},{"key":"825_CR21","volume-title":"Reasoning About Uncertainty","author":"JY Halpern","year":"2003","unstructured":"Halpern, J.Y.: Reasoning About Uncertainty. The MIT Press, Cambridge (2003)"},{"key":"825_CR22","unstructured":"Hardt, M., Price, E., Srebro, N.: Equality of opportunity in supervised learning. In: Proceedings of NIPS, pp. 3315\u20133323 (2016)"},{"key":"825_CR23","doi-asserted-by":"publisher","unstructured":"Huang, X., Kwiatkowska, M., Wang, S., Wu, M.: Safety verification of deep neural networks. In: Proceedings of CAV, pp. 3\u201329 (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_1","DOI":"10.1007\/978-3-319-63387-9_1"},{"issue":"1","key":"825_CR24","doi-asserted-by":"publisher","first-page":"3","DOI":"10.3233\/JCS-2004-12102","volume":"12","author":"D Hughes","year":"2004","unstructured":"Hughes, D., Shmatikov, V.: Information hiding, anonymity and privacy: a modular approach. J. Comput. Secur. 12(1), 3\u201336 (2004)","journal-title":"J. Comput. Secur."},{"key":"825_CR25","unstructured":"Jonker, H.L., Pieters, W.: Receipt-freeness as a special case of anonymity in epistemic logic. In: Proceedings of Workshop on Trustworthy Elections (WOTE\u201906) (2006)"},{"key":"825_CR26","doi-asserted-by":"publisher","unstructured":"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\u2013117 (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"825_CR27","doi-asserted-by":"publisher","unstructured":"Kawamoto, Y.: Statistical epistemic logic. In: The Art of Modelling Computational Systems: A Journey from Logic and Concurrency to Security and Privacy\u2014Essays Dedicated to Catuscia Palamidessi on the Occasion of Her 60th Birthday, LNCS, vol. 11760, pp. 344\u2013362. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-31175-9_20","DOI":"10.1007\/978-3-030-31175-9_20"},{"key":"825_CR28","doi-asserted-by":"publisher","unstructured":"Kawamoto, Y.: Towards logical specification of statistical machine learning. In: Proceedings of SEFM, LNCS, vol. 11724, pp. 293\u2013311. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-30446-1_16","DOI":"10.1007\/978-3-030-30446-1_16"},{"issue":"4","key":"825_CR29","doi-asserted-by":"publisher","first-page":"559","DOI":"10.11540\/jsiamt.17.4_559","volume":"17","author":"Y Kawamoto","year":"2007","unstructured":"Kawamoto, Y., Mano, K., Sakurada, H., Hagiya, M.: Partial knowledge of functions and verification of anonymity. Trans. Jpn. Soc. Ind. Appl. Math. 17(4), 559\u2013576 (2007). https:\/\/doi.org\/10.11540\/jsiamt.17.4_559","journal-title":"Trans. Jpn. Soc. Ind. Appl. Math."},{"issue":"5\u20136","key":"825_CR30","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"SA Kripke","year":"1963","unstructured":"Kripke, S.A.: Semantical analysis of modal logic I normal modal propositional calculi. Math. Log. Q. 9(5\u20136), 67\u201396 (1963)","journal-title":"Math. Log. Q."},{"key":"825_CR31","doi-asserted-by":"crossref","unstructured":"Lewis, D.: A subjectivist\u2019s guide to objective chance. In: Studies in Inductive Logic and Probability, vol. II, pp. 263\u2013293. University of California Press, Berkeley (1980)","DOI":"10.1525\/9780520318328-009"},{"key":"825_CR32","unstructured":"Madry, A., Makelov, A., Schmidt, L., Tsipras, D., Vladu, A.: Towards deep learning models resistant to adversarial attacks. In: Proceedings of ICLR (2018)"},{"key":"825_CR33","doi-asserted-by":"publisher","unstructured":"Moosavi-Dezfooli, S., Fawzi, A., Frossard, P.: Deepfool: a simple and accurate method to fool deep neural networks. In: Proceedings of CVPR, pp. 2574\u20132582 (2016). https:\/\/doi.org\/10.1109\/CVPR.2016.282","DOI":"10.1109\/CVPR.2016.282"},{"key":"825_CR34","doi-asserted-by":"publisher","unstructured":"Pardo, R., Schneider, G.: A formal privacy policy framework for social networks. In: Proceedings of SEFM, pp. 378\u2013392 (2014). https:\/\/doi.org\/10.1007\/978-3-319-10431-7_30","DOI":"10.1007\/978-3-319-10431-7_30"},{"key":"825_CR35","doi-asserted-by":"publisher","unstructured":"Pei, K., Cao, Y., Yang, J., Jana, S.: Deepxplore: automated whitebox testing of deep learning systems. In: Proceedings of SOSP, pp. 1\u201318 (2017). https:\/\/doi.org\/10.1145\/3132747.3132785","DOI":"10.1145\/3132747.3132785"},{"key":"825_CR36","unstructured":"Prior, A.N.: Time and modality (1957)"},{"issue":"1\u20132","key":"825_CR37","doi-asserted-by":"publisher","first-page":"107","DOI":"10.1007\/s10994-006-5833-1","volume":"62","author":"M Richardson","year":"2006","unstructured":"Richardson, M., Domingos, P.M.: Markov logic networks. Mach. Learn. 62(1\u20132), 107\u2013136 (2006). https:\/\/doi.org\/10.1007\/s10994-006-5833-1","journal-title":"Mach. Learn."},{"key":"825_CR38","doi-asserted-by":"publisher","unstructured":"Seshia, S.A., Desai, A., Dreossi, T., Fremont, D.J., Ghosh, S., Kim, E., Shivakumar, S., Vazquez-Chanlatte, M., Yue, X.: Formal specification for deep neural networks. In: Proceedings of ATVA, pp. 20\u201334 (2018). https:\/\/doi.org\/10.1007\/978-3-030-01090-4_2","DOI":"10.1007\/978-3-030-01090-4_2"},{"key":"825_CR39","doi-asserted-by":"publisher","first-page":"814","DOI":"10.1007\/3-540-48119-2_45","volume":"1","author":"PF Syverson","year":"1999","unstructured":"Syverson, P.F., Stubblebine, S.G.: Group principals and the formalization of anonymity. World Congress Form. Methods 1, 814\u2013833 (1999). https:\/\/doi.org\/10.1007\/3-540-48119-2_45","journal-title":"World Congress Form. Methods"},{"key":"825_CR40","unstructured":"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)"},{"key":"825_CR41","doi-asserted-by":"publisher","unstructured":"Tian, Y., Pei, K., Jana, S., Ray, B.: Deeptest: automated testing of deep-neural-network-driven autonomous cars. In: Proceedings of ICSE, pp. 303\u2013314 (2018). https:\/\/doi.org\/10.1145\/3180155.3180220","DOI":"10.1145\/3180155.3180220"},{"key":"825_CR42","doi-asserted-by":"publisher","unstructured":"Udeshi, S., Arora, P., Chattopadhyay, S.: Automated directed fairness testing. In: Proceedings of ASE, pp. 98\u2013108. ACM (2018). https:\/\/doi.org\/10.1145\/3238147.3238165","DOI":"10.1145\/3238147.3238165"},{"issue":"3","key":"825_CR43","first-page":"64","volume":"5","author":"L Vaserstein","year":"1969","unstructured":"Vaserstein, L.: Markovian processes on countable space product describing large systems of automata. Probl. Peredachi Inf. 5(3), 64\u201372 (1969)","journal-title":"Probl. Peredachi Inf."},{"key":"825_CR44","volume-title":"An Essay in Modal Logic","author":"GH von Wright","year":"1951","unstructured":"von Wright, G.H.: An Essay in Modal Logic. North-Holland Pub. Co., Amsterdam (1951)"},{"issue":"3","key":"825_CR45","doi-asserted-by":"publisher","first-page":"338","DOI":"10.1016\/S0019-9958(65)90241-X","volume":"8","author":"L Zadeh","year":"1965","unstructured":"Zadeh, L.: Fuzzy sets. Inf. Control 8(3), 338\u2013353 (1965). https:\/\/doi.org\/10.1016\/S0019-9958(65)90241-X","journal-title":"Inf. Control"},{"key":"825_CR46","doi-asserted-by":"publisher","unstructured":"Zafar, M.B., Valera, I., Gomez-Rodriguez, M., Gummadi, K.P.: Fairness beyond disparate treatment & disparate impact: learning classification without disparate mistreatment. In: Proceedings of WWW, pp. 1171\u20131180 (2017). https:\/\/doi.org\/10.1145\/3038912.3052660","DOI":"10.1145\/3038912.3052660"}],"container-title":["Software and Systems Modeling"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00825-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10270-020-00825-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10270-020-00825-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,8,14]],"date-time":"2024-08-14T05:10:36Z","timestamp":1723612236000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10270-020-00825-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,9,19]]},"references-count":46,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2021,4]]}},"alternative-id":["825"],"URL":"https:\/\/doi.org\/10.1007\/s10270-020-00825-2","relation":{},"ISSN":["1619-1366","1619-1374"],"issn-type":[{"value":"1619-1366","type":"print"},{"value":"1619-1374","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,9,19]]},"assertion":[{"value":"2 March 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 June 2020","order":2,"name":"revised","label":"Revised","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 August 2020","order":3,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"19 September 2020","order":4,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}