{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,25]],"date-time":"2026-01-25T00:12:58Z","timestamp":1769299978816,"version":"3.49.0"},"reference-count":43,"publisher":"Springer Science and Business Media LLC","issue":"2","license":[{"start":{"date-parts":[[2018,9,22]],"date-time":"2018-09-22T00:00:00Z","timestamp":1537574400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["713999"],"award-info":[{"award-number":["713999"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100010663","name":"H2020 European Research Council","doi-asserted-by":"publisher","award":["713999"],"award-info":[{"award-number":["713999"]}],"id":[{"id":"10.13039\/100010663","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2019,8]]},"DOI":"10.1007\/s10817-018-9481-5","type":"journal-article","created":{"date-parts":[[2018,9,22]],"date-time":"2018-09-22T06:41:07Z","timestamp":1537598467000},"page":"347-368","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["A Formal Proof of the Expressiveness of Deep Learning"],"prefix":"10.1007","volume":"63","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-7158-3595","authenticated-orcid":false,"given":"Alexander","family":"Bentkamp","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jasmin Christian","family":"Blanchette","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Dietrich","family":"Klakow","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2018,9,22]]},"reference":[{"issue":"4","key":"9481_CR1","doi-asserted-by":"publisher","first-page":"635","DOI":"10.1145\/1186785.1186794","volume":"32","author":"BW Bader","year":"2006","unstructured":"Bader, B.W., Kolda, T.G.: Algorithm 862: MATLAB tensor classes for fast algorithm prototyping. ACM Trans. Math. Softw. 32(4), 635\u2013653 (2006)","journal-title":"ACM Trans. Math. Softw."},{"key":"9481_CR2","unstructured":"Bentkamp, A.: Expressiveness of deep learning. Archive of Formal Proofs (2016). Formal proof development \n                    http:\/\/isa-afp.org\/entries\/Deep_Learning.shtml"},{"key":"9481_CR3","unstructured":"Bentkamp, A.: An Isabelle formalization of the expressiveness of deep learning. M.Sc. thesis, Universit\u00e4t des Saarlandes (2016). \n                    http:\/\/matryoshka.gforge.inria.fr\/pubs\/bentkamp_msc_thesis.pdf"},{"key":"9481_CR4","doi-asserted-by":"crossref","unstructured":"Bentkamp, A., Blanchette, J.C., Klakow, D.: A formal proof of the expressiveness of deep learning. In: Ayala-Rinc\u00f3n, M., Mu\u00f1oz, C.A. (eds.) Interactive Theorem Proving (ITP 2017), LNCS, vol. 10499, pp. 46\u201364. Springer (2017)","DOI":"10.1007\/978-3-319-66107-0_4"},{"key":"9481_CR5","doi-asserted-by":"crossref","unstructured":"Bernard, S., Bertot, Y., Rideau, L., Strub, P.: Formal proofs of transcendence for $e$ and $\\pi $ as an application of multivariate and symmetric polynomials. In: Avigad, J., Chlipala, A. (eds.) Certified Programs and Proofs (CPP 2016), pp. 76\u201387. ACM (2016)","DOI":"10.1145\/2854065.2854072"},{"key":"9481_CR6","doi-asserted-by":"crossref","unstructured":"Bertot, Y., Gonthier, G., Biha, S.O., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C.A., Tahar, S. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2008), vol. 5170, pp. 86\u2013101. Springer (2008)","DOI":"10.1007\/978-3-540-71067-7_11"},{"key":"9481_CR7","unstructured":"Bhat, S.: Syntactic foundations for machine learning. Ph.D. thesis, Georgia Institute of Technology (2013). \n                    https:\/\/smartech.gatech.edu\/bitstream\/handle\/1853\/47700\/bhat_sooraj_b_201305_phd.pdf"},{"issue":"2","key":"9481_CR8","doi-asserted-by":"publisher","first-page":"155","DOI":"10.1007\/s10817-015-9335-3","volume":"56","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., B\u00f6hme, S., Fleury, M., Smolka, S.J., Steckermeier, A.: Semi-intelligible Isar proofs from machine-generated proofs. J. Autom. Reason. 56(2), 155\u2013200 (2016)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"9481_CR9","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9362-8","volume":"57","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Greenaway, D., Kaliszyk, C., K\u00fchlwein, D., Urban, J.: A learning-based fact selector for Isabelle\/HOL. J. Autom. Reason. 57(3), 219\u2013244 (2016)","journal-title":"J. Autom. Reason."},{"key":"9481_CR10","doi-asserted-by":"crossref","unstructured":"Boender, J., Kamm\u00fcller, F., Nagarajan, R.: Formalization of quantum protocols using Coq. In: Heunen, C., Selinger, P., Vicary, J. (eds.) Workshop on Quantum Physics and Logic (QPL 2015), EPTCS, vol. 195, pp. 71\u201383 (2015)","DOI":"10.4204\/EPTCS.195.6"},{"key":"9481_CR11","doi-asserted-by":"crossref","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) Interactive Theorem Proving (ITP 2010), LNCS, vol. 6172, pp. 179\u2013194. Springer (2010)","DOI":"10.1007\/978-3-642-14052-5_14"},{"issue":"263","key":"9481_CR12","doi-asserted-by":"publisher","first-page":"1559","DOI":"10.1090\/S0025-5718-08-02060-7","volume":"77","author":"P B\u00fcrgisser","year":"2008","unstructured":"B\u00fcrgisser, P., Cucker, F., Lotz, M.: The probability that a slightly perturbed numerical analysis problem is difficult. Math. Comput. 77(263), 1559\u20131583 (2008)","journal-title":"Math. Comput."},{"key":"9481_CR13","unstructured":"Caron, R., Traynor, T.: The zero set of a polynomial. Technical report, University of Windsor (2005). \n                    http:\/\/www1.uwindsor.ca\/math\/sites\/uwindsor.ca.math\/files\/05-03.pdf"},{"issue":"2","key":"9481_CR14","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Log. 5(2), 56\u201368 (1940)","journal-title":"J. Symb. Log."},{"key":"9481_CR15","doi-asserted-by":"crossref","unstructured":"Cohen, N., Sharir, O., Shashua, A.: Deep SimNets. In: Computer Vision and Pattern Recognition (CVPR 2016), pp. 4782\u20134791. IEEE Computer Society (2016)","DOI":"10.1109\/CVPR.2016.517"},{"key":"9481_CR16","unstructured":"Cohen, N., Sharir, O., Shashua, A.: On the expressive power of deep learning: a tensor analysis. In: Feldman, V., Rakhlin, A., Shamir, O. (eds.) Conference on Learning Theory (COLT 2016), JMLR Workshop and Conference Proceedings, vol.\u00a049, pp. 698\u2013728. JMLR.org (2016)"},{"key":"9481_CR17","unstructured":"Cohen, N., Shashua, A.: Convolutional rectifier networks as generalized tensor decompositions. In: Balcan, M., Weinberger, K.Q. (eds.) International Conference on Machine Learning (ICML 2016), JMLR Workshop and Conference Proceedings, vol.\u00a048, pp. 955\u2013963. JMLR.org (2016)"},{"key":"9481_CR18","unstructured":"Cohen, N., Shashua, A.: Inductive bias of deep convolutional networks through pooling geometry. CoRR arXiv:1605.06743 (2016)"},{"key":"9481_CR19","unstructured":"Cohen, N., Tamari, R., Shashua, A.: Boosting dilated convolutional networks with mixed tensor decompositions. CoRR arXiv:1703.06846 (2017)"},{"key":"9481_CR20","doi-asserted-by":"crossref","unstructured":"de\u00a0Moura, L., Bj\u00f8rner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2008), LNCS, vol. 4963, pp. 337\u2013340. Springer (2008)","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"9481_CR21","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-09724-4","volume-title":"Edinburgh LCF: A Mechanised Logic of Computation, LNCS","author":"MJC Gordon","year":"1979","unstructured":"Gordon, M.J.C., Milner, R., Wadsworth, C.P.: Edinburgh LCF: A Mechanised Logic of Computation, LNCS, vol. 78. Springer, Berlin (1979)"},{"key":"9481_CR22","unstructured":"Haftmann, F., Lochbihler, A., Schreiner, W.: Towards abstract and executable multivariate polynomials in Isabelle. In: Nipkow, T., Paulson, L., Wenzel, M. (eds.) Isabelle Workshop 2014 (2014)"},{"key":"9481_CR23","unstructured":"Hardt, M., Recht, B., Singer, Y.: Train faster, generalize better: stability of stochastic gradient descent. In: Balcan, M., Weinberger, K.Q. (eds.) International Conference on Machine Learning (ICML 2016), JMLR Workshop and Conference Proceedings, vol.\u00a048, pp. 1225\u20131234. JMLR (2016)"},{"key":"9481_CR24","doi-asserted-by":"crossref","unstructured":"Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2005), LNCS, vol. 3603, pp. 114\u2013129. Springer (2005)","DOI":"10.1007\/11541868_8"},{"key":"9481_CR25","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: van Eekelen, M.C.J.D., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) Interactive Theorem Proving (ITP 2011), LNCS, vol. 6898, pp. 135\u2013151. Springer (2011)","DOI":"10.1007\/978-3-642-22863-6_12"},{"key":"9481_CR26","unstructured":"Immler, F., Maletzky, A.: Gr\u00f6bner bases theory. Archive of Formal Proofs (2016). Formal proof development \n                    http:\/\/isa-afp.org\/entries\/Groebner_Bases.shtml"},{"key":"9481_CR27","unstructured":"Kam, R.: Case studies in proof checking. Master\u2019s thesis, San Jose State University (2007). \n                    http:\/\/scholarworks.sjsu.edu\/cgi\/viewcontent.cgi?context=etd_projects&article=1149"},{"key":"9481_CR28","unstructured":"Kawaguchi, K.: Deep learning without poor local minima. In: Lee, D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems (NIPS 2016), NIPS, vol.\u00a029, pp. 586\u2013594 (2016)"},{"key":"9481_CR29","unstructured":"Kobayashi, H., Chen, L., Murao, H.: Groups, rings and modules. Archive of Formal Proofs (2004). Formal proof development \n                    http:\/\/isa-afp.org\/entries\/Group-Ring-Module.shtml"},{"key":"9481_CR30","doi-asserted-by":"crossref","unstructured":"Liu, L., Aravantinos, V., Hasan, O., Tahar, S.: On the formal analysis of HMM using theorem proving. In: Merz, S., Pang, J. (eds.) International Conference on Formal Engineering Methods (ICFEM 2014), LNCS, vol. 8829, pp. 316\u2013331. Springer (2014)","DOI":"10.1007\/978-3-319-11737-9_21"},{"issue":"5","key":"9481_CR31","doi-asserted-by":"publisher","first-page":"1875","DOI":"10.1090\/S0002-9939-2014-12397-5","volume":"143","author":"M Lotz","year":"2015","unstructured":"Lotz, M.: On the volume of tubular neighborhoods of real algebraic varieties. Proc. Am. Math. Soc. 143(5), 1875\u20131889 (2015)","journal-title":"Proc. Am. Math. Soc."},{"key":"9481_CR32","doi-asserted-by":"crossref","unstructured":"Murphy, C., Gray, P., Stewart, G.: Verified perceptron convergence theorem. In: Shpeisman, T., Gottschlich, J. (eds.) Machine Learning and Programming Languages (MAPL 2017), pp. 43\u201350. ACM (2017)","DOI":"10.1145\/3088525.3088673"},{"key":"9481_CR33","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics: With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle\/HOL. Springer, Berlin (2014)"},{"key":"9481_CR34","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic, LNCS, vol. 2283. Springer, Berlin (2002)"},{"key":"9481_CR35","unstructured":"Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: Sutcliffe, G., Schulz, S., Ternovska, E. (eds.) International Workshop on the Implementation of Logics (IWIL-2010), EPiC, vol.\u00a02, pp. 1\u201311. EasyChair (2012)"},{"key":"9481_CR36","doi-asserted-by":"crossref","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) Theorem Proving in Higher Order Logics (TPHOLs 2007), LNCS, vol. 4732, pp. 232\u2013245. Springer (2007)","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"9481_CR37","doi-asserted-by":"crossref","unstructured":"Poon, H., Domingos, P.M.: Sum\u2013product networks: a new deep architecture. In: Cozman, F.G., Pfeffer, A. (eds.) Uncertainty in Artificial Intelligence (UAI 2011), pp. 337\u2013346. AUAI Press (2011)","DOI":"10.1109\/ICCVW.2011.6130310"},{"key":"9481_CR38","unstructured":"Prathamesh, T.V.H.: Tensor product of matrices. Archive of Formal Proofs (2016). Formal proof development \n                    http:\/\/isa-afp.org\/entries\/Matrix_Tensor.shtml"},{"key":"9481_CR39","unstructured":"Selsam, D., Liang, P., Dill, D.L.: Developing bug-free machine learning systems with formal mathematics. In: Precup D., Teh, Y.W. (eds.) International Conference on Machine Learning (ICML 2017), Proceedings of Machine Learning Research, vol.\u00a070, pp. 3047\u20133056. PMLR (2017)"},{"key":"9481_CR40","unstructured":"Sternagel, C., Thiemann, R.: Executable multivariate polynomials. Archive of Formal Proofs (2010). Formal proof development \n                    http:\/\/isa-afp.org\/entries\/Polynomials.shtml"},{"key":"9481_CR41","unstructured":"Thiemann, R., Yamada, A.: Matrices, Jordan normal forms, and spectral radius theory. Archive of Formal Proofs (2015). Formal proof development \n                    http:\/\/isa-afp.org\/entries\/Jordan_Normal_Form.shtml"},{"key":"9481_CR42","doi-asserted-by":"crossref","unstructured":"Tishby, N., Zaslavsky, N.: Deep learning and the information bottleneck principle. In: Information Theory Workshop (ITW 2015), pp. 1\u20135. IEEE (2015)","DOI":"10.1109\/ITW.2015.7133169"},{"key":"9481_CR43","doi-asserted-by":"crossref","unstructured":"Wenzel, M.: Isar\u2014a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Hirschowitz, A., Paulin-Mohring, C., Th\u00e9ry, L. (eds.) Theorem Proving in Higher Order Logics (TPHOLs \u201999), LNCS, vol. 1690, pp. 167\u2013184. Springer (1999)","DOI":"10.1007\/3-540-48256-3_12"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9481-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-018-9481-5\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-018-9481-5.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,9,21]],"date-time":"2019-09-21T19:05:03Z","timestamp":1569092703000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-018-9481-5"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,9,22]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2019,8]]}},"alternative-id":["9481"],"URL":"https:\/\/doi.org\/10.1007\/s10817-018-9481-5","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"value":"0168-7433","type":"print"},{"value":"1573-0670","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018,9,22]]},"assertion":[{"value":"25 February 2018","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"29 August 2018","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"22 September 2018","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}