{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,6]],"date-time":"2026-04-06T11:08:34Z","timestamp":1775473714087,"version":"3.50.1"},"publisher-location":"Cham","reference-count":62,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030535179","type":"print"},{"value":"9783030535186","type":"electronic"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-53518-6_1","type":"book-chapter","created":{"date-parts":[[2020,7,17]],"date-time":"2020-07-17T15:17:50Z","timestamp":1594999070000},"page":"3-20","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":17,"title":["A Promising Path Towards Autoformalization and General Artificial Intelligence"],"prefix":"10.1007","author":[{"given":"Christian","family":"Szegedy","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,7,17]]},"reference":[{"key":"1_CR1","unstructured":"Alemi, A.A., Chollet, F., E\u00e9n, N., Irving, G., Szegedy, C., Urban, J.: Deepmath - deep sequence models for premise selection. In: Lee, D.D., Sugiyama, M., von Luxburg, U., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems 29: Annual Conference on Neural Information Processing Systems 2016, Barcelona, Spain, 5\u201310 December 2016, pp. 2235\u20132243 (2016)"},{"key":"1_CR2","unstructured":"Andrychowicz, M., et al.: Hindsight experience replay. In: Advances in Neural Information Processing Systems 30 (NIPS 2017), pp. 5048\u20135058 (2017)"},{"key":"1_CR3","unstructured":"Bansal, K., Loos, S.M., Rabe, M.N., Szegedy, C.: Learning to reason in large theories without imitation. arXiv preprint arXiv:1905.10501 (2019)"},{"key":"1_CR4","unstructured":"Bansal, K., Loos, S.M., Rabe, M.N., Szegedy, C., Wilcox, S.: HOList: an environment for machine learning of higher-order theorem proving. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning, ICML 2019, Proceedings of Machine Learning Research, Long Beach, California, USA, 9\u201315 June 2019, vol. 97, pp. 454\u2013463. PMLR (2019)"},{"key":"1_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-49059-0_14","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Biere","year":"1999","unstructured":"Biere, A., Cimatti, A., Clarke, E., Zhu, Y.: Symbolic model checking without BDDs. In: Cleaveland, W.R. (ed.) TACAS 1999. LNCS, vol. 1579, pp. 193\u2013207. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-49059-0_14"},{"issue":"1","key":"1_CR6","first-page":"101","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reasoning 9(1), 101\u2013148 (2016)","journal-title":"J. Formalized Reasoning"},{"key":"1_CR7","unstructured":"The Coq Proof Assistant. http:\/\/coq.inria.fr"},{"key":"1_CR8","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction - CADE-25","author":"L de Moura","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (System Description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"1_CR9","unstructured":"Devlin, J., Chang, M.-W., Lee, K., Toutanova, K.: BERT: pre-training of deep bidirectional transformers for language understanding. In: Proceedings of the 2019 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies (Long and Short Papers), vol. 1, pp. 4171\u20134186 (2019)"},{"key":"1_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"502","DOI":"10.1007\/978-3-540-24605-3_37","volume-title":"Theory and Applications of Satisfiability Testing","author":"N E\u00e9n","year":"2004","unstructured":"E\u00e9n, N., S\u00f6rensson, N.: An extensible SAT-solver. In: Giunchiglia, E., Tacchella, A. (eds.) SAT 2003. LNCS, vol. 2919, pp. 502\u2013518. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-24605-3_37"},{"key":"1_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3","volume-title":"First-order Logic and Automated Theorem Proving","author":"M Fitting","year":"2012","unstructured":"Fitting, M.: First-order Logic and Automated Theorem Proving. Springer, New York (2012). https:\/\/doi.org\/10.1007\/978-1-4612-2360-3"},{"key":"1_CR12","unstructured":"Garrabrant, S., Benson-Tilsen, T., Critch, A., Soares, N., Taylor, J.: Logical induction. arXiv preprint arXiv:1609.03543 (2016)"},{"key":"1_CR13","doi-asserted-by":"crossref","unstructured":"Gatys, L.A., Ecker, A.S., Bethge, M.: Image style transfer using convolutional neural networks. In: 2016 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2016, Las Vegas, NV, USA, 27\u201330 June 2016, pp. 2414\u20132423. IEEE Computer Society (2016)","DOI":"10.1109\/CVPR.2016.265"},{"key":"1_CR14","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J.: TacticToe: learning to reason with HOL4 tactics. In: Eiter, T., Sands, D. (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 7\u201312 May 2017, EPiC Series in Computing, vol. 46, pp. 125\u2013143. EasyChair (2017)"},{"issue":"1","key":"1_CR15","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1002\/minf.201501008","volume":"35","author":"E Gawehn","year":"2016","unstructured":"Gawehn, E., Hiss, J.A., Schneider, G.: Deep learning in drug discovery. Mol. Inform. 35(1), 3\u201314 (2016)","journal-title":"Mol. Inform."},{"issue":"11","key":"1_CR16","first-page":"1382","volume":"55","author":"G Gonthier","year":"2008","unstructured":"Gonthier, G.: Formal proof-the four-color theorem. Not. AMS 55(11), 1382\u20131393 (2008)","journal-title":"Not. AMS"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"163","DOI":"10.1007\/978-3-642-39634-2_14","volume-title":"Interactive Theorem Proving","author":"G Gonthier","year":"2013","unstructured":"Gonthier, G., et al.: A machine-checked proof of the odd order theorem. In: Blazy, S., Paulin-Mohring, C., Pichardie, D. (eds.) ITP 2013. LNCS, vol. 7998, pp. 163\u2013179. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-39634-2_14"},{"key":"1_CR18","unstructured":"Google\u2019s scalable supercomputers for machine learning, Cloud TPU Pods, are now publicly available in beta. https:\/\/bit.ly\/2YkZh3i"},{"key":"1_CR19","doi-asserted-by":"crossref","unstructured":"Gordon, A., et al.: MorphNet: Fast & simple resource-constrained structure learning of deep networks. In: 2018 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2018, Salt Lake City, UT, USA, 18\u201322 June 2018, pp. 1586\u20131595. IEEE Computer Society (2018)","DOI":"10.1109\/CVPR.2018.00171"},{"key":"1_CR20","doi-asserted-by":"publisher","first-page":"729","DOI":"10.1613\/jair.1.11222","volume":"62","author":"K Grace","year":"2018","unstructured":"Grace, K., Salvatier, J., Dafoe, A., Zhang, B., Evans, O.: When will AI exceed human performance? evidence from AI experts. J. Artif. Intell. Res. 62, 729\u2013754 (2018)","journal-title":"J. Artif. Intell. Res."},{"key":"1_CR21","unstructured":"Hadjeres, G., Pachet, F., Nielsen, F.: DeepBach: a steerable model for Bach chorales generation. In: Proceedings of the 34th International Conference on Machine Learning, vol. 70, pp. 1362\u20131371. JMLR (2017)"},{"key":"1_CR22","doi-asserted-by":"crossref","unstructured":"Hales, T., et al.: A formal proof of the Kepler conjecture. In: Forum of Mathematics, Pi, vol. 5. Cambridge University Press (2017)","DOI":"10.1017\/fmp.2017.1"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/BFb0031814","volume-title":"Formal Methods in Computer-Aided Design","author":"J Harrison","year":"1996","unstructured":"Harrison, J.: HOL light: a tutorial introduction. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 265\u2013269. Springer, Heidelberg (1996). https:\/\/doi.org\/10.1007\/BFb0031814"},{"key":"1_CR24","doi-asserted-by":"crossref","unstructured":"He, K., Zhang, X., Ren, S., Sun, J.: Deep residual learning for image recognition. In: 2016 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2016, Las Vegas, NV, USA, 27\u201330 June 2016, pp. 770\u2013778. IEEE Computer Society (2016)","DOI":"10.1109\/CVPR.2016.90"},{"key":"1_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"228","DOI":"10.1007\/978-3-319-40970-2_15","volume-title":"Theory and Applications of Satisfiability Testing \u2013 SAT 2016","author":"MJH Heule","year":"2016","unstructured":"Heule, M.J.H., Kullmann, O., Marek, V.W.: Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer. In: Creignou, N., Le Berre, D. (eds.) SAT 2016. LNCS, vol. 9710, pp. 228\u2013245. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40970-2_15"},{"key":"1_CR26","unstructured":"Huang, D., Dhariwal, P., Song, D., Sutskever, I.: GamePad: a learning environment for theorem proving. In: 7th International Conference on Learning Representations, ICLR 2019, New Orleans, LA, USA, 6\u20139 May 2019. OpenReview.net (2019)"},{"issue":"1","key":"1_CR27","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1007\/s11786-014-0182-0","volume":"9","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: HOL (y) hammer: online ATP service for HOL light. Math. Comput. Sci. 9(1), 5\u201322 (2015)","journal-title":"Math. Comput. Sci."},{"key":"1_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"227","DOI":"10.1007\/978-3-319-22102-1_15","volume-title":"Interactive Theorem Proving","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J., Vysko\u010dil, J.: Learning to parse on aligned corpora (Rough Diamond). In: Urban, C., Zhang, X. (eds.) ITP 2015. LNCS, vol. 9236, pp. 227\u2013233. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-22102-1_15"},{"key":"1_CR29","doi-asserted-by":"crossref","unstructured":"Kaliszyk, C., Urban, J., Vyskocil, J.: System description: statistical parsing of informalized Mizar formulas. In: Jebelean, T., Negru, V., Petcu, D., Zaharie, D., Ida, T., Watt, S.M., (eds.) 19th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing, SYNASC 2017, Timisoara, Romania, 21\u201324 September 2017, pp. 169\u2013172. IEEE Computer Society (2017)","DOI":"10.1109\/SYNASC.2017.00036"},{"key":"1_CR30","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"282","DOI":"10.1007\/11871842_29","volume-title":"Machine Learning: ECML 2006","author":"L Kocsis","year":"2006","unstructured":"Kocsis, L., Szepesv\u00e1ri, C.: Bandit based Monte-Carlo planning. In: F\u00fcrnkranz, J., Scheffer, T., Spiliopoulou, M. (eds.) ECML 2006. LNCS (LNAI), vol. 4212, pp. 282\u2013293. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11871842_29"},{"key":"1_CR31","unstructured":"Lample, G., Charton, F.: Deep learning for symbolic mathematics. In: 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, 26\u201330 April 2020. OpenReview.net (2020)"},{"key":"1_CR32","unstructured":"Lample, G., Conneau, A., Denoyer, L., Ranzato, M.: Unsupervised machine translation using monolingual corpora only. In: 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, 30 April\u20133 May 2018, Conference Track Proceedings. OpenReview.net (2018)"},{"key":"1_CR33","unstructured":"Lee, D., Szegedy, C., Rabe, M.N., Loos, S.M., Bansal, K.: Mathematical reasoning in latent space. In: 8th International Conference on Learning Representations, ICLR 2020, Addis Ababa, Ethiopia, 26\u201330 April 2020. OpenReview.net (2020)"},{"key":"1_CR34","unstructured":"Liu, Y., et al.: RoBERTa: a robustly optimized BERT pretraining approach. arXiv preprint arXiv:1907.11692 (2019)"},{"key":"1_CR35","unstructured":"Loos, S., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: Eiter, T., Sands, D. (eds.) LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Maun, Botswana, 7\u201312 May 2017, EPiC Series in Computing, vol. 46, pp. 85\u2013105. EasyChair (2017)"},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"McCarthy, J.: Computer programs for checking mathematical proofs. In: A Paper Presented at the Symposium on Recursive Function Theory, New York, April 1961","DOI":"10.1090\/pspum\/005\/9998"},{"key":"1_CR37","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"88","DOI":"10.1007\/11542384_13","volume-title":"The Seventeen Provers of the World","author":"N Megill","year":"2006","unstructured":"Megill, N.: Metamath. In: Wiedijk, F. (ed.) The Seventeen Provers of the World. LNCS (LNAI), vol. 3600, pp. 88\u201395. Springer, Heidelberg (2006). https:\/\/doi.org\/10.1007\/11542384_13"},{"key":"1_CR38","unstructured":"The Mizar Mathematical Library. http:\/\/mizar.org"},{"key":"1_CR39","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1017\/CBO9780511800481.011","volume":"9","author":"N Nisan","year":"2007","unstructured":"Nisan, N., et al.: Introduction to mechanism design (for computer scientists). Algorithmic Game Theor. 9, 209\u2013242 (2007)","journal-title":"Algorithmic Game Theor."},{"key":"1_CR40","unstructured":"Paliwal, A., Loos, S., Rabe, M., Bansal, K., Szegedy, C.: Graph representations for higher-order logic and theorem proving. In: The Thirty-Fourth AAAI Conference on Artificial Intelligence, AAAI 2020, New York, NY, USA, 7\u201312 February 2020. AAAI Press (2020)"},{"key":"1_CR41","doi-asserted-by":"crossref","unstructured":"Peters, M.E., et al.: Deep contextualized word representations. In: Walker, M.A., Ji, H., Stent, A. (eds.) Proceedings of the 2018 Conference of the North American Chapter of the Association for Computational Linguistics: Human Language Technologies, NAACL-HLT 2018, New Orleans, Louisiana, USA, 1\u20136 June 2018, (Long Papers), vol. 1, pp. 2227\u20132237. Association for Computational Linguistics (2018)","DOI":"10.18653\/v1\/N18-1202"},{"issue":"6419","key":"1_CR42","doi-asserted-by":"publisher","first-page":"1140","DOI":"10.1126\/science.aar6404","volume":"362","author":"D Silver","year":"2018","unstructured":"Silver, D., et al.: A general reinforcement learning algorithm that masters chess, shogi, and go through self-play. Science 362(6419), 1140\u20131144 (2018)","journal-title":"Science"},{"issue":"7676","key":"1_CR43","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1038\/nature24270","volume":"550","author":"D Silver","year":"2017","unstructured":"Silver, D., et al.: Mastering the game of go without human knowledge. Nature 550(7676), 354 (2017)","journal-title":"Nature"},{"key":"1_CR44","unstructured":"Simon, D.L.: Checking number theory proofs in natural language. Ph.D thesis (1990)"},{"key":"1_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_6"},{"key":"1_CR46","doi-asserted-by":"crossref","unstructured":"Szegedy, C., et al.: Going deeper with convolutions. In: IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2015, Boston, MA, USA, 7\u201312 June 2015, pp. 1\u20139. IEEE Computer Society (2015)","DOI":"10.1109\/CVPR.2015.7298594"},{"key":"1_CR47","unstructured":"Tan, M., Le, Q.V.: EfficientNet: rethinking model scaling for convolutional neural networks. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning, ICML 2019, Long Beach, California, USA, 9\u201315 June 2019, Proceedings of Machine Learning Research, vol. 97, pp. 6105\u20136114. PMLR (2019)"},{"key":"1_CR48","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"203","DOI":"10.1007\/3-540-36469-2_16","volume-title":"Mathematical Knowledge Management","author":"J Urban","year":"2003","unstructured":"Urban, J.: Translating Mizar for first order theorem provers. In: Asperti, A., Buchberger, B., Davenport, J.H. (eds.) MKM 2003. LNCS, vol. 2594, pp. 203\u2013215. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/3-540-36469-2_16"},{"issue":"1\u20132","key":"1_CR49","first-page":"21","volume":"37","author":"J Urban","year":"2006","unstructured":"Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reasoning 37(1\u20132), 21\u201343 (2006)","journal-title":"J. Autom. Reasoning"},{"key":"1_CR50","unstructured":"Urban, J.: MaLARea: a metasystem for automated reasoning in large theories. In: Sutcliffe, G., Urban, J., Schulz, S. (eds.) Proceedings of the CADE-21 Workshop on Empirically Successful Automated Reasoning in Large Theories, Bremen, Germany, 17th July 2007, CEUR Workshop Proceedings, vol. 257. CEUR-WS.org (2007)"},{"key":"1_CR51","unstructured":"Vaswani, A., et al.: Attention is all you need. In: Guyon, I., et al. (eds.) Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, Long Beach, CA, USA, 4\u20139 December 2017, pp. 5998\u20136008 (2017)"},{"key":"1_CR52","unstructured":"Wang, M., Tang, Y., Wang, J., Deng, J.: Premise selection for theorem proving by deep graph embedding. In: Advances in Neural Information Processing Systems 30 (NIPS 2017), pp. 2786\u20132796 (2017)"},{"key":"1_CR53","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"33","DOI":"10.1007\/978-3-540-71067-7_7","volume-title":"Theorem Proving in Higher Order Logics","author":"M Wenzel","year":"2008","unstructured":"Wenzel, M., Paulson, L.C., Nipkow, T.: The Isabelle framework. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 33\u201338. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71067-7_7"},{"key":"1_CR54","doi-asserted-by":"crossref","unstructured":"Wu, Z., Pan, S., Chen, F., Long, G., Zhang, C., Philip, S.Y.: A comprehensive survey on graph neural networks. In: IEEE Transactions on Neural Networks and Learning Systems, pp. 1\u201321 (2020)","DOI":"10.1109\/TNNLS.2020.2978386"},{"key":"1_CR55","unstructured":"Yang, K., Deng, J.: Learning to prove theorems via interacting with proof assistants. In: Chaudhuri, K., Salakhutdinov, R. (eds.) Proceedings of the 36th International Conference on Machine Learning, ICML 2019, Long Beach, California, USA, 9\u201315 June 2019, Proceedings of Machine Learning Research, vol. 97, pp. 6984\u20136994. PMLR (2019)"},{"key":"1_CR56","unstructured":"Yang, Z., Dai, Z., Yang, Y., Carbonell, J.G., Salakhutdinov, R., Le, Q.V.: XLNet: generalized autoregressive pretraining for language understanding. In: Wallach, H.M., et al. (eds.) Advances in Neural Information Processing Systems 32: Annual Conference on Neural Information Processing Systems 2019, NeurIPS 2019, Canada, Vancouver, BC, 8\u201314 December 2019, pp. 5754\u20135764 (2019)"},{"key":"1_CR57","unstructured":"Yu, A.W., et al.: QANet: combining local convolution with global self-attention for reading comprehension. In: 6th International Conference on Learning Representations, ICLR 2018, Vancouver, BC, Canada, 30 April\u20133 May 2018, Conference Track Proceedings. OpenReview.net (2018)"},{"issue":"8","key":"1_CR58","doi-asserted-by":"publisher","first-page":"1177","DOI":"10.1109\/TNNLS.2012.2200299","volume":"23","author":"SE Yuksel","year":"2012","unstructured":"Yuksel, S.E., Wilson, J.N., Gader, P.D.: Twenty years of mixture of experts. IEEE Trans. Neural Networks Learn. Syst. 23(8), 1177\u20131193 (2012)","journal-title":"IEEE Trans. Neural Networks Learn. Syst."},{"key":"1_CR59","doi-asserted-by":"crossref","unstructured":"Zhu, J.-Y., Park, T., Isola, P., Efros, A.A.: Unpaired image-to-image translation using cycle-consistent adversarial networks. In: 2017 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2017, Honolulu, HI, USA, 21\u201326 July 2017, pp. 2223\u20132232. IEEE Computer Society (2017)","DOI":"10.1109\/ICCV.2017.244"},{"key":"1_CR60","unstructured":"Zinn, C.: Understanding informal mathematical discourse. Ph.D thesis, Institut f\u00fcr Informatik, Universit\u00e4t Erlangen-N\u00fcrnberg (2004)"},{"key":"1_CR61","unstructured":"Zombori, Z., Csisz\u00e1rik, A., Michalewski, H., Kaliszyk, C., Urban, J.: Towards finding longer proofs. arXiv preprint arXiv:1905.13100 (2019)"},{"key":"1_CR62","unstructured":"Zoph, B., Le, Q.V.: Neural architecture search with reinforcement learning. In: 5th International Conference on Learning Representations, ICLR 2017, Toulon, France, 24\u201326 April 2017, Conference Track Proceedings. OpenReview.net (2017)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-53518-6_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,11,3]],"date-time":"2022-11-03T04:31:32Z","timestamp":1667449892000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-53518-6_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030535179","9783030535186"],"references-count":62,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-53518-6_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"17 July 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bertinoro","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Italy","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"13","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cicm-conference.org\/2020\/cicm.php","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"35","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"15","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"9","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3-4","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}