{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,4,10]],"date-time":"2025-04-10T04:30:30Z","timestamp":1744259430092,"version":"3.40.3"},"publisher-location":"Cham","reference-count":28,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030810962"},{"type":"electronic","value":"9783030810979"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-81097-9_6","type":"book-chapter","created":{"date-parts":[[2021,7,19]],"date-time":"2021-07-19T23:04:38Z","timestamp":1626735878000},"page":"84-89","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Improving Stateful Premise Selection with Transformers"],"prefix":"10.1007","author":[{"given":"Krsto","family":"Prorokovi\u0107","sequence":"first","affiliation":[]},{"given":"Michael","family":"Wand","sequence":"additional","affiliation":[]},{"given":"J\u00fcrgen","family":"Schmidhuber","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,20]]},"reference":[{"key":"6_CR1","doi-asserted-by":"crossref","unstructured":"Chen, T., Guestrin, C.: XGBoost: a scalable tree boosting system. In: Proceedings of the 22nd ACM SIGKDD International Conference on Knowledge Discovery and Data Mining, pp. 785\u2013794 (2016)","DOI":"10.1145\/2939672.2939785"},{"issue":"2","key":"6_CR2","first-page":"153","volume":"3","author":"A Grabowski","year":"2010","unstructured":"Grabowski, A., Kornilowicz, A., Naumowicz, A.: Mizar in a nutshell. J. Formaliz. Reason. 3(2), 153\u2013245 (2010)","journal-title":"J. Formaliz. Reason."},{"issue":"8","key":"6_CR3","doi-asserted-by":"publisher","first-page":"1735","DOI":"10.1162\/neco.1997.9.8.1735","volume":"9","author":"S Hochreiter","year":"1997","unstructured":"Hochreiter, S., Schmidhuber, J.: Long short-term memory. Neural Comput. 9(8), 1735\u20131780 (1997)","journal-title":"Neural Comput."},{"key":"6_CR4","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"299","DOI":"10.1007\/978-3-642-22438-6_23","volume-title":"Automated Deduction \u2013 CADE-23","author":"K Hoder","year":"2011","unstructured":"Hoder, K., Voronkov, A.: Sine qua non for large theory reasoning. In: Bj\u00f8rner, N., Sofronie-Stokkermans, V. (eds.) CADE 2011. LNCS (LNAI), vol. 6803, pp. 299\u2013314. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22438-6_23"},{"key":"6_CR5","unstructured":"Irving, G., Szegedy, C., Alemi, A.A., Een, N., Chollet, F., Urban, J.: Deepmath - deep sequence models for premise selection. In: Lee, D., Sugiyama, M., Luxburg, U., Guyon, I., Garnett, R. (eds.) Advances in Neural Information Processing Systems, vol. 29. Curran Associates, Inc. (2016). https:\/\/proceedings.neurips.cc\/paper\/2016\/file\/f197002b9a0853eca5e046d9ca4663d5-Paper.pdf"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"138","DOI":"10.1007\/978-3-030-53518-6_9","volume-title":"Intelligent Computer Mathematics","author":"C Kaliszyk","year":"2020","unstructured":"Kaliszyk, C., Rabe, F.: A survey of languages for formalizing mathematics. In: Benzm\u00fcller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 138\u2013156. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_9"},{"issue":"2","key":"6_CR7","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/s10817-014-9303-3","volume":"53","author":"C Kaliszyk","year":"2014","unstructured":"Kaliszyk, C., Urban, J.: Learning-assisted automated reasoning with Flyspeck. J. Autom. Reason. 53(2), 173\u2013213 (2014)","journal-title":"J. Autom. Reason."},{"issue":"3","key":"6_CR8","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/s10817-015-9330-8","volume":"55","author":"C Kaliszyk","year":"2015","unstructured":"Kaliszyk, C., Urban, J.: Mizar 40 for Mizar 40. J. Autom. Reason. 55(3), 245\u2013256 (2015)","journal-title":"J. Autom. Reason."},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"Klein, G., Kim, Y., Deng, Y., Senellart, J., Rush, A.: OpenNMT: open-source toolkit for neural machine translation. In: Proceedings of ACL 2017, System Demonstrations, pp. 67\u201372. Association for Computational Linguistics, Vancouver, Canada (Jul 2017). https:\/\/www.aclweb.org\/anthology\/P17-4012","DOI":"10.18653\/v1\/P17-4012"},{"issue":"1\u20132","key":"6_CR10","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1002\/nav.3800020109","volume":"2","author":"HW Kuhn","year":"1955","unstructured":"Kuhn, H.W.: The Hungarian method for the assignment problem. Naval Res. Logist. Q. 2(1\u20132), 83\u201397 (1955)","journal-title":"Naval Res. Logist. Q."},{"key":"6_CR11","unstructured":"Loos, S., Irving, G., Szegedy, C., Kaliszyk, C.: Deep network guided proof search. In: LPAR-21, 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, pp. 85\u2013105 (2017). http:\/\/arxiv.org\/pdf\/1701.06972.pdf. ISSN 2398\u20137340"},{"key":"6_CR12","doi-asserted-by":"crossref","unstructured":"Luong, M.T., Pham, H., Manning, C.D.: Effective approaches to attention-based neural machine translation. In: Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, pp. 1412\u20131421 (2015)","DOI":"10.18653\/v1\/D15-1166"},{"key":"6_CR13","unstructured":"Megill, N., Wheeler, D.A.: Metamath: A Computer Language for Mathematical Proofs (2019). http:\/\/us.metamath.org\/downloads\/metamath.pdf"},{"issue":"1","key":"6_CR14","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jal.2007.07.004","volume":"7","author":"J Meng","year":"2009","unstructured":"Meng, J., Paulson, L.C.: Lightweight relevance filtering for machine-generated resolution problems. J. Appl. Log. 7(1), 41\u201357 (2009)","journal-title":"J. Appl. Log."},{"key":"6_CR15","doi-asserted-by":"publisher","unstructured":"Ols\u00e1k, M., Kaliszyk, C., Urban, J.: Property invariant embedding for automated reasoning. In: Giacomo, G.D., et al. (eds.) ECAI 2020\u201324th European Conference on Artificial Intelligence, 29 Aug \u2013 8 Sept 2020, Santiago de Compostela, Spain, Aug 29 \u2013 Sept 8, 2020 - Including 10th Conference on Prestigious Applications of Artificial Intelligence (PAIS 2020). Frontiers in Artificial Intelligence and Applications, vol. 325, pp. 1395\u20131402. IOS Press (2020). https:\/\/doi.org\/10.3233\/FAIA200244","DOI":"10.3233\/FAIA200244"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"Paliwal, A., Loos, S., Rabe, M., Bansal, K., Szegedy, C.: Graph representations for higher-order logic and theorem proving. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, pp. 2967\u20132974 (2020)","DOI":"10.1609\/aaai.v34i03.5689"},{"key":"6_CR17","unstructured":"Paszke, A., et al.: Pytorch: an imperative style, high-performance deep learning library. In: Wallach, H., Larochelle, H., Beygelzimer, A., d\u2019Alch\u00e9-Buc, F., Fox, E., Garnett, R. (eds.) Advances in Neural Information Processing Systems 32, pp. 8024\u20138035. Curran Associates, Inc. (2019). http:\/\/papers.neurips.cc\/paper\/9015-pytorch-an-imperative-style-high-performance-deep-learning-library.pdf"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"566","DOI":"10.1007\/978-3-319-94205-6_37","volume-title":"Automated Reasoning","author":"B Piotrowski","year":"2018","unstructured":"Piotrowski, B., Urban, J.: ATPboost: learning premise selection in binary setting with ATP feedback. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 566\u2013574. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_37"},{"key":"6_CR19","doi-asserted-by":"publisher","unstructured":"Piotrowski, B., Urban, J.: Stateful premise selection by recurrent neural networks. In: Albert, E., Kovacs, L. (eds.) LPAR23, LPAR-23: 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning. EPiC Series in Computing, vol. 73, pp. 409\u2013422. EasyChair (2020). 0). https:\/\/doi.org\/10.29007\/j5hd. https:\/\/easychair.org\/publications\/paper\/g38n","DOI":"10.29007\/j5hd"},{"key":"6_CR20","unstructured":"Polu, S., Sutskever, I.: Generative language modeling for automated theorem proving. CoRR abs\/2009.03393 (2020). https:\/\/arxiv.org\/abs\/2009.03393"},{"key":"6_CR21","unstructured":"Schlag, I., Irie, K., Schmidhuber, J.: Linear transformers are secretly fast weight memory systems. CoRR abs\/2102.11174 (2021). https:\/\/arxiv.org\/abs\/2102.11174"},{"key":"6_CR22","doi-asserted-by":"publisher","first-page":"460","DOI":"10.1007\/978-1-4471-2063-6_110","volume-title":"ICANN \u201993","author":"J Schmidhuber","year":"1993","unstructured":"Schmidhuber, J.: Reducing the ratio between learning complexity and number of time varying variables in fully recurrent nets. In: Gielen, S., Kappen, B. (eds.) ICANN 1993, pp. 460\u2013463. Springer, London (1993). https:\/\/doi.org\/10.1007\/978-1-4471-2063-6_110"},{"key":"6_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-16242-8","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","year":"2010","unstructured":"Ferm\u00fcller, C.G., Voronkov, A. (eds.): LPAR 2010. LNCS, vol. 6397. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-16242-8"},{"key":"6_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-642-17511-4_1","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"G Sutcliffe","year":"2010","unstructured":"Sutcliffe, G.: The TPTP world \u2013 infrastructure for automated reasoning. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 1\u201312. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-17511-4_1"},{"key":"6_CR25","first-page":"3104","volume":"27","author":"I Sutskever","year":"2014","unstructured":"Sutskever, I., Vinyals, O., Le, Q.V.: Sequence to sequence learning with neural networks. Adv. Neural Inf. Process. Syst. 27, 3104\u20133112 (2014)","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"6_CR26","doi-asserted-by":"crossref","unstructured":"Tsivtsivadze, E., Urban, J., Geuvers, H., Heskes, T.: Semantic graph kernels for automated reasoning. In: Proceedings of the 2011 SIAM International Conference on Data Mining, pp. 795\u2013803. SIAM (2011)","DOI":"10.1137\/1.9781611972818.68"},{"key":"6_CR27","doi-asserted-by":"crossref","unstructured":"Urban, J.: MPTP 0.2: design, implementation, and initial experiments. J. Autom. Reason. 37(1\u20132), 21\u201343 (2006)","DOI":"10.1007\/s10817-006-9032-3"},{"key":"6_CR28","first-page":"5998","volume":"30","author":"A Vaswani","year":"2017","unstructured":"Vaswani, A., et al.: Attention is all you need. Adv. Neural Inf. Process. Syst. 30, 5998\u20136008 (2017)","journal-title":"Adv. Neural Inf. Process. Syst."}],"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-81097-9_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,19]],"date-time":"2021-07-19T23:06:19Z","timestamp":1626735979000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81097-9_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030810962","9783030810979"],"references-count":28,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81097-9_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 July 2021","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":"Timisoara","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Romania","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2021\/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":"38","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":"12","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":"8","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":"32% - 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,5","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)"}}]}}