{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T02:43:08Z","timestamp":1762310588939,"version":"build-2065373602"},"reference-count":267,"publisher":"Springer Science and Business Media LLC","issue":"6","license":[{"start":{"date-parts":[[2025,10,14]],"date-time":"2025-10-14T00:00:00Z","timestamp":1760400000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2025,10,14]],"date-time":"2025-10-14T00:00:00Z","timestamp":1760400000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100003484","name":"Heinrich-Heine-Universit\u00e4t D\u00fcsseldorf","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100003484","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Empir Software Eng"],"published-print":{"date-parts":[[2025,12]]},"abstract":"Abstract<\/jats:title>\n \n Context<\/jats:title>\n With artificial intelligence (AI) being well established within the daily lives of research communities, we turn our gaze toward formal methods (FM). FM aim to provide sound and verifiable reasoning about problems in computer science.<\/jats:p>\n <\/jats:sec>\n \n Objective<\/jats:title>\n We conduct a systematic mapping study to overview the current landscape of research publications that apply AI to FM. We aim to identify how FM can benefit from AI techniques and highlight areas for further research. Our focus lies on the previous five years (2019\u20132023) of research.<\/jats:p>\n <\/jats:sec>\n \n Method<\/jats:title>\n Following the proposed guidelines for systematic mapping studies, we searched for relevant publications in four major databases, defined inclusion and exclusion criteria, and applied extensive snowballing to uncover potential additional sources.<\/jats:p>\n <\/jats:sec>\n \n Results<\/jats:title>\n This investigation results in 189 entries which we explored to find current trends and highlight research gaps. We find a strong focus on AI in the area of theorem proving while other subfields of FM are less represented.<\/jats:p>\n <\/jats:sec>\n \n Conclusions<\/jats:title>\n The mapping study provides a quantitative overview of the modern state of AI application in FM. The current trend of the field is yet to mature. Many primary studies focus on practical application, yet we identify a lack of theoretical groundwork, standard benchmarks, or case studies. Further, we identify issues regarding shared training data sets and standard benchmarks.<\/jats:p>\n <\/jats:sec>","DOI":"10.1007\/s10664-025-10729-8","type":"journal-article","created":{"date-parts":[[2025,10,14]],"date-time":"2025-10-14T15:57:44Z","timestamp":1760457464000},"update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Application of AI to formal methods \u2014 an analysis of current trends"],"prefix":"10.1007","volume":"30","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2231-8656","authenticated-orcid":false,"given":"Sebastian","family":"Stock","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0819-5554","authenticated-orcid":false,"given":"Jannik","family":"Dunkelau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1210-5953","authenticated-orcid":false,"given":"Atif","family":"Mashkoor","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2025,10,14]]},"reference":[{"key":"10729_CR1","unstructured":"Abate A, Edwards A, Giacobbe M (2022) Neural abstractions. In: Koyejo S, Mohamed S, Agarwal A, Belgrave D, Cho K, Oh A (eds.) Advances in neural information processing systems 35 (NeurIPS 2022), vol 35, pp 26432\u201326447. Curran Associates, Inc., New Orleans, LA, USA. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2022\/file\/a922b7121007768f78f770c404415375-Paper-Conference.pdf"},{"issue":"1","key":"10729_CR2","doi-asserted-by":"publisher","first-page":"738","DOI":"10.1109\/TPAMI.2022.3140382","volume":"45","author":"I Abdelaziz","year":"2023","unstructured":"Abdelaziz I, Crouse M, Makni B, Austel V, Cornelio C, Ikbal S, Kapanipathi P, Makondo N, Srinivas K, Witbrock M, Fokoue A (2023) Learning to guide a saturation-based theorem prover. IEEE Trans Pattern Anal Mach Intell 45(1):738\u2013751. https:\/\/doi.org\/10.1109\/TPAMI.2022.3140382","journal-title":"IEEE Trans Pattern Anal Mach Intell"},{"key":"10729_CR3","unstructured":"Abran A, Moore JW, Bourque P, Dupuis R (eds) (2004) Software engineering body of knowledge vol 25. IEEE Computer Society, Los Alamitos, CA, USA. https:\/\/www.computer.org\/education\/bodies-of-knowledge\/software-engineering"},{"key":"10729_CR4","doi-asserted-by":"publisher","unstructured":"Allamanis M (2022) In: Wu L, Cui P, Pei J, Zhao L (eds) Graph neural networks in program analysis, pp 483\u2013497. Springer, Singapore. https:\/\/doi.org\/10.1007\/978-981-16-6054-2_22","DOI":"10.1007\/978-981-16-6054-2_22"},{"key":"10729_CR5","doi-asserted-by":"publisher","unstructured":"Amadini R, Gabbrielli M, Mauro J (2013) An empirical evaluation of portfolios approaches for solving CSPs. In: Gomes C, Sellmann M (eds.) Integration of AI and OR Techniques in Constraint Programming for Combinatorial Optimization Problems, pp 316\u2013324. Springer, Yorktown Heights, NY, USA.https:\/\/doi.org\/10.1007\/978-3-642-38171-3_21","DOI":"10.1007\/978-3-642-38171-3_21"},{"key":"10729_CR6","unstructured":"Amizadeh S, Matusevych S, Weimer M (2019) Learning to solve Circuit-SAT: An unsupervised differentiable approach. In: International conference on learning representations. OpenReview.net, New Orleans, LA, USA. https:\/\/openreview.net\/forum?id=BJxgz2R9t7"},{"key":"10729_CR7","unstructured":"Amrani M, L\u00facio L, Bibal A (2018) ML + FV= $$\\heartsuit$$? a survey on the application of machine learning to formal verification. arXiv:1806.03600 [cs.SE]"},{"key":"10729_CR8","doi-asserted-by":"publisher","unstructured":"Atkari A, Dhargalkar N, Angne H (2020) Employing machine learning models to solve uniform random 3-SAT. In: Jain LC, Tsihrintzis GA, Balas VE, Sharma DK (eds.) Data Communication and Networks. Advances in Intelligent Systems and Computing, vol. 1049, pp 255\u2013264. Springer, New Delhi, India. https:\/\/doi.org\/10.1007\/978-981-15-0132-6_17","DOI":"10.1007\/978-981-15-0132-6_17"},{"key":"10729_CR9","unstructured":"Ayg\u00fcn E, Anand A, Orseau L, Glorot X, Mcaleer SM, Firoiu V, Zhang LM, Precup, D, Mourad S (2022) Proving theorems using incremental learning and hindsight experience replay. In: Chaudhuri K, Jegelka S, Song L, Szepesvari C, Niu G, Sabato S (eds) Proceedings of the 39th international conference on machine learning. Proceedings of machine learning research, vol 162, pp 1198\u20131210. PMLR, Baltimore, MA, USA. https:\/\/proceedings.mlr.press\/v162\/aygun22a.html"},{"issue":"11","key":"10729_CR10","doi-asserted-by":"publisher","first-page":"1193","DOI":"10.3897\/jucs.76563","volume":"27","author":"A Baghdasaryan","year":"2021","unstructured":"Baghdasaryan A, Bolibekyan H (2021) On recurrent neural network based theorem prover for first order minimal logic. J Univ Comput Sci 27(11):1193\u20131202. https:\/\/doi.org\/10.3897\/jucs.76563","journal-title":"J Univ Comput Sci"},{"key":"10729_CR11","unstructured":"Baier C, Katoen J-P (2008) Principles of Model Checking. MIT press, Cambridge, MA, USA. https:\/\/mitpress.mit.edu\/9780262026499\/principles-of-model-checking\/"},{"key":"10729_CR12","unstructured":"Bansal K, Loos S, Rabe M, Szegedy C, Wilcox S (2019) HOList: An environment for machine learning of higher order logic theorem proving. In: Chaudhuri K, Salakhutdinov R (eds) Proceedings of the 36th international conference on machine learning. proceedings of machine learning research, vol 97, pp 454\u2013463. PMLR, Long Beach, CA, USA. https:\/\/proceedings.mlr.press\/v97\/bansal19a.html"},{"key":"10729_CR13","doi-asserted-by":"publisher","unstructured":"Barenkamp M, Rebstadt J, Thomas O (2020) Applications of AI in classical software engineering. AI Perspectives 2. https:\/\/doi.org\/10.1186\/s42467-020-00005-4","DOI":"10.1186\/s42467-020-00005-4"},{"key":"10729_CR14","doi-asserted-by":"publisher","unstructured":"Barrett C, Tinelli C (2018) Satisfiability Modulo Theories. In: Clarke EM, Henzinger TA, Veith H, Bloem R (eds) Handbook of Model Checking, pp 305\u2013343. Springer, Cham. https:\/\/doi.org\/10.1007\/978-3-319-10575-8_11","DOI":"10.1007\/978-3-319-10575-8_11"},{"issue":"3","key":"10729_CR15","doi-asserted-by":"publisher","first-page":"1135","DOI":"10.1007\/s10270-022-00983-5","volume":"21","author":"A Barriga","year":"2022","unstructured":"Barriga A, Rutle A, Heldal R (2022) AI-powered model repair: an experience report\u2013lessons learned, challenges, and opportunities. Softw Syst Model 21(3):1135\u20131157. https:\/\/doi.org\/10.1007\/s10270-022-00983-5","journal-title":"Softw Syst Model"},{"key":"10729_CR16","unstructured":"B\u00e1rtek F, Suda M (2020) Learning precedences from simple symbol features. In: Fontaine P, Korovin K, Kotsireas IS, R\u00fcmmer P, Tourret S (eds.) PAAR+SC-Square 2020 Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2020. CEUR Workshop Proceedings, vol. 2752, pp 21\u201333. CEUR-WS.org, Virtual Event. https:\/\/ceur-ws.org\/Vol-2752\/paper2.pdf"},{"key":"10729_CR17","doi-asserted-by":"publisher","unstructured":"B\u00e1rtek F, Suda M (2021) Neural precedence recommender. In: Platzer A, Sutcliffe G (eds.) Automated Deduction \u2013 CADE 28. Lecture Notes in Computer Science, vol. 12699, pp 525\u2013542. Springer, Virtual Event. https:\/\/doi.org\/10.1007\/978-3-030-79876-5_30","DOI":"10.1007\/978-3-030-79876-5_30"},{"key":"10729_CR18","doi-asserted-by":"publisher","unstructured":"Bennaceur A, Meinke K (2018) In: Bennaceur A, H\u00e4hnle R, Meinke K (eds.) Machine Learning for Software Analysis: Models, Methods, and Applications. Lecture Notes in Computer Science, vol. 11026, pp 3\u201349. Springer, Dagstuhl Castle, Germany. https:\/\/doi.org\/10.1007\/978-3-319-96562-8_1","DOI":"10.1007\/978-3-319-96562-8_1"},{"key":"10729_CR19","doi-asserted-by":"publisher","unstructured":"Berden S, Kumar M, Kolb S, Guns T (2022) Learning MAX-SAT models from examples using genetic algorithms and knowledge compilation. In: 28th International conference on principles and practice of constraint programming. Leibniz International Proceedings in Informatics, LIPIcs, vol. 235, pp 1\u201317. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Haifa, Israel. https:\/\/doi.org\/10.4230\/LIPIcs.CP.2022.8","DOI":"10.4230\/LIPIcs.CP.2022.8"},{"key":"10729_CR20","doi-asserted-by":"publisher","unstructured":"Bertot Y, Cast\u00e9ran P (2013) Interactive Theorem Proving and Program Development, 1st edn Texts in Theoretical Computer Science. An EATCS Series. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-662-07964-5","DOI":"10.1007\/978-3-662-07964-5"},{"key":"10729_CR21","doi-asserted-by":"publisher","unstructured":"Besbas A, Belaiche L, Slatnia S, Kahloul L, Khalgui M (2022) Machine learning solutions to model checking: A brief literature review. In: 2022 International Symposium on iNnovative Informatics of Biskra (ISNIB), pp 1\u20134. IEEE, Biskra, Algeria. https:\/\/doi.org\/10.1109\/ISNIB57382.2022.10076160","DOI":"10.1109\/ISNIB57382.2022.10076160"},{"key":"10729_CR22","doi-asserted-by":"publisher","unstructured":"Beskyd F, Surynek P (2022) Parameter setting in SAT solver using machine learning techniques. In: Rocha A, Steels L, VandenHerik J (eds.) Proceedings of the 14th International Conference on Agentes and Artifical Inteligence. ICAART, vol. 2, pp 586\u2013597. SciTePress, Virtual Event. https:\/\/doi.org\/10.5220\/0010910200003116","DOI":"10.5220\/0010910200003116"},{"key":"10729_CR23","unstructured":"Biere A, Heule M, Maaren H (eds) (2015) Handbook of Satisfiability, 2nd edn. Frontiers in artificial intelligence and applications, vol 336. IOS press, Amsterdam. https:\/\/ebooks.iospress.nl\/volume\/handbook-of-satisfiability-second-edition"},{"key":"10729_CR24","doi-asserted-by":"publisher","unstructured":"Blaauwbroek L, Urban J, Geuvers H (2020) Tactic learning and proving for the Coq proof assistant. In: Albert E, Kovacs L (eds) 23rd International conference on logic for programming, artificial intelligence and reasoning. EPiC series in computing, vol 73, pp 138\u2013150. EasyChair, Virtual Event. https:\/\/doi.org\/10.29007\/wg1q","DOI":"10.29007\/wg1q"},{"key":"10729_CR25","unstructured":"Blanchette JC, El\u00a0Ouraoui D, Fontaine P, Kaliszyk C (2019) Machine learning for instance selection in SMT solving. In: 4th Conference on artificial intelligence and theorem proving. AITP Conference, Obergurgl, Austria. https:\/\/aitp-conference.org\/2019\/abstract\/paper%2017.pdf"},{"key":"10729_CR26","unstructured":"Blanchette JC, K\u00fchlwein D, Geschke S, Loewe B, Schlicht P (2014) A survey of axiom selection as a machine learning problem. In: Stefan\u00a0Geschke, P.S. Benedikt\u00a0Loewe (ed.) Infinity, Computability, and Metamathematics: Festschrift Celebrating the 60th Birthdays of Peter Koepke and Philip Welch, pp. 1\u201315. College Publications, London, UK. https:\/\/hdl.handle.net\/2066\/132733"},{"key":"10729_CR27","doi-asserted-by":"publisher","first-page":"219","DOI":"10.1007\/s10817-016-9362-8","volume":"57","author":"JC Blanchette","year":"2016","unstructured":"Blanchette JC, Greenaway D, Kaliszyk C, K\u00fchlwein D, Urban J (2016) A learning-based fact selector for Isabelle\/HOL. J Autom Reason 57:219\u2013244. https:\/\/doi.org\/10.1007\/s10817-016-9362-8","journal-title":"J Autom Reason"},{"key":"10729_CR28","unstructured":"Bordg A, Stathopoulos YA, Paulson LC (2022) A parallel corpus of natural language and isabelle artefacts. In: 7th Conference on artificial intelligence and theorem proving. AITP Conference, Aussois and online, France. https:\/\/aitp-conference.org\/2022\/abstract\/AITP_2022_paper_8.pdf"},{"issue":"1","key":"10729_CR29","doi-asserted-by":"publisher","first-page":"5","DOI":"10.1023\/a:1010933404324","volume":"45","author":"L Breiman","year":"2001","unstructured":"Breiman L (2001) Random forests. Mach Learn 45(1):5\u201332. https:\/\/doi.org\/10.1023\/a:1010933404324","journal-title":"Mach Learn"},{"key":"10729_CR30","doi-asserted-by":"publisher","DOI":"10.1201\/9781315139470","author":"L Breiman","year":"1984","unstructured":"Breiman L, Friedman J, Stone CJ, Olshen RA (1984) Classification and Regression Trees. Taylor & Francis New York NY. https:\/\/doi.org\/10.1201\/9781315139470","journal-title":"Taylor & Francis New York NY"},{"key":"10729_CR31","unstructured":"Brockman G, Cheung V, Pettersson L, Schneider J, Schulman J, Tang J, Zaremba W (2016) OpenAI Gym. arXiv:1606.01540 [cs.LG]"},{"key":"10729_CR32","unstructured":"Brown CE, Gauthier T (2020) Self-learned formula synthesis in set theory. In: 5th Conference on artificial intelligence and theorem proving. AITP Conference, Aussois, France. https:\/\/aitp-conference.org\/2020\/abstract\/paper_1.pdf"},{"key":"10729_CR33","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1007\/s10817-013-9283-8","volume":"51","author":"CE Brown","year":"2013","unstructured":"Brown CE (2013) Reducing higher-order theorem proving to a sequence of SAT problems. J Automated Reason 51:57\u201377. https:\/\/doi.org\/10.1007\/s10817-013-9283-8","journal-title":"J Automated Reason"},{"key":"10729_CR34","doi-asserted-by":"publisher","unstructured":"Brunello, A., Montanari A, Reynolds M (2019) Synthesis of LTL Formulas from Natural Language Texts: State of the Art and Research Directions. In: Gamper J, Pinchinat S, Sciavicco G (eds.) 26th International Symposium on Temporal Representation and Reasoning (TIME 2019). Leibniz International Proceedings in Informatics (LIPIcs), vol. 147, pp 1\u201319. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, M\u00e1laga, Spain. https:\/\/doi.org\/10.4230\/LIPIcs.TIME.2019.17","DOI":"10.4230\/LIPIcs.TIME.2019.17"},{"key":"10729_CR35","doi-asserted-by":"publisher","unstructured":"Buzhinsky I (2019) Formalization of natural language requirements into temporal logics: a survey. In: 2019 IEEE 17th International conference on industrial informatics (INDIN), pp 400\u2013406. IEEE, Helsinki, Finland. https:\/\/doi.org\/10.1109\/INDIN41052.2019.8972130","DOI":"10.1109\/INDIN41052.2019.8972130"},{"key":"10729_CR36","doi-asserted-by":"publisher","unstructured":"Cai C-H, Sun J, Dobbie G (2019a) Automatic B-model repair using model checking and machine learning. Autom Softw Eng 26(3):653\u2013704. https:\/\/doi.org\/10.1007\/s10515-019-00264-4","DOI":"10.1007\/s10515-019-00264-4"},{"key":"10729_CR37","doi-asserted-by":"publisher","unstructured":"Cai C-H, Sun J, Dobbie G (2022) B model quality assessments on automated reachability repair with ISO\/IEC 25010. Sci Comput Program 214:102732. https:\/\/doi.org\/10.1016\/j.scico.2021.102732","DOI":"10.1016\/j.scico.2021.102732"},{"key":"10729_CR38","doi-asserted-by":"publisher","unstructured":"Cai C-H, Sun J, Dobbie G, Lee SU-J (2019b) Achieving abstract machine reachability with learning-based model fulfilment. In: 2019 26th Asia-Pacific software engineering conference (APSEC), Putrajaya, Malaysia, pp 260\u2013267. https:\/\/doi.org\/10.1109\/APSEC48747.2019.00043","DOI":"10.1109\/APSEC48747.2019.00043"},{"key":"10729_CR39","doi-asserted-by":"publisher","unstructured":"Cameron C, Chen R, Hartford J, Leyton-Brown K (2020) Predicting propositional satisfiability via end-to-end learning. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 34, pp 3324\u20133331. AAAI Press, New York, NY, USA.https:\/\/doi.org\/10.1609\/aaai.v34i04.5733","DOI":"10.1609\/aaai.v34i04.5733"},{"key":"10729_CR40","doi-asserted-by":"publisher","unstructured":"Cao W, Wu Y, Wang Q, Zhang J, Zhang X, Qiu M (2022) A novel RVFL-based algorithm selection approach for software model checking. In: Memmi G, Yang B, Kong L, Zhang T, Qiu M (eds) Knowledge science, engineering and management. Lecture notes in computer science, vol 13370, pp 414\u2013425. Springer, Singapore. https:\/\/doi.org\/10.1007\/978-3-031-10989-8_33","DOI":"10.1007\/978-3-031-10989-8_33"},{"key":"10729_CR41","doi-asserted-by":"publisher","unstructured":"Cao W, Xie Z, Zhou X, Xu Z, Zhou C, Theodoropoulos G, Wang Q (2020) A learning framework for intelligent selection of software verification algorithms. J Artif Intell 2(4):177\u2013187. https:\/\/doi.org\/10.32604\/jai.2020.014829","DOI":"10.32604\/jai.2020.014829"},{"key":"10729_CR42","doi-asserted-by":"publisher","unstructured":"Chang K-H (2023) Artificial intelligence and information processing: A systematic literature review. Mathematics 11(11). https:\/\/doi.org\/10.3390\/math11112420","DOI":"10.3390\/math11112420"},{"issue":"1","key":"10729_CR43","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/s44196-022-00139-9","volume":"15","author":"W Chang","year":"2022","unstructured":"Chang W, Zhang H, Luo J (2022) Predicting propositional satisfiability based on graph attention networks. Int J Computat Intell Syst 15(1):84. https:\/\/doi.org\/10.1007\/s44196-022-00139-9","journal-title":"Int J Computat Intell Syst"},{"issue":"3","key":"10729_CR44","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3641289","volume":"15","author":"Y Chang","year":"2024","unstructured":"Chang Y, Wang X, Wang J, Wu Y, Yang L, Zhu K, Chen H, Yi X, Wang C, Wang Y, Ye W, Zhang Y, Chang Y, Yu PS, Yang Q, Xie X (2024) A survey on evaluation of large language models. ACM Trans Intell Syst Technol 15(3):1\u201345. https:\/\/doi.org\/10.1145\/3641289","journal-title":"ACM Trans Intell Syst Technol"},{"key":"10729_CR45","unstructured":"Chang O, Flokas L, Lipson H, Spranger M (2020) Assessing SATNet\u2019s ability to solve the symbol grounding problem. In: Larochelle H, Ranzato M, Hadsell R, Balcan MF, Lin H (eds.) Advances in Neural Information Processing Systems, vol. 33, pp 1428\u20131439. Curran Associates, Inc., Virtual Event. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2020\/file\/0ff8033cf9437c213ee13937b1c4c455-Paper.pdf"},{"key":"10729_CR46","doi-asserted-by":"publisher","unstructured":"Chen J, Wei J, Feng Y, Bastani O, Dillig I (2019) Relational verification using reinforcement learning. Proceedings of the ACM on programming languages 3(OOPSLA), 1\u201330. https:\/\/doi.org\/10.1145\/3360567","DOI":"10.1145\/3360567"},{"key":"10729_CR47","doi-asserted-by":"publisher","unstructured":"Cherukuri H, Ferrari A, Spoletini P (2022) Towards explainable formal methods: From LTL to natural language with neural machine translation. In: Gervasi V, Vogelsang A (eds.) International working conference on requirements engineering: foundation for software quality. Lecture notes in computer science, vol 13216, pp 79\u201386. Springer, Birmingham, UK. https:\/\/doi.org\/10.1007\/978-3-030-98464-9_7","DOI":"10.1007\/978-3-030-98464-9_7"},{"key":"10729_CR48","doi-asserted-by":"publisher","unstructured":"Chowdhary KR (2020) Natural Language Processing. Fundamentals of Artificial Intelligence, pp 603\u2013649. Springer, New Delhi. https:\/\/doi.org\/10.1007\/978-81-322-3972-7_19","DOI":"10.1007\/978-81-322-3972-7_19"},{"key":"10729_CR49","doi-asserted-by":"publisher","unstructured":"Chvalovsk\u00fd K, Jakub\u016fv J, Ol\u0161\u00e1k M, Urban J (2021) Learning theorem proving components. In: Anupam\u00a0Das SN (ed.) Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science, vol. 12842, pp 266\u2013278. Springer, Birmingham, UK. https:\/\/doi.org\/10.1007\/978-3-030-86059-2_16","DOI":"10.1007\/978-3-030-86059-2_16"},{"key":"10729_CR50","doi-asserted-by":"publisher","unstructured":"Chvalovsk\u00fd K, Jakub\u016fv J, Suda M, Urban J (2019) ENIGMA-NG: Efficient neural and gradient-boosted inference guidance for E. In: Fontaine P (ed.) International Conference on Automated Deduction. Lecture Notes in Computer Science, vol. 11716, pp 197\u2013215. Springer, Natal, Brazil. https:\/\/doi.org\/10.1007\/978-3-030-29436-6_12","DOI":"10.1007\/978-3-030-29436-6_12"},{"key":"10729_CR51","doi-asserted-by":"publisher","unstructured":"Chvalovsk\u1ef3 K, Korovin K, Piepenbrock J, Urban J (2023) Guiding an instantiation prover with graph neural networks. In: Piskac R, Voronkov A (eds.) Proceedings of 24th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning. EPiC Series in Computing, vol. 94, pp 112\u2013123. EasyChair, Manizales, Colombia. https:\/\/doi.org\/10.29007\/tp23","DOI":"10.29007\/tp23"},{"key":"10729_CR52","doi-asserted-by":"publisher","unstructured":"Clarke EM, Henzinger TA, Veith H, Bloem R et al (2018) Handbook of Model Checking. Springer Cham. https:\/\/doi.org\/10.1007\/978-3-319-10575-8","DOI":"10.1007\/978-3-319-10575-8"},{"issue":"4","key":"10729_CR53","doi-asserted-by":"publisher","first-page":"626","DOI":"10.1145\/242223.242257","volume":"28","author":"EM Clarke","year":"1996","unstructured":"Clarke EM, Wing JM (1996) Formal methods: State of the art and future directions. ACM Comput Surv 28(4):626\u2013643. https:\/\/doi.org\/10.1145\/242223.242257","journal-title":"ACM Comput Surv"},{"issue":"1","key":"10729_CR54","doi-asserted-by":"publisher","first-page":"21","DOI":"10.1109\/TIT.1967.1053964","volume":"13","author":"T Cover","year":"1967","unstructured":"Cover T, Hart P (1967) Nearest neighbor pattern classification. IEEE Trans Inf Theory 13(1):21\u201327. https:\/\/doi.org\/10.1109\/TIT.1967.1053964","journal-title":"IEEE Trans Inf Theory"},{"key":"10729_CR55","doi-asserted-by":"publisher","unstructured":"Crouse M, Abdelaziz I, Makni B, Whitehead S, Cornelio C, Kapanipathi P, Srinivas K, Thost V, Witbrock M, Fokoue A (2021) A deep reinforcement learning approach to first-order logic theorem proving. In: Proceedings of the AAAI conference on artificial intelligence, vol. 35, pp 6279\u20136287. AAAI Press, Virtual Event. https:\/\/doi.org\/10.1609\/aaai.v35i7.16780","DOI":"10.1609\/aaai.v35i7.16780"},{"key":"10729_CR56","doi-asserted-by":"publisher","unstructured":"Dalla M, Visentin A, O\u2019Sullivan B (2021) Automated SAT problem feature extraction using convolutional autoencoders. In: 2021 IEEE 33rd International conference on tools with artificial intelligence (ICTAI), pp 232\u2013239. IEEE, Washington, DC, USA. https:\/\/doi.org\/10.1109\/ictai52525.2021.00039","DOI":"10.1109\/ictai52525.2021.00039"},{"key":"10729_CR57","unstructured":"Danisovszky M, Yang ZG, Kusper G (2020) Classification of SAT problem instances by machine learning methods. In: Kov\u00e1sznai G, Istv\u00e1n F, T\u00f3m\u00e1cs T (eds.) Proceedings of the 11th International Conference on Applied Informatics. CEUR Workshop Proceedings, vol. 2650, pp 94\u2013104. CEUR-WS.org, Eger, Hungary. https:\/\/ceur-ws.org\/Vol-2650\/paper11.pdf"},{"key":"10729_CR58","unstructured":"Dunkelau J, Baldus L (2021) Ranking model checking backends for automated selection via classification and regression learning. In: Monica DD, Pozzato GL, Scala E (eds) OVERLAY\u201921: Workshop on artificial intelligence and fOrmal VERification, Logic, Automata, and sYnthesis, 22nd September, 2021, Padova, Italy. CEUR Workshop Proceedings, vol 2987, pp 77\u201382. CEUR Workshop Proceedings, Padua, Italy. https:\/\/ceur-ws.org\/Vol-2987\/paper14.pdf"},{"key":"10729_CR59","doi-asserted-by":"publisher","unstructured":"Dunkelau J, Krings S, Schmidt J (2019) Automated backend selection for ProB using deep learning. In: Julia M,\u00a0Badger KYR (ed.) NASA Formal Methods Symposium. Lecture Notes in Computer Science, vol. 11460, pp 130\u2013147. Springer, Houston, TX, USA. https:\/\/doi.org\/10.1007\/978-3-030-20652-9_9","DOI":"10.1007\/978-3-030-20652-9_9"},{"key":"10729_CR60","doi-asserted-by":"publisher","unstructured":"Dunkelau J, Schmidt J, Leuschel M (2020) Analysing ProB\u2019s constraint solving backends. In: Alexander\u00a0Raschke FH Dominique\u00a0M\u00e9ry (ed.) Rigorous State-Based Methods: 7th International Conference, ABZ 2020. Lecture Notes in Computer Science, vol. 12071, pp 107\u2013123. Springer, Ulm, Germany. https:\/\/doi.org\/10.1007\/978-3-030-48077-6_8","DOI":"10.1007\/978-3-030-48077-6_8"},{"key":"10729_CR61","doi-asserted-by":"publisher","unstructured":"Dyba T, Dingsoyr T, Hanssen GK (2007) Applying systematic reviews to diverse study types: An experience report. In: First international symposium on empirical software engineering and measurement (ESEM 2007), pp 225\u2013234. IEEE, Madrid, Spain. https:\/\/doi.org\/10.1109\/ESEM.2007.59","DOI":"10.1109\/ESEM.2007.59"},{"key":"10729_CR62","doi-asserted-by":"publisher","unstructured":"Elahi M, Afolaranmi SO, Martinez Lastra JL, Perez Garcia JA (2023) A comprehensive literature review of the applications of AI techniques through the lifecycle of industrial equipment. Discover Artif Intell 3. https:\/\/doi.org\/10.1007\/s44163-023-00089-x","DOI":"10.1007\/s44163-023-00089-x"},{"key":"10729_CR63","doi-asserted-by":"publisher","unstructured":"England M (2018) Machine learning for mathematical software. In: Davenport JH, Kauers M, Labahn G, Urban J (eds.) Mathematical Software \u2013 ICMS 2018. Lecture Notes in Computer Science, vol. 10931, pp 165\u2013174. Springer, South Bend, IN, USA. https:\/\/doi.org\/10.1007\/978-3-319-96418-8_20","DOI":"10.1007\/978-3-319-96418-8_20"},{"issue":"2","key":"10729_CR64","doi-asserted-by":"publisher","first-page":"287","DOI":"10.1007\/s10817-020-09576-7","volume":"65","author":"M F\u00e4rber","year":"2020","unstructured":"F\u00e4rber M, Kaliszyk C, Urban J (2020) Machine learning guidance for connection tableaux. J Autom Reason 65(2):287\u2013320. https:\/\/doi.org\/10.1007\/s10817-020-09576-7","journal-title":"J Autom Reason"},{"key":"10729_CR65","unstructured":"Farooque M, Keni A (2023) A brief analogy of NNs and literal selection procedures within SAT solvers. In: International conference on life sciences, engineering and technology. International Society for Technology, Education, and Science (ISTES), Denver, CO, USA. https:\/\/scholarsphere.psu.edu\/resources\/d1c83077-8e2f-40e7-94fb-4026b828b7b9"},{"key":"10729_CR66","doi-asserted-by":"publisher","unstructured":"Ferreira D, Freitas A (2020) Premise selection in natural language mathematical texts. In: Jurafsky D, Chai J, Schluter N, Tetreault J (eds.) Proceedings of the 58th Annual Meeting of the Association for Computational Linguistics, pp 7365\u20137374. Association for Computational Linguistics, Virtual Event. https:\/\/doi.org\/10.18653\/v1\/2020.acl-main.657","DOI":"10.18653\/v1\/2020.acl-main.657"},{"key":"10729_CR67","unstructured":"Firoiu V, Aygun E, Anand A, Ahmed Z, Glorot X, Orseau L, Zhang L, Precup D, Mourad S (2021) Training a first-order theorem prover from synthetic data. In: 1st Mathematical reasoning in general artificial intelligence workshop, ICLR 2021. Math-AI Organizers, Virtual Event. https:\/\/mathai-iclr.github.io\/papers\/papers\/MATHAI_18_paper.pdf"},{"key":"10729_CR68","doi-asserted-by":"publisher","unstructured":"First E, Brun Y (2022) Diversity-driven automated formal verification. In: Proceedings of the 44th international conference on software engineering. ICSE \u201922, pp 749\u2013761. Association for Computing Machinery, Pittsburgh, PA, USA. https:\/\/doi.org\/10.1145\/3510003.3510138","DOI":"10.1145\/3510003.3510138"},{"key":"10729_CR69","doi-asserted-by":"publisher","unstructured":"First E, Brun Y, Guha A (2020) TacTok: Semantics-aware proof synthesis. Proceed ACM Program Languages 4(OOPSLA):1\u201331. https:\/\/doi.org\/10.1145\/3428299","DOI":"10.1145\/3428299"},{"key":"10729_CR70","doi-asserted-by":"publisher","unstructured":"Fournier T, Lallouet A, Cropsal T, Glorian G, Papadopoulos A, Petitet A, Perez G, Sekar S, Suijlen W (2022) A deep reinforcement learning heuristic for SAT based on antagonist graph neural networks. In: 2022 IEEE 34th International conference on tools with artificial intelligence (ICTAI), pp 1218\u20131222. IEEE, Macao, China. https:\/\/doi.org\/10.1109\/ICTAI56018.2022.00185","DOI":"10.1109\/ICTAI56018.2022.00185"},{"key":"10729_CR71","doi-asserted-by":"publisher","unstructured":"Framil M, Cabalar P, Santos J (2022) A MaxSAT solver based on\u00a0differential evolution (preliminary report). In: Marreiros G, Martins B, Paiva A, Ribeiro B, Sardinha A (eds.) Progress in Artificial Intelligence. Lecture Notes in Computer Science, vol. 13566, pp 676\u2013687. Springer, Lisbon, Portugal. https:\/\/doi.org\/10.1007\/978-3-031-16474-3_55","DOI":"10.1007\/978-3-031-16474-3_55"},{"issue":"2","key":"10729_CR72","doi-asserted-by":"publisher","first-page":"220","DOI":"10.3897\/jucs.2020.013","volume":"26","author":"H Fu","year":"2020","unstructured":"Fu H, Xu Y, Chen S, Liu J (2020) Improving WalkSAT for random 3-SAT problems. J Univ Comput Sci 26(2):220\u2013243. https:\/\/doi.org\/10.3897\/jucs.2020.013","journal-title":"J Univ Comput Sci"},{"key":"10729_CR73","doi-asserted-by":"publisher","unstructured":"Fuchs T, Bach J, Iser M (2023) Active learning for SAT solver benchmarking. In: Sankaranarayanan S, Sharygina N (eds.) Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 13993, pp. 407\u2013425. Springer, Paris, France. https:\/\/doi.org\/10.1007\/978-3-031-30823-9_21","DOI":"10.1007\/978-3-031-30823-9_21"},{"key":"10729_CR74","doi-asserted-by":"publisher","unstructured":"Fuggitti F, Chakraborti T (2023) NL2LTL\u2013a python package for converting natural language (NL) instructions to linear temporal logic (LTL) formulas. In: AAAI-23 Special Programs, IAAI-23, EAAI-23, Student Papers and Demonstrations, vol. 37. AAAI Press, Washington, DC, USA. https:\/\/doi.org\/10.1609\/aaai.v37i13.27068","DOI":"10.1609\/aaai.v37i13.27068"},{"key":"10729_CR75","unstructured":"Gallier JH (2015) Logic for Computer Science: Foundations of Automatic Theorem Proving, 2nd edn. Courier Dover Publications, USA. https:\/\/store.doverpublications.com\/products\/9780486780825"},{"key":"10729_CR76","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10703-023-00430-1","volume":"60","author":"V Ganesh","year":"2023","unstructured":"Ganesh V, Seshia SA, Jha S (2023) Machine learning and logic: a new frontier in artificial intelligence. Formal Methods Syst Design 60:1\u201326. https:\/\/doi.org\/10.1007\/s10703-023-00430-1","journal-title":"Formal Methods Syst Design"},{"key":"10729_CR77","doi-asserted-by":"publisher","unstructured":"Garz\u00f3n I, Mesejo P, Gir\u00e1ldez-Cru J (2022) On the performance of deep generative models of realistic SAT instances. In: Meel KS, Strichman O (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 236, pp 1\u201319. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Haifa, Israel. https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2022.3","DOI":"10.4230\/LIPIcs.SAT.2022.3"},{"key":"10729_CR78","doi-asserted-by":"publisher","unstructured":"Gauthier T (2020) Deep reinforcement learning for synthesizing functions in higher-order logic. In: Albert E, Kovacs L (eds) 3rd International conference on logic for programming, artificial intelligence and reasoning. EPiC Series in Computing, vol 73, pp 230\u2013248. EasyChair, Virtual Event. https:\/\/doi.org\/10.29007\/7jmg","DOI":"10.29007\/7jmg"},{"issue":"2","key":"10729_CR79","doi-asserted-by":"publisher","first-page":"257","DOI":"10.1007\/s10817-020-09580-x","volume":"65","author":"T Gauthier","year":"2020","unstructured":"Gauthier T, Kaliszyk C, Urban J, Kumar R, Norrish M (2020) TacticToe: Learning to prove with tactics. J Autom Reason 65(2):257\u2013286. https:\/\/doi.org\/10.1007\/s10817-020-09580-x","journal-title":"J Autom Reason"},{"key":"10729_CR80","doi-asserted-by":"publisher","unstructured":"Giacobbe M, Kroening D, Parsert J (2022) Neural termination analysis. In: Roychoudhury A, Cadar C, Kim M (eds) Proceedings of the 30th ACM joint european software engineering conference and symposium on the foundations of software engineering. ESEC\/FSE 2022, pp 633\u2013645. Association for Computing Machinery, Singapore, Singapore. https:\/\/doi.org\/10.1145\/3540250.3549120","DOI":"10.1145\/3540250.3549120"},{"key":"10729_CR81","unstructured":"Glorot X, Anand A, Aygun E, Mourad S, Kohli P, Precup D (2019) Learning representations of logical formulae using graph neural networks. In: Workshop on graph representation learning at 33rd neural information processing systems. Graph Representation Learning Committee, Vancouver, Canada. https:\/\/grlearning.github.io\/papers\/58.pdf"},{"key":"10729_CR82","doi-asserted-by":"publisher","unstructured":"Goertzel ZA (2020) Make E smart again (short paper). In: Peltier N, Sofronie-Stokkermans V (eds) Automated reasoning: 10th international joint conference, IJCAR 2020. Lecture Notes in Computer Science, vol 12167, pp 408\u2013415. Springer, Paris, France. https:\/\/doi.org\/10.1007\/978-3-030-51054-1_26","DOI":"10.1007\/978-3-030-51054-1_26"},{"key":"10729_CR83","doi-asserted-by":"publisher","unstructured":"Goertzel ZA, Chvalovsk\u00fd K, Jakub\u016fv J, Ol\u0161\u00e1k M, Urban J (2021) Fast and slow Enigmas and parental guidance. In: Konev B, Reger G (eds.) International Symposium on Frontiers of Combining Systems. Lecture Notes in Computer Science, vol. 12941, pp 173\u2013191. Springer, Birmingham, UK. https:\/\/doi.org\/10.1007\/978-3-030-86205-3_10","DOI":"10.1007\/978-3-030-86205-3_10"},{"key":"10729_CR84","doi-asserted-by":"publisher","unstructured":"Goertzel ZA, Jakub\u016fv J, Kaliszyk C, Ol\u0161\u00e1k M, Piepenbrock J, Urban J (2022) The Isabelle ENIGMA. In: Andronick J, Moura L (eds.) 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 237, pp 1\u201321. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Haifa, Israel. https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2022.16","DOI":"10.4230\/LIPIcs.ITP.2022.16"},{"key":"10729_CR85","doi-asserted-by":"publisher","unstructured":"Goertzel Z, Jakub\u016fv J, Urban J (2019) ENIGMAWatch: ProofWatch meets ENIGMA. In: Cerrito S, Popescu A (eds.) Automated Reasoning with Analytic Tableaux and Related Methods. Lecture Notes in Computer Science, vol. 11714, pp 374\u2013388. Springer, London, UK. https:\/\/doi.org\/10.1007\/978-3-030-29026-9_21","DOI":"10.1007\/978-3-030-29026-9_21"},{"key":"10729_CR86","unstructured":"Goertzel Z, Urban J (2019) Usefulness of lemmas via graph neural networks. In: 4th Conference on artificial intelligence and theorem proving. AITP Conference, Obergurgl, Austria. https:\/\/aitp-conference.org\/2019\/abstract\/AITP_2019_paper_32.pdf"},{"key":"10729_CR87","doi-asserted-by":"publisher","unstructured":"Goldberg EI, Prasad MR, Brayton RK (2001) Using SAT for combinational equivalence checking. In: Proceedings Design, Automation and Test in Europe. Conference and Exhibition 2001, pp. 114\u2013121. IEEE, Munich, Germany. https:\/\/doi.org\/10.1109\/DATE.2001.915010","DOI":"10.1109\/DATE.2001.915010"},{"key":"10729_CR88","unstructured":"Goodfellow I, Bengio Y, Courville A (2016) Deep Learning. MIT Press, Cambridge, MA. http:\/\/www.deeplearningbook.org"},{"key":"10729_CR89","doi-asserted-by":"publisher","unstructured":"Granmo O-C, Bouhmala N (2010) Using learning automata to enhance local-search based SAT solvers with learning capability. In: Zhang Y (ed.) Application of Machine Learning. IntechOpen, London, UK. https:\/\/doi.org\/10.5772\/8610","DOI":"10.5772\/8610"},{"key":"10729_CR90","doi-asserted-by":"publisher","unstructured":"Gross D, Jansen N, Junges S, P\u00e9rez GA (2022) COOL-MC: A comprehensive tool for reinforcement learning and model checking. In: Dong W, Talpin J-P (eds) International symposium on dependable software engineering: Theories, tools, and applications. lecture notes in computer science, vol 13649, pp 41\u201349. Springer, Beijing, China. https:\/\/doi.org\/10.1007\/978-3-031-21213-0_3","DOI":"10.1007\/978-3-031-21213-0_3"},{"key":"10729_CR91","doi-asserted-by":"publisher","first-page":"640","DOI":"10.1007\/s11633-022-1396-2","volume":"20","author":"W Guo","year":"2023","unstructured":"Guo W, Zhen H-L, Li X, Luo W, Yuan M, Jin Y, Yan J (2023) Machine learning methods in solving the boolean satisfiability problem. Mach Intell Res 20:640\u2013655. https:\/\/doi.org\/10.1007\/s11633-022-1396-2","journal-title":"Mach Intell Res"},{"key":"10729_CR92","doi-asserted-by":"publisher","unstructured":"Haltermann J, Wehrheim H (2022) Machine learning based invariant generation: A framework and reproducibility study. In: 2022 IEEE Conference on software testing, verification and validation (ICST), pp 12\u201323. IEEE, Valencia, Spain. https:\/\/doi.org\/10.1109\/ICST53961.2022.00012","DOI":"10.1109\/ICST53961.2022.00012"},{"key":"10729_CR93","unstructured":"Han JM (2020) Learning cubing heuristics for SAT from DRAT proofs. In: 5th Conference on artificial intelligence and theorem proving. AITP Conference, Aussois, France. https:\/\/aitp-conference.org\/2020\/abstract\/paper_23.pdf"},{"key":"10729_CR94","unstructured":"Han JM, Rute J, Wu Y, Ayers E, Polu S (2022) Proof artifact co-training for theorem proving with language models. In: International conference on learning representations. OpenReview.net, Virtual Event. https:\/\/openreview.net\/forum?id=rpxJc9j04U"},{"key":"10729_CR95","unstructured":"Han JM, Xu T, Polu S, Neelakantan A, Radford A (2021) Contrastive finetuning of generative language models for informal premise selection. In: 6th Conference on artificial intelligence and theorem proving. AITP Conference, Virtual Event. https:\/\/aitp-conference.org\/2021\/abstract\/paper_21.pdf"},{"key":"10729_CR96","doi-asserted-by":"publisher","unstructured":"He J, Bartocci E, Ni\u010dkovi\u0107 D, Isakovic H, Grosu R (2022) DeepSTL: From english requirements to signal temporal logic. In: Proceedings of the 44th international conference on software engineering. ICSE \u201922, pp 610\u2013622. Association for Computing Machinery, Pittsburgh, Pennsylvania. https:\/\/doi.org\/10.1145\/3510003.3510171","DOI":"10.1145\/3510003.3510171"},{"issue":"1","key":"10729_CR97","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1108\/dta-07-2018-0068","volume":"53","author":"C Hireche","year":"2019","unstructured":"Hireche C, Drias H (2019) Multidimensional appropriate clustering and DBSCAN for SAT solving. Data Technol Appl 53(1):85\u2013107. https:\/\/doi.org\/10.1108\/dta-07-2018-0068","journal-title":"Data Technol Appl"},{"key":"10729_CR98","doi-asserted-by":"publisher","unstructured":"Hireche C, Drias H, Moulai H (2020) Grid based clustering for satisfiability solving. Appl Soft Comput J 88:106069. https:\/\/doi.org\/10.1016\/j.asoc.2020.106069","DOI":"10.1016\/j.asoc.2020.106069"},{"key":"10729_CR99","unstructured":"Holden EK, Korovin K (2019) SMAC and XGBoost your theorem prover. In: 4th Conference on artificial intelligence and theorem proving, Obergurgl, Austria. https:\/\/aitp-conference.org\/2019\/abstract\/paper%2031.pdf"},{"key":"10729_CR100","doi-asserted-by":"publisher","unstructured":"Holden SB (2021) Machine learning for automated theorem proving: Learning to solve SAT and QSAT. Found Trends\u00aeMach Learn 14(6):807\u2013989. https:\/\/doi.org\/10.1561\/2200000081","DOI":"10.1561\/2200000081"},{"key":"10729_CR101","first-page":"481","volume-title":"Handbook of Satisfiability","author":"HH Hoos","year":"2021","unstructured":"Hoos HH, Hutter F, Leyton-Brown K (2021) Automated configuration and selection of SAT solvers. In: Biere A, Heule M, Maaren H, Walsh T (eds) Handbook of Satisfiability. IOS Press, Amsterdam, NL, pp 481\u2013507"},{"issue":"5","key":"10729_CR102","doi-asserted-by":"publisher","first-page":"1431","DOI":"10.1109\/TC.2022.3197956","volume":"75","author":"M Hu","year":"2022","unstructured":"Hu M, Zhang M, Mallet F, Fu X, Chen M (2022) Accelerating reinforcement learning-based CCSL specification synthesis using curiosity-driven exploration. IEEE Trans Comput 75(5):1431\u20131446. https:\/\/doi.org\/10.1109\/TC.2022.3197956","journal-title":"IEEE Trans Comput"},{"key":"10729_CR103","unstructured":"Huang D, Dhariwal P, Song D, Sutskever I (2019) GamePad: A learning environment for theorem proving. In: International conference on learning representations. OpenReview.net, New Orleans, LA, USA. https:\/\/openreview.net\/forum?id=r1xwKoR9Y7"},{"key":"10729_CR104","doi-asserted-by":"publisher","unstructured":"Huang J, Zhen H-L, Wang N, Mao H, Yuan M, Huang Y (2022) Neural fault analysis for SAT-based ATPG. In: 2022 IEEE International test conference (ITC), pp 36\u201345. IEEE, Anaheim, CA, USA. https:\/\/doi.org\/10.1109\/ITC50671.2022.00010","DOI":"10.1109\/ITC50671.2022.00010"},{"key":"10729_CR105","doi-asserted-by":"publisher","unstructured":"H\u016fla J, Moj\u017e\u00ed\u0161ek D, Janota M (2021) Graph neural networks for scheduling of SMT solvers. In: 2021 IEEE 33rd international conference on tools with artificial intelligence (ICTAI), pp 447\u2013451. IEEE, Washington, DC, USA.https:\/\/doi.org\/10.1109\/ICTAI52525.2021.00072","DOI":"10.1109\/ICTAI52525.2021.00072"},{"issue":"6377","key":"10729_CR106","doi-asserted-by":"publisher","first-page":"725","DOI":"10.1126\/science.359.6377.725","volume":"359","author":"M Hutson","year":"2018","unstructured":"Hutson M (2018) Artificial intelligence faces reproducibility crisis. Science 359(6377):725\u2013726. https:\/\/doi.org\/10.1126\/science.359.6377.725","journal-title":"Science"},{"key":"10729_CR107","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.artint.2013.10.003","volume":"206","author":"F Hutter","year":"2014","unstructured":"Hutter F, Xu L, Hoos HH, Leyton-Brown K (2014) Algorithm runtime prediction: Methods & evaluation. Artif Intell 206:79\u2013111. https:\/\/doi.org\/10.1016\/j.artint.2013.10.003","journal-title":"Artif Intell"},{"key":"10729_CR108","doi-asserted-by":"publisher","unstructured":"Hu G, Zhang W, Zhang H (2023) NeuroPDR: Integrating neural networks in the PDR algorithm for hardware model checking. In: 2023 ACM\/IEEE 5th workshop on machine learning for CAD (MLCAD). MLCAD, pp 1\u20136. IEEE, Snowbird, UT, USA. https:\/\/doi.org\/10.1109\/MLCAD58807.2023.10299875","DOI":"10.1109\/MLCAD58807.2023.10299875"},{"key":"10729_CR109","doi-asserted-by":"publisher","unstructured":"Jaeger M, Larsen KG, Tibo A (2020) From statistical model checking to run-time monitoring using a bayesian network approach. In: Deshmukh J, Ni\u010dkovi\u0107 D (eds) Runtime verification. Lecture notes in computer science, vol 12399, pp 517\u2013535. Springer, Los Angeles, CA, USA. https:\/\/doi.org\/10.1007\/978-3-030-60508-7_30","DOI":"10.1007\/978-3-030-60508-7_30"},{"key":"10729_CR110","doi-asserted-by":"publisher","unstructured":"Jakub\u016fv J, Chvalovsk\u00fd K, Ol\u0161\u00e1k M, Piotrowski B, Suda M, Urban J (2020) ENIGMA anonymous: Symbol-independent inference guiding machine (system description). In: Peltier N, Sofronie-Stokkermans V (eds.) Automated Reasoning. Lecture Notes in Computer Science, vol. 12167, pp 448\u2013463. Springer, Paris, France. https:\/\/doi.org\/10.1007\/978-3-030-51054-1_29","DOI":"10.1007\/978-3-030-51054-1_29"},{"key":"10729_CR111","unstructured":"Jakub\u016fv J, Janota M, Piotrowski B, Piepenbrock J, Reynolds A (2023) Selecting quantifiers for instantiation in SMT. In: Graham-Lengrand S, Preiner M (eds.) Proceedings of the 21st International Workshop on Satisfiability Modulo Theories (SMT 2023). CEUR Workshop Proceedings, vol. 3439. CEUR-WS.org, Rome, Italy. https:\/\/ceur-ws.org\/Vol-3429\/short10.pdf"},{"key":"10729_CR112","doi-asserted-by":"publisher","unstructured":"Jakubuv J, Urban J (2019) Hammering Mizar by learning clause guidance. In: Harrison J, O\u2019Leary J, Tolmach A (eds.) 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), vol. 141, pp 1\u20138. Schloss Dagstuhl\u2013Leibniz-Zentrum fuer Informatik, Portland, OR, USA. https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2019.34","DOI":"10.4230\/LIPIcs.ITP.2019.34"},{"key":"10729_CR113","doi-asserted-by":"publisher","unstructured":"Janota M, Piepenbrock J, Piotrowski B (2022) Towards learning quantifier instantiation in SMT. In: Meel KS, Strichman O (eds.) 25th International Conference on Theory and Applications of Satisfiability Testing (SAT 2022). Leibniz International Proceedings in Informatics (LIPIcs), vol. 236, pp 1\u201318. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Haifa, Israel. https:\/\/doi.org\/10.4230\/LIPIcs.SAT.2022.7","DOI":"10.4230\/LIPIcs.SAT.2022.7"},{"key":"10729_CR114","unstructured":"Jiang AQ, Li W, Han JM, Wu Y (2021) LISA: Language models of ISAbelle proofs. In: 6th Conference on artificial intelligence and theorem proving. AITP Conference, Assouis and online, France. https:\/\/aitp-conference.org\/2021\/abstract\/paper_17.pdf"},{"key":"10729_CR115","unstructured":"Jiang AQ, Li W, Tworkowski S, Czechowski K, Odrzyg\u00f3\u017ad\u017a T, Mi\u0142\u00a0o\u015b P, Wu Y, Jamnik M (2022) Thor: Wielding hammers to integrate language models and automated theorem provers. In: Koyejo S, Mohamed S, Agarwal A, Belgrave D, Cho K, Oh A (eds.) Advances in Neural Information Processing Systems 35 (NeurIPS 2022), vol. 35, pp 8360\u20138373. Curran Associates, Inc., New Orleans, LA, USA. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2022\/file\/377c25312668e48f2e531e2f2c422483-Paper-Conference.pdf"},{"key":"10729_CR116","doi-asserted-by":"publisher","unstructured":"Jiang X, Xie M, Ma L, Dong L, Li D (2023) International publication trends in the application of artificial intelligence in ophthalmology research: an updated bibliometric analysis. Ann Translational Med 11(5). https:\/\/doi.org\/10.21037\/atm-22-3773","DOI":"10.21037\/atm-22-3773"},{"key":"10729_CR117","doi-asserted-by":"publisher","unstructured":"Jordan MI (1997) Serial order: A parallel distributed processing approach. In: Donahoe JW, Dorsel VP (eds) Neural-Network Models of Cognition. Advances in Psychology, vol. 121, pp 471\u2013495. North-Holland, Amsterdam. https:\/\/doi.org\/10.1016\/S0166-4115(97)80111-2","DOI":"10.1016\/S0166-4115(97)80111-2"},{"key":"10729_CR118","doi-asserted-by":"publisher","first-page":"237","DOI":"10.1613\/jair.301","volume":"4","author":"LP Kaelbling","year":"1996","unstructured":"Kaelbling LP, Littman ML, Moore AW (1996) Reinforcement learning: A survey. J Artif Intell Res 4:237\u2013285. https:\/\/doi.org\/10.1613\/jair.301","journal-title":"J Artif Intell Res"},{"key":"10729_CR119","doi-asserted-by":"publisher","unstructured":"Kecman V (2005) Support Vector Machines \u2013 An Introduction. In: Wang, L. (ed.) Support Vector Machines: Theory and Applications, pp 1\u201347. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/10984697_1","DOI":"10.1007\/10984697_1"},{"key":"10729_CR120","doi-asserted-by":"publisher","first-page":"3713","DOI":"10.1007\/s11042-022-13428-4","volume":"82","author":"D Khurana","year":"2023","unstructured":"Khurana D, Koli A, Khatter K, Singh S (2023) Natural language processing: state of the art, current trends and challenges. Multimed Tools Appl 82:3713\u20133744. https:\/\/doi.org\/10.1007\/s11042-022-13428-4","journal-title":"Multimed Tools Appl"},{"issue":"3","key":"10729_CR121","doi-asserted-by":"publisher","first-page":"233","DOI":"10.1504\/IJAIP.2013.056447","volume":"5","author":"Y Kilani","year":"2013","unstructured":"Kilani Y, Bsoul M, Alsarhan A, Al-Khasawneh A (2013) A survey of the satisfiability-problems solving algorithms. Int J Adv Intell Paradigms 5(3):233\u2013256. https:\/\/doi.org\/10.1504\/IJAIP.2013.056447","journal-title":"Int J Adv Intell Paradigms"},{"key":"10729_CR122","doi-asserted-by":"publisher","unstructured":"Kitchenham BA, Budgen D, Brereton OP (2010) The value of mapping studies \u2013 a participant-observer case study. In: Proceedings of the 14th international conference on evaluation and assessment in software engineering. EASE\u201910, pp 25\u201333. BCS Learning & Development Ltd., Swindon, UK. https:\/\/doi.org\/10.14236\/ewic\/EASE2010.4","DOI":"10.14236\/ewic\/EASE2010.4"},{"key":"10729_CR123","unstructured":"Kitchenham B, Charters S et al (2007) Guidelines for performing systematic literature reviews in software engineering. Technical report, Keele University. https:\/\/legacyfileshare.elsevier.com\/promis_misc\/525444systematicreviewsguide.pdf"},{"key":"10729_CR124","doi-asserted-by":"publisher","unstructured":"Kobayashi N, Sekiyama T, Sato I, Unno H (2021) Toward neural-network-guided program synthesis and verification. In: Dr\u0103goi C, Mukherjee S, Namjoshi K (eds) Static analysis. Lecture notes in computer science, vol 12931, pp 236\u2013260. Springer, Chicago, IL, USA. https:\/\/doi.org\/10.1007\/978-3-030-88806-0_12","DOI":"10.1007\/978-3-030-88806-0_12"},{"issue":"7","key":"10729_CR125","doi-asserted-by":"publisher","first-page":"3771","DOI":"10.1109\/TSE.2023.3271065","volume":"49","author":"S Kommrusch","year":"2023","unstructured":"Kommrusch S, Monperrus M, Pouchet L-N (2023) Self-supervised learning to prove equivalence between straight-line programs via rewrite rules. IEEE Trans Softw Eng 49(7):3771\u20133792. https:\/\/doi.org\/10.1109\/TSE.2023.3271065","journal-title":"IEEE Trans Softw Eng"},{"key":"10729_CR126","doi-asserted-by":"publisher","unstructured":"Koscinski V, Gambardella C, Gerstner E, Zappavigna M, Cassetti J, Mirakhorli M (2021) A natural language processing technique for formalization of systems requirement specifications. In: Yue T, Mirakhorli M (eds) 2021 IEEE 29th international requirements engineering conference workshops (REW). REW, pp 350\u2013356. IEEE, Virtual Event. https:\/\/doi.org\/10.1109\/REW53955.2021.00062","DOI":"10.1109\/REW53955.2021.00062"},{"key":"10729_CR127","doi-asserted-by":"publisher","unstructured":"Kumar M, Kolb S, Teso S, De Raedt L (2023) Learning MAX-SAT from contextual examples for combinatorial optimisation. Artif Intell 314:103794. https:\/\/doi.org\/10.1016\/j.artint.2022.103794","DOI":"10.1016\/j.artint.2022.103794"},{"key":"10729_CR128","doi-asserted-by":"publisher","unstructured":"Kumazawa T, Takada K, Takimoto M, Kambayashi Y (2019) Ant colony optimization based model checking extended by smell-like pheromone with hop counts. Swarm Evolutionary Comput 44:511\u2013521. https:\/\/doi.org\/10.1016\/j.swevo.2018.06.002","DOI":"10.1016\/j.swevo.2018.06.002"},{"key":"10729_CR129","doi-asserted-by":"publisher","unstructured":"Kumazawa T, Takimoto M, Kambayashi Y (2020) A survey on the applications of swarm intelligence to software verification. In: Tan Y (ed.) Handbook of Research on Fireworks Algorithms and Swarm Intelligence, pp 376\u2013398. IGI Global, Hershey, PA. https:\/\/doi.org\/10.4018\/978-1-7998-1659-1.ch017","DOI":"10.4018\/978-1-7998-1659-1.ch017"},{"key":"10729_CR130","doi-asserted-by":"publisher","unstructured":"Kumazawa T, Takimoto M, Kambayashi Y (2021) Exploration strategies for model checking with ant colony OptimizationQD. In: Nguyen NT, Iliadis L, Maglogiannis I, Trawi\u0144ski B (eds) Computational collective intelligence, pp 264\u2013276. Springer, Rhodes, Greece. https:\/\/doi.org\/10.1007\/978-3-030-88081-1_20","DOI":"10.1007\/978-3-030-88081-1_20"},{"key":"10729_CR131","doi-asserted-by":"publisher","unstructured":"Kumazawa T, Takimoto M, Kambayashi Y (2022) A safety checking algorithm with multi-swarm particle swarm optimization. In: Fieldsend JE (ed) Proceedings of the genetic and evolutionary computation conference companion. GECCO \u201922, pp 786\u2013789. Association for Computing Machinery, Boston, MA, USA. https:\/\/doi.org\/10.1145\/3520304.3528918","DOI":"10.1145\/3520304.3528918"},{"key":"10729_CR132","doi-asserted-by":"publisher","unstructured":"Kumazawa T, Takimoto M, Kodama Y, Kambayashi Y (2023) Enhancing safety checking coverage with multi-swarm particle swarm optimization. In: Mathieu P, Dignum F, Novais P, Prieta F (eds) Advances in practical applications of agents, multi-agent systems, and cognitive mimetics. The PAAMS Collection. Lecture Notes in Computer Science, vol 13955, pp 137\u2013148. Springer, Guimar\u00e3es, Portugal. https:\/\/doi.org\/10.1007\/978-3-031-37616-0_12","DOI":"10.1007\/978-3-031-37616-0_12"},{"key":"10729_CR133","unstructured":"Kurin V, Godil S, Whiteson S, Catanzaro B (2020) Can Q-learning with graph networks learn a generalizable branching heuristic for a SAT solver? In: Larochelle H, Ranzato M, Hadsell R, Balcan MF, Lin H (eds.) Advances in Neural Information Processing Systems, vol. 33, pp 9608\u20139621. Curran Associates, Inc., Virtual Event. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2020\/file\/6d70cb65d15211726dcce4c0e971e21c-Paper.pdf"},{"key":"10729_CR134","unstructured":"Lample G, Lacroix T, Lachaux M-A, Rodriguez A, Hayat A, Lavril T, Ebner G, Martinet X (2022) HyperTree proof search for neural theorem proving. In: Koyejo S, Mohamed S, Agarwal A, Belgrave D, Cho K, Oh A (eds) Advances in neural information processing systems 35 (NeurIPS 2022), vol 35, pp 26337\u201326349. Curran Associates, Inc., New Orleans, LA, USA. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2022\/file\/a8901c5e85fb8e1823bbf0f755053672-Paper-Conference.pdf"},{"issue":"2","key":"10729_CR135","doi-asserted-by":"publisher","first-page":"193","DOI":"10.3233\/idt-180036","volume":"13","author":"M Lassouaoui","year":"2019","unstructured":"Lassouaoui M, Boughaci D, Benhamou B (2019) A multilevel synergy Thompson sampling hyper-heuristic for solving Max-SAT. Intell Decision Technol 13(2):193\u2013210. https:\/\/doi.org\/10.3233\/idt-180036","journal-title":"Intell Decision Technol"},{"key":"10729_CR136","unstructured":"Laurent J, Platzer A (2021) Designing a theorem prover for reinforcement learning and neural guidance. In: 6th Conference on artificial intelligence and theorem proving. AITP Conference, Aussois and online, France. https:\/\/aitp-conference.org\/2021\/abstract\/paper_8.pdf"},{"key":"10729_CR137","unstructured":"Laurent J, Platzer A (2022) Learning to find proofs and theorems by learning to refine search strategies: The case of loop invariant synthesis. In: Koyejo S, Mohamed S, Agarwal A, Belgrave D, Cho K, Oh A (eds) Advances in neural information processing systems, vol 35, pp 4843\u20134856. Curran Associates, Inc., New Orleans, LA, USA. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2022\/file\/1f14ac136d55c34a18a04ce3db083599-Paper-Conference.pdf"},{"key":"10729_CR138","doi-asserted-by":"publisher","unstructured":"LeCun Y, Kavukcuoglu K, Farabet C (2010) Convolutional networks and applications in vision. In: Proceedings of 2010 IEEE International symposium on circuits and systems, pp 253\u2013256. IEEE, Paris, France. https:\/\/doi.org\/10.1109\/ISCAS.2010.5537907","DOI":"10.1109\/ISCAS.2010.5537907"},{"key":"10729_CR139","unstructured":"Lederman G, Rabe M, Seshia S, Lee EA (2020) Learning heuristics for quantified Boolean formulas through reinforcement learning. In: International conference on learning representations. OpenReview.net, Addis Ababa, Ethiopia. https:\/\/openreview.net\/forum?id=BJluxREKDB"},{"key":"10729_CR140","doi-asserted-by":"publisher","unstructured":"Leeson W, Dwyer MB, Filieri A (2023) Sibyl: Improving software engineering tools with SMT selection. In: 2023 IEEE\/ACM 45th International conference on software engineering (ICSE), pp 2185\u20132197. IEEE, Melbourne, Australia. https:\/\/doi.org\/10.1109\/ICSE48619.2023.00184","DOI":"10.1109\/ICSE48619.2023.00184"},{"key":"10729_CR141","doi-asserted-by":"publisher","unstructured":"Leventi-Peetz AM, Peetz J-V, Rohde M (2020) ML supported predictions for SAT solvers performance. In: Arai K, Bhatia R, Kapoor S (eds.) Proceedings of the Future Technologies Conference (FTC) 2019. Advances in Intelligent Systems and Computing, vol. 1069, pp 64\u201378. Springer, San Francisco, CA, USA. https:\/\/doi.org\/10.1007\/978-3-030-32520-6_7","DOI":"10.1007\/978-3-030-32520-6_7"},{"key":"10729_CR142","unstructured":"Li Z, Si X (2022) NSNet: A general neural probabilistic framework for satisfiability problems. In: Koyejo S, Mohamed S, Agarwal A, Belgrave D, Cho K, Oh A (eds.) Advances in Neural Information Processing Systems 35 (NeurIPS 2022), vol. 35, pp 25573\u201325585. Curran Associates, Inc., New Orleans, LA, USA. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2022\/file\/a40462acc6959034c6aa6dfb8e696415-Paper-Conference.pdf"},{"key":"10729_CR143","doi-asserted-by":"publisher","unstructured":"Liu J, Chen Y, Tan B, Dillig I, Feng Y (2023) Learning contract invariants using reinforcement learning. In: Proceedings of the 37th IEEE\/ACM international conference on automated software engineering. ASE \u201922. Association for computing machinery, Rochester, MI, USA. https:\/\/doi.org\/10.1145\/3551349.3556962","DOI":"10.1145\/3551349.3556962"},{"key":"10729_CR144","unstructured":"Liu Q, Wu Z, Wang Z, Sutcliffe G (2020) Evaluation of axiom selection techniques. In: Boris\u00a0Konev AS Claudia\u00a0Schon (ed.) PAAR+SC-Square 2020 Practical Aspects of Automated Reasoning and Satisfiability Checking and Symbolic Computation Workshop 2020. CEUR Workshop Proceedings, vol. 2752, pp 63\u201375. CEUR-WS.org, Virtual Event. https:\/\/ceur-ws.org\/Vol-2752\/paper5.pdf"},{"key":"10729_CR145","doi-asserted-by":"publisher","unstructured":"Liu Q, Xu Y, He X (2022) Attention recurrent cross-graph neural network for selecting premises. Int J Mach Learn Cybernet 13:1301\u20131315. https:\/\/doi.org\/10.1007\/s13042-021-01448-9","DOI":"10.1007\/s13042-021-01448-9"},{"key":"10729_CR146","doi-asserted-by":"publisher","unstructured":"Lorenz J-H, Nickerl J (2020) The potential of restarts for ProbSAT. In: Moreno-D\u00edaz R, Pichler F, Quesada-Arencibia A (eds.) Computer Aided Systems Theory \u2013 EUROCAST 2019. Lecture Notes in Computer Science, vol. 12013, pp 352\u2013360. Springer, Las Palmas de Gran Canaria, Spain. https:\/\/doi.org\/10.1007\/978-3-030-45093-9_43","DOI":"10.1007\/978-3-030-45093-9_43"},{"key":"10729_CR147","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1080\/23270012.2019.1570365","volume":"6","author":"Y Lu","year":"2019","unstructured":"Lu Y (2019) Artificial intelligence: a survey on evolution, models, applications and future trends. J Manag Anal 6:1\u201329. https:\/\/doi.org\/10.1080\/23270012.2019.1570365","journal-title":"J Manag Anal"},{"key":"10729_CR148","doi-asserted-by":"publisher","unstructured":"Luo W, Wan H, Du J, Li X, Fu Y, Ye R, Zhang D (2022) Teaching LTLf satisfiability checking to neural networks. In: Raedt LD (ed) Proceedings of the thirty-first international joint conference on artificial intelligence (IJCAI-22), pp 3292\u20133298. International Joint Conferences on Artificial Intelligence Organization, Vienna, Austria. https:\/\/doi.org\/10.24963\/ijcai.2022\/457","DOI":"10.24963\/ijcai.2022\/457"},{"key":"10729_CR149","doi-asserted-by":"publisher","unstructured":"Luo W, Wan H, Zhang D, Du J, Su H (2023) Checking LTL satisfiability via end-to-end learning. In: Proceedings of the 37th IEEE\/ACM international conference on automated software engineering. ASE \u201922. Association for Computing Machinery, Rochester, MI, USA. https:\/\/doi.org\/10.1145\/3551349.3561163","DOI":"10.1145\/3551349.3561163"},{"key":"10729_CR150","doi-asserted-by":"publisher","unstructured":"Ma Y, Cao Z, Liu Y (2019) Genetic algorithm-based assume-guarantee reasoning for stochastic model checking. In: Song Y, Acharya S, Nguyen N (eds) IEEE\/ACIS 17th International conference on software engineering research, mangement and applications (SERA). SERA, pp 124\u2013127. IEEE, Honolulu, Hawaii, USA. https:\/\/doi.org\/10.1109\/SERA.2019.8886798","DOI":"10.1109\/SERA.2019.8886798"},{"key":"10729_CR151","doi-asserted-by":"publisher","unstructured":"Mangla C, Holden SB, Paulson LC (2022) Bayesian ranking for\u00a0strategy scheduling in\u00a0automated theorem provers. In: Blanchette J, Kov\u00e1cs L, Pattinson D (eds.) International Joint Conference on Automated Reasoning. Lecture Notes in Computer Science, vol. 13385, pp 559\u2013577. Springer, Haifa, Israel. https:\/\/doi.org\/10.1007\/978-3-031-10769-6_33","DOI":"10.1007\/978-3-031-10769-6_33"},{"issue":"3","key":"10729_CR152","doi-asserted-by":"publisher","first-page":"035032","DOI":"10.1088\/2632-2153\/ac0496","volume":"2","author":"R Marino","year":"2021","unstructured":"Marino R (2021) Learning from survey propagation: a neural network for MAX-E-3-SAT. Mach Learn Sci Technol 2(3):035032. https:\/\/doi.org\/10.1088\/2632-2153\/ac0496","journal-title":"Mach Learn Sci Technol"},{"key":"10729_CR153","unstructured":"Mitchell M (1998) An Introduction to Genetic Algorithms. MIT press, Cambridge, MA. https:\/\/direct.mit.edu\/books\/monograph\/4675\/An-Introduction-to-Genetic-Algorithms"},{"key":"10729_CR154","unstructured":"Mitchell TM (1997) Machine Learning. McGraw-Hill Professional, New York, NY, USA. https:\/\/www.cs.cmu.edu\/~tom\/mlbook.html"},{"key":"10729_CR155","unstructured":"Montgomery DC, Peck EA, Vining GG (2021) Introduction to Linear Regression Analysis, 6th edn. Wiley series in probability and statistics. John Wiley & Sons, New Jersey. https:\/\/www.wiley-vch.de\/en\/areas-interest\/mathematics-statistics\/statistics-16st\/regression-analysis-16st4\/introduction-to-linear-regression-analysis-978-1-119-57872-7"},{"key":"10729_CR156","unstructured":"Morris M, Minervini P, Blunsom P (2022) Learning proof path selection policies in neural theorem proving. In: Garcez EJ-R (ed.) Proceedings of the 16th International Workshop on Neural-Symbolic Learning and Reasoning (NeSy). CEUR Workshop Proceedings, vol. 3212. CEUR-WS.org, Siena, Italy. https:\/\/ceur-ws.org\/Vol-3212\/paper5.pdf"},{"key":"10729_CR157","doi-asserted-by":"publisher","unstructured":"Mo G, Xiong Y, Huang W, Ma L (2020) Automated theorem proving via interacting with proof assistants by dynamic strategies. In: Guerrero J (ed) 2020 6th International conference on big data computing and communications (BIGCOM), pp 71\u201375. IEEE, Deqing, China. https:\/\/doi.org\/10.1109\/bigcom51056.2020.00016","DOI":"10.1109\/bigcom51056.2020.00016"},{"key":"10729_CR158","doi-asserted-by":"publisher","unstructured":"Nagashima Y (2019) Towards evolutionary theorem proving for isabelle\/HOL. In: L\u00f3pez-Ib\u00e1\u00f1ez M (ed.) Proceedings of the Genetic and Evolutionary Computation Conference Companion. GECCO \u201919, pp 419\u2013420. Association for Computing Machinery, Prague, Czech Republic. https:\/\/doi.org\/10.1145\/3319619.3321921","DOI":"10.1145\/3319619.3321921"},{"key":"10729_CR159","doi-asserted-by":"publisher","unstructured":"Nagashima Y (2020) Simple dataset for proof method recommendation in Isabelle\/HOL. In: Benzm\u00fcller C, Miller B (eds) Intelligent computer mathematics. Lecture notes in computer science, vol 12236, pp 297\u2013302. Springer, Bertinoro, Italy. https:\/\/doi.org\/10.1007\/978-3-030-53518-6_21","DOI":"10.1007\/978-3-030-53518-6_21"},{"key":"10729_CR160","doi-asserted-by":"publisher","unstructured":"Nawaz MS, Fournier-Viger P, Zhang J (2020) Proof learning in PVS with utility pattern mining. IEEE Access 8:119806\u2013119818. https:\/\/doi.org\/10.1109\/ACCESS.2020.3004199","DOI":"10.1109\/ACCESS.2020.3004199"},{"key":"10729_CR161","doi-asserted-by":"publisher","unstructured":"Nawaz MS, Nawaz MZ, Hasan O, Fournier-Viger P, Sun M (2021) An evolutionary\/heuristic-based proof searching framework for interactive theorem prover. Appl Soft Comput 104:107200. https:\/\/doi.org\/10.1016\/j.asoc.2021.107200","DOI":"10.1016\/j.asoc.2021.107200"},{"key":"10729_CR162","doi-asserted-by":"publisher","unstructured":"Nawaz MS, Nawaz MZ, Hasan O, Fournier-Viger P, Sun M (2021) Proof searching and prediction in HOL4 with evolutionary\/heuristic and deep learning techniques. Appl Intell 51:1580\u20131601. https:\/\/doi.org\/10.1007\/s10489-020-01837-7","DOI":"10.1007\/s10489-020-01837-7"},{"key":"10729_CR163","doi-asserted-by":"publisher","unstructured":"Nawaz MS, Sun M, Fournier-Viger P (2019) Proof guidance in PVS with sequential pattern mining. In: Hojjat H, Massink M (eds) International conference on fundamentals of software engineering. Lecture notes in computer science, vol 11761, pp 45\u201360. Springer, Tehran, Iran. https:\/\/doi.org\/10.1007\/978-3-030-31517-7_4","DOI":"10.1007\/978-3-030-31517-7_4"},{"key":"10729_CR164","doi-asserted-by":"publisher","unstructured":"Nayak A, Timmapathini HP, Murali V, Ponnalagu K, Venkoparao VG, Post A (2022) Req2Spec: Transforming software requirements into formal specifications using natural language processing. In: Gervasi A Vincenzoand\u00a0Vogelsang (ed) Requirements Engineering: Foundation for Software Quality. Lecture Notes in Computer Science, vol 13216, pp 87\u201395. Springer, Birmingham, UK. https:\/\/doi.org\/10.1007\/978-3-030-98464-9_8","DOI":"10.1007\/978-3-030-98464-9_8"},{"key":"10729_CR165","doi-asserted-by":"publisher","unstructured":"Nejati S, Le\u00a0Frioux L, Ganesh V (2020) A machine learning based splitting heuristic for divide-and-conquer solvers. In: Simonis H (ed.) Principles and Practice of Constraint Programming. Lecture Notes in Computer Science, vol. 12333, pp 899\u2013916. Springer, Louvain-la-Neuve, Belgium. https:\/\/doi.org\/10.1007\/978-3-030-58475-7_52","DOI":"10.1007\/978-3-030-58475-7_52"},{"key":"10729_CR166","doi-asserted-by":"publisher","unstructured":"Nie P, Palmskog K, Li JJ, Gligoric M (2020) Deep generation of Coq lemma names using elaborated terms. In: Peltier N, Sofronie-Stokkermans V (eds) International joint conference on automated reasoning. Lecture notes in computer science, vol 12167, pp 97\u2013118. Springer, Paris, France. https:\/\/doi.org\/10.1007\/978-3-030-51054-1_6","DOI":"10.1007\/978-3-030-51054-1_6"},{"key":"10729_CR167","doi-asserted-by":"publisher","unstructured":"Nikoli\u0107 M, Marinkovi\u0107 V, Kov\u00e1cs Z, Jani\u010di\u0107 P (2019) Portfolio theorem proving and prover runtime prediction for geometry. Ann Math Artif Intell 85:119\u2013146. https:\/\/doi.org\/10.1007\/s10472-018-9598-6","DOI":"10.1007\/s10472-018-9598-6"},{"key":"10729_CR168","doi-asserted-by":"publisher","unstructured":"Nurcahyadi T, Blum C, Many\u00e0 F (2022) Negative learning ant colony optimization for MaxSAT. Int J Computat Intell Syst 15(1). https:\/\/doi.org\/10.1007\/s44196-022-00120-6","DOI":"10.1007\/s44196-022-00120-6"},{"key":"10729_CR169","doi-asserted-by":"publisher","unstructured":"Ols\u00e1k M, Kaliszyk C, Urban J (2020) Property invariant embedding for automated reasoning. In: De Giacomo G, Catala A, Dilkina B, Milano M, Barro S, Bugar\u00edn A, Lang J (eds.) 24th European Conference on Artificial Intelligence. Fronties in Artificial Intelligence and Applications, vol. 325, pp 1395\u20131402. Santiago de Compostela, Spain. https:\/\/doi.org\/10.3233\/FAIA200244. https:\/\/ebooks.iospress.nl\/publication\/55039","DOI":"10.3233\/FAIA200244"},{"key":"10729_CR170","doi-asserted-by":"publisher","unstructured":"Ozolins E, Freivalds K, Draguns A, Gaile E, Zakovskis R, Kozlovics S (2022) Goal-aware neural SAT solver. In: 2022 International Joint Conference on Neural Networks (IJCNN), pp 1\u20138. IEEE, Padua, Italy. https:\/\/doi.org\/10.1109\/IJCNN55064.2022.9892733","DOI":"10.1109\/IJCNN55064.2022.9892733"},{"key":"10729_CR171","unstructured":"Palermo J, Ye J, Han JM (2022) Synthetic proof term data augmentation for theorem proving with language models. In: 7th Conference on artificial intelligence and theorem proving. AITP Conference, Aussois, France. https:\/\/aitp-conference.org\/2022\/abstract\/AITP_2022_paper_5.pdf"},{"key":"10729_CR172","doi-asserted-by":"publisher","unstructured":"Paliwal A, Loos S, Rabe M, Bansal K, Szegedy C (2020) Graph representations for higher-order logic and theorem proving. In: Proceedings of the AAAI conference on artificial intelligence, vol 34, pp 2967\u20132974. AAAI Press, New York, NY, USA. https:\/\/doi.org\/10.1609\/aaai.v34i03.5689","DOI":"10.1609\/aaai.v34i03.5689"},{"key":"10729_CR173","doi-asserted-by":"publisher","unstructured":"Pan Z, Mishra P (2022) A survey on hardware vulnerability analysis using machine learning. IEEE Access 10:49508\u201349527. https:\/\/doi.org\/10.1109\/ACCESS.2022.3173287","DOI":"10.1109\/ACCESS.2022.3173287"},{"key":"10729_CR174","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.infsof.2015.03.007","volume":"64","author":"K Petersen","year":"2015","unstructured":"Petersen K, Vakkalanka S, Kuzniarz L (2015) Guidelines for conducting systematic mapping studies in software engineering: An update. Inf Softw Technol 64:1\u201318. https:\/\/doi.org\/10.1016\/j.infsof.2015.03.007","journal-title":"Inf Softw Technol"},{"key":"10729_CR175","doi-asserted-by":"publisher","unstructured":"Piepenbrock J, Heskes T, Janota M, Urban J (2021) Learning equational theorem proving. In: 6th Conference on artificial intelligence and theorem proving. AITP Conference, Aussois, France. https:\/\/doi.org\/10.48550\/ARXIV.2102.05547. https:\/\/aitpconference.org\/2021\/abstract\/paper_20.pdf","DOI":"10.48550\/ARXIV.2102.05547"},{"key":"10729_CR176","doi-asserted-by":"publisher","unstructured":"Piepenbrock J, Heskes T, Janota M, Urban J (2022) Guiding an automated theorem prover with neural rewriting. In: Blanchette J, Kov\u00e1cs L, Pattinson D (eds) International joint conference on automated reasoning. Lecture notes in computer science, vol 13385, pp 597\u2013617. Springer, Haifa, Israel. https:\/\/doi.org\/10.1007\/978-3-031-10769-6","DOI":"10.1007\/978-3-031-10769-6"},{"key":"10729_CR177","doi-asserted-by":"publisher","unstructured":"Pimpalkhare N (2021) Dynamic algorithm selection for SMT. In: Proceedings of the 35th IEEE\/ACM international conference on automated software engineering. ASE \u201920, pp 1376\u20131378. Association for Computing Machinery, Virtual Event.https:\/\/doi.org\/10.1145\/3324884.3418922","DOI":"10.1145\/3324884.3418922"},{"key":"10729_CR178","doi-asserted-by":"publisher","unstructured":"Pimpalkhare N, Mora F, Polgreen E, Seshia SA (2021) MedleySolver: Online SMT algorithm selection. In: Chu-Min\u00a0Li FM (ed.) Theory and Applications of Satisfiability Testing \u2014 SAT 2021. Lecture Notes in Computer Science, vol. 12831, pp 453\u2013470. Springer, Barcelona, Spain. https:\/\/doi.org\/10.1007\/978-3-030-80223-3_31","DOI":"10.1007\/978-3-030-80223-3_31"},{"key":"10729_CR179","doi-asserted-by":"publisher","unstructured":"Piotrowski B, Urban J (2020) Guiding inferences in connection tableau by recurrent neural networks. In: Benzm\u00fcller C, Miller B (eds) Intelligent computer mathematics. lecture notes in computer science, vol 12236, pp 309\u2013314. Springer, Bertinoro, Italy. https:\/\/doi.org\/10.1007\/978-3-030-53518-6_23","DOI":"10.1007\/978-3-030-53518-6_23"},{"key":"10729_CR180","doi-asserted-by":"publisher","unstructured":"Piotrowski B, Urban J (2020) Stateful premise selection by recurrent neural networks. In: Albert E, Kovacs L (eds.) 23rd International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR-23). EPiC Series in Computing, vol. 73, pp 409\u2013422. EasyChair, Virtual Event. https:\/\/doi.org\/10.29007\/j5hd","DOI":"10.29007\/j5hd"},{"issue":"1","key":"10729_CR181","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1007\/s11219-020-09542-x","volume":"30","author":"E Pira","year":"2022","unstructured":"Pira E (2022) Using knowledge discovery to propose a two-phase model checking for safety analysis of graph transformations. Softw Qual J 30(1):37\u201364. https:\/\/doi.org\/10.1007\/s11219-020-09542-x","journal-title":"Softw Qual J"},{"issue":"2251","key":"10729_CR182","doi-asserted-by":"publisher","first-page":"20220044","DOI":"10.1098\/rsta.2022.0044","volume":"381","author":"G Poesia","year":"2023","unstructured":"Poesia G, Goodman ND (2023) Peano: learning formal mathematical reasoning. Philosophical Trans Royal Soc Math Phys Eng Sci 381(2251):20220044. https:\/\/doi.org\/10.1098\/rsta.2022.0044","journal-title":"Philosophical Trans Royal Soc Math Phys Eng Sci"},{"key":"10729_CR183","unstructured":"Poesia G, Dong W, Goodman N (2021) Contrastive reinforcement learning of symbolic reasoning domains. In: Ranzato M, Beygelzimer A, Dauphin Y, Liang PS, Vaughan JW (eds) Advances in neural information processing systems, vol 34, pp 15946\u201315956. Curran Associates, Inc., Virtual Event. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2021\/file\/859555c74e9afd45ab771c615c1e49a6-Paper.pdf"},{"key":"10729_CR184","doi-asserted-by":"publisher","first-page":"91","DOI":"10.1007\/s10844-021-00666-5","volume":"58","author":"A Popescu","year":"2022","unstructured":"Popescu A, Polat-Erdeniz S, Felfernig A, Uta M, Atas M, Le V-M, Pilsl K, Enzelsberger M, Tran TNT (2022) An overview of machine learning techniques in constraint solving. J Intell Inf Syst 58:91\u2013118. https:\/\/doi.org\/10.1007\/s10844-021-00666-5","journal-title":"J Intell Inf Syst"},{"key":"10729_CR185","doi-asserted-by":"publisher","unstructured":"Puccetti A, De\u00a0Chalendar G, Gibello P-Y (2021) Combining formal and machine learning techniques for the generation of JML specifications. In: Cok DR (ed) FTfJP \u201921: Proceedings of the 23rd ACM international workshop on formal techniques for java-like programs. FTfJP, pp 59\u201364. Association for Computing Machinery, Virtual Event. https:\/\/doi.org\/10.1145\/3464971.3468425","DOI":"10.1145\/3464971.3468425"},{"issue":"8","key":"10729_CR186","doi-asserted-by":"publisher","first-page":"2057","DOI":"10.1093\/logcom\/exab006","volume":"31","author":"S Purga\u0141","year":"2021","unstructured":"Purga\u0141 S, Parsert J, Kaliszyk C (2021) A study of continuous vector representations for theorem proving. J Log Comput 31(8):2057\u20132083. https:\/\/doi.org\/10.1093\/logcom\/exab006","journal-title":"J Log Comput"},{"key":"10729_CR187","doi-asserted-by":"publisher","unstructured":"Qian H (2021) Research on automation strategy of Coq. In: Sun X, Zhang X, Xia Z, Bertino E (eds) Advances in artificial intelligence and security. Communications in computer and information science, vol 1423, pp 656\u2013665. Springer, Dublin, Ireland. https:\/\/doi.org\/10.1007\/978-3-030-78618-2_54","DOI":"10.1007\/978-3-030-78618-2_54"},{"key":"10729_CR188","doi-asserted-by":"publisher","unstructured":"Rafe V, Darghayedi M, Pira E (2019) MS-ACO: a multi-stage ant colony optimization to refute complex software systems specified through graph transformation. Soft Comput 23:4531\u20134556. https:\/\/doi.org\/10.1007\/s00500-018-3444-y","DOI":"10.1007\/s00500-018-3444-y"},{"key":"10729_CR189","doi-asserted-by":"publisher","unstructured":"Rawson M, Reger G (2019) A neurally-guided, parallel theorem prover. In: Herzig A, Popescu A (eds) Frontiers of combining systems: 12th international symposium, FroCoS 2019. Lecture notes in computer science, vol 11715, pp 40\u201356. Springer, London, UK. https:\/\/doi.org\/10.1007\/978-3-030-29007-8_3","DOI":"10.1007\/978-3-030-29007-8_3"},{"key":"10729_CR190","doi-asserted-by":"publisher","unstructured":"Rawson M, Reger G (2021) lazyCoP: Lazy paramodulation meets neurally guided search. In: Das A, Negri S (eds) Automated reasoning with analytic tableaux and related methods. Lecture notes in computer science, vol 12842, pp 187\u2013199. Springer, Birmingham, UK. https:\/\/doi.org\/10.1007\/978-3-030-86059-2_11","DOI":"10.1007\/978-3-030-86059-2_11"},{"key":"10729_CR191","doi-asserted-by":"publisher","unstructured":"Reichel T, Henderson RW, Touchet A, Gardner A, Ringer T (2023) Proof repair infrastructure for supervised models: Building a large proof repair dataset. In: Naumowicz A, Thiemann R (eds) 14th International conference on interactive theorem proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), vol 268, pp 1\u201320. Schloss Dagstuhl \u2013 Leibniz-Zentrum f\u00fcr Informatik, Bialystok, Poland. https:\/\/doi.org\/10.4230\/LIPIcs.ITP.2023.26","DOI":"10.4230\/LIPIcs.ITP.2023.26"},{"issue":"1","key":"10729_CR192","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1007\/s10515-020-00270-x","volume":"27","author":"C Richter","year":"2020","unstructured":"Richter C, H\u00fcllermeier E, Jakobs M-C, Wehrheim H (2020) Algorithm selection for software validation based on graph kernels. Autom Softw Eng 27(1):153\u2013186. https:\/\/doi.org\/10.1007\/s10515-020-00270-x","journal-title":"Autom Softw Eng"},{"key":"10729_CR193","doi-asserted-by":"publisher","unstructured":"Richter C, Wehrheim H (2020) Attend and represent: a novel view on algorithm selection for software verification. In: Proceedings of the 35th IEEE\/ACM international conference on automated software engineering. Association for computing machinery, virtual event. https:\/\/doi.org\/10.1145\/3324884.3416633","DOI":"10.1145\/3324884.3416633"},{"key":"10729_CR194","volume-title":"Principles of Neurodynamics: Perceptrons and the Theory of Brain Mechanisms","author":"F Rosenblatt","year":"1962","unstructured":"Rosenblatt F (1962) Principles of Neurodynamics: Perceptrons and the Theory of Brain Mechanisms. Spartan Books, Washington, DC"},{"key":"10729_CR195","doi-asserted-by":"publisher","unstructured":"Sadeg S, Hamdad L, Kada O, Benatchba K, Habbas Z (2021) Meta-learning to select the best metaheuristic for the MaxSAT problem. In: Chikhi S, Amine A, Chaoui A, Saidouni DE, Kholladi MK (eds.) International Symposium on Modelling and Implementation of Complex Systems. Lecture Notes in Networks and Systems, vol. 156, pp 122\u2013135. Springer, Batna, Algeria. https:\/\/doi.org\/10.1007\/978-3-030-58861-8_9","DOI":"10.1007\/978-3-030-58861-8_9"},{"key":"10729_CR196","doi-asserted-by":"publisher","unstructured":"Sadreddin A, Mouhoub M, Sadaoui S (2022) Portfolio selection for SAT instances. In: 2022 IEEE International Conference on Systems, Man, and Cybernetics (SMC), pp 2962\u20132967. IEEE, Prague, Czech Republic. https:\/\/doi.org\/10.1109\/SMC53654.2022.9945151","DOI":"10.1109\/SMC53654.2022.9945151"},{"key":"10729_CR197","doi-asserted-by":"publisher","unstructured":"Sanchez-Stern A, Alhessi Y, Saul L, Lerner S (2020) Generating correctness proofs with neural networks. In: Sen K, Naik M (eds) Proceedings of the 4th ACM SIGPLAN international workshop on machine learning and programming languages. MAPL \u201920. Association for computing machinery, New York, NY, USA. https:\/\/doi.org\/10.1145\/3394450.3397466","DOI":"10.1145\/3394450.3397466"},{"key":"10729_CR198","doi-asserted-by":"publisher","unstructured":"Sanchez-Stern A, First E, Zhou T, Kaufman Z, Brun Y, Ringer T (2023) Passport: Improving automated formal verification using identifiers. ACM Trans Program Languages Systems 45(2). https:\/\/doi.org\/10.1145\/3593374","DOI":"10.1145\/3593374"},{"key":"10729_CR199","doi-asserted-by":"publisher","unstructured":"Sarker IH (2021) Deep learning: A comprehensive overview on techniques, taxonomy, applications and research directions. SN Comput Sci 2. https:\/\/doi.org\/10.1007\/s42979-021-00815-1","DOI":"10.1007\/s42979-021-00815-1"},{"key":"10729_CR200","doi-asserted-by":"publisher","unstructured":"Scott J, Niemetz A, Preiner M, Nejati S, Ganesh V (2021) MachSMT: A machine learning-based algorithm selector for SMT solvers. In: Groote JF, Larsen KG (eds.) International Conference on Tools and Algorithms for the Construction and Analysis of Systems. Lecture Notes in Computer Science, vol. 12652, pp 303\u2013325. Springer, Luxembourg City, Luxembourg. https:\/\/doi.org\/10.1007\/978-3-030-72013-1_16","DOI":"10.1007\/978-3-030-72013-1_16"},{"key":"10729_CR201","doi-asserted-by":"publisher","unstructured":"Scott J, Niemetz A, Preiner M, Nejati S, Ganesh V (2023) Algorithm selection for SMT. Int J Softw Tools Technol Transfer 25:219\u2013239. https:\/\/doi.org\/10.1007\/s10009-023-00696-0","DOI":"10.1007\/s10009-023-00696-0"},{"key":"10729_CR202","doi-asserted-by":"publisher","unstructured":"Scott J, Sudula T, Rehman H, Mora F, Ganesh V (2021) BanditFuzz: Fuzzing SMT solvers with multi-agent reinforcement learning. In: Huisman M, P\u0103s\u0103reanu C, Zhan N (eds.) International Symposium on Formal Methods. Lecture Notes in Computer Science, vol. 13047, pp 103\u2013121. Springer, Virtual Event. https:\/\/doi.org\/10.1007\/978-3-030-90870-6_6","DOI":"10.1007\/978-3-030-90870-6_6"},{"key":"10729_CR203","doi-asserted-by":"crossref","unstructured":"Sejnowski TJ (2018) The Deep Learning Revolution. MIT press, Cambridge, MA. https:\/\/mitpress.mit.edu\/9780262038034\/the-deep-learning-revolution\/","DOI":"10.7551\/mitpress\/11474.001.0001"},{"key":"10729_CR204","doi-asserted-by":"publisher","unstructured":"Selsam D, Bj\u00f8rner N (2019) Guiding high-performance SAT solvers with Unsat-Core predictions. In: Janota M, Lynce I (eds.) Theory and Applications of Satisfiability Testing \u2013 SAT 2019. Lecture Notes in Computer Science, vol. 11628, pp 336\u2013353. Springer, Lisbon, Portugal. https:\/\/doi.org\/10.1007\/978-3-030-24258-9_24","DOI":"10.1007\/978-3-030-24258-9_24"},{"key":"10729_CR205","unstructured":"Selsam D, Lamm M, B\u00fcnz B, Liang P, Moura L, Dill DL (2019) Learning a SAT solver from single-bit supervision. In: International Conference on Learning Representations. OpenReview.net, New Orleans, LA, USA. https:\/\/openreview.net\/forum?id=HJMC_iA5tm"},{"key":"10729_CR206","doi-asserted-by":"publisher","first-page":"140896","DOI":"10.1109\/ACCESS.2021.3119746","volume":"9","author":"S Shafiq","year":"2021","unstructured":"Shafiq S, Mashkoor A, Mayr-Dorn C, Egyed A (2021) A literature review of using machine learning in software development life cycle stages. IEEE Access 9:140896\u2013140920. https:\/\/doi.org\/10.1109\/ACCESS.2021.3119746","journal-title":"IEEE Access"},{"key":"10729_CR207","doi-asserted-by":"publisher","unstructured":"Shigyo Y, Katayama T (2020) Proposal of an approach to generate VDM++ specifications from natural language specification by machine learning. In: IEEE Global Conference on consumer electronics (GCCE), pp 292\u2013296. IEEE, Kobe, Japan. https:\/\/doi.org\/10.1109\/GCCE50665.2020.9292047","DOI":"10.1109\/GCCE50665.2020.9292047"},{"key":"10729_CR208","doi-asserted-by":"publisher","unstructured":"Shminke B (2022) gym-saturation: an OpenAI Gym environment for saturation provers. J Open Source Softw 7(71):3849. https:\/\/doi.org\/10.21105\/joss.03849","DOI":"10.21105\/joss.03849"},{"key":"10729_CR209","doi-asserted-by":"publisher","unstructured":"Shtrichman O (2000) Tuning SAT checkers for bounded model checking. In: Emerson EA, Sistla AP (eds.) Computer Aided Verification, pp. 480\u2013494. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/10722167_36","DOI":"10.1007\/10722167_36"},{"issue":"2","key":"10729_CR210","doi-asserted-by":"publisher","first-page":"14","DOI":"10.1109\/48.551","volume":"13","author":"AB Simmons","year":"1988","unstructured":"Simmons AB, Chappell SG (1988) Artificial intelligence-definition and practice. IEEE J Oceanic Eng 13(2):14\u201342. https:\/\/doi.org\/10.1109\/48.551","journal-title":"IEEE J Oceanic Eng"},{"key":"10729_CR211","doi-asserted-by":"publisher","unstructured":"Si X, Naik A, Dai H, Naik M, Song L (2020) Code2Inv: A deep learning framework for program verification. In: Lahiri SK, Wang C (eds) International conference on computer aided verification. Lecture notes in computer science, vol 12225, pp 151\u2013164. Springer, Los Angeles, CA, USA. https:\/\/doi.org\/10.1007\/978-3-030-53291-8_9","DOI":"10.1007\/978-3-030-53291-8_9"},{"key":"10729_CR212","doi-asserted-by":"publisher","unstructured":"Suda M (2021) Improving ENIGMA-style clause selection while learning from history. In: Platzer A, Sutcliffe G (eds.) Automated Deduction \u2013 CADE 28. Lecture Notes in Computer Science, vol. 12699, pp 543\u2013561. Springer, Virtual Event. https:\/\/doi.org\/10.1007\/978-3-030-79876-5_31","DOI":"10.1007\/978-3-030-79876-5_31"},{"key":"10729_CR213","doi-asserted-by":"publisher","unstructured":"Suda M (2021) Vampire with a brain is a good ITP hammer. In: Konev G Borisand\u00a0Reger (ed) Frontiers of combining systems. Lecture notes in computer science, vol 12941, pp 192\u2013209. Springer, Birmingham, UK. https:\/\/doi.org\/10.1007\/978-3-030-86205-3_11","DOI":"10.1007\/978-3-030-86205-3_11"},{"key":"10729_CR214","doi-asserted-by":"publisher","unstructured":"Sun L, Gerault D, Benamira A, Peyrin T (2020) NeuroGIFT: Using a machine learning based SAT solver for cryptanalysis. In: Dolev S, Kolesnikov V, Lodha S, Weiss G (eds.) International Symposium on Cyber Security Cryptography and Machine Learning. Lecture Notes in Computer Science, vol. 12161, pp 62\u201384. Springer, Be\u2019er Sheva, Israel. https:\/\/doi.org\/10.1007\/978-3-030-49785-9_5","DOI":"10.1007\/978-3-030-49785-9_5"},{"key":"10729_CR215","unstructured":"Sutton RS, Barto AG (2018) Reinforcement Learning: An Introduction, 2nd edn. MIT Press, Cambridge, MA. http:\/\/incompleteideas.net\/book\/the-book-2nd.html"},{"key":"10729_CR216","doi-asserted-by":"publisher","unstructured":"Szegedy C (2020) A promising path towards autoformalization and general artificial intelligence. In: Benzm\u00fcller C, Miller B (eds.) Intelligent Computer Mathematics. Lecture Notes in Computer Science, vol. 12236, pp 3\u201320. Springer, Bertinoro, Italy. https:\/\/doi.org\/10.1007\/978-3-030-53518-6_1","DOI":"10.1007\/978-3-030-53518-6_1"},{"key":"10729_CR217","doi-asserted-by":"publisher","unstructured":"Tipping ME (2004) Bayesian Inference: An Introduction to Principles and Practice in Machine Learning. In: Bousquet O, Luxburg U, R\u00e4tsch G (eds) Advanced Lectures on Machine Learning, pp 41\u201362. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-540-28650-9_3","DOI":"10.1007\/978-3-540-28650-9_3"},{"key":"10729_CR218","unstructured":"Tran THH, Martinc M, Doucet A, Pollak S (2022) IJS at TextGraphs-16 natural language premise selection task: Will contextual information improve natural language premise selection? In: Ustalov D, Gao Y, Panchenko A, Valentino M, Thayaparan M, Nguyen TH, Penn G, Ramesh A, Jana A (eds.) Proceedings of TextGraphs-16: Graph-based Methods for Natural Language Processing, pp 114\u2013118. Association for Computational Linguistics, Gyeongju, Republic of Korea. https:\/\/aclanthology.org\/2022.textgraphs-1.12"},{"key":"10729_CR219","doi-asserted-by":"publisher","unstructured":"Tsutomu\u00a0Kumazawa MT, Kambayashi Y (2022) Exploration strategies for balancing efficiency and comprehensibility in model checking with ant colony optimization. J Inf Telecommun 6(3):341\u2013359. https:\/\/doi.org\/10.1080\/24751839.2022.2047470","DOI":"10.1080\/24751839.2022.2047470"},{"key":"10729_CR220","unstructured":"Tworkowski S, Mikula M, Odrzyg\u00f3\u017ad\u017a T, Czechowski K, Antoniak S, Jiang AQ, Szegedy C, Kuci\u0144ski L, Mil\u00f3s P, Wu Y (2022) Formal premise selection with language models. In: 7th Conference on artificial intelligence and theorem proving. AITP Conference, Aussois, France. https:\/\/aitp-conference.org\/2022\/abstract\/AITP_2022_paper_32.pdf"},{"key":"10729_CR221","doi-asserted-by":"publisher","first-page":"147","DOI":"10.1016\/S1571-0661(04)80659-5","volume":"86","author":"J Urban","year":"2003","unstructured":"Urban J (2003) MPTP 0.1 - system description. Electron Notes Theoretical Comput Sci 86:147\u2013152. https:\/\/doi.org\/10.1016\/S1571-0661(04)80659-5","journal-title":"Electron Notes Theoretical Comput Sci"},{"key":"10729_CR222","doi-asserted-by":"publisher","unstructured":"Urban J, Jakub\u016fv J (2020) First neural conjecturing datasets and experiments. In: Benzm\u00fcller C, Miller B (eds) Intelligent computer mathematics. lecture notes in computer science, vol 12236, pp 315\u2013323. Springer, Bertinoro, Italy. https:\/\/doi.org\/10.1007\/978-3-030-53518-6_24","DOI":"10.1007\/978-3-030-53518-6_24"},{"key":"10729_CR223","doi-asserted-by":"publisher","unstructured":"Urban J, Vysko\u010dil J (2013) Theorem Proving in Large Formal Mathematics as an Emerging AI Field. In: Bonacina MP, Stickel ME (eds.) Automated Reasoning and Mathematics. Lecture Notes in Computer Science, vol. 7788, pp 240\u2013257. Springer, Berlin, Heidelberg. https:\/\/doi.org\/10.1007\/978-3-642-36675-8_13","DOI":"10.1007\/978-3-642-36675-8_13"},{"key":"10729_CR224","unstructured":"Vaswani A, Shazeer N, Parmar N, Uszkoreit J, Jones L, Gomez AN, Kaiser Lu, Polosukhin I (2017) Attention is all you need. In: Guyon I, Luxburg UV, Bengio S, Wallach H, Fergus R, Vishwanathan S, Garnett R (eds) Advances in Neural Information Processing Systems, vol. 30, pp. 5998\u20136008. Curran Associates, Inc., Long Beach, CA, USA. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2017\/file\/3f5ee243547dee91fbd053c1c4a845aa-Paper.pdf"},{"key":"10729_CR225","doi-asserted-by":"publisher","first-page":"108561","DOI":"10.1109\/ACCESS.2020.3000907","volume":"8","author":"F Wang","year":"2020","unstructured":"Wang F, Cao Z, Tan L, Zong H (2020) Survey on learning-based formal methods: Taxonomy, applications and possible future directions. IEEE Access 8:108561\u2013108578. https:\/\/doi.org\/10.1109\/ACCESS.2020.3000907","journal-title":"IEEE Access"},{"key":"10729_CR226","doi-asserted-by":"publisher","unstructured":"Wang Q, Cao W, Jiang J, Zhao Y, Ming Z (2021) NNRW-based algorithm selection for software model checking. In: Cao J, Vong CM, Miche Y, Lendasse A (eds) Proceedings of ELM2019. Proceedings in adaptation, learning and optimization, vol 14, pp 11\u201321. Springer, Yangzhou, China. https:\/\/doi.org\/10.1007\/978-3-030-58989-9_2","DOI":"10.1007\/978-3-030-58989-9_2"},{"key":"10729_CR227","unstructured":"Wang M, Deng J (2020) Learning to prove theorems by learning to generate theorems. In: Larochelle H, Ranzato M, Hadsell R, Balcan MF, Lin H (eds) Advances in neural information processing systems, vol 33, pp 18146\u201318157. Curran Associates, Inc., Virtual Event. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2020\/file\/d2a27e83d429f0dcae6b937cf440aeb1-Paper.pdf"},{"key":"10729_CR228","doi-asserted-by":"publisher","unstructured":"Wang Q, Jiang J, Zhao Y, Cao W, Wang C, Li S (2021) Algorithm selection for software verification based on adversarial LSTM. In: 2021 7th IEEE Intl conference on big data security on cloud (BigDataSecurity), IEEE Intl Conference on High Performance and Smart Computing, (HPSC) and IEEE Intl Conference on Intelligent Data and Security (IDS). IEEE, New York, NY, USA. https:\/\/doi.org\/10.1109\/bigdatasecurityhpscids52275.2021.00026","DOI":"10.1109\/bigdatasecurityhpscids52275.2021.00026"},{"key":"10729_CR229","doi-asserted-by":"publisher","unstructured":"Wang Y, Roohi N, West M, Viswanathan M, Dullerud GE (2020) Statistically model checking PCTL specifications on markov decision processes via reinforcement learning. In: 2020 59th IEEE conference on decision and control (CDC), pp 1392\u20131397. IEEE, Jeju, South Korea. https:\/\/doi.org\/10.1109\/CDC42340.2020.9303982","DOI":"10.1109\/CDC42340.2020.9303982"},{"key":"10729_CR230","doi-asserted-by":"publisher","unstructured":"Wang J, Wang C (2023) Learning to synthesize relational invariants. In: Proceedings of the 37th IEEE\/ACM international conference on automated software engineering. ASE \u201922. Association for computing machinery, Rochester, MI, USA. https:\/\/doi.org\/10.1145\/3551349.3556942","DOI":"10.1145\/3551349.3556942"},{"key":"10729_CR231","doi-asserted-by":"publisher","unstructured":"Wang W, Wang K, Zhang M, Khurshid S (2019) Learning to optimize the Alloy Analyzer. In: 2019 12th IEEE Conference on software testing, validation and verification (ICST), pp 228\u2013239. IEEE, Xi\u2019an, China. https:\/\/doi.org\/10.1109\/ICST.2019.00031","DOI":"10.1109\/ICST.2019.00031"},{"key":"10729_CR232","doi-asserted-by":"publisher","unstructured":"Wang H, Yuan Y, Liu Z, Shen J, Yin Y, Xiong J, Xie E, Shi H, Li Y, Li L, Yin J, Li Z, Liang X (2023) DT-solver: Automated theorem proving with dynamic-tree sampling guided by proof-level value function. In: Proceedings of the 61st Annual meeting of the association for computational linguistics, vol 1, pp 12632\u201312646. Association for Computational Linguistics, Toronto, Canada. https:\/\/doi.org\/10.18653\/v1\/2023.acl-long.706","DOI":"10.18653\/v1\/2023.acl-long.706"},{"key":"10729_CR233","doi-asserted-by":"publisher","unstructured":"Wei Y (2022) Applying autoencoder to automated theorem proving. In: 4th International conference on frontiers technology of information and computer (ICFTIC). IEEE, Qingdao, China. https:\/\/doi.org\/10.1109\/icftic57696.2022.10075262","DOI":"10.1109\/icftic57696.2022.10075262"},{"key":"10729_CR234","unstructured":"Welleck S, Liu J, Lu X, Hajishirzi H, Choi Y (2022) NaturalProver: Grounded mathematical proof generation with language models. In: Koyejo S, Mohamed S, Agarwal A, Belgrave D, Cho K, Oh A (eds.) Advances in Neural Information Processing Systems 35 (NeurIPS 2022), vol. 35, pp 4913\u20134927. Curran Associates, Inc., New Orleans, LA, USA. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2022\/file\/1fc548a8243ad06616eee731e0572927-Paper-Conference.pdf"},{"key":"10729_CR235","doi-asserted-by":"publisher","unstructured":"Wohlin C (2014) Guidelines for snowballing in systematic literature studies and a replication in software engineering. In: Proceedings of the 18th international conference on evaluation and assessment in software engineering. EASE \u201914. Association for Computing Machinery, London, UK. https:\/\/doi.org\/10.1145\/2601248.2601268","DOI":"10.1145\/2601248.2601268"},{"key":"10729_CR236","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1592434.1592436","volume":"41","author":"J Woodcock","year":"2009","unstructured":"Woodcock J, Larsen PG, Bicarregui J, Fitzgerald J (2009) Formal methods: Practice and experience. ACM Comput Surv 41:1\u201336. https:\/\/doi.org\/10.1145\/1592434.1592436","journal-title":"ACM Comput Surv"},{"issue":"5","key":"10729_CR237","doi-asserted-by":"publisher","first-page":"1122","DOI":"10.1109\/JAS.2023.123618","volume":"10","author":"T Wu","year":"2023","unstructured":"Wu T, He S, Liu J, Sun S, Liu K, Han Q-L, Tang Y (2023) A brief overview of ChatGPT: The history, status quo and potential future development. IEEE\/CAA J Autom Sinica 10(5):1122\u20131136. https:\/\/doi.org\/10.1109\/JAS.2023.123618","journal-title":"IEEE\/CAA J Autom Sinica"},{"key":"10729_CR238","unstructured":"Wu Y, Jiang AQ, Li W, Rabe M, Staats C, Jamnik M, Szegedy C (2022a) Autoformalization with large language models. In: Koyejo S, Mohamed S, Agarwal A, Belgrave D, Cho K, Oh A (eds) Advances in neural information processing systems 35 (NeurIPS 2022), vol 35, pp 32353\u201332368. Curran Associates, Inc., New Orleans, LA, USA. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2022\/file\/d0c6bc641a56bebee9d985b937307367-Paper-Conference.pdf"},{"key":"10729_CR239","unstructured":"Wu Y, Jiang A, Grosse R, Ba J (2020) Neural theorem proving on inequality problems. In: 5th Conference on artificial intelligence and theorem proving. AITP Conference, Obergurgl, Austria. https:\/\/aitp-conference.org\/2020\/abstract\/paper_18.pdf"},{"key":"10729_CR240","unstructured":"Wu Y, Jiang A, Li W, Rabe MN, Staats C, Jamnik M, Szegedy C (2022b) Autoformalization for neural theorem proving. In: 7th Conference on artificial intelligence and theorem proving. AITP Conference, Aussois, France. https:\/\/aitp-conference.org\/2022\/abstract\/AITP_2022_paper_33.pdf"},{"key":"10729_CR241","unstructured":"Wu M, Norrish M, Walder C, Dezfouli A (2020) Reinforcement learning for interactive theorem proving in HOL4. In: 5th Conference on artificial intelligence and theorem proving. AITP Conference, Aussois, France. https:\/\/aitp-conference.org\/2020\/abstract\/paper_7.pdf"},{"key":"10729_CR242","unstructured":"Wu M, Norrish M, Walder C, Dezfouli A (2021) TacticZero: Learning to prove theorems from scratch with deep reinforcement learning. In: Ranzato M, Beygelzimer A, Dauphin Y, Liang PS, Vaughan JW (eds) Advances in neural information processing systems, vol 34, pp 9330\u20139342. Curran Associates, Inc., Virtual Event. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2021\/file\/4dea382d82666332fb564f2e711cbc71-Paper.pdf"},{"key":"10729_CR243","doi-asserted-by":"publisher","unstructured":"Xu R, Chen J, He F (2022) Data-driven loop bound learning for termination analysis. In: Proceedings of the 44th international conference on software engineering. ICSE \u201922, pp 499\u2013510. Association for computing machinery, Pittsburgh, PA, USA. https:\/\/doi.org\/10.1145\/3510003.3510220","DOI":"10.1145\/3510003.3510220"},{"key":"10729_CR244","doi-asserted-by":"publisher","unstructured":"Xu L, Hoos HHH, Leyton-Brown K (2021) Predicting satisfiability at the phase transition. In: Proceedings of the AAAI Conference on Artificial Intelligence, vol. 26, pp 584\u2013590. AAAI Press, Toronto, Canada. https:\/\/doi.org\/10.1609\/aaai.v26i1.8142","DOI":"10.1609\/aaai.v26i1.8142"},{"key":"10729_CR245","doi-asserted-by":"publisher","unstructured":"Xu R, Lieberherr K (2022) Towards tackling QSAT problems with deep learning and monte carlo tree search. In: Arai, K. (ed.) Intelligent Computing. Lecture Notes in Networks and Systems, vol. 507, pp 45\u201358. Springer, London, UK.https:\/\/doi.org\/10.1007\/978-3-031-10464-0_4","DOI":"10.1007\/978-3-031-10464-0_4"},{"key":"10729_CR246","unstructured":"Yang K, Deng J (2019) Learning to prove theorems via interacting with proof assistants. In: Chaudhuri K, Salakhutdinov R (eds) Proceedings of the 36th international conference on machine learning. Proceedings of machine learning research, vol 97, pp 6984\u20136994. PMLR, Long Beach, CA, USA. https:\/\/proceedings.mlr.press\/v97\/yang19a.html"},{"key":"10729_CR247","unstructured":"Yan Z, Li M, Shi Z, Zhang W, Chen Y-C, Zhang H (2023) The elephant in the room: Variable dependency in GNN-based SAT solving. In: First International Workshop on Deep Learning-aided Verification. OpenReview.net, Paris, France. https:\/\/openreview.net\/forum?id=yOyxNRK5MOM"},{"key":"10729_CR248","doi-asserted-by":"publisher","unstructured":"Yao P, Huang H, Tang W, Shi Q, Wu R, Zhang C (2021) Fuzzing SMT solvers via two-dimensional input space exploration. In: Proceedings of the 30th ACM SIGSOFT international symposium on software testing and analysis. ISSTA 2021, pp 322\u2013335. Association for Computing Machinery, Virtual Event. https:\/\/doi.org\/10.1145\/3460319.3464803","DOI":"10.1145\/3460319.3464803"},{"key":"10729_CR249","doi-asserted-by":"publisher","unstructured":"Yao J, Ryan G, Wong J, Jana S, Gu R (2020) Learning nonlinear loop invariants with gated continuous logic networks. In: Donaldson AF, Torlak E (eds) Proceedings of the 41st ACM SIGPLAN conference on programming language design and implementation. PLDI 2020, pp 106\u2013120. Association for Computing Machinery, London, UK. https:\/\/doi.org\/10.1145\/3385412.3385986","DOI":"10.1145\/3385412.3385986"},{"key":"10729_CR250","unstructured":"Yolcu E, Poczos B (2019) Learning local search heuristics for boolean satisfiability. In: Wallach H, Larochelle H, Beygelzimer A, Alch\u00e9-Buc F, Fox E, Garnett R (eds.) Advances in Neural Information Processing Systems, vol. 32. Curran Associates, Inc., Vancouver, Canada. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2019\/file\/12e59a33dea1bf0630f46edfe13d6ea2-Paper.pdf"},{"key":"10729_CR251","unstructured":"You J, Wu H, Barrett C, Ramanujan R, Leskovec J (2019) G2SAT: Learning to generate SAT formulas. In: Wallach H, Larochelle H, Beygelzimer A, Alch\u00e9-Buc F, Fox E, Garnett R (eds.) Advances in Neural Information Processing Systems 32 (NeurIPS 2019), vol. 32. Curran Associates, Inc., Vancouver, Canada. https:\/\/proceedings.neurips.cc\/paper_files\/paper\/2019\/file\/daea32adcae6abcb548134fa98f139f9-Paper.pdf"},{"key":"10729_CR252","doi-asserted-by":"publisher","unstructured":"Yu S, Wang T, Wang J (2023) Loop invariant inference through SMT solving enhanced reinforcement learning. In: Just R, Fraser G (eds) Proceedings of the 32nd ACM SIGSOFT international symposium on software testing and analysis. ISSTA 2023, pp 175\u2013187. Association for Computing Machinery, Seattle, WA, USA. https:\/\/doi.org\/10.1145\/3597926.3598047","DOI":"10.1145\/3597926.3598047"},{"issue":"8","key":"10729_CR253","doi-asserted-by":"publisher","first-page":"488","DOI":"10.1016\/j.sysarc.2004.10.006","volume":"51","author":"Z Zeng","year":"2005","unstructured":"Zeng Z, Talupuru KR, Ciesielski M (2005) Functional test generation based on word-level SAT. J Syst Architect 51(8):488\u2013511. https:\/\/doi.org\/10.1016\/j.sysarc.2004.10.006","journal-title":"J Syst Architect"},{"key":"10729_CR254","doi-asserted-by":"publisher","unstructured":"Zhang L, Blaauwbroek L, Kaliszyk C, Urban J (2023) Learning proof transformations and its applications in interactive theorem proving. In: Sattler U, Suda M (eds) Frontiers of combining systems: 14th international symposium. lecture notes in computer science, vol 14279, pp 236\u2013254. Springer, Prague, Czech Republic. https:\/\/doi.org\/10.1007\/978-3-031-43369-6_13","DOI":"10.1007\/978-3-031-43369-6_13"},{"key":"10729_CR255","doi-asserted-by":"publisher","unstructured":"Zhang L, Blaauwbroek L, Piotrowski B, \u010cern\u1ef3 P, Kaliszyk C, Urban J (2021) Online machine learning techniques for Coq: A comparison. In: Kamareddine F, Sacerdoti\u00a0Coen C (eds) Intelligent computer mathematics. Lecture notes in computer science, vol 12833, pp 67\u201383. Springer, Timisoara, Romania. https:\/\/doi.org\/10.1007\/978-3-030-81097-9_5","DOI":"10.1007\/978-3-030-81097-9_5"},{"key":"10729_CR256","doi-asserted-by":"publisher","unstructured":"Zhang X, Li Y, Hong W, Sun M (2019) Using recurrent neural network to predict tactics for proving component connector properties in Coq. In: 2019 International symposium on theoretical aspects of software engineering (TASE), pp 107\u2013112. IEEE, Guilin, China. https:\/\/doi.org\/10.1109\/TASE.2019.00-12","DOI":"10.1109\/TASE.2019.00-12"},{"key":"10729_CR257","doi-asserted-by":"publisher","unstructured":"Zhang W, Sun Z, Zhu Q, Li G, Cai S, Xiong Y, Zhang L (2020) NLocalSAT: boosting local search with solution prediction. In: Bessiere C (ed.) Proceedings of the Twenty-Ninth International Joint Conference on Artificial Intelligence, pp 1177\u20131183. International Joint Conferences on Artificial Intelligence Organization, Yokohama, Japan. https:\/\/doi.org\/10.24963\/ijcai.2020\/164","DOI":"10.24963\/ijcai.2020\/164"},{"key":"10729_CR258","doi-asserted-by":"publisher","unstructured":"Zhang C, Zhang Y, Mao J, Chen W, Yue L, Bai G, Xu M (2022) Towards better generalization for neural network-based SAT solvers. In: Gama J, Li T, Yu Y, Chen E, Zheng Y, Teng F (eds.) Advances in Knowledge Discovery and Data Mining. Lecture Notes in Artificial Intelligence, vol. 13281, pp 199\u2013210. Springer, Chengdu, China. https:\/\/doi.org\/10.1007\/978-3-031-05936-0_16","DOI":"10.1007\/978-3-031-05936-0_16"},{"key":"10729_CR259","doi-asserted-by":"publisher","unstructured":"Zheng J, He K, Zhou J, Jin Y, Li C-M, Many\u00e0 F (2022) BandMaxSAT: A local search MaxSAT solver with multi-armed bandit. In: Raedt LD (ed.) Thirty-First International Joint Conference on Artificial Intelligence (IJCAI-22), pp. 1901\u20131907. International Joint Conferences on Artificial Intelligence Organization, Vienna, Austria. https:\/\/doi.org\/10.24963\/ijcai.2022\/264","DOI":"10.24963\/ijcai.2022\/264"},{"key":"10729_CR260","doi-asserted-by":"publisher","first-page":"57","DOI":"10.1016\/j.aiopen.2021.01.001","volume":"1","author":"J Zhou","year":"2020","unstructured":"Zhou J, Cui G, Hu S, Zhang Z, Yang C, Liu Z, Wang L, Li C, Sun M (2020) Graph neural networks: A review of methods and applications. AI Open 1:57\u201381. https:\/\/doi.org\/10.1016\/j.aiopen.2021.01.001","journal-title":"AI Open"},{"key":"10729_CR261","doi-asserted-by":"publisher","unstructured":"Zhu W (2022) Approximate model checking based on deep forest. In: 2022 International conference on artificial intelligence and computer information technology (AICIT). AICIT, pp 1\u20134. IEEE, Yichang, China. https:\/\/doi.org\/10.1109\/AICIT55386.2022.9930208","DOI":"10.1109\/AICIT55386.2022.9930208"},{"key":"10729_CR262","doi-asserted-by":"publisher","unstructured":"Zhu W, Wu H (2022) CTL model checking based on binary classification of machine learning. Int Arab J Inf Technol 19(2):249\u2013260. https:\/\/doi.org\/10.34028\/iajit\/19\/2\/12","DOI":"10.34028\/iajit\/19\/2\/12"},{"key":"10729_CR263","doi-asserted-by":"publisher","unstructured":"Zhu W, Wu H, Deng M (2019) LTL model checking based on binary classification of machine learning. IEEE Access 7:135703\u2013135719. https:\/\/doi.org\/10.1109\/ACCESS.2019.2942762","DOI":"10.1109\/ACCESS.2019.2942762"},{"key":"10729_CR264","unstructured":"Zombori Z, Csisz\u00e1rik A, Michalewski H, Kaliszyk C, Urban J (2019) Curriculum learning and theorem proving. In: 4th Conference on artificial intelligence and theorem proving. AITP Conference, Obergurgl, Austria. https:\/\/aitp-conference.org\/2019\/abstract\/paper%2013.pdf"},{"key":"10729_CR265","doi-asserted-by":"publisher","unstructured":"Zombori Z, Csisz\u00e1rik A, Michalewski H, Kaliszyk C, Urban J (2021) Towards finding longer proofs. In: Das A, Negri S (eds) Automated reasoning with analytic tableaux and related methods. Lecture notes in computer science, vol 12842, pp 167\u2013186. Springer, Birmingham, UK. https:\/\/doi.org\/10.1007\/978-3-030-86059-2_10","DOI":"10.1007\/978-3-030-86059-2_10"},{"key":"10729_CR266","doi-asserted-by":"publisher","unstructured":"Zombori Z, Urban J, Brown CE (2020) Prolog technology reinforcement learning prover. In: Peltier N, Sofronie-Stokkermans V (eds) Automated Reasoning. Lecture notes in computer science, vol 12167, pp 489\u2013507. Springer, Paris, France. https:\/\/doi.org\/10.1007\/978-3-030-51054-1_33","DOI":"10.1007\/978-3-030-51054-1_33"},{"key":"10729_CR267","doi-asserted-by":"publisher","unstructured":"Zombori Z, Urban J, Ol\u0161\u00e1k M (2021) The role of entropy in guiding a connection prover. In: Das A, Negri S (eds) International conference on automated reasoning with analytic tableaux and related methods. lecture notes in computer science, vol 12842, pp 218\u2013235. Springer, Birmingham, UK. https:\/\/doi.org\/10.1007\/978-3-030-86059-2_13","DOI":"10.1007\/978-3-030-86059-2_13"}],"container-title":["Empirical Software Engineering"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-025-10729-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10664-025-10729-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10664-025-10729-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,11,5]],"date-time":"2025-11-05T02:40:45Z","timestamp":1762310445000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10664-025-10729-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,14]]},"references-count":267,"journal-issue":{"issue":"6","published-print":{"date-parts":[[2025,12]]}},"alternative-id":["10729"],"URL":"https:\/\/doi.org\/10.1007\/s10664-025-10729-8","relation":{},"ISSN":["1382-3256","1573-7616"],"issn-type":[{"type":"print","value":"1382-3256"},{"type":"electronic","value":"1573-7616"}],"subject":[],"published":{"date-parts":[[2025,10,14]]},"assertion":[{"value":"2 December 2024","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"3 September 2025","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"14 October 2025","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Declarations"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":2,"name":"Ethics","group":{"name":"EthicsHeading","label":"Conflicts of Interest"}},{"value":"Not applicable.","order":3,"name":"Ethics","group":{"name":"EthicsHeading","label":"Ethical Approval"}},{"value":"Not applicable.","order":4,"name":"Ethics","group":{"name":"EthicsHeading","label":"Informed Consent"}},{"value":"Not applicable.","order":5,"name":"Ethics","group":{"name":"EthicsHeading","label":"Clinical Trial Number"}}],"article-number":"175"}}