{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,13]],"date-time":"2026-04-13T10:48:09Z","timestamp":1776077289421,"version":"3.50.1"},"reference-count":30,"publisher":"Oxford University Press (OUP)","issue":"5","license":[{"start":{"date-parts":[[2022,6,10]],"date-time":"2022-06-10T00:00:00Z","timestamp":1654819200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/academic.oup.com\/journals\/pages\/open_access\/funder_policies\/chorus\/standard_publication_model"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2023,9,25]]},"abstract":"<jats:title>Abstract<\/jats:title>\n               <jats:p>Neural networks are widely used in systems of artificial intelligence, but due to their black box nature, they have so far evaded formal analysis to certify that they satisfy desirable properties, mainly when they perform critical tasks. In this work, we introduce methods for the formal analysis of reachability and robustness of neural networks that are modeled as rational McNaughton functions by, first, stating such properties in the language of \u0141ukasiewicz infinitely-valued logic and, then, using the reasoning techniques of such logical system. We also present a case study where we employ the proposed techniques in an actual neural network that we trained to predict whether it will rain tomorrow in Australia.<\/jats:p>","DOI":"10.1093\/jigpal\/jzac050","type":"journal-article","created":{"date-parts":[[2022,4,26]],"date-time":"2022-04-26T12:30:04Z","timestamp":1650976204000},"page":"805-821","source":"Crossref","is-referenced-by-count":8,"title":["Proving properties of binary classification neural networks via \u0141ukasiewicz logic"],"prefix":"10.1093","volume":"31","author":[{"given":"Sandro","family":"Preto","sequence":"first","affiliation":[{"name":"Institute of Mathematics and Statistics, University of S\u00e3o Paulo , Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marcelo","family":"Finger","sequence":"additional","affiliation":[{"name":"Institute of Mathematics and Statistics, University of S\u00e3o Paulo , Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"286","published-online":{"date-parts":[[2022,6,10]]},"reference":[{"key":"2023092607151071200_ref1","doi-asserted-by":"crossref","first-page":"5","DOI":"10.1023\/A:1008311022292","article-title":"Finiteness in infinite-valued \u0141ukasiewicz logic","volume":"9","author":"Aguzzoli","year":"2000","journal-title":"Journal of Logic, Language and Information"},{"key":"2023092607151071200_ref2","doi-asserted-by":"crossref","first-page":"361","DOI":"10.1109\/ISMVL.2001.924596","article-title":"Weierstrass approximations by \u0141ukasiewicz formulas with one quantified variable","volume-title":"Proceedings of the 31st IEEE International Symposium on Multiple-Valued Logic","author":"Aguzzoli","year":"2001"},{"key":"2023092607151071200_ref3","first-page":"315","volume-title":"Weierstrass Approximation Theorem and \u0141ukasiewicz Formulas With One Quantified Variable","author":"Aguzzoli","year":"2003"},{"key":"2023092607151071200_ref4","first-page":"777","article-title":"An algorithm for the automatic generation of a logical formula representing a control law","volume":"10","author":"Amato","year":"2000","journal-title":"Neural Network World"},{"key":"2023092607151071200_ref5","doi-asserted-by":"crossref","first-page":"506","DOI":"10.1109\/NAFIPS.2002.1018111","article-title":"Neural networks and rational \u0141ukasiewicz logic","volume-title":"2002 Annual Meeting of the North American Fuzzy Information Processing Society Proceedings. NAFIPS-FLINT 2002 (Cat. No. 02TH8622)","author":"Amato","year":"2002"},{"key":"2023092607151071200_ref6","doi-asserted-by":"crossref","first-page":"25","DOI":"10.1109\/ISMVL.2012.63","article-title":"Building automated theorem provers for infinitely-valued logics with satisfiability modulo theory solvers","volume-title":"2012 IEEE 42nd International Symposium on Multiple-Valued Logic","author":"Ans\u00f3tegui","year":"2012"},{"key":"2023092607151071200_ref7","volume-title":"Adversarial training and provable defenses: bridging the gap","author":"Balunovic","year":"2020"},{"key":"2023092607151071200_ref8","volume-title":"The satisfiability modulo theories library (SMT-LIB)","author":"Barrett","year":"2016"},{"key":"2023092607151071200_ref9","volume-title":"Introduction to linear optimization","author":"Bertsimas","year":"1997"},{"key":"2023092607151071200_ref10","doi-asserted-by":"crossref","first-page":"30","DOI":"10.1109\/ISMVL.2015.10","article-title":"Finding hard instances of satisfiability in \u0141ukasiewicz logics","volume-title":"Multiple-Valued Logic (ISMVL), 2015 IEEE International Symposium on","author":"Bofill","year":"2015"},{"key":"2023092607151071200_ref11","doi-asserted-by":"crossref","first-page":"20","DOI":"10.1038\/538020a","article-title":"Can we open the black box of AI?","volume":"538","author":"Castelvecchi","year":"2016","journal-title":"Nature"},{"key":"2023092607151071200_ref12","doi-asserted-by":"crossref","DOI":"10.1007\/978-94-015-9480-6","volume-title":"Algebraic Foundations of Many-Valued Reasoning","author":"Cignoli","year":"2000"},{"key":"2023092607151071200_ref13","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1007\/978-3-319-33747-0_16","article-title":"\u0141ukasiewicz equivalent neural networks","volume-title":"Advances in Neural Networks","author":"Di Nola","year":"2016"},{"key":"2023092607151071200_ref14","doi-asserted-by":"crossref","first-page":"737","DOI":"10.1007\/978-3-319-08867-9_49","article-title":"Yices 2.2","volume-title":"Computer-Aided Verification (CAV\u20192014)","author":"Dutertre","year":"2014"},{"key":"2023092607151071200_ref15","first-page":"184","article-title":"Logic in times of big data","volume-title":"A True Polymath: A Tribute to Francisco Antonio Doria","author":"Finger","year":"2020"},{"key":"2023092607151071200_ref16","doi-asserted-by":"crossref","first-page":"194","DOI":"10.1007\/978-3-319-94205-6_14","article-title":"Probably half true: probabilistic satisfiability over \u0141ukasiewicz infinitely-valued logic","volume-title":"Automated Reasoning","author":"Finger","year":"2018"},{"key":"2023092607151071200_ref17","doi-asserted-by":"crossref","first-page":"1269","DOI":"10.1007\/s10817-020-09558-9","article-title":"Probably partially true: satisfiability for \u0141ukasiewicz infinitely-valued probabilistic logic and related topics","volume":"64","author":"Finger","year":"2020","journal-title":"Journal of Automated Reasoning"},{"key":"2023092607151071200_ref18","volume-title":"The SCIP optimization suite 7.0","author":"Gamrath","year":"2020"},{"key":"2023092607151071200_ref19","volume-title":"Deep Learning","author":"Goodfellow","year":"2016"},{"key":"2023092607151071200_ref20","volume-title":"Reluplex: An Efficient SMT Solver for Verifying Deep Neural Networks","author":"Katz","year":"2017"},{"key":"2023092607151071200_ref21","doi-asserted-by":"crossref","first-page":"443","DOI":"10.1007\/978-3-030-25540-4_26","article-title":"The marabou framework for verification and analysis of deep neural networks","volume-title":"Computer Aided Verification: 31st International Conference, CAV 2019, New York City, NY, USA, July 15\u201318, 2019, Proceedings, Part I","author":"Katz","year":"2019"},{"key":"2023092607151071200_ref22","doi-asserted-by":"crossref","first-page":"861","DOI":"10.1016\/S0893-6080(05)80131-5","article-title":"Multilayer feedforward networks with a nonpolynomial activation function can approximate any function","volume":"6","author":"Leshno","year":"1993","journal-title":"Neural Networks"},{"key":"2023092607151071200_ref23","article-title":"Neural network branching for neural network verification","volume-title":"International Conference on Learning Representations","author":"Jingyue,","year":"2020"},{"key":"2023092607151071200_ref24","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2307\/2268660","article-title":"A theorem about infinite-valued sentential logic","volume":"16","author":"McNaughton","year":"1951","journal-title":"Journal of Symbolic Logic"},{"key":"2023092607151071200_ref25","doi-asserted-by":"crossref","first-page":"145","DOI":"10.1016\/0304-3975(87)90083-1","article-title":"Satisfiability in many-valued sentential logic is NP-complete","volume":"52","author":"Mundici","year":"1987","journal-title":"Theoretical Computer Science"},{"key":"2023092607151071200_ref26","doi-asserted-by":"crossref","first-page":"596","DOI":"10.2307\/2275410","article-title":"A constructive proof of McNaughton\u2019s theorem in infinite-valued logic","volume":"59","author":"Mundici","year":"1994","journal-title":"The Journal of Symbolic Logic"},{"key":"2023092607151071200_ref27","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1016\/j.entcs.2020.08.009","article-title":"An efficient algorithm for representing piecewise linear functions into logic","volume":"351","author":"Preto,","year":"2020","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"2023092607151071200_ref28","doi-asserted-by":"crossref","DOI":"10.1017\/S096012952200010X","article-title":"Efficient representation of piecewise linear functions into \u0141ukasiewicz logic modulo satisfiability","author":"Preto","year":"2022","journal-title":"Mathematical Structures in Computer Science"},{"key":"2023092607151071200_ref29","doi-asserted-by":"crossref","first-page":"109","DOI":"10.1007\/s10898-020-00949-1","article-title":"Advances in verification of relu neural networks","volume":"81","author":"R\u00f6ssig","year":"2021","journal-title":"Journal of Global Optimization"},{"key":"2023092607151071200_ref30","article-title":"Intriguing\nproperties of neural networks","volume-title":"2nd International Conference on Learning Representations, ICLR 2014, Banff, AB, Canada, April 14\u201316, 2014, Conference Track Proceedings","author":"Szegedy","year":"2014"}],"container-title":["Logic Journal of the IGPL"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/31\/5\/805\/51754079\/jzac050.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/academic.oup.com\/jigpal\/article-pdf\/31\/5\/805\/51754079\/jzac050.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,9,26]],"date-time":"2023-09-26T07:15:47Z","timestamp":1695712547000},"score":1,"resource":{"primary":{"URL":"https:\/\/academic.oup.com\/jigpal\/article\/31\/5\/805\/6603904"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,6,10]]},"references-count":30,"journal-issue":{"issue":"5","published-online":{"date-parts":[[2022,6,10]]},"published-print":{"date-parts":[[2023,9,25]]}},"URL":"https:\/\/doi.org\/10.1093\/jigpal\/jzac050","relation":{},"ISSN":["1367-0751","1368-9894"],"issn-type":[{"value":"1367-0751","type":"print"},{"value":"1368-9894","type":"electronic"}],"subject":[],"published-other":{"date-parts":[[2023,10]]},"published":{"date-parts":[[2022,6,10]]}}}