乐胖代购免代理版

{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,12]],"date-time":"2024-09-12T00:16:42Z","timestamp":1726100202983},"reference-count":57,"publisher":"Springer Science and Business Media LLC","issue":"1","license":[{"start":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T00:00:00Z","timestamp":1636416000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T00:00:00Z","timestamp":1636416000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/100000185","name":"defense advanced research projects agency","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100000185","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000287","name":"royal academy of engineering","doi-asserted-by":"crossref","id":[{"id":"10.13039\/501100000287","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Auton Agent Multi-Agent Syst"],"published-print":{"date-parts":[[2022,4]]},"abstract":"Abstract<\/jats:title>We introduce a model for agent-environment systems where the agents are implemented via feed-forward ReLU neural networks and the environment is non-deterministic. We study the verification problem of such systems against CTL properties. We show that verifying these systems against reachability properties is undecidable. We introduce a bounded fragment of CTL, show its usefulness in identifying shallow bugs in the system, and prove that the verification problem against specifications in bounded CTL is in coNExpTime<\/jats:sc>andPSpace<\/jats:sc>-hard. We introduce sequential and parallel algorithms for MILP-based verification of agent-environment systems, present an implementation, and report the experimental results obtained against a variant of the VerticalCAS use-case and the frozen lake scenario.<\/jats:p>","DOI":"10.1007\/s10458-021-09529-3","type":"journal-article","created":{"date-parts":[[2021,11,9]],"date-time":"2021-11-09T06:08:56Z","timestamp":1636438136000},"update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":11,"title":["Formal verification of neural agents in non-deterministic environments"],"prefix":"10.1007","volume":"36","author":[{"given":"Michael E.","family":"Akintunde","sequence":"first","affiliation":[]},{"given":"Elena","family":"Botoeva","sequence":"additional","affiliation":[]},{"given":"Panagiotis","family":"Kouvaros","sequence":"additional","affiliation":[]},{"ORCID":"http:\/\/orcid.org\/0000-0003-3420-723X","authenticated-orcid":false,"given":"Alessio","family":"Lomuscio","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,11,9]]},"reference":[{"key":"9529_CR1","unstructured":"Akintunde, M., Botoeva, E., Kouvaros, P., & Lomuscio, A. (2020). Formal verification of neural agents in non-deterministic environments. In Proceedings of the 19th international conference on autonomous agents and multi-agent systems (AAMAS20) (pp. 25\u201333). IFAAMAS."},{"key":"9529_CR2","doi-asserted-by":"crossref","unstructured":"Akintunde, M., Kevorchian, A., Lomuscio, A., & Pirovano, E. (2019). Verification of RNN-based neural agent-environment systems. In Proceedings of the 33rd AAAI conference on artificial intelligence (AAAI19) (pp. 6006\u20136013). AAAI Press.","DOI":"10.1609\/aaai.v33i01.33016006"},{"key":"9529_CR3","unstructured":"Akintunde, M., Lomuscio, A., Maganti, L., & Pirovano, E. (2018). Reachability analysis for neural agent-environment systems. In Proceedings of the 16th international conference on principles of knowledge representation and reasoning (KR18) (pp. 184\u2013193). AAAI Press."},{"key":"9529_CR4","doi-asserted-by":"crossref","unstructured":"Anderson, R., Huchette, J., Ma, W., Tjandraatmadja, C., & Vielma, J. (2020). Strong mixed-integer programming formulations for trained neural networks. Mathematical Programming pp. 1\u201337.","DOI":"10.1007\/s10107-020-01474-5"},{"key":"9529_CR5","unstructured":"Bastani, O., Ioannou, Y., Lampropoulos, L., Vytiniotis, D., Nori, A., & Criminisi, A. (2016). Measuring neural net robustness with constraints. In Proceedings of the 30th international conference on neural information processing systems (NIPS16) (pp. 2613\u20132621)."},{"key":"9529_CR6","doi-asserted-by":"crossref","unstructured":"Battern, B., Kouvaros, P., Lomuscio, A., & Y. Zheng. (2021). Efficient neural network verification via layer-based semidefinite relaxations and linear cuts. In Proceedings of the 30th international joint conference on artificial intelligence (IJCAI21). To Appear. ijcai.org.","DOI":"10.24963\/ijcai.2021\/301"},{"key":"9529_CR7","doi-asserted-by":"crossref","unstructured":"Biere, A., Cimatti, A., Clarke, E., Strichman, O., & Zhu, Y. (2003). Bounded model checking. In Highly dependable software. Advances in computers (Vol.\u00a058). Academic Press. Pre-print.","DOI":"10.1016\/S0065-2458(03)58003-2"},{"issue":"2","key":"9529_CR8","doi-asserted-by":"publisher","first-page":"239","DOI":"10.1007\/s10458-006-5955-7","volume":"12","author":"R Bordini","year":"2006","unstructured":"Bordini, R., Fisher, M., Visser, W., & Wooldridge, M. (2006). Verifying multi-agent programs by model checking. Autonomous Agents and Multi-Agent Systems, 12(2), 239\u2013256.","journal-title":"Autonomous Agents and Multi-Agent Systems"},{"key":"9529_CR9","doi-asserted-by":"crossref","unstructured":"Botoeva, E., Kouvaros, P., Kronqvist, J., Lomuscio, A., & Misener, R. (2020). Efficient verification of neural networks via dependency analysis. In Proceedings of the 34th AAAI conference on artificial intelligence (AAAI20) (pp. 3291\u20133299). AAAI Press.","DOI":"10.1609\/aaai.v34i04.5729"},{"issue":"42","key":"9529_CR10","first-page":"1","volume":"21","author":"R Bunel","year":"2020","unstructured":"Bunel, R., Lu, J., Turkaslan, I., Kohli, P., Torr, P., & Mudigonda, P. (2020). Branch and bound for piecewise linear neural network verification. Journal of Machine Learning Research, 21(42), 1\u201339.","journal-title":"Journal of Machine Learning Research"},{"key":"9529_CR11","doi-asserted-by":"crossref","unstructured":"Cheng, C., N\u00fchrenberg, G., & Ruess, H. (2017). Maximum resilience of artificial neural networks. In International symposium on automated technology for verification and analysis (ATVA17) (pp. 251\u2013268). Springer.","DOI":"10.1007\/978-3-319-68167-2_18"},{"issue":"1","key":"9529_CR12","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1023\/A:1011276507260","volume":"19","author":"E Clarke","year":"2001","unstructured":"Clarke, E., Biere, A., Raimi, R., & Zhu, Y. (2001). Bounded model checking using satisfiability solving. Formal Methods in System Design, 19(1), 7\u201334.","journal-title":"Formal Methods in System Design"},{"key":"9529_CR13","volume-title":"Model checking","author":"E Clarke","year":"1999","unstructured":"Clarke, E., Grumberg, O., & Peled, D. (1999). Model checking. The MIT Press."},{"key":"9529_CR14","unstructured":"Doan, T., Yao, Y., Alechina, N., & Logan, B. (2014). Verifying heterogeneous multi-agent programs. In Proceedings of the 13th international conference on autonomous agents and multi-agent systems (AAMAS14) (pp. 149\u2013156)."},{"key":"9529_CR15","doi-asserted-by":"crossref","unstructured":"Dutta, S., Chen, X., & Sankaranarayanan, S. (2019). Reachability analysis for neural feedback systems using regressive polynomial rule inference. In Proceedings of the 22nd ACM international conference on hybrid systems: Computation and control (HSCC19) (pp. 157\u2013168). ACM.","DOI":"10.1145\/3302504.3311807"},{"key":"9529_CR16","unstructured":"Dvijotham, K., Stanforth, R., Gowal, S., Mann, T., & Kohli, P. (2018). A dual approach to scalable verification of deep networks. arXiv preprint arXiv:1803.06567."},{"key":"9529_CR17","doi-asserted-by":"crossref","unstructured":"Ehlers, R. (2017). Formal verification of piece-wise linear feed-forward neural networks. In Proceedings of the 15th international symposium on automated technology for verification and analysis (ATVA17). Lecture notes in computer science (Vol. 10482, pp. 269\u2013286). Springer.","DOI":"10.1007\/978-3-319-68167-2_19"},{"issue":"4","key":"9529_CR18","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/BF00355298","volume":"4","author":"E Emerson","year":"1992","unstructured":"Emerson, E., Mok, A., Sistla, A., & Srinivasan, J. (1992). Quantitative temporal reasoning. Real-Time Systems, 4(4), 331\u2013352.","journal-title":"Real-Time Systems"},{"key":"9529_CR19","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/5803.001.0001","volume-title":"Reasoning about knowledge","author":"R Fagin","year":"1995","unstructured":"Fagin, R., Halpern, J., Moses, Y., & Vardi, M. (1995). Reasoning about knowledge. MIT Press."},{"key":"9529_CR20","doi-asserted-by":"crossref","unstructured":"Gammie, P., & van\u00a0der Meyden, R. (2004). MCK: Model checking the logic of knowledge. In Proceedings of 16th international conference on computer aided verification (CAV04). Lecture notes in computer science (Vol. 3114, pp. 479\u2013483). Springer.","DOI":"10.1007\/978-3-540-27813-9_41"},{"key":"9529_CR21","volume-title":"Deep learning","author":"A Goodfellow","year":"2016","unstructured":"Goodfellow, A., Bengio, Y., & Courville, A. (2016). Deep learning (Vol. 1). Cambridge: MIT press."},{"key":"9529_CR22","doi-asserted-by":"publisher","DOI":"10.1137\/1.9780898717730","volume-title":"Linear and nonlinear optimization","author":"I Griva","year":"2009","unstructured":"Griva, I., Nash, S., & Sofer, A. (2009). Linear and nonlinear optimization (Vol. 108). Siam."},{"key":"9529_CR23","unstructured":"Gu, Z., Rothberg, E., & Bixby, R. (2020). Gurobi optimizer reference manual. http:\/\/www.gurobi.com"},{"issue":"5","key":"9529_CR24","doi-asserted-by":"publisher","first-page":"93:1","DOI":"10.1145\/3236009","volume":"51","author":"R Guidotti","year":"2019","unstructured":"Guidotti, R., Monreale, A., Ruggieri, S., Turini, F., Giannotti, F., & Pedreschi, D. (2019). A survey of methods for explaining black box models. ACM Computing Surveys, 51(5), 93:1-93:42.","journal-title":"ACM Computing Surveys"},{"key":"9529_CR25","volume-title":"Neural networks: A comprehensive foundation","author":"S Haykin","year":"1999","unstructured":"Haykin, S. (1999). Neural networks: A comprehensive foundation. Prentice Hall."},{"key":"9529_CR26","unstructured":"Henriksen, P., & Lomuscio, A. (2020). Efficient neural network verification via adaptive refinement and adversarial search. In Proceedings of the 24th European conference on artificial intelligence (ECAI20) (pp. 2513\u20132520). IOS Press."},{"key":"9529_CR27","doi-asserted-by":"crossref","unstructured":"Henriksen, P., & Lomuscio, A. (2021). DEEPSPLIT: An efficient splitting method for neural network verification via indirect effect analysis. In Proceedings of the 30th international joint conference on artificial intelligence (IJCAI21). To Appear. ijcai.org.","DOI":"10.24963\/ijcai.2021\/351"},{"issue":"106","key":"9529_CR28","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3358228","volume":"18","author":"C Huang","year":"2019","unstructured":"Huang, C., Fan, J., Li, W., Chen, X., & Zhu, Q. (2019). ReachNN: Reachability analysis of neural-network controlled systems. ACM Transactions on Embedded Computing Systems (TECS), 18(106), 1\u201322.","journal-title":"ACM Transactions on Embedded Computing Systems (TECS)"},{"key":"9529_CR29","doi-asserted-by":"publisher","first-page":"100270","DOI":"10.1016\/j.cosrev.2020.100270","volume":"37","author":"X Huang","year":"2020","unstructured":"Huang, X., Kroening, D., Ruan, W., Sharp, J., Sun, Y., Thamo, E., Wu, M., & Yi, X. (2020). A survey of safety and trustworthiness of deep neural networks: Verification, testing, adversarial attack and defence, and interpretability. Computer Science Reviews, 37, 100270.","journal-title":"Computer Science Reviews"},{"issue":"6","key":"9529_CR30","doi-asserted-by":"publisher","first-page":"1083","DOI":"10.1016\/0005-1098(92)90053-I","volume":"28","author":"K Hunt","year":"1992","unstructured":"Hunt, K., Sbarbaro, D., Zbikowski, R., & Gawthrop, P. (1992). Neural networks for control systems: A survey. Automatica, 28(6), 1083\u20131112.","journal-title":"Automatica"},{"key":"9529_CR31","doi-asserted-by":"crossref","unstructured":"Ivanov, R., Weimer, J., Alur, R., Pappas, G., & Lee, I. (2019). Verisig: Verifying safety properties of hybrid systems with neural network controllers. In Proceedings of the 22nd ACM international conference on hybrid systems: Computation and control (HSCC19) (pp. 169\u2013178).","DOI":"10.1145\/3302504.3311806"},{"key":"9529_CR32","unstructured":"Julian, K., & Kochenderfer, M. (2019). A reachability method for verifying dynamical systems with deep neural network controllers. arXiv preprint arXiv:1903.00520."},{"key":"9529_CR33","doi-asserted-by":"crossref","unstructured":"Julian, K., Lopez, J., Brush, J., Owen, M., & Kochenderfer, M. (2016). Policy compression for aircraft collision avoidance systems. In Proceedings of the 35th digital avionics systems conference (DASC16) (pp. 1\u201310).","DOI":"10.1109\/DASC.2016.7778091"},{"key":"9529_CR34","doi-asserted-by":"crossref","unstructured":"Katz, G., Barrett, C., Dill, D., Julian, K., & Kochenderfer, M. (2017). Reluplex: An efficient SMT solver for verifying deep neural networks. In Proceedings of the 29th international conference on computer aided verification (CAV17). Lecture notes in computer science (Vol. 10426, pp. 97\u2013117). Springer.","DOI":"10.1007\/978-3-319-63387-9_5"},{"key":"9529_CR35","doi-asserted-by":"publisher","first-page":"152","DOI":"10.1016\/j.artint.2016.01.008","volume":"234","author":"P Kouvaros","year":"2016","unstructured":"Kouvaros, P., & Lomuscio, A. (2016). Parameterised verification for multi-agent systems. Artificial Intelligence, 234, 152\u2013189.","journal-title":"Artificial Intelligence"},{"key":"9529_CR36","unstructured":"Kouvaros, P., & Lomuscio, A. (2018). Formal verification of cnn-based perception systems. arXiv preprint arXiv:1811.11373."},{"key":"9529_CR37","doi-asserted-by":"crossref","unstructured":"Kouvaros, P., & Lomuscio, A. (2021). Towards scalable complete verification of relu neural networks via dependency-based branching. In Proceedings of the 30th international joint conference on artificial intelligence (IJCAI21). To Appear. ijcai.org.","DOI":"10.24963\/ijcai.2021\/364"},{"key":"9529_CR38","unstructured":"Krizhevsky, A., Sutskever, I., & Hinton, G. (2012). Imagenet classification with deep convolutional neural networks. In Proceedings of the 25th international conference on neural information processing systems (NIPS12) (pp. 1097\u20131105). Curran Associates, Inc."},{"key":"9529_CR39","unstructured":"Liu, C., Arnon, T., Lazaru, C., Barrett, C., & Kochenderfer, M. (2019). Algorithms for verifying deep neural networks. arXiv preprint arXiv:1903.06758."},{"key":"9529_CR40","unstructured":"Lomuscio, A., & Maganti, L. (2017). An approach to reachability analysis for feed-forward relu neural networks. arXiv:1706.07351."},{"issue":"1","key":"9529_CR41","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-015-0378-x","volume":"19","author":"A Lomuscio","year":"2017","unstructured":"Lomuscio, A., Qu, H., & Raimondi, F. (2017). MCMAS: A model checker for the verification of multi-agent systems. Software Tools for Technology Transfer, 19(1), 9\u201330.","journal-title":"Software Tools for Technology Transfer"},{"issue":"1\u20132","key":"9529_CR42","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1162\/artl.1993.1.1_2.135","volume":"1","author":"P Maes","year":"1993","unstructured":"Maes, P. (1993). Modeling adaptive autonomous agents. Artificial Life, 1(1\u20132), 135\u2013162.","journal-title":"Artificial Life"},{"key":"9529_CR43","unstructured":"Nair, V., & Hinton, G. (2010). Rectified linear units improve restricted Boltzmann machines. In Proceedings of the 27th international conference on machine learning (ICML10) (pp. 807\u2013814). Omnipress."},{"key":"9529_CR44","doi-asserted-by":"crossref","unstructured":"Narodytska, N. (2018). Formal analysis of deep binarized neural networks. In Proceedings of the 27th international joint conference on artificial intelligence, (IJCAI18) (pp. 5692\u20135696).","DOI":"10.24963\/ijcai.2018\/811"},{"key":"9529_CR45","unstructured":"OpenAI: Frozenlake-v0. https:\/\/gym.openai.com\/envs\/FrozenLake-v0\/ (2019)."},{"key":"9529_CR46","volume-title":"Combinatorial optimization: Algorithms and omplexity","author":"CH Papadimitriou","year":"1982","unstructured":"Papadimitriou, C. H., & Steiglitz, K. (1982). Combinatorial optimization: Algorithms and omplexity. Prentice-Hall Inc."},{"issue":"2","key":"9529_CR47","first-page":"167","volume":"55","author":"W Penczek","year":"2003","unstructured":"Penczek, W., & Lomuscio, A. (2003). Verifying epistemic properties of multi-agent systems via bounded model checking. Fundamenta Informaticae, 55(2), 167\u2013185.","journal-title":"Fundamenta Informaticae"},{"key":"9529_CR48","doi-asserted-by":"crossref","unstructured":"Redmon, J., Divvala, S., Girshick, R., & Farhadi, A. (2016). You only look once: Unified, real-time object detection. In Proceedings of the IEEE conference on computer vision and pattern recognition (CVPR16) (pp. 779\u2013788).","DOI":"10.1109\/CVPR.2016.91"},{"issue":"1","key":"9529_CR49","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1006\/jcss.1995.1013","volume":"50","author":"H Siegelmann","year":"1995","unstructured":"Siegelmann, H., & Sontag, E. (1995). On the computational power of neural nets. Journal of Computer and System Sciences, 50(1), 132\u2013150.","journal-title":"Journal of Computer and System Sciences"},{"key":"9529_CR50","doi-asserted-by":"crossref","unstructured":"Singh, G., Gehr, T., P\u00fcschel, M., & Vechev, P. (2019). An abstract domain for certifying neural networks. In ACM on programming languages (Vol.\u00a03, pp. 1\u201330). ACM Press.","DOI":"10.1145\/3290354"},{"key":"9529_CR51","volume-title":"Reinforcement learning: An introduction","author":"R Sutton","year":"1998","unstructured":"Sutton, R., & Barto, A. (1998). Reinforcement learning: An introduction. MIT Press."},{"key":"9529_CR52","unstructured":"Szegedy, C., Zaremba, W., Sutskever, I., Bruna, J., Erhan, D., Goodfellow, I., & Fergus, R. (2014). Intriguing properties of neural networks. In Proceedings of the 2nd international conference on learning representations (ICLR14)."},{"key":"9529_CR53","unstructured":"Tjeng, V., Xiao, K., & Tedrake, R. (2019). Evaluating robustness of neural networks with mixed integer programming. In Proceedings of the 7th international conference on learning representations (ICLR19)."},{"key":"9529_CR54","unstructured":"VENMAS: VErification of Neural Multi-Agent Systems. https:\/\/vas.doc.ic.ac.uk\/software\/neural (2020)."},{"key":"9529_CR55","unstructured":"Wang, S., Pei, K., Whitehouse, J., Yang, J., & Jana, S. (2018). Efficient formal safety analysis of neural networks. In Advances in neural information processing systems (NeurIPS18) (pp. 6367\u20136377)."},{"key":"9529_CR56","volume-title":"Operations research: Applications and algorithms","author":"W Winston","year":"1987","unstructured":"Winston, W. (1987). Operations research: Applications and algorithms. Duxbury Press."},{"key":"9529_CR57","doi-asserted-by":"crossref","unstructured":"Xiang, W., H., Rosenfeld, J., & Johnson, T. (2018). Reachable set estimation and safety verification for piecewise linear systems with neural network controllers. In 2018 Annual American control conference (ACC) (pp. 1574\u20131579). AACC.","DOI":"10.23919\/ACC.2018.8431048"}],"container-title":["Autonomous Agents and Multi-Agent Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-021-09529-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s10458-021-09529-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s10458-021-09529-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T20:07:21Z","timestamp":1726085241000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s10458-021-09529-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,11,9]]},"references-count":57,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2022,4]]}},"alternative-id":["9529"],"URL":"https:\/\/doi.org\/10.1007\/s10458-021-09529-3","relation":{},"ISSN":["1387-2532","1573-7454"],"issn-type":[{"type":"print","value":"1387-2532"},{"type":"electronic","value":"1573-7454"}],"subject":[],"published":{"date-parts":[[2021,11,9]]},"assertion":[{"value":"14 August 2021","order":1,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"9 November 2021","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}],"article-number":"6"}}