{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T08:53:51Z","timestamp":1743152031637,"version":"3.40.3"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783031107689"},{"type":"electronic","value":"9783031107696"}],"license":[{"start":{"date-parts":[[2022,1,1]],"date-time":"2022-01-01T00:00:00Z","timestamp":1640995200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T00:00:00Z","timestamp":1659312000000},"content-version":"vor","delay-in-days":212,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2022]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Automated theorem provers (ATPs) are today used to attack open problems in several areas of mathematics. An ongoing project by Kinyon and Veroff uses Prover9 to search for the proof of the Abelian Inner Mapping (AIM) Conjecture, one of the top open conjectures in quasigroup theory. In this work, we improve Prover9 on a benchmark of AIM problems by neural synthesis of useful alternative formulations of the goal. In particular, we design the 3SIL (stratified shortest solution imitation learning) method. 3SIL trains a neural predictor through a reinforcement learning (RL) loop to propose correct rewrites of the conjecture that guide the search.<\/jats:p><jats:p>3SIL is first developed on a simpler, Robinson arithmetic rewriting task for which the reward structure is similar to theorem proving. There we show that 3SIL outperforms other RL methods. Next we train 3SIL on the AIM benchmark and show that the final trained network, deciding what actions to take within the equational rewriting environment, proves 70.2% of problems, outperforming Waldmeister (65.5%). When we combine the rewrites suggested by the network with Prover9, we prove 8.3% more theorems than Prover9 in the same time, bringing the performance of the combined system to 90%.<\/jats:p>","DOI":"10.1007\/978-3-031-10769-6_35","type":"book-chapter","created":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:02:56Z","timestamp":1659315776000},"page":"597-617","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Guiding an\u00a0Automated Theorem Prover with\u00a0Neural Rewriting"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8385-9157","authenticated-orcid":false,"given":"Jelle","family":"Piepenbrock","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3398-5235","authenticated-orcid":false,"given":"Tom","family":"Heskes","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3487-784X","authenticated-orcid":false,"given":"Mikol\u00e1\u0161","family":"Janota","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1384-1613","authenticated-orcid":false,"given":"Josef","family":"Urban","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,8,1]]},"reference":[{"issue":"2","key":"35_CR1","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1007\/s10817-013-9286-5","volume":"52","author":"J Alama","year":"2013","unstructured":"Alama, J., Heskes, T., K\u00fchlwein, D., Tsivtsivadze, E., Urban, J.: Premise selection for mathematics by corpus analysis and kernel methods. J. Autom. Reason. 52(2), 191\u2013213 (2013). https:\/\/doi.org\/10.1007\/s10817-013-9286-5","journal-title":"J. Autom. Reason."},{"unstructured":"Bansal, K., Loos, S., Rabe, M., Szegedy, C., Wilcox, S.: HOList: an environment for machine learning of higher order logic theorem proving. In: International Conference on Machine Learning, pp. 454\u2013463 (2019)","key":"35_CR2"},{"unstructured":"Barhate, N.: Implementation of PPO algorithm. https:\/\/github.com\/nikhilbarhate99","key":"35_CR3"},{"unstructured":"Berner, C., et al.: DOTA 2 with large scale deep reinforcement learning. arXiv preprint arXiv:1912.06680 (2019)","key":"35_CR4"},{"key":"35_CR5","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/978-3-030-53518-6_17","volume-title":"Intelligent Computer Mathematics","author":"L Blaauwbroek","year":"2020","unstructured":"Blaauwbroek, L., Urban, J., Geuvers, H.: The Tactician. In: Benzm\u00fcller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 271\u2013277. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_17"},{"issue":"1","key":"35_CR6","doi-asserted-by":"publisher","first-page":"101","DOI":"10.6092\/issn.1972-5787\/4593","volume":"9","author":"JC Blanchette","year":"2016","unstructured":"Blanchette, J.C., Kaliszyk, C., Paulson, L.C., Urban, J.: Hammering towards QED. J. Formalized Reason. 9(1), 101\u2013148 (2016). https:\/\/doi.org\/10.6092\/issn.1972-5787\/4593","journal-title":"J. Formalized Reason."},{"unstructured":"Brown, C.E., Piotrowski, B., Urban, J.: Learning to advise an equational prover. Artif. Intell. Theorem Proving, 1\u201313 (2020)","key":"35_CR7"},{"unstructured":"Ch\u00e9telat, D.: Implementation of ACER algorithm. https:\/\/github.com\/dchetelat\/acer","key":"35_CR8"},{"key":"35_CR9","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"197","DOI":"10.1007\/978-3-030-29436-6_12","volume-title":"Automated Deduction \u2013 CADE 27","author":"K Chvalovsk\u00fd","year":"2019","unstructured":"Chvalovsk\u00fd, K., Jakub\u016fv, J., Suda, M., Urban, J.: ENIGMA-NG: efficient neural and gradient-boosted inference guidance for E. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 197\u2013215. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_12"},{"key":"35_CR10","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 de Moura","year":"2008","unstructured":"de 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). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"unstructured":"Gauthier, T.: Deep reinforcement learning in HOL4. arXiv preprint arXiv:1910.11797v1 (2019)","key":"35_CR11"},{"unstructured":"Gauthier, T.: Deep reinforcement learning for synthesizing functions in higher-order logic. In: International Conference on Logic for Programming, Artificial Intelligence and Reasoning (2020)","key":"35_CR12"},{"key":"35_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-030-53518-6_18","volume-title":"Intelligent Computer Mathematics","author":"T Gauthier","year":"2020","unstructured":"Gauthier, T.: Tree neural networks in HOL4. In: Benzm\u00fcller, C., Miller, B. (eds.) CICM 2020. LNCS (LNAI), vol. 12236, pp. 278\u2013283. Springer, Cham (2020). https:\/\/doi.org\/10.1007\/978-3-030-53518-6_18"},{"key":"35_CR14","first-page":"1","volume":"65","author":"T Gauthier","year":"2020","unstructured":"Gauthier, T., Kaliszyk, C., Urban, J., Kumar, R., Norrish, M.: TacticToe: learning to prove with tactics. J. Autom. Reason. 65, 1\u201330 (2020)","journal-title":"J. Autom. Reason."},{"doi-asserted-by":"crossref","unstructured":"Graves, A., Fern\u00e1ndez, S., Gomez, F., Schmidhuber, J.: Connectionist temporal classification: labelling unsegmented sequence data with recurrent neural networks. In: Proceedings of the 23rd International Conference on Machine Learning, pp. 369\u2013376 (2006)","key":"35_CR15","DOI":"10.1145\/1143844.1143891"},{"key":"35_CR16","first-page":"3293","volume":"27","author":"H He","year":"2014","unstructured":"He, H., Daume, H., III., Eisner, J.M.: Learning to search in branch and bound algorithms. Adv. Neural Inf. Process. Syst. 27, 3293\u20133301 (2014)","journal-title":"Adv. Neural Inf. Process. Syst."},{"doi-asserted-by":"crossref","unstructured":"He, K., Zhang, X., Ren, S., Sun, J.: Deep residual learning for image recognition. In: Proceedings of the IEEE Conference on Computer Vision and Pattern Recognition, pp. 770\u2013778 (2016)","key":"35_CR17","DOI":"10.1109\/CVPR.2016.90"},{"key":"35_CR18","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1023\/A:1005872405899","volume":"18","author":"T Hillenbrand","year":"2004","unstructured":"Hillenbrand, T., Buch, A., Vogt, R., L\u00f6chner, B.: WALDMEISTER - high-performance equational deduction. J. Autom. Reasoning 18, 265\u2013270 (2004)","journal-title":"J. Autom. Reasoning"},{"issue":"1","key":"35_CR19","first-page":"9","volume":"86","author":"T Hillenbrand","year":"2003","unstructured":"Hillenbrand, T.: Citius altius fortius: lessons learned from the theorem prover Waldmeister. ENTCS 86(1), 9\u201321 (2003)","journal-title":"ENTCS"},{"key":"35_CR20","first-page":"2096","volume":"27","author":"O Irsoy","year":"2014","unstructured":"Irsoy, O., Cardie, C.: Deep recursive neural networks for compositionality in language. Adv. Neural Inf. Process. Syst. 27, 2096\u20132104 (2014)","journal-title":"Adv. Neural Inf. Process. Syst."},{"key":"35_CR21","first-page":"8822","volume":"31","author":"C Kaliszyk","year":"2018","unstructured":"Kaliszyk, C., Urban, J., Michalewski, H., Ol\u0161\u00e1k, M.: Reinforcement learning of theorem proving. Adv. Neural Inf. Process. Syst. 31, 8822\u20138833 (2018)","journal-title":"Adv. Neural Inf. Process. Syst."},{"unstructured":"Kingma, D.P., Ba, J.: Adam: a method for stochastic optimization. arXiv preprint arXiv:1412.6980 (2014)","key":"35_CR22"},{"unstructured":"Kinyon, M.: Proof simplification and automated theorem proving. CoRR abs\/1808.04251 (2018). http:\/\/arxiv.org\/abs\/1808.04251","key":"35_CR23"},{"key":"35_CR24","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/978-3-642-36675-8_8","volume-title":"Automated Reasoning and Mathematics","author":"M Kinyon","year":"2013","unstructured":"Kinyon, M., Veroff, R., Vojt\u011bchovsk\u00fd, P.: Loops with abelian inner mapping groups: an application of automated deduction. In: Bonacina, M.P., Stickel, M.E. (eds.) Automated Reasoning and Mathematics. LNCS (LNAI), vol. 7788, pp. 151\u2013164. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36675-8_8"},{"unstructured":"McCune, W.: Prover9 and Mace (2010). http:\/\/www.cs.unm.edu\/~mccune\/prover9\/","key":"35_CR25"},{"unstructured":"McCune, W.: Prover9. https:\/\/github.com\/ai4reason\/Prover9","key":"35_CR26"},{"unstructured":"Mnih, V., et al.: Asynchronous methods for deep reinforcement learning. In: International Conference on Machine Learning, pp. 1928\u20131937 (2016)","key":"35_CR27"},{"issue":"7540","key":"35_CR28","doi-asserted-by":"publisher","first-page":"529","DOI":"10.1038\/nature14236","volume":"518","author":"V Mnih","year":"2015","unstructured":"Mnih, V., et al.: Human-level control through deep reinforcement learning. Nature 518(7540), 529\u2013533 (2015)","journal-title":"Nature"},{"unstructured":"Oh, J., Guo, Y., Singh, S., Lee, H.: Self-imitation learning. In: International Conference on Machine Learning, pp. 3878\u20133887 (2018)","key":"35_CR29"},{"issue":"2","key":"35_CR30","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1145\/321812.321814","volume":"21","author":"RA Overbeek","year":"1974","unstructured":"Overbeek, R.A.: A new class of automated theorem-proving algorithms. J. ACM 21(2), 191\u2013200 (1974). https:\/\/doi.org\/10.1145\/321812.321814","journal-title":"J. ACM"},{"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, vol. 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":"35_CR31"},{"issue":"2\u20133","key":"35_CR32","doi-asserted-by":"publisher","first-page":"267","DOI":"10.3233\/AIC-2010-0460","volume":"23","author":"J Phillips","year":"2010","unstructured":"Phillips, J., Stanovsk\u00fd, D.: Automated theorem proving in quasigroup and loop theory. AI Commun. 23(2\u20133), 267\u2013283 (2010)","journal-title":"AI Commun."},{"unstructured":"PyTorch: RL Examples. https:\/\/github.com\/pytorch\/examples\/tree\/main\/reinforcement_learning","key":"35_CR33"},{"unstructured":"Ross, S., Gordon, G., Bagnell, D.: A reduction of imitation learning and structured prediction to no-regret online learning. In: Proceedings of the 14th International Conference on Artificial Intelligence and Statistics, pp. 627\u2013635 (2011)","key":"35_CR34"},{"unstructured":"Schulman, J., Levine, S., Abbeel, P., Jordan, M., Moritz, P.: Trust region policy optimization. In: Bach, F., Blei, D. (eds.) Proceedings of the 32nd International Conference on Machine Learning. Proceedings of Machine Learning Research, vol. 37, pp. 1889\u20131897. PMLR, Lille (2015). https:\/\/proceedings.mlr.press\/v37\/schulman15.html","key":"35_CR35"},{"unstructured":"Schulman, J., Wolski, F., Dhariwal, P., Radford, A., Klimov, O.: Proximal policy optimization algorithms. arXiv preprint arXiv:1707.06347 (2017)","key":"35_CR36"},{"issue":"2\u20133","key":"35_CR37","first-page":"111","volume":"15","author":"S Schulz","year":"2002","unstructured":"Schulz, S.: E - a brainiac theorem prover. AI Commun. 15(2\u20133), 111\u2013126 (2002)","journal-title":"AI Commun."},{"key":"35_CR38","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"495","DOI":"10.1007\/978-3-030-29436-6_29","volume-title":"Automated Deduction \u2013 CADE 27","author":"S Schulz","year":"2019","unstructured":"Schulz, S., Cruanes, S., Vukmirovi\u0107, P.: Faster, Higher, Stronger: E 2.3. In: Fontaine, P. (ed.) CADE 2019. LNCS (LNAI), vol. 11716, pp. 495\u2013507. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29436-6_29"},{"unstructured":"Schulz, S.: Eprover. https:\/\/wwwlehre.dhbw-stuttgart.de\/~sschulz\/E\/E.html","key":"35_CR39"},{"issue":"7587","key":"35_CR40","doi-asserted-by":"publisher","first-page":"484","DOI":"10.1038\/nature16961","volume":"529","author":"D Silver","year":"2016","unstructured":"Silver, D.: Mastering the game of go with deep neural networks and tree search. Nature 529(7587), 484\u2013489 (2016)","journal-title":"Nature"},{"issue":"7676","key":"35_CR41","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\u2013359 (2017)","journal-title":"Nature"},{"key":"35_CR42","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"602","DOI":"10.1007\/978-3-030-79876-5_35","volume-title":"Automated Deduction \u2013 CADE 28","author":"N Smallbone","year":"2021","unstructured":"Smallbone, N.: Twee: an equational theorem prover. In: Platzer, A., Sutcliffe, G. (eds.) CADE 2021. LNCS (LNAI), vol. 12699, pp. 602\u2013613. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-79876-5_35"},{"unstructured":"Smallbone, N.: Twee 2.4.1. https:\/\/github.com\/nick8325\/twee\/releases\/download\/2.4.1\/twee-2.4.1-linux-amd64","key":"35_CR43"},{"issue":"5\u20136","key":"35_CR44","doi-asserted-by":"publisher","first-page":"373","DOI":"10.3233\/AIC-190627","volume":"32","author":"G Sutcliffe","year":"2020","unstructured":"Sutcliffe, G.: The CADE-27 automated theorem proving system competition - CASC-27. AI Commun. 32(5\u20136), 373\u2013389 (2020)","journal-title":"AI Commun."},{"key":"35_CR45","volume-title":"Reinforcement Learning: An Introduction","author":"RS Sutton","year":"2018","unstructured":"Sutton, R.S., Barto, A.G.: Reinforcement Learning: An Introduction. MIT press, Cambridge (2018)"},{"unstructured":"Hillenbrand, T., Buch, A., Vogt, R., L\u00f6chner, B.: Waldmeister (2022). https:\/\/www.mpi-inf.mpg.de\/departments\/automation-of-logic\/software\/waldmeister\/download","key":"35_CR46"},{"doi-asserted-by":"crossref","unstructured":"Torabi, F., Warnell, G., Stone, P.: Behavioral cloning from observation. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence, IJCAI 2018, pp. 4950\u20134957. AAAI Press (2018)","key":"35_CR47","DOI":"10.24963\/ijcai.2018\/687"},{"issue":"3","key":"35_CR48","doi-asserted-by":"publisher","first-page":"223","DOI":"10.1007\/BF00252178","volume":"16","author":"R Veroff","year":"1996","unstructured":"Veroff, R.: Using hints to increase the effectiveness of an automated reasoning program: Case studies. J. Autom. Reason. 16(3), 223\u2013239 (1996). https:\/\/doi.org\/10.1007\/BF00252178","journal-title":"J. Autom. Reason."},{"unstructured":"Wang, Z., et al.: Sample efficient actor-critic with experience replay. In: International Conference on Learning Representations (2016)","key":"35_CR49"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-10769-6_35","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,8,1]],"date-time":"2022-08-01T01:16:43Z","timestamp":1659316603000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-10769-6_35"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022]]},"ISBN":["9783031107689","9783031107696"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-10769-6_35","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2022]]},"assertion":[{"value":"1 August 2022","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Haifa","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Israel","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2022","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 August 2022","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 August 2022","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2022","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/easychair.org\/smart-program\/FLoC2022\/IJCAR-index.html","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":"85","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":"32","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":"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.2","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.2","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)"}}]}}