{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T16:02:16Z","timestamp":1743091336069,"version":"3.40.3"},"publisher-location":"Cham","reference-count":22,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031656262"},{"type":"electronic","value":"9783031656279"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2024,7,26]],"date-time":"2024-07-26T00:00:00Z","timestamp":1721952000000},"content-version":"vor","delay-in-days":207,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p><jats:italic>Symbolic Machine Learning Prover (SMLP)<\/jats:italic>is a tool and a library for system exploration based on data samples obtained by simulating or executing the system on a number of input vectors. SMLP aims at exploring the system based on this data by taking a grey-box approach: SMLP uses symbolic reasoning for ML model exploration and optimization under verification and stability constraints, based on SMT, constraint, and neural network solvers. In addition, the model exploration is guided by probabilistic and statistical methods in a closed feedback loop with the system\u2019s response. SMLP has been applied in industrial setting at Intel for analyzing and optimizing hardware designs at the analog level. SMLP is a general purpose tool and can be applied to any system that can be sampled and modeled by machine learning models.<\/jats:p>","DOI":"10.1007\/978-3-031-65627-9_11","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T19:01:31Z","timestamp":1721934091000},"page":"219-233","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["SMLP: Symbolic Machine Learning Prover"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2386-7489","authenticated-orcid":false,"given":"Franz","family":"Brau\u00dfe","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-9883-6997","authenticated-orcid":false,"given":"Zurab","family":"Khasidashvili","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-0740-621X","authenticated-orcid":false,"given":"Konstantin","family":"Korovin","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"issue":"1","key":"11_CR1","doi-asserted-by":"publisher","first-page":"35","DOI":"10.1002\/widm.1144","volume":"5","author":"M Atzmueller","year":"2015","unstructured":"Atzmueller, M.: Subgroup discovery. WIREs Data Mining Knowl. Discov. 5(1), 35\u201349 (2015)","journal-title":"WIREs Data Mining Knowl. Discov."},{"key":"11_CR2","doi-asserted-by":"publisher","unstructured":"Barbosa, H.: cvc5: a versatile and industrial-strength SMT solver. In: TACAS 2022. LNCS, vol. 13243, pp. 415\u2013442. Springer, Cham (2022). https:\/\/doi.org\/10.1007\/978-3-030-99524-9_24","DOI":"10.1007\/978-3-030-99524-9_24"},{"issue":"1","key":"11_CR3","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1111\/j.2517-6161.1951.tb00067.x","volume":"13","author":"GEP Box","year":"1951","unstructured":"Box, G.E.P., Wilson, K.B.: On the experimental attainment of optimum conditions. J. Royal Stat. Soc. Ser. B (Methodological) 13(1), 1\u201345 (1951)","journal-title":"J. Royal Stat. Soc. Ser. B (Methodological)"},{"key":"11_CR4","unstructured":"Brau\u00dfe, F., Khasidashvili, Z., Korovin., K.: Selecting stable safe configurations for systems modelled by neural networks with ReLU activation. In: 2020 Formal Methods in Computer Aided Design, FMCAD 2020, Haifa, Israel, 21\u201324 September 2020, pp. 119\u2013127. IEEE (2020)"},{"key":"11_CR5","doi-asserted-by":"crossref","unstructured":"Brau\u00dfe, F., Khasidashvili, Z., Korovin, K.: Combining constraint solving and bayesian techniques for system optimization. In:\u00a0De Raedt, L. (ed.) Proceedings of the Thirty-First International Joint Conference on Artificial Intelligence, IJCAI 2022, Vienna, Austria, 23\u201329 July 2022, pp. 1788\u20131794. ijcai.org (2022)","DOI":"10.24963\/ijcai.2022\/249"},{"key":"11_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/978-3-030-29007-8_8","volume-title":"Frontiers of Combining Systems","author":"F Brau\u00dfe","year":"2019","unstructured":"Brau\u00dfe, F., Korovin, K., Korovina, M., M\u00fcller, N.: A CDCL-style calculus for solving non-linear constraints. In: Herzig, A., Popescu, A. (eds.) FroCoS 2019. LNCS (LNAI), vol. 11715, pp. 131\u2013148. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-29007-8_8"},{"key":"11_CR7","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2023.114125","volume":"975","author":"F Brau\u00dfe","year":"2023","unstructured":"Brau\u00dfe, F., Korovin, K., Korovina, M.V., M\u00fcller, N.T.: The KSMT calculus is a $$\\delta $$-complete decision procedure for non-linear constraints. Theor. Comput. Sci. 975, 114125 (2023)","journal-title":"Theor. Comput. Sci."},{"key":"11_CR8","doi-asserted-by":"crossref","unstructured":"Brau\u00dfe, F., Khasidashvili, Z., Korovin, K.: SMLP: symbolic machine learning prover (user manual). CoRR, abs\/2405.10215 (2024)","DOI":"10.1007\/978-3-031-65627-9_11"},{"issue":"3","key":"11_CR9","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1007\/s10009-023-00703-4","volume":"25","author":"C Brix","year":"2023","unstructured":"Brix, C., M\u00fcller, M.N., Bak, S., Johnson, T.T., Liu, C.: First three years of the international verification of neural networks competition (VNN-COMP). Int. J. Softw. Tools Technol. Transf. 25(3), 329\u2013339 (2023)","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"11_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"93","DOI":"10.1007\/978-3-642-36742-7_7","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"A Cimatti","year":"2013","unstructured":"Cimatti, A., Griggio, A., Schaafsma, B.J., Sebastiani, R.: The MathSAT5 SMT solver. In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 93\u2013107. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-36742-7_7"},{"key":"11_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1007\/978-3-540-78800-3_24","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"L de Moura","year":"2008","unstructured":"de Moura, L., Bj\u00f8rner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337\u2013340. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24"},{"key":"11_CR12","doi-asserted-by":"crossref","unstructured":"Demarchi, S., Guidotti, D., Pulina, L., Tacchella, A.: Supporting standardization of neural networks verification with VNN-LIB and CoCoNet. In: Proceedings of the 6th Workshop on Formal Methods for ML-Enabled Autonomous Systems, vol.\u00a016, pp. 47\u201358 (2023)","DOI":"10.29007\/5pdh"},{"issue":"2","key":"11_CR13","doi-asserted-by":"publisher","first-page":"185","DOI":"10.1142\/S0219720005001004","volume":"3","author":"CHQ Ding","year":"2005","unstructured":"Ding, C.H.Q., Peng, H.: Minimum redundancy feature selection from microarray gene expression data. J. Bioinform. Comput. Biol. 3(2), 185\u2013206 (2005)","journal-title":"J. Bioinform. Comput. Biol."},{"key":"11_CR14","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","volume-title":"Computer Aided Verification","author":"B Dutertre","year":"2014","unstructured":"Dutertre, B.: Yices\u00a02.2. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 737\u2013744. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08867-9_49"},{"key":"11_CR15","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"286","DOI":"10.1007\/978-3-642-31365-3_23","volume-title":"Automated Reasoning","author":"S Gao","year":"2012","unstructured":"Gao, S., Avigad, J., Clarke, E.M.: $$\\delta $$-complete decision procedures for satisfiability\u00a0over\u00a0the reals. In: Gramlich, B., Miller, D., Sattler, U. (eds.) IJCAR 2012. LNCS (LNAI), vol. 7364, pp. 286\u2013300. Springer, Heidelberg (2012). https:\/\/doi.org\/10.1007\/978-3-642-31365-3_23"},{"key":"11_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","volume-title":"Computer Aided Verification","author":"G Katz","year":"2019","unstructured":"Katz, G., et al.: The Marabou framework for verification and analysis of deep neural networks. In: Dillig, I., Tasiran, S. (eds.) CAV 2019, Part I. LNCS, vol. 11561, pp. 443\u2013452. Springer, Cham (2019). https:\/\/doi.org\/10.1007\/978-3-030-25540-4_26"},{"issue":"3","key":"11_CR17","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s41060-021-00251-7","volume":"11","author":"Z Khasidashvili","year":"2021","unstructured":"Khasidashvili, Z., Norman, A.J.: Feature range analysis. Int. J. Data Sci. Anal. 11(3), 195\u2013219 (2021)","journal-title":"Int. J. Data Sci. Anal."},{"key":"11_CR18","unstructured":"Kl\u00f6sgen, W.: Explora: a multipattern and multistrategy discovery assistant. In: Fayyad, U.M., Piatetsky-Shapiro, G., Smyth, P., Uthurusamy, R. (eds.) Advances in Knowledge Discovery and Data Mining, pp. 249\u2013271. AAAI\/MIT Press (1996)"},{"key":"11_CR19","doi-asserted-by":"crossref","unstructured":"Manukovsky, A., Shlepnev, Y., Khasidashvili, Z.: Machine learning based design space exploration and applications to signal integrity analysis of 112Gb SerDes systems. In: 2021 IEEE 71st Electronic Components and Technology Conference (ECTC), pp. 1234\u20131245 (2021)","DOI":"10.1109\/ECTC32696.2021.00201"},{"key":"11_CR20","unstructured":"Wang, S., et al.: Beta-CROWN: efficient bound propagation with per-neuron split constraints for complete and incomplete neural network verification. Adv. Neural Inf. Process. Syst. 34 (2021)"},{"key":"11_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"78","DOI":"10.1007\/3-540-63223-9_108","volume-title":"Principles of Data Mining and Knowledge Discovery","author":"S Wrobel","year":"1997","unstructured":"Wrobel, S.: An algorithm for multi-relational discovery of subgroups. In: Komorowski, J., Zytkow, J. (eds.) PKDD 1997. LNCS, vol. 1263, pp. 78\u201387. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-63223-9_108"},{"key":"11_CR22","unstructured":"Xu, K., et al.: Fast and Complete: enabling complete neural network verification with rapid and massively parallel incomplete verifiers. In: International Conference on Learning Representations (2021)"}],"container-title":["Lecture Notes in Computer Science","Computer Aided Verification"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-65627-9_11","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,11,24]],"date-time":"2024-11-24T21:17:46Z","timestamp":1732483066000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-65627-9_11"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031656262","9783031656279"],"references-count":22,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-65627-9_11","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CAV","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Computer Aided Verification","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Montreal, QC","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Canada","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"24 July 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 July 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"36","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cav2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/i-cav.org\/2024\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}