{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T06:44:21Z","timestamp":1762325061147,"version":"3.40.3"},"publisher-location":"Cham","reference-count":40,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030798758"},{"type":"electronic","value":"9783030798765"}],"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:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,7,5]],"date-time":"2021-07-05T00:00:00Z","timestamp":1625443200000},"content-version":"vor","delay-in-days":185,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We re-examine the topic of machine-learned clause selection guidance in saturation-based theorem provers. The central idea, recently popularized by the ENIGMA system, is to learn a classifier for recognizing clauses that appeared in previously discovered proofs. In subsequent runs, clauses classified positively are prioritized for selection. We propose several improvements to this approach and experimentally confirm their viability. For the demonstration, we use a recursive neural network to classify clauses based on their derivation history and the presence or absence of automatically supplied theory axioms therein. The automatic theorem prover Vampire guided by the network achieves a 41\u00a0% improvement on a relevant subset of SMT-LIB in a real time evaluation.<\/jats:p>","DOI":"10.1007\/978-3-030-79876-5_31","type":"book-chapter","created":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:20:19Z","timestamp":1625649619000},"page":"543-561","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Improving ENIGMA-style Clause Selection while Learning From History"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0989-5800","authenticated-orcid":false,"given":"Martin","family":"Suda","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,5]]},"reference":[{"key":"31_CR1","unstructured":"Ayg\u00fcn, E., Ahmed, Z., Anand, A., Firoiu, V., Glorot, X., Orseau, L., et\u00a0al.: Learning to prove from synthetic theorems. CoRR abs\/2006.11259 (2020)"},{"key":"31_CR2","unstructured":"Ba, L.J., Kiros, J.R., Hinton, G.E.: Layer normalization. CoRR abs\/1607.06450 (2016)"},{"key":"31_CR3","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: Rewrite-based equational theorem proving with selection and simplification. J. Log. Comput. 4(3), 217\u2013247 (1994). https:\/\/doi.org\/10.1093\/logcom\/4.3.217","DOI":"10.1093\/logcom\/4.3.217"},{"key":"31_CR4","doi-asserted-by":"publisher","unstructured":"Bachmair, L., Ganzinger, H.: Resolution theorem proving. In: Robinson and Voronkov [28], pp. 19\u201399. https:\/\/doi.org\/10.1016\/b978-044450813-3\/50004-7","DOI":"10.1016\/b978-044450813-3\/50004-7"},{"key":"31_CR5","unstructured":"Barrett, C., Fontaine, P., Tinelli, C.: The Satisfiability Modulo Theories Library (SMT-LIB) (2016), www.SMT-LIB.org"},{"key":"31_CR6","doi-asserted-by":"publisher","unstructured":"Bradley, A.R., Manna, Z., Sipma, H.B.: What\u2019s decidable about arrays? In: Emerson, E.A., Namjoshi, K.S. (eds.) Verification, Model Checking, and Abstract Interpretation, 7th International Conference, VMCAI 2006, Charleston, SC, USA, January 8-10, 2006, Proceedings. LNCS, vol. 3855, pp. 427\u2013442. Springer (2006). https:\/\/doi.org\/10.1007\/11609773_28","DOI":"10.1007\/11609773_28"},{"key":"31_CR7","doi-asserted-by":"publisher","unstructured":"Chvalovsk\u00fd, K., Jakubuv, J., Suda, M., Urban, J.: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. In: Fontaine [9], pp. 197\u2013215. https:\/\/doi.org\/10.1007\/978-3-030-29436-6_12","DOI":"10.1007\/978-3-030-29436-6_12"},{"key":"31_CR8","doi-asserted-by":"crossref","unstructured":"Denzinger, J., Schulz, S.: Learning Domain Knowledge to Improve Theorem Proving. In: McRobbie, M., Slaney, J. (eds.) Proc. of the 13th CADE, New Brunswick. pp. 62\u201376. No. 1104 in LNAI, Springer (1996)","DOI":"10.1007\/3-540-61511-3_69"},{"key":"31_CR9","doi-asserted-by":"publisher","unstructured":"Fontaine, P. (ed.): Automated Deduction - CADE 27 - 27th InternationalConference on Automated Deduction, Natal, Brazil, August 27-30, 2019, Proceedings, LNCS, vol. 11716. Springer (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6","DOI":"10.1007\/978-3-030-29436-6"},{"key":"31_CR10","unstructured":"Gleiss, B., Suda, M.: Layered clause selection for saturation-based theorem proving. In: Fontaine, P., Korovin, K., Kotsireas, I.S., R\u00fcmmer, P., Tourret, S. (eds.) Joint Proceedings of the 7th Workshop on Practical Aspects of Automated Reasoning (PAAR) and the 5th Satisfiability Checking and Symbolic Computation Workshop (SC-Square), co-located with the 10th International Joint Conference on Automated Reasoning (IJCAR 2020), Paris, France, June-July, 2020 (Virtual). CEUR Workshop Proceedings, vol. 2752, pp. 34\u201352. CEUR-WS.org (2020), http:\/\/ceur-ws.org\/Vol-2752\/paper3.pdf"},{"key":"31_CR11","doi-asserted-by":"publisher","unstructured":"Gleiss, B., Suda, M.: Layered clause selection for theory reasoning - (short paper). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part I. LNCS, vol. 12166, pp. 402\u2013409. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51074-9_23","DOI":"10.1007\/978-3-030-51074-9_23"},{"key":"31_CR12","doi-asserted-by":"publisher","unstructured":"Goller, C., K\u00fcchler, A.: Learning task-dependent distributed representations by backpropagation through structure. In: Proceedings of International Conference on Neural Networks (ICNN\u201996), Washington, DC, USA, June 3-6, 1996. pp. 347\u2013352. IEEE (1996). https:\/\/doi.org\/10.1109\/ICNN.1996.548916","DOI":"10.1109\/ICNN.1996.548916"},{"key":"31_CR13","unstructured":"Goodfellow, I.J., Bengio, Y., Courville, A.C.: Deep Learning. Adaptive computation and machine learning, MIT Press (2016), http:\/\/www.deeplearningbook.org\/"},{"key":"31_CR14","unstructured":"Irving, G., Szegedy, C., Alemi, A.A., E\u00e9n, N., Chollet, F., 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, December 5-10, 2016, Barcelona, Spain. pp. 2235\u20132243 (2016), https:\/\/proceedings.neurips.cc\/paper\/2016\/hash\/f197002b9a0853eca5e046d9ca4663d5-Abstract.html"},{"key":"31_CR15","doi-asserted-by":"publisher","unstructured":"Jakubuv, J., Chvalovsk\u00fd, K., Ols\u00e1k, M., Piotrowski, B., Suda, M., Urban, J.: ENIGMA anonymous: Symbol-independent inference guiding machine (system description). In: Peltier, N., Sofronie-Stokkermans, V. (eds.) Automated Reasoning - 10th International Joint Conference, IJCAR 2020, Paris, France, July 1-4, 2020, Proceedings, Part II. LNCS, vol. 12167, pp. 448\u2013463. Springer (2020). https:\/\/doi.org\/10.1007\/978-3-030-51054-1_29","DOI":"10.1007\/978-3-030-51054-1_29"},{"key":"31_CR16","doi-asserted-by":"publisher","unstructured":"Jakubuv, J., Urban, J.: ENIGMA: efficient learning-based inference guiding machine. In: Geuvers, H., England, M., Hasan, O., Rabe, F., Teschke, O. (eds.) Intelligent Computer Mathematics - 10th International Conference, CICM 2017, Edinburgh, UK, July 17-21, 2017, Proceedings. LNCS, vol. 10383, pp. 292\u2013302. Springer (2017). https:\/\/doi.org\/10.1007\/978-3-319-62075-6_20","DOI":"10.1007\/978-3-319-62075-6_20"},{"key":"31_CR17","doi-asserted-by":"publisher","unstructured":"Jakubuv, J., Urban, J.: Enhancing ENIGMA given clause guidance. In: Rabe, F., Farmer, W.M., Passmore, G.O., Youssef, A. (eds.) Intelligent Computer Mathematics - 11th International Conference, CICM 2018, Hagenberg, Austria, August 13-17, 2018, Proceedings. LNCS, vol. 11006, pp. 118\u2013124. Springer (2018). https:\/\/doi.org\/10.1007\/978-3-319-96812-4_11","DOI":"10.1007\/978-3-319-96812-4_11"},{"key":"31_CR18","doi-asserted-by":"publisher","unstructured":"Jakubuv, J., Urban, J.: Hammering Mizar by learning clause guidance (short paper). In: Harrison, J., O\u2019Leary, J., Tolmach, A. (eds.) 10th International Conference on Interactive Theorem Proving, ITP 2019, September 9-12, 2019, Portland, OR, USA. LIPIcs, vol. 141, pp. 34:1\u201334:8. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.34","DOI":"10.4230\/LIPIcs.ITP.2019.34"},{"key":"31_CR19","unstructured":"Kingma, D.P., Ba, J.: Adam: A method for stochastic optimization. In: Bengio, Y., LeCun, Y. (eds.) 3rd International Conference on Learning Representations, ICLR 2015, San Diego, CA, USA, May 7-9, 2015, Conference Track Proceedings (2015), http:\/\/arxiv.org\/abs\/1412.6980"},{"key":"31_CR20","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Robillard, S., Voronkov, A.: Coming to terms with quantified reasoning. In: Castagna, G., Gordon, A.D. (eds.) Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, POPL 2017, Paris, France, January 18-20, 2017. pp. 260\u2013270. ACM (2017). https:\/\/doi.org\/10.1145\/3009837.3009887","DOI":"10.1145\/3009837.3009887"},{"key":"31_CR21","doi-asserted-by":"publisher","unstructured":"Kov\u00e1cs, L., Voronkov, A.: First-order theorem proving and Vampire. In: Sharygina, N., Veith, H. (eds.) Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings. LNCS, vol. 8044, pp. 1\u201335. Springer (2013). https:\/\/doi.org\/10.1007\/978-3-642-39799-8_1","DOI":"10.1007\/978-3-642-39799-8_1"},{"key":"31_CR22","doi-asserted-by":"publisher","unstructured":"Loos, S.M., 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, May 7-12, 2017. EPiC Series in Computing, vol. 46, pp. 85\u2013105. EasyChair (2017). https:\/\/doi.org\/10.29007\/8mwc","DOI":"10.29007\/8mwc"},{"key":"31_CR23","doi-asserted-by":"publisher","unstructured":"Nieuwenhuis, R., Rubio, A.: Paramodulation-based theorem proving. In: Robinson and Voronkov [28], pp. 371\u2013443. https:\/\/doi.org\/10.1016\/b978-044450813-3\/50009-6","DOI":"10.1016\/b978-044450813-3\/50009-6"},{"key":"31_CR24","doi-asserted-by":"publisher","unstructured":"Ols\u00e1k, M., Kaliszyk, C., Urban, J.: Property invariant embedding for automated reasoning. In: Giacomo, G.D., Catal\u00e1, A., Dilkina, B., Milano, M., Barro, S., Bugar\u00edn, A., Lang, J. (eds.) ECAI 2020 - 24th European Conference on Artificial Intelligence, 29 August-8 September 2020, Santiago de Compostela, Spain, August 29 - September 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":"31_CR25","unstructured":"Paszke, A., Gross, S., Massa, F., Lerer, A., Bradbury, J., Chanan, G., et al.: Pytorch: An imperative style, high-performance deep learning library. In: Wallach, H., Larochelle, H., Beygelzimer, A., dAlch\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":"31_CR26","doi-asserted-by":"publisher","unstructured":"Reger, G., Suda, M., Voronkov, A.: Playing with AVATAR. In: Felty, A.P., Middeldorp, A. (eds.) Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings. LNCS, vol. 9195, pp. 399\u2013415. Springer (2015). https:\/\/doi.org\/10.1007\/978-3-319-21401-6_28","DOI":"10.1007\/978-3-319-21401-6_28"},{"key":"31_CR27","doi-asserted-by":"publisher","unstructured":"Riazanov, A., Voronkov, A.: Limited resource strategy in resolution theorem proving. J. Symb. Comput. 36(1-2), 101\u2013115 (2003). https:\/\/doi.org\/10.1016\/S0747-7171(03)00040-3","DOI":"10.1016\/S0747-7171(03)00040-3"},{"key":"31_CR28","unstructured":"Robinson, J.A., Voronkov, A. (eds.): Handbook of Automated Reasoning (in 2 volumes). Elsevier and MIT Press (2001)"},{"key":"31_CR29","doi-asserted-by":"publisher","unstructured":"Sandler, M., Howard, A.G., Zhu, M., Zhmoginov, A., Chen, L.: Mobilenetv 2: Inverted residuals and linear bottlenecks. In: 2018 IEEE Conference on Computer Vision and Pattern Recognition, CVPR 2018, Salt Lake City, UT, USA, June 18-22, 2018. pp. 4510\u20134520. IEEE Computer Society (2018). https:\/\/doi.org\/10.1109\/CVPR.2018.00474","DOI":"10.1109\/CVPR.2018.00474"},{"key":"31_CR30","unstructured":"Schulz, S.: Learning Search Control Knowledge for Equational Deduction. No. 230 in DISKI, Akademische Verlagsgesellschaft Aka GmbH Berlin (2000)"},{"key":"31_CR31","doi-asserted-by":"publisher","unstructured":"Schulz, S., Cruanes, S., Vukmirovic, P.: Faster, higher, stronger: E 2.3. In: Fontaine [9], pp. 495\u2013507. https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29","DOI":"10.1007\/978-3-030-29436-6_29"},{"key":"31_CR32","doi-asserted-by":"publisher","unstructured":"Schulz, S., M\u00f6hrmann, M.: Performance of clause selection heuristics for saturation-based theorem proving. In: Olivetti, N., Tiwari, A. (eds.) Automated Reasoning - 8th International Joint Conference, IJCAR 2016, Coimbra, Portugal, June 27 - July 2, 2016, Proceedings. LNCS, vol. 9706, pp. 330\u2013345. Springer (2016). https:\/\/doi.org\/10.1007\/978-3-319-40229-1_23","DOI":"10.1007\/978-3-319-40229-1_23"},{"key":"31_CR33","doi-asserted-by":"publisher","unstructured":"Smith, L.N.: Cyclical learning rates for training neural networks. In: 2017 IEEE Winter Conference on Applications of Computer Vision, WACV 2017, Santa Rosa, CA, USA, March 24-31, 2017. pp. 464\u2013472. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/WACV.2017.58","DOI":"10.1109\/WACV.2017.58"},{"key":"31_CR34","unstructured":"Smith, L.N., Topin, N.: Super-convergence: Very fast training of residual networks using large learning rates. CoRR abs\/1708.07120 (2017)"},{"key":"31_CR35","unstructured":"Srivastava, N., Hinton, G.E., Krizhevsky, A., Sutskever, I., Salakhutdinov, R.: Dropout: a simple way to prevent neural networks from overfitting. J. Mach. Learn. Res. 15(1), 1929\u20131958 (2014), http:\/\/dl.acm.org\/citation.cfm?id=2670313"},{"key":"31_CR36","doi-asserted-by":"publisher","unstructured":"Tammet, T.: GKC: A reasoning system for large knowledge bases. In: Fontaine [9], pp. 538\u2013549. https:\/\/doi.org\/10.1007\/978-3-030-29436-6_32","DOI":"10.1007\/978-3-030-29436-6_32"},{"key":"31_CR37","unstructured":"Urban, J.: personal communication"},{"key":"31_CR38","unstructured":"Vaswani, A., Shazeer, N., Parmar, N., Uszkoreit, J., Jones, L., Gomez, A.N., et al.: Attention is all you need. In: Guyon, I., von Luxburg, U., Bengio, S., Wallach, H.M., Fergus, R., Vishwanathan, S.V.N., Garnett, R. (eds.) Advances in Neural Information Processing Systems 30: Annual Conference on Neural Information Processing Systems 2017, December 4-9, 2017, Long Beach, CA, USA. pp. 5998\u20136008 (2017), https:\/\/proceedings.neurips.cc\/paper\/2017\/hash\/3f5ee243547dee91fbd053c1c4a845aa-Abstract.html"},{"key":"31_CR39","doi-asserted-by":"publisher","unstructured":"Voronkov, A.: AVATAR: the architecture for first-order theorem provers. In: Biere, A., Bloem, R. (eds.) Computer Aided Verification - 26th International Conference, CAV 2014, Held as Part of the Vienna Summer of Logic, VSL 2014, Vienna, Austria, July 18-22, 2014. Proceedings. LNCS, vol. 8559, pp. 696\u2013710. Springer (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_46","DOI":"10.1007\/978-3-319-08867-9_46"},{"key":"31_CR40","doi-asserted-by":"publisher","unstructured":"Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS version 3.5. In: Schmidt, R.A. (ed.) Automated Deduction - CADE-22, 22nd International Conference on Automated Deduction, Montreal, Canada, August 2-7, 2009. Proceedings. LNCS, vol. 5663, pp. 140\u2013145. Springer (2009). https:\/\/doi.org\/10.1007\/978-3-642-02959-2_10","DOI":"10.1007\/978-3-642-02959-2_10"}],"container-title":["Lecture Notes in Computer Science","Automated Deduction \u2013 CADE 28"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-79876-5_31","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,7]],"date-time":"2021-07-07T09:34:52Z","timestamp":1625650492000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-79876-5_31"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030798758","9783030798765"],"references-count":40,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-79876-5_31","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":"5 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CADE","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Deduction","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"15 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cade2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.cs.cmu.edu\/~mheule\/CADE28\/","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":"76","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":"29","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":"0","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":"38% - 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":"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)"}},{"value":"2 invited papers and 7 system descriptions are also included.","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)"}}]}}