{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,5]],"date-time":"2026-01-05T22:11:54Z","timestamp":1767651114836,"version":"3.40.3"},"publisher-location":"Cham","reference-count":36,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030242572"},{"type":"electronic","value":"9783030242589"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-24258-9_25","type":"book-chapter","created":{"date-parts":[[2019,6,28]],"date-time":"2019-06-28T21:02:31Z","timestamp":1561755751000},"page":"354-370","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":30,"title":["Verifying Binarized Neural Networks by Angluin-Style Learning"],"prefix":"10.1007","author":[{"given":"Andy","family":"Shih","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Adnan","family":"Darwiche","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Arthur","family":"Choi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,6,29]]},"reference":[{"issue":"2","key":"25_CR1","doi-asserted-by":"publisher","first-page":"87","DOI":"10.1016\/0890-5401(87)90052-6","volume":"75","author":"D Angluin","year":"1987","unstructured":"Angluin, D.: Learning regular sets from queries and counterexamples. Inf. Comput. 75(2), 87\u2013106 (1987)","journal-title":"Inf. Comput."},{"key":"25_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"108","DOI":"10.1007\/978-3-540-45193-8_8","volume-title":"Principles and Practice of Constraint Programming \u2013 CP 2003","author":"O Bailleux","year":"2003","unstructured":"Bailleux, O., Boufkhad, Y.: Efficient CNF encoding of boolean cardinality constraints. In: Rossi, F. (ed.) CP 2003. LNCS, vol. 2833, pp. 108\u2013122. Springer, Heidelberg (2003). https:\/\/doi.org\/10.1007\/978-3-540-45193-8_8"},{"key":"25_CR3","doi-asserted-by":"crossref","unstructured":"Bova, S.: SDDs are exponentially more succinct than OBDDs. In: Proceedings of the Thirtieth AAAI Conference on Artificial Intelligence, pp. 929\u2013935 (2016)","DOI":"10.1609\/aaai.v30i1.10107"},{"key":"25_CR4","doi-asserted-by":"publisher","first-page":"677","DOI":"10.1109\/TC.1986.1676819","volume":"C\u201335","author":"RE Bryant","year":"1986","unstructured":"Bryant, R.E.: Graph-based algorithms for boolean function manipulation. IEEE Trans. Comput. C\u201335, 677\u2013691 (1986)","journal-title":"IEEE Trans. Comput."},{"issue":"3\u20134","key":"25_CR5","first-page":"137","volume":"10","author":"M Cadoli","year":"1997","unstructured":"Cadoli, M., Donini, F.M.: A survey on knowledge compilation. AI Commun. 10(3\u20134), 137\u2013150 (1997)","journal-title":"AI Commun."},{"key":"25_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1007\/978-3-030-03592-1_16","volume-title":"Verified Software. Theories, Tools, and Experiments","author":"C-H Cheng","year":"2018","unstructured":"Cheng, C.-H., N\u00fchrenberg, G., Huang, C.-H., Ruess, H.: Verification of binarized neural networks via inter-neuron factoring (Short Paper). In: Piskac, R., R\u00fcmmer, P. (eds.) VSTTE 2018. LNCS, vol. 11294, pp. 279\u2013290. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-03592-1_16"},{"key":"25_CR7","unstructured":"Choi, A., Shi, W., Shih, A., Darwiche, A.: Compiling neural networks into tractable Boolean circuits. In: AAAI Spring Symposium on Verification of Neural Networks (VNN19) (2019)"},{"issue":"9","key":"25_CR8","doi-asserted-by":"publisher","first-page":"1415","DOI":"10.1016\/j.ijar.2012.04.005","volume":"53","author":"A Choi","year":"2012","unstructured":"Choi, A., Xue, Y., Darwiche, A.: Same-decision probability: a confidence measure for threshold-based decisions. Int. J. Approximate Reasoning (IJAR) 53(9), 1415\u20131428 (2012)","journal-title":"Int. J. Approximate Reasoning (IJAR)"},{"key":"25_CR9","unstructured":"Courbariaux, M., Hubara, I., Soudry, D., El-Yaniv, R., Bengio, Y.: Binarized neural networks: training deep neural networks with weights and activations constrained to +1 or $$-$$ 1 (2016)"},{"key":"25_CR10","unstructured":"Darwiche, A.: SDD: a new canonical representation of propositional knowledge bases. In: Proceedings of the 22nd International Joint Conference on Artificial Intelligence (IJCAI), pp. 819\u2013826 (2011)"},{"key":"25_CR11","doi-asserted-by":"crossref","unstructured":"Darwiche, A.: Tractable knowledge representation formalisms. In: Tractability: Practical Approaches to Hard Problems, pp. 141\u2013172. Cambridge University Press (2014)","DOI":"10.1017\/CBO9781139177801.006"},{"key":"25_CR12","doi-asserted-by":"publisher","first-page":"229","DOI":"10.1613\/jair.989","volume":"17","author":"A Darwiche","year":"2002","unstructured":"Darwiche, A., Marquis, P.: A knowledge compilation map. JAIR 17, 229\u2013264 (2002)","journal-title":"JAIR"},{"key":"25_CR13","doi-asserted-by":"publisher","first-page":"191","DOI":"10.1613\/jair.2097","volume":"29","author":"J Huang","year":"2007","unstructured":"Huang, J., Darwiche, A.: The language of search. J. Artif. Intell. Res. 29, 191\u2013219 (2007)","journal-title":"J. Artif. Intell. Res."},{"key":"25_CR14","unstructured":"Hubara, I., Courbariaux, M., Soudry, D., El-Yaniv, R., Bengio, Y.: Binarized neural networks. In: Advances in Neural Information Processing Systems (NIPS), pp. 4107\u20134115 (2016)"},{"issue":"5","key":"25_CR15","doi-asserted-by":"publisher","first-page":"550","DOI":"10.1109\/34.291440","volume":"16","author":"JJ Hull","year":"1994","unstructured":"Hull, J.J.: A database for handwritten text recognition research. IEEE Trans. Pattern Anal. Mach. Intell. 16(5), 550\u2013554 (1994)","journal-title":"IEEE Trans. Pattern Anal. Mach. Intell."},{"key":"25_CR16","doi-asserted-by":"crossref","unstructured":"Ignatiev, A., Narodytska, N., Marques-Silva, J.: Abduction-based explanations for machine learning models. In: Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI) (2019)","DOI":"10.1609\/aaai.v33i01.33011511"},{"key":"25_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"99","DOI":"10.1007\/978-3-319-57288-8_7","volume-title":"NASA Formal Methods","author":"S Jha","year":"2017","unstructured":"Jha, S., Raman, V., Pinto, A., Sahai, T., Francis, M.: On learning sparse boolean formulae for explaining AI decisions. In: Barrett, C., Davies, M., Kahsai, T. (eds.) NFM 2017. LNCS, vol. 10227, pp. 99\u2013114. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-57288-8_7"},{"issue":"7","key":"25_CR18","doi-asserted-by":"publisher","first-page":"693","DOI":"10.1007\/s00236-017-0294-5","volume":"54","author":"S Jha","year":"2017","unstructured":"Jha, S., Seshia, S.A.: A theory of formal synthesis via inductive learning. Acta Informatica 54(7), 693\u2013726 (2017)","journal-title":"Acta Informatica"},{"key":"25_CR19","unstructured":"Kahlert, L., Kr\u00fcger, F., Manthey, N., Stephan, A.: Riss solver framework v5. 05 (2015)"},{"key":"25_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"97","DOI":"10.1007\/978-3-319-63387-9_5","volume-title":"Computer Aided Verification","author":"G Katz","year":"2017","unstructured":"Katz, G., Barrett, C., Dill, D.L., Julian, K., Kochenderfer, M.J.: Reluplex: an efficient SMT solver for verifying deep neural networks. In: Majumdar, R., Kun\u010dak, V. (eds.) CAV 2017. LNCS, vol. 10426, pp. 97\u2013117. Springer, Cham (2017). https:\/\/doi.org\/10.1007\/978-3-319-63387-9_5"},{"key":"25_CR21","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/3897.001.0001","volume-title":"An Introduction to Computational Learning Theory","author":"M Kearns","year":"1994","unstructured":"Kearns, M., Vazirani, U.V.: An Introduction to Computational Learning Theory. MIT Press, Cambridge (1994)"},{"key":"25_CR22","unstructured":"Koul, A., Fern, A., Greydanus, S.: Learning finite state representations of recurrent policy networks. In: Proceedings of the Seventh International Conference on Learning Representations (ICLR) (2019)"},{"key":"25_CR23","unstructured":"Leofante, F., Narodytska, N., Pulina, L., Tacchella, A.: Automated verification of neural networks: advances, challenges and perspectives. CoRR abs\/1805.09938 (2018). http:\/\/arxiv.org\/abs\/1805.09938"},{"key":"25_CR24","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-58940-9","volume-title":"Algorithms and Data Structures in VLSI Design: OBDD - Foundations and Applications","author":"C Meinel","year":"1998","unstructured":"Meinel, C., Theobald, T.: Algorithms and Data Structures in VLSI Design: OBDD - Foundations and Applications. Springer, Heidelberg (1998)"},{"issue":"2","key":"25_CR25","doi-asserted-by":"publisher","first-page":"178","DOI":"10.1016\/j.ic.2005.05.003","volume":"201","author":"A Nakamura","year":"2005","unstructured":"Nakamura, A.: An efficient query learning algorithm for ordered binary decision diagrams. Inf. Comput. 201(2), 178\u2013198 (2005)","journal-title":"Inf. Comput."},{"key":"25_CR26","doi-asserted-by":"crossref","unstructured":"Narodytska, N., Kasiviswanathan, S.P., Ryzhyk, L., Sagiv, M., Walsh, T.: Verifying properties of binarized deep neural networks. In: Proceedings of the Thirty-Second AAAI Conference on Artificial Intelligence (AAAI) (2018)","DOI":"10.1609\/aaai.v32i1.12206"},{"key":"25_CR27","unstructured":"Oztok, U., Darwiche, A.: A top-down compiler for sentential decision diagrams. In: Proceedings of the 24th International Joint Conference on Artificial Intelligence (IJCAI), pp. 3141\u20133148 (2015)"},{"key":"25_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"243","DOI":"10.1007\/978-3-642-14295-6_24","volume-title":"Computer Aided Verification","author":"L Pulina","year":"2010","unstructured":"Pulina, L., Tacchella, A.: An abstraction-refinement approach to verification of artificial neural networks. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 243\u2013257. Springer, Heidelberg (2010). https:\/\/doi.org\/10.1007\/978-3-642-14295-6_24"},{"issue":"2","key":"25_CR29","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1145\/226643.226644","volume":"43","author":"B Selman","year":"1996","unstructured":"Selman, B., Kautz, H.A.: Knowledge compilation and theory approximation. J. ACM 43(2), 193\u2013224 (1996)","journal-title":"J. ACM"},{"key":"25_CR30","unstructured":"Shih, A., Choi, A., Darwiche, A.: Formal verification of Bayesian network classifiers. In: Proceedings of the 9th International Conference on Probabilistic Graphical Models (PGM) (2018)"},{"key":"25_CR31","doi-asserted-by":"crossref","unstructured":"Shih, A., Choi, A., Darwiche, A.: A symbolic approach to explaining Bayesian network classifiers. In: Proceedings of the 27th International Joint Conference on Artificial Intelligence (IJCAI) (2018)","DOI":"10.24963\/ijcai.2018\/708"},{"key":"25_CR32","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-1-4899-5327-8_25","volume-title":"Studies in Constructive Mathematics and Mathematical Logic Part 2","author":"G. S. Tseitin","year":"1970","unstructured":"Tseitin, G.: On the complexity of derivation in propositional calculus. In: Studies in Constructive Mathematics and Mathematical Logic, pp. 115\u2013125 (1968)"},{"key":"25_CR33","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898719789","volume-title":"Branching Programs and Binary Decision Diagrams","author":"I Wegener","year":"2000","unstructured":"Wegener, I.: Branching Programs and Binary Decision Diagrams. SIAM, Philadelphia (2000)"},{"key":"25_CR34","unstructured":"Weiss, G., Goldberg, Y., Yahav, E.: Extracting automata from recurrent neural networks using queries and counterexamples. In: Proceedings of the 35th International Conference on Machine Learning (ICML), pp. 5244\u20135253 (2018)"},{"key":"25_CR35","unstructured":"Weng, T.W., et al.: Towards fast computation of certified robustness for ReLU networks. In: Proceedings of the Thirty-Fifth International Conference on Machine Learning (ICML) (2018)"},{"key":"25_CR36","doi-asserted-by":"crossref","unstructured":"Zhang, H., Zhang, P., Hsieh, C.J.: RecurJac: an efficient recursive algorithm for bounding jacobian matrix of general neural networks and its applications. In: Proceedings of the Thirty-Third AAAI Conference on Artificial Intelligence (AAAI) (2019)","DOI":"10.1609\/aaai.v33i01.33015757"}],"container-title":["Lecture Notes in Computer Science","Theory and Applications of Satisfiability Testing \u2013 SAT 2019"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-24258-9_25","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,9,22]],"date-time":"2022-09-22T10:33:56Z","timestamp":1663842836000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-24258-9_25"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030242572","9783030242589"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-24258-9_25","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"29 June 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"SAT","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Theory and Applications of Satisfiability Testing","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Lisbon","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 July 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"12 July 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"22","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"sat2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/sat2019.tecnico.ulisboa.pt\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"64","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"19","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"7","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}