{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,25]],"date-time":"2025-06-25T00:10:08Z","timestamp":1750810208660,"version":"3.41.0"},"publisher-location":"Cham","reference-count":34,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319661063"},{"type":"electronic","value":"9783319661070"}],"license":[{"start":{"date-parts":[[2017,1,1]],"date-time":"2017-01-01T00:00:00Z","timestamp":1483228800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2017]]},"DOI":"10.1007\/978-3-319-66107-0_4","type":"book-chapter","created":{"date-parts":[[2017,8,20]],"date-time":"2017-08-20T14:13:59Z","timestamp":1503238439000},"page":"46-64","source":"Crossref","is-referenced-by-count":1,"title":["A Formal Proof of the Expressiveness of Deep Learning"],"prefix":"10.1007","author":[{"given":"Alexander","family":"Bentkamp","sequence":"first","affiliation":[]},{"given":"Jasmin Christian","family":"Blanchette","sequence":"additional","affiliation":[]},{"given":"Dietrich","family":"Klakow","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"issue":"4","key":"4_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":"4_CR2","unstructured":"Bentkamp, A.: Expressiveness of deep learning. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/Deep_Learning.shtml. Formal proof development"},{"key":"4_CR3","unstructured":"Bentkamp, A.: An Isabelle formalization of the expressiveness of deep learning. M.Sc. thesis, Universit\u00e4t des Saarlandes (2016). http:\/\/matryoshka.gforge.inria.fr\/pubs\/bentkamp_msc_thesis.pdf"},{"key":"4_CR4","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.) CPP 2016, pp. 76\u201387. ACM (2016)","DOI":"10.1145\/2854065.2854072"},{"key":"4_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Y Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical big operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 86\u2013101. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_11"},{"key":"4_CR6","unstructured":"Bhat, S.: Syntactic foundations for machine learning. Ph.D. thesis, Georgia Institute of Technology (2013). https:\/\/smartech.gatech.edu\/bitstream\/handle\/1853\/47700\/bhat_sooraj_b_201305_phd.pdf"},{"issue":"2","key":"4_CR7","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":"4_CR8","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":"4_CR9","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.) QPL 2015. EPTCS, vol. 195, pp. 71\u201383 (2015)","DOI":"10.4204\/EPTCS.195.6"},{"key":"4_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-14052-5_14","volume-title":"Interactive Theorem Proving","author":"S B\u00f6hme","year":"2010","unstructured":"B\u00f6hme, S., Weber, T.: Fast LCF-style proof reconstruction for Z3. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 179\u2013194. Springer, Heidelberg (2010). 10.1007\/978-3-642-14052-5_14"},{"issue":"263","key":"4_CR11","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":"4_CR12","unstructured":"Caron, R., Traynor, T.: The zero set of a polynomial. Technical report, University of Windsor (2005). http:\/\/www1.uwindsor.ca\/math\/sites\/uwindsor.ca.math\/files\/05-03.pdf"},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"Cohen, N., Sharir, O., Shashua, A.: Deep SimNets. In: CVPR 2016, pp. 4782\u20134791. IEEE Computer Society (2016)","DOI":"10.1109\/CVPR.2016.517"},{"key":"4_CR14","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.) COLT 2016. JMLR Workshop and Conference Proceedings, vol. 49, pp. 698\u2013728. JMLR.org (2016)"},{"key":"4_CR15","unstructured":"Cohen, N., Shashua, A.: Convolutional rectifier networks as generalized tensor decompositions. In: Balcan, M., Weinberger, K.Q. (eds.) ICML 2016. JMLR Workshop and Conference Proceedings, vol. 48, pp. 955\u2013963. JMLR.org (2016)"},{"key":"4_CR16","unstructured":"Cohen, N., Shashua, A.: Inductive bias of deep convolutional networks through pooling geometry. CoRR abs\/1605.06743 (2016)"},{"key":"4_CR17","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":"4_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"114","DOI":"10.1007\/11541868_8","volume-title":"Theorem Proving in Higher Order Logics","author":"J Harrison","year":"2005","unstructured":"Harrison, J.: A HOL theory of Euclidean space. In: Hurd, J., Melham, T. (eds.) TPHOLs 2005. LNCS, vol. 3603, pp. 114\u2013129. Springer, Heidelberg (2005). 10.1007\/11541868_8"},{"key":"4_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1007\/978-3-642-22863-6_12","volume-title":"Interactive Theorem Proving","author":"J H\u00f6lzl","year":"2011","unstructured":"H\u00f6lzl, J., Heller, A.: Three chapters of measure theory in Isabelle\/HOL. In: Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 135\u2013151. Springer, Heidelberg (2011). 10.1007\/978-3-642-22863-6_12"},{"key":"4_CR20","unstructured":"Immler, F., Maletzky, A.: Gr\u00f6bner bases theory. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/Groebner_Bases.shtml. Formal proof development"},{"key":"4_CR21","unstructured":"Kam, R.: Case studies in proof checking. Master\u2019s thesis, San Jose State University (2007). http:\/\/scholarworks.sjsu.edu\/cgi\/viewcontent.cgi?context=etd_projects &article=1149"},{"key":"4_CR22","unstructured":"Kobayashi, H., Chen, L., Murao, H.: Groups, rings and modules. Archive of Formal Proofs (2004). http:\/\/isa-afp.org\/entries\/Group-Ring-Module.shtml. Formal proof development"},{"key":"4_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"316","DOI":"10.1007\/978-3-319-11737-9_21","volume-title":"Formal Methods and Software Engineering","author":"L Liu","year":"2014","unstructured":"Liu, L., Aravantinos, V., Hasan, O., Tahar, S.: On the formal analysis of HMM using theorem proving. In: Merz, S., Pang, J. (eds.) ICFEM 2014. LNCS, vol. 8829, pp. 316\u2013331. Springer, Cham (2014). 10.1007\/978-3-319-11737-9_21"},{"issue":"5","key":"4_CR24","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. Amer. Math. Soc. 143(5), 1875\u20131889 (2015)","journal-title":"Proc. Amer. Math. Soc."},{"key":"4_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L Moura","year":"2008","unstructured":"Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). 10.1007\/978-3-540-78800-3_24"},{"key":"4_CR26","unstructured":"Murphy, T., Gray, P., Stewart, G.: Certified convergent perceptron learning (unpublished draft). http:\/\/oucsace.cs.ohiou.edu\/~gstewart\/papers\/coqperceptron.pdf"},{"key":"4_CR27","series-title":"Lecture Notes in Computer Science","volume-title":"Isabelle\/HOL","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"4_CR28","doi-asserted-by":"crossref","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.) IWIL-2010. EPiC, vol. 2, pp. 1\u201311. EasyChair (2012)","DOI":"10.29007\/36dt"},{"key":"4_CR29","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"232","DOI":"10.1007\/978-3-540-74591-4_18","volume-title":"Theorem Proving in Higher Order Logics","author":"LC Paulson","year":"2007","unstructured":"Paulson, L.C., Susanto, K.W.: Source-level proof reconstruction for interactive theorem proving. In: Schneider, K., Brandt, J. (eds.) TPHOLs 2007. LNCS, vol. 4732, pp. 232\u2013245. Springer, Heidelberg (2007). 10.1007\/978-3-540-74591-4_18"},{"key":"4_CR30","doi-asserted-by":"crossref","unstructured":"Poon, H., Domingos, P.M.: Sum-product networks: a new deep architecture. In: Cozman, F.G., Pfeffer, A. (eds.) UAI 2011, pp. 337\u2013346. AUAI Press (2011)","DOI":"10.1109\/ICCVW.2011.6130310"},{"key":"4_CR31","unstructured":"Prathamesh, T.V.H.: Tensor product of matrices. Archive of Formal Proofs (2016). http:\/\/isa-afp.org\/entries\/Matrix_Tensor.shtml. Formal proof development"},{"key":"4_CR32","unstructured":"Sternagel, C., Thiemann, R.: Executable multivariate polynomials. Archive of Formal Proofs (2010). http:\/\/isa-afp.org\/entries\/Polynomials.shtml. Formal proof development"},{"key":"4_CR33","unstructured":"Thiemann, R., Yamada, A.: Matrices, Jordan normal forms, and spectral radius theory. Archive of Formal Proofs (2015). http:\/\/isa-afp.org\/entries\/Jordan_Normal_Form.shtml. Formal proof development"},{"key":"4_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"167","DOI":"10.1007\/3-540-48256-3_12","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"1999","unstructured":"Wenzel, M.: Isar\u2014a generic interpretative approach to readable formal proof documents. In: Bertot, Y., Dowek, G., Th\u00e9ry, L., Hirschowitz, A., Paulin, C. (eds.) TPHOLs 1999. LNCS, vol. 1690, pp. 167\u2013183. Springer, Heidelberg (1999). 10.1007\/3-540-48256-3_12"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-66107-0_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,24]],"date-time":"2025-06-24T23:39:00Z","timestamp":1750808340000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-319-66107-0_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017]]},"ISBN":["9783319661063","9783319661070"],"references-count":34,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-66107-0_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2017]]}}}