[{"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"publisher":"Association for the Advancement of Artificial Intelligence","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","ec_funded":1,"publication":"Proceedings of the 37th AAAI Conference on Artificial Intelligence","day":"26","author":[{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","last_name":"Zikelic","first_name":"Dorde"},{"first_name":"Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias"},{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"first_name":"Krishnendu","last_name":"Chatterjee","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X","full_name":"Chatterjee, Krishnendu"}],"arxiv":1,"title":"Learning control policies for stochastic systems with reach-avoid guarantees","project":[{"grant_number":"101020093","name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020"},{"name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020","grant_number":"863818"},{"grant_number":"665385","name":"International IST Doctoral Program","call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425"}],"issue":"10","language":[{"iso":"eng"}],"keyword":["General Medicine"],"conference":{"end_date":"2023-02-14","name":"AAAI: Conference on Artificial Intelligence","location":"Washington, DC, United States","start_date":"2023-02-07"},"publication_identifier":{"eissn":["2374-3468"],"issn":["2159-5399"]},"quality_controlled":"1","doi":"10.1609/aaai.v37i10.26407","year":"2023","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.","_id":"14830","type":"conference","oa_version":"Preprint","month":"06","abstract":[{"lang":"eng","text":"We study the problem of learning controllers for discrete-time non-linear stochastic dynamical systems with formal reach-avoid guarantees. This work presents the first method for providing formal reach-avoid guarantees, which combine and generalize stability and safety guarantees, with a tolerable probability threshold p in [0,1] over the infinite time horizon. Our method leverages advances in machine learning literature and it represents formal certificates as neural networks. In particular, we learn a certificate in the form of a reach-avoid supermartingale (RASM), a novel notion that we introduce in this work. Our RASMs provide reachability and avoidance guarantees by imposing constraints on what can be viewed as a stochastic extension of level sets of Lyapunov functions for deterministic systems. Our approach solves several important problems -- it can be used to learn a control policy from scratch, to verify a reach-avoid specification for a fixed control policy, or to fine-tune a pre-trained policy if it does not satisfy the reach-avoid specification. We validate our approach on 3 stochastic non-linear reinforcement learning tasks."}],"date_updated":"2025-07-14T09:10:02Z","page":"11926-11935","date_created":"2024-01-18T07:44:31Z","volume":37,"status":"public","external_id":{"arxiv":["2210.05308"]},"citation":{"apa":"Zikelic, D., Lechner, M., Henzinger, T. A., &#38; Chatterjee, K. (2023). Learning control policies for stochastic systems with reach-avoid guarantees. In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i> (Vol. 37, pp. 11926–11935). Washington, DC, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">https://doi.org/10.1609/aaai.v37i10.26407</a>","ista":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. 2023. Learning control policies for stochastic systems with reach-avoid guarantees. Proceedings of the 37th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 37, 11926–11935.","mla":"Zikelic, Dorde, et al. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, vol. 37, no. 10, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–35, doi:<a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">10.1609/aaai.v37i10.26407</a>.","ama":"Zikelic D, Lechner M, Henzinger TA, Chatterjee K. Learning control policies for stochastic systems with reach-avoid guarantees. In: <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>. Vol 37. Association for the Advancement of Artificial Intelligence; 2023:11926-11935. doi:<a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">10.1609/aaai.v37i10.26407</a>","short":"D. Zikelic, M. Lechner, T.A. Henzinger, K. Chatterjee, in:, Proceedings of the 37th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2023, pp. 11926–11935.","chicago":"Zikelic, Dorde, Mathias Lechner, Thomas A Henzinger, and Krishnendu Chatterjee. “Learning Control Policies for Stochastic Systems with Reach-Avoid Guarantees.” In <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, 37:11926–35. Association for the Advancement of Artificial Intelligence, 2023. <a href=\"https://doi.org/10.1609/aaai.v37i10.26407\">https://doi.org/10.1609/aaai.v37i10.26407</a>.","ieee":"D. Zikelic, M. Lechner, T. A. Henzinger, and K. Chatterjee, “Learning control policies for stochastic systems with reach-avoid guarantees,” in <i>Proceedings of the 37th AAAI Conference on Artificial Intelligence</i>, Washington, DC, United States, 2023, vol. 37, no. 10, pp. 11926–11935."},"related_material":{"record":[{"relation":"earlier_version","id":"14600","status":"public"}]},"intvolume":"        37","publication_status":"published","date_published":"2023-06-26T00:00:00Z"},{"article_processing_charge":"No","ec_funded":1,"scopus_import":"1","article_type":"original","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","department":[{"_id":"ToHe"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Association for the Advancement of Artificial Intelligence","arxiv":1,"title":"GoTube: Scalable statistical verification of continuous-depth models","day":"28","author":[{"full_name":"Gruenbacher, Sophie A.","last_name":"Gruenbacher","first_name":"Sophie A."},{"full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","last_name":"Lechner","first_name":"Mathias"},{"full_name":"Hasani, Ramin","first_name":"Ramin","last_name":"Hasani"},{"last_name":"Rus","first_name":"Daniela","full_name":"Rus, Daniela"},{"last_name":"Henzinger","first_name":"Thomas A","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"full_name":"Smolka, Scott A.","first_name":"Scott A.","last_name":"Smolka"},{"first_name":"Radu","last_name":"Grosu","full_name":"Grosu, Radu"}],"language":[{"iso":"eng"}],"issue":"6","keyword":["General Medicine"],"project":[{"grant_number":"Z211","name":"The Wittgenstein Prize","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF"},{"_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","name":"Vigilant Algorithmic Monitoring of Software","grant_number":"101020093"}],"quality_controlled":"1","doi":"10.1609/aaai.v36i6.20631","publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"],"isbn":["978577358350"]},"_id":"12510","year":"2022","acknowledgement":"SG is funded by the Austrian Science Fund (FWF) project number W1255-N23. ML and TH are supported in part by FWF under grant Z211-N23 (Wittgenstein Award) and the ERC-2020-AdG 101020093. SS is supported by NSF awards DCL-2040599, CCF-1918225, and CPS-1446832. RH and DR are partially supported by Boeing. RG is partially supported by Horizon-2020 ECSEL Project grant No. 783163 (iDev40).","date_created":"2023-02-05T17:27:42Z","volume":36,"date_updated":"2023-09-26T10:46:59Z","abstract":[{"lang":"eng","text":"We introduce a new statistical verification algorithm that formally quantifies the behavioral robustness of any time-continuous process formulated as a continuous-depth model. Our algorithm solves a set of global optimization (Go) problems over a given time horizon to construct a tight enclosure (Tube) of the set of all process executions starting from a ball of initial states. We call our algorithm GoTube. Through its construction, GoTube ensures that the bounding tube is conservative up to a desired probability and up to a desired tightness.\r\n GoTube is implemented in JAX and optimized to scale to complex continuous-depth neural network models. Compared to advanced reachability analysis tools for time-continuous neural networks, GoTube does not accumulate overapproximation errors between time steps and avoids the infamous wrapping effect inherent in symbolic techniques. We show that GoTube substantially outperforms state-of-the-art verification tools in terms of the size of the initial ball, speed, time-horizon, task completion, and scalability on a large set of experiments.\r\n GoTube is stable and sets the state-of-the-art in terms of its ability to scale to time horizons well beyond what has been previously possible."}],"type":"journal_article","month":"06","oa_version":"Preprint","page":"6755-6764","citation":{"chicago":"Gruenbacher, Sophie A., Mathias Lechner, Ramin Hasani, Daniela Rus, Thomas A Henzinger, Scott A. Smolka, and Radu Grosu. “GoTube: Scalable Statistical Verification of Continuous-Depth Models.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence, 2022. <a href=\"https://doi.org/10.1609/aaai.v36i6.20631\">https://doi.org/10.1609/aaai.v36i6.20631</a>.","ieee":"S. A. Gruenbacher <i>et al.</i>, “GoTube: Scalable statistical verification of continuous-depth models,” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 36, no. 6. Association for the Advancement of Artificial Intelligence, pp. 6755–6764, 2022.","short":"S.A. Gruenbacher, M. Lechner, R. Hasani, D. Rus, T.A. Henzinger, S.A. Smolka, R. Grosu, Proceedings of the AAAI Conference on Artificial Intelligence 36 (2022) 6755–6764.","ama":"Gruenbacher SA, Lechner M, Hasani R, et al. GoTube: Scalable statistical verification of continuous-depth models. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. 2022;36(6):6755-6764. doi:<a href=\"https://doi.org/10.1609/aaai.v36i6.20631\">10.1609/aaai.v36i6.20631</a>","apa":"Gruenbacher, S. A., Lechner, M., Hasani, R., Rus, D., Henzinger, T. A., Smolka, S. A., &#38; Grosu, R. (2022). GoTube: Scalable statistical verification of continuous-depth models. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v36i6.20631\">https://doi.org/10.1609/aaai.v36i6.20631</a>","ista":"Gruenbacher SA, Lechner M, Hasani R, Rus D, Henzinger TA, Smolka SA, Grosu R. 2022. GoTube: Scalable statistical verification of continuous-depth models. Proceedings of the AAAI Conference on Artificial Intelligence. 36(6), 6755–6764.","mla":"Gruenbacher, Sophie A., et al. “GoTube: Scalable Statistical Verification of Continuous-Depth Models.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 36, no. 6, Association for the Advancement of Artificial Intelligence, 2022, pp. 6755–64, doi:<a href=\"https://doi.org/10.1609/aaai.v36i6.20631\">10.1609/aaai.v36i6.20631</a>."},"intvolume":"        36","external_id":{"arxiv":["2107.08467"]},"status":"public","main_file_link":[{"url":"https://arxiv.org/abs/2107.08467","open_access":"1"}],"date_published":"2022-06-28T00:00:00Z","oa":1,"publication_status":"published"},{"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Association for the Advancement of Artificial Intelligence","article_type":"original","ec_funded":1,"article_processing_charge":"No","scopus_import":"1","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","day":"28","author":[{"last_name":"Lechner","first_name":"Mathias","full_name":"Lechner, Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87"},{"last_name":"Zikelic","first_name":"Dorde","orcid":"0000-0002-4681-1699","id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","full_name":"Zikelic, Dorde"},{"last_name":"Chatterjee","first_name":"Krishnendu","full_name":"Chatterjee, Krishnendu","id":"2E5DCA20-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4561-241X"},{"last_name":"Henzinger","first_name":"Thomas A","orcid":"0000-0002-2985-7724","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","full_name":"Henzinger, Thomas A"}],"title":"Stability verification in stochastic control systems via neural network supermartingales","arxiv":1,"project":[{"name":"Vigilant Algorithmic Monitoring of Software","_id":"62781420-2b32-11ec-9570-8d9b63373d4d","call_identifier":"H2020","grant_number":"101020093"},{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E","call_identifier":"H2020"},{"name":"International IST Doctoral Program","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","grant_number":"665385"}],"issue":"7","language":[{"iso":"eng"}],"keyword":["General Medicine"],"publication_identifier":{"eissn":["2374-3468"],"isbn":["9781577358350"],"issn":["2159-5399"]},"quality_controlled":"1","doi":"10.1609/aaai.v36i7.20695","year":"2022","acknowledgement":"This work was supported in part by the ERC-2020-AdG 101020093, ERC CoG 863818 (FoRM-SMArt) and the European Union’s Horizon 2020 research and innovation programme\r\nunder the Marie Skłodowska-Curie Grant Agreement No. 665385.","_id":"12511","month":"06","type":"journal_article","oa_version":"Preprint","date_updated":"2025-07-14T09:09:58Z","abstract":[{"text":"We consider the problem of formally verifying almost-sure (a.s.) asymptotic stability in discrete-time nonlinear stochastic control systems. While verifying stability in deterministic control systems is extensively studied in the literature, verifying stability in stochastic control systems is an open problem. The few existing works on this topic either consider only specialized forms of stochasticity or make restrictive assumptions on the system, rendering them inapplicable to learning algorithms with neural network policies. \r\n In this work, we present an approach for general nonlinear stochastic control problems with two novel aspects: (a) instead of classical stochastic extensions of Lyapunov functions, we use ranking supermartingales (RSMs) to certify a.s. asymptotic stability, and (b) we present a method for learning neural network RSMs. \r\n We prove that our approach guarantees a.s. asymptotic stability of the system and\r\n provides the first method to obtain bounds on the stabilization time, which stochastic Lyapunov functions do not.\r\n Finally, we validate our approach experimentally on a set of nonlinear stochastic reinforcement learning environments with neural network policies.","lang":"eng"}],"page":"7326-7336","date_created":"2023-02-05T17:29:50Z","volume":36,"external_id":{"arxiv":["2112.09495"]},"status":"public","citation":{"chicago":"Lechner, Mathias, Dorde Zikelic, Krishnendu Chatterjee, and Thomas A Henzinger. “Stability Verification in Stochastic Control Systems via Neural Network Supermartingales.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence, 2022. <a href=\"https://doi.org/10.1609/aaai.v36i7.20695\">https://doi.org/10.1609/aaai.v36i7.20695</a>.","ieee":"M. Lechner, D. Zikelic, K. Chatterjee, and T. A. Henzinger, “Stability verification in stochastic control systems via neural network supermartingales,” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 36, no. 7. Association for the Advancement of Artificial Intelligence, pp. 7326–7336, 2022.","short":"M. Lechner, D. Zikelic, K. Chatterjee, T.A. Henzinger, Proceedings of the AAAI Conference on Artificial Intelligence 36 (2022) 7326–7336.","ama":"Lechner M, Zikelic D, Chatterjee K, Henzinger TA. Stability verification in stochastic control systems via neural network supermartingales. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. 2022;36(7):7326-7336. doi:<a href=\"https://doi.org/10.1609/aaai.v36i7.20695\">10.1609/aaai.v36i7.20695</a>","apa":"Lechner, M., Zikelic, D., Chatterjee, K., &#38; Henzinger, T. A. (2022). Stability verification in stochastic control systems via neural network supermartingales. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v36i7.20695\">https://doi.org/10.1609/aaai.v36i7.20695</a>","mla":"Lechner, Mathias, et al. “Stability Verification in Stochastic Control Systems via Neural Network Supermartingales.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 36, no. 7, Association for the Advancement of Artificial Intelligence, 2022, pp. 7326–36, doi:<a href=\"https://doi.org/10.1609/aaai.v36i7.20695\">10.1609/aaai.v36i7.20695</a>.","ista":"Lechner M, Zikelic D, Chatterjee K, Henzinger TA. 2022. Stability verification in stochastic control systems via neural network supermartingales. Proceedings of the AAAI Conference on Artificial Intelligence. 36(7), 7326–7336."},"intvolume":"        36","related_material":{"record":[{"relation":"dissertation_contains","id":"14539","status":"public"}]},"oa":1,"publication_status":"published","main_file_link":[{"open_access":"1","url":"https://arxiv.org/abs/2112.09495"}],"date_published":"2022-06-28T00:00:00Z"},{"citation":{"short":"T. Meggendorfer, in:, Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022, Association for the Advancement of Artificial Intelligence, 2022, pp. 9858–9867.","chicago":"Meggendorfer, Tobias. “Risk-Aware Stochastic Shortest Path.” In <i>Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022</i>, 36:9858–67. Association for the Advancement of Artificial Intelligence, 2022. <a href=\"https://doi.org/10.1609/aaai.v36i9.21222\">https://doi.org/10.1609/aaai.v36i9.21222</a>.","ieee":"T. Meggendorfer, “Risk-aware stochastic shortest path,” in <i>Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022</i>, Virtual, 2022, vol. 36, no. 9, pp. 9858–9867.","apa":"Meggendorfer, T. (2022). Risk-aware stochastic shortest path. In <i>Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022</i> (Vol. 36, pp. 9858–9867). Virtual: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v36i9.21222\">https://doi.org/10.1609/aaai.v36i9.21222</a>","mla":"Meggendorfer, Tobias. “Risk-Aware Stochastic Shortest Path.” <i>Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022</i>, vol. 36, no. 9, Association for the Advancement of Artificial Intelligence, 2022, pp. 9858–67, doi:<a href=\"https://doi.org/10.1609/aaai.v36i9.21222\">10.1609/aaai.v36i9.21222</a>.","ista":"Meggendorfer T. 2022. Risk-aware stochastic shortest path. Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022. Conference on Artificial Intelligence vol. 36, 9858–9867.","ama":"Meggendorfer T. Risk-aware stochastic shortest path. In: <i>Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022</i>. Vol 36. Association for the Advancement of Artificial Intelligence; 2022:9858-9867. doi:<a href=\"https://doi.org/10.1609/aaai.v36i9.21222\">10.1609/aaai.v36i9.21222</a>"},"intvolume":"        36","external_id":{"arxiv":["2203.01640"]},"status":"public","main_file_link":[{"url":" https://doi.org/10.48550/arXiv.2203.01640","open_access":"1"}],"date_published":"2022-06-28T00:00:00Z","publication_status":"published","oa":1,"_id":"12568","year":"2022","date_created":"2023-02-19T23:00:56Z","volume":36,"date_updated":"2023-02-20T07:19:12Z","abstract":[{"lang":"eng","text":"We treat the problem of risk-aware control for stochastic shortest path (SSP) on Markov decision processes (MDP). Typically, expectation is considered for SSP, which however is oblivious to the incurred risk. We present an alternative view, instead optimizing conditional value-at-risk (CVaR), an established risk measure. We treat both Markov chains as well as MDP and introduce, through novel insights, two algorithms, based on linear programming and value iteration, respectively. Both algorithms offer precise and provably correct solutions. Evaluation of our prototype implementation shows that risk-aware control is feasible on several moderately sized models."}],"oa_version":"Preprint","type":"conference","month":"06","page":"9858-9867","language":[{"iso":"eng"}],"issue":"9","conference":{"end_date":"2022-03-01","name":"Conference on Artificial Intelligence","location":"Virtual","start_date":"2022-02-22"},"quality_controlled":"1","doi":"10.1609/aaai.v36i9.21222","publication_identifier":{"isbn":["1577358767"],"eissn":["2374-3468"]},"scopus_import":"1","article_processing_charge":"No","publication":"Proceedings of the 36th AAAI Conference on Artificial Intelligence, AAAI 2022","department":[{"_id":"KrCh"}],"publisher":"Association for the Advancement of Artificial Intelligence","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","title":"Risk-aware stochastic shortest path","arxiv":1,"day":"28","author":[{"last_name":"Meggendorfer","first_name":"Tobias","id":"b21b0c15-30a2-11eb-80dc-f13ca25802e1","orcid":"0000-0002-1712-2165","full_name":"Meggendorfer, Tobias"}]},{"_id":"10665","acknowledgement":"This research was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein\r\nAward), ERC CoG 863818 (FoRM-SMArt), and the European Union’s Horizon 2020 research and innovation programme under the Marie Skłodowska-Curie Grant Agreement No. 665385.\r\n","year":"2021","volume":35,"file_date_updated":"2022-01-26T07:41:16Z","date_created":"2022-01-25T15:15:02Z","page":"3787-3795","oa_version":"Published Version","month":"05","type":"conference","date_updated":"2025-07-14T09:10:11Z","abstract":[{"text":"Formal verification of neural networks is an active topic of research, and recent advances have significantly increased the size of the networks that verification tools can handle. However, most methods are designed for verification of an idealized model of the actual network which works over real arithmetic and ignores rounding imprecisions. This idealization is in stark contrast to network quantization, which is a technique that trades numerical precision for computational efficiency and is, therefore, often applied in practice. Neglecting rounding errors of such low-bit quantized neural networks has been shown to lead to wrong conclusions about the network’s correctness. Thus, the desired approach for verifying quantized neural networks would be one that takes these rounding errors\r\ninto account. In this paper, we show that verifying the bitexact implementation of quantized neural networks with bitvector specifications is PSPACE-hard, even though verifying idealized real-valued networks and satisfiability of bit-vector specifications alone are each in NP. Furthermore, we explore several practical heuristics toward closing the complexity gap between idealized and bit-exact verification. In particular, we propose three techniques for making SMT-based verification of quantized neural networks more scalable. Our experiments demonstrate that our proposed methods allow a speedup of up to three orders of magnitude over existing approaches.","lang":"eng"}],"related_material":{"record":[{"relation":"dissertation_contains","status":"public","id":"11362"}]},"intvolume":"        35","citation":{"ista":"Henzinger TA, Lechner M, Zikelic D. 2021. Scalable verification of quantized neural networks. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Association for the Advancement of Artificial Intelligence, Technical Tracks, vol. 35, 3787–3795.","mla":"Henzinger, Thomas A., et al. “Scalable Verification of Quantized Neural Networks.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 35, no. 5A, AAAI Press, 2021, pp. 3787–95.","apa":"Henzinger, T. A., Lechner, M., &#38; Zikelic, D. (2021). Scalable verification of quantized neural networks. In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i> (Vol. 35, pp. 3787–3795). Virtual: AAAI Press.","ama":"Henzinger TA, Lechner M, Zikelic D. Scalable verification of quantized neural networks. In: <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Vol 35. AAAI Press; 2021:3787-3795.","short":"T.A. Henzinger, M. Lechner, D. Zikelic, in:, Proceedings of the AAAI Conference on Artificial Intelligence, AAAI Press, 2021, pp. 3787–3795.","ieee":"T. A. Henzinger, M. Lechner, and D. Zikelic, “Scalable verification of quantized neural networks,” in <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, Virtual, 2021, vol. 35, no. 5A, pp. 3787–3795.","chicago":"Henzinger, Thomas A, Mathias Lechner, and Dorde Zikelic. “Scalable Verification of Quantized Neural Networks.” In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, 35:3787–95. AAAI Press, 2021."},"alternative_title":["Technical Tracks"],"status":"public","external_id":{"arxiv":["2012.08185"]},"ddc":["000"],"date_published":"2021-05-28T00:00:00Z","main_file_link":[{"url":"https://ojs.aaai.org/index.php/AAAI/article/view/16496","open_access":"1"}],"oa":1,"publication_status":"published","has_accepted_license":"1","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","article_processing_charge":"No","ec_funded":1,"scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"AAAI Press","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"title":"Scalable verification of quantized neural networks","arxiv":1,"author":[{"first_name":"Thomas A","last_name":"Henzinger","full_name":"Henzinger, Thomas A","id":"40876CD8-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-2985-7724"},{"id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias","last_name":"Lechner","first_name":"Mathias"},{"id":"294AA7A6-F248-11E8-B48F-1D18A9856A87","orcid":"0000-0002-4681-1699","full_name":"Zikelic, Dorde","last_name":"Zikelic","first_name":"Dorde"}],"day":"28","file":[{"creator":"mlechner","content_type":"application/pdf","relation":"main_file","file_size":137235,"success":1,"file_name":"16496-Article Text-19990-1-2-20210518 (1).pdf","access_level":"open_access","date_created":"2022-01-26T07:41:16Z","checksum":"2bc8155b2526a70fba5b7301bc89dbd1","date_updated":"2022-01-26T07:41:16Z","file_id":"10684"}],"conference":{"start_date":"2021-02-02","location":"Virtual","name":"AAAI: Association for the Advancement of Artificial Intelligence","end_date":"2021-02-09"},"issue":"5A","language":[{"iso":"eng"}],"project":[{"call_identifier":"H2020","_id":"2564DBCA-B435-11E9-9278-68D0E5697425","name":"International IST Doctoral Program","grant_number":"665385"},{"call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize","grant_number":"Z211"},{"grant_number":"863818","name":"Formal Methods for Stochastic Models: Algorithms and Applications","call_identifier":"H2020","_id":"0599E47C-7A3F-11EA-A408-12923DDC885E"}],"quality_controlled":"1","publication_identifier":{"eissn":["2374-3468"],"isbn":["978-1-57735-866-4"],"issn":["2159-5399"]}},{"has_accepted_license":"1","publication_status":"published","oa":1,"main_file_link":[{"open_access":"1","url":"https://ojs.aaai.org/index.php/AAAI/article/view/17372"}],"date_published":"2021-05-28T00:00:00Z","ddc":["000"],"status":"public","external_id":{"arxiv":["2012.08863"]},"alternative_title":["Technical Tracks"],"citation":{"short":"S. Grunbacher, R. Hasani, M. Lechner, J. Cyranka, S.A. Smolka, R. Grosu, in:, Proceedings of the AAAI Conference on Artificial Intelligence, AAAI Press, 2021, pp. 11525–11535.","ieee":"S. Grunbacher, R. Hasani, M. Lechner, J. Cyranka, S. A. Smolka, and R. Grosu, “On the verification of neural ODEs with stochastic guarantees,” in <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, Virtual, 2021, vol. 35, no. 13, pp. 11525–11535.","chicago":"Grunbacher, Sophie, Ramin Hasani, Mathias Lechner, Jacek Cyranka, Scott A Smolka, and Radu Grosu. “On the Verification of Neural ODEs with Stochastic Guarantees.” In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, 35:11525–35. AAAI Press, 2021.","mla":"Grunbacher, Sophie, et al. “On the Verification of Neural ODEs with Stochastic Guarantees.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 35, no. 13, AAAI Press, 2021, pp. 11525–35.","ista":"Grunbacher S, Hasani R, Lechner M, Cyranka J, Smolka SA, Grosu R. 2021. On the verification of neural ODEs with stochastic guarantees. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Association for the Advancement of Artificial Intelligence, Technical Tracks, vol. 35, 11525–11535.","apa":"Grunbacher, S., Hasani, R., Lechner, M., Cyranka, J., Smolka, S. A., &#38; Grosu, R. (2021). On the verification of neural ODEs with stochastic guarantees. In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i> (Vol. 35, pp. 11525–11535). Virtual: AAAI Press.","ama":"Grunbacher S, Hasani R, Lechner M, Cyranka J, Smolka SA, Grosu R. On the verification of neural ODEs with stochastic guarantees. In: <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Vol 35. AAAI Press; 2021:11525-11535."},"intvolume":"        35","oa_version":"Published Version","type":"conference","month":"05","date_updated":"2022-05-24T06:33:14Z","abstract":[{"lang":"eng","text":"We show that Neural ODEs, an emerging class of timecontinuous neural networks, can be verified by solving a set of global-optimization problems. For this purpose, we introduce Stochastic Lagrangian Reachability (SLR), an\r\nabstraction-based technique for constructing a tight Reachtube (an over-approximation of the set of reachable states\r\nover a given time-horizon), and provide stochastic guarantees in the form of confidence intervals for the Reachtube bounds. SLR inherently avoids the infamous wrapping effect (accumulation of over-approximation errors) by performing local optimization steps to expand safe regions instead of repeatedly forward-propagating them as is done by deterministic reachability methods. To enable fast local optimizations, we introduce a novel forward-mode adjoint sensitivity method to compute gradients without the need for backpropagation. Finally, we establish asymptotic and non-asymptotic convergence rates for SLR."}],"page":"11525-11535","date_created":"2022-01-25T15:47:20Z","file_date_updated":"2022-01-26T07:38:08Z","volume":35,"year":"2021","acknowledgement":"The authors would like to thank the reviewers for their insightful comments. RH and RG were partially supported by\r\nHorizon-2020 ECSEL Project grant No. 783163 (iDev40). RH was partially supported by Boeing. ML was supported\r\nin part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). SG was funded by FWF\r\nproject W1255-N23. JC was partially supported by NAWA Polish Returns grant PPN/PPO/2018/1/00029. SS was supported by NSF awards DCL-2040599, CCF-1918225, and CPS-1446832.\r\n","_id":"10669","publication_identifier":{"isbn":["978-1-57735-866-4"],"eissn":["2374-3468"],"issn":["2159-5399"]},"quality_controlled":"1","project":[{"grant_number":"Z211","_id":"25F42A32-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","name":"The Wittgenstein Prize"}],"issue":"13","language":[{"iso":"eng"}],"conference":{"end_date":"2021-02-09","name":"AAAI: Association for the Advancement of Artificial Intelligence","location":"Virtual","start_date":"2021-02-02"},"day":"28","file":[{"date_updated":"2022-01-26T07:38:08Z","file_id":"10680","checksum":"468d07041e282a1d46ffdae92f709630","date_created":"2022-01-26T07:38:08Z","access_level":"open_access","success":1,"file_name":"17372-Article Text-20866-1-2-20210518.pdf","content_type":"application/pdf","relation":"main_file","file_size":286906,"creator":"mlechner"}],"author":[{"full_name":"Grunbacher, Sophie","last_name":"Grunbacher","first_name":"Sophie"},{"last_name":"Hasani","first_name":"Ramin","full_name":"Hasani, Ramin"},{"first_name":"Mathias","last_name":"Lechner","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias"},{"full_name":"Cyranka, Jacek","last_name":"Cyranka","first_name":"Jacek"},{"full_name":"Smolka, Scott A","last_name":"Smolka","first_name":"Scott A"},{"last_name":"Grosu","first_name":"Radu","full_name":"Grosu, Radu"}],"title":"On the verification of neural ODEs with stochastic guarantees","arxiv":1,"department":[{"_id":"GradSch"},{"_id":"ToHe"}],"publisher":"AAAI Press","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","article_processing_charge":"No","publication":"Proceedings of the AAAI Conference on Artificial Intelligence"},{"arxiv":1,"title":"Liquid time-constant networks","day":"28","file":[{"creator":"mlechner","file_size":4302669,"relation":"main_file","content_type":"application/pdf","file_name":"16936-Article Text-20430-1-2-20210518 (1).pdf","success":1,"access_level":"open_access","date_created":"2022-01-26T07:36:03Z","checksum":"0f06995fba06dbcfa7ed965fc66027ff","file_id":"10678","date_updated":"2022-01-26T07:36:03Z"}],"author":[{"full_name":"Hasani, Ramin","first_name":"Ramin","last_name":"Hasani"},{"last_name":"Lechner","first_name":"Mathias","id":"3DC22916-F248-11E8-B48F-1D18A9856A87","full_name":"Lechner, Mathias"},{"full_name":"Amini, Alexander","first_name":"Alexander","last_name":"Amini"},{"first_name":"Daniela","last_name":"Rus","full_name":"Rus, Daniela"},{"full_name":"Grosu, Radu","last_name":"Grosu","first_name":"Radu"}],"article_processing_charge":"No","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","department":[{"_id":"GradSch"},{"_id":"ToHe"}],"publisher":"AAAI Press","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","quality_controlled":"1","publication_identifier":{"issn":["2159-5399"],"isbn":["978-1-57735-866-4"],"eissn":["2374-3468"]},"issue":"9","language":[{"iso":"eng"}],"conference":{"end_date":"2021-02-09","start_date":"2021-02-02","location":"Virtual","name":"AAAI: Association for the Advancement of Artificial Intelligence"},"project":[{"grant_number":"Z211","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425","name":"The Wittgenstein Prize"}],"date_created":"2022-01-25T15:48:36Z","file_date_updated":"2022-01-26T07:36:03Z","volume":35,"oa_version":"Published Version","type":"conference","month":"05","date_updated":"2022-05-24T06:36:54Z","abstract":[{"text":"We introduce a new class of time-continuous recurrent neural network models. Instead of declaring a learning system’s dynamics by implicit nonlinearities, we construct networks of linear first-order dynamical systems modulated via nonlinear interlinked gates. The resulting models represent dynamical systems with varying (i.e., liquid) time-constants coupled to their hidden state, with outputs being computed by numerical differential equation solvers. These neural networks exhibit stable and bounded behavior, yield superior expressivity within the family of neural ordinary differential equations, and give rise to improved performance on time-series prediction tasks. To demonstrate these properties, we first take a theoretical approach to find bounds over their dynamics, and compute their expressive power by the trajectory length measure in a latent trajectory space. We then conduct a series of time-series prediction experiments to manifest the approximation capability of Liquid Time-Constant Networks (LTCs) compared to classical and modern RNNs.","lang":"eng"}],"page":"7657-7666","_id":"10671","year":"2021","acknowledgement":"R.H. and D.R. are partially supported by Boeing. R.H. and R.G. were partially supported by the Horizon-2020 ECSEL\r\nProject grant No. 783163 (iDev40). M.L. was supported in part by the Austrian Science Fund (FWF) under grant Z211-N23 (Wittgenstein Award). A.A. is supported by the National Science Foundation (NSF) Graduate Research Fellowship Program. This research work is partially drawn from the PhD dissertation of R.H.","main_file_link":[{"url":"https://ojs.aaai.org/index.php/AAAI/article/view/16936","open_access":"1"}],"date_published":"2021-05-28T00:00:00Z","ddc":["000"],"has_accepted_license":"1","publication_status":"published","oa":1,"citation":{"short":"R. Hasani, M. Lechner, A. Amini, D. Rus, R. Grosu, in:, Proceedings of the AAAI Conference on Artificial Intelligence, AAAI Press, 2021, pp. 7657–7666.","chicago":"Hasani, Ramin, Mathias Lechner, Alexander Amini, Daniela Rus, and Radu Grosu. “Liquid Time-Constant Networks.” In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, 35:7657–66. AAAI Press, 2021.","ieee":"R. Hasani, M. Lechner, A. Amini, D. Rus, and R. Grosu, “Liquid time-constant networks,” in <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, Virtual, 2021, vol. 35, no. 9, pp. 7657–7666.","apa":"Hasani, R., Lechner, M., Amini, A., Rus, D., &#38; Grosu, R. (2021). Liquid time-constant networks. In <i>Proceedings of the AAAI Conference on Artificial Intelligence</i> (Vol. 35, pp. 7657–7666). Virtual: AAAI Press.","mla":"Hasani, Ramin, et al. “Liquid Time-Constant Networks.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 35, no. 9, AAAI Press, 2021, pp. 7657–66.","ista":"Hasani R, Lechner M, Amini A, Rus D, Grosu R. 2021. Liquid time-constant networks. Proceedings of the AAAI Conference on Artificial Intelligence. AAAI: Association for the Advancement of Artificial Intelligence, Technical Tracks, vol. 35, 7657–7666.","ama":"Hasani R, Lechner M, Amini A, Rus D, Grosu R. Liquid time-constant networks. In: <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Vol 35. AAAI Press; 2021:7657-7666."},"intvolume":"        35","external_id":{"arxiv":["2006.04439"]},"status":"public","alternative_title":["Technical Tracks"]},{"department":[{"_id":"DaAl"}],"user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"AAAI Press","ec_funded":1,"scopus_import":"1","article_processing_charge":"No","publication":"35th AAAI Conference on Artificial Intelligence, AAAI 2021","day":"18","author":[{"full_name":"Kungurtsev, Vyacheslav","first_name":"Vyacheslav","last_name":"Kungurtsev"},{"first_name":"Malcolm","last_name":"Egan","full_name":"Egan, Malcolm"},{"first_name":"Bapi","last_name":"Chatterjee","full_name":"Chatterjee, Bapi","id":"3C41A08A-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-3650-940X","id":"4A899BFC-F248-11E8-B48F-1D18A9856A87","full_name":"Alistarh, Dan-Adrian","last_name":"Alistarh","first_name":"Dan-Adrian"}],"title":"Asynchronous optimization methods for efficient training of deep neural networks with guarantees","arxiv":1,"project":[{"grant_number":"754411","_id":"260C2330-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","name":"ISTplus - Postdoctoral Fellowships"},{"name":"Elastic Coordination for Scalable Machine Learning","_id":"268A44D6-B435-11E9-9278-68D0E5697425","call_identifier":"H2020","grant_number":"805223"}],"language":[{"iso":"eng"}],"issue":"9B","conference":{"end_date":"2021-02-09","start_date":"2021-02-02","name":"AAAI: Conference on Artificial Intelligence","location":"Virtual, Online"},"publication_identifier":{"issn":["2159-5399"],"eissn":["2374-3468"],"isbn":["9781713835974"]},"quality_controlled":"1","year":"2021","acknowledgement":"Vyacheslav Kungurtsev was supported by the OP VVV project CZ.02.1.01/0.0/0.0/16 019/0000765 “Research Center for Informatics. Bapi Chatterjee was supported by the European Union’s Horizon 2020 research and innovation programme under the Marie Sklodowska-Curie grant agreement No. 754411 (ISTPlus). Dan Alistarh has received funding from the European Research Council (ERC) under the European Union’s Horizon 2020 research and innovation programme (grant agreement No 805223 ScaleML).","_id":"11436","date_updated":"2022-06-07T06:53:36Z","abstract":[{"lang":"eng","text":"Asynchronous distributed algorithms are a popular way to reduce synchronization costs in large-scale optimization, and in particular for neural network training. However, for nonsmooth and nonconvex objectives, few convergence guarantees exist beyond cases where closed-form proximal operator solutions are available. As training most popular deep neural networks corresponds to optimizing nonsmooth and nonconvex objectives, there is a pressing need for such convergence guarantees. In this paper, we analyze for the first time the convergence of stochastic asynchronous optimization for this general class of objectives. In particular, we focus on stochastic subgradient methods allowing for block variable partitioning, where the shared model is asynchronously updated by concurrent processes. To this end, we use a probabilistic model which captures key features of real asynchronous scheduling between concurrent processes. Under this model, we establish convergence with probability one to an invariant set for stochastic subgradient methods with momentum. From a practical perspective, one issue with the family of algorithms that we consider is that they are not efficiently supported by machine learning frameworks, which mostly focus on distributed data-parallel strategies. To address this, we propose a new implementation strategy for shared-memory based training of deep neural networks for a partitioned but shared model in single- and multi-GPU settings. Based on this implementation, we achieve on average1.2x speed-up in comparison to state-of-the-art training methods for popular image classification tasks, without compromising accuracy."}],"type":"conference","oa_version":"Preprint","month":"05","page":"8209-8216","date_created":"2022-06-05T22:01:52Z","volume":35,"status":"public","external_id":{"arxiv":["1905.11845"]},"citation":{"ama":"Kungurtsev V, Egan M, Chatterjee B, Alistarh D-A. Asynchronous optimization methods for efficient training of deep neural networks with guarantees. In: <i>35th AAAI Conference on Artificial Intelligence, AAAI 2021</i>. Vol 35. AAAI Press; 2021:8209-8216.","ista":"Kungurtsev V, Egan M, Chatterjee B, Alistarh D-A. 2021. Asynchronous optimization methods for efficient training of deep neural networks with guarantees. 35th AAAI Conference on Artificial Intelligence, AAAI 2021. AAAI: Conference on Artificial Intelligence vol. 35, 8209–8216.","mla":"Kungurtsev, Vyacheslav, et al. “Asynchronous Optimization Methods for Efficient Training of Deep Neural Networks with Guarantees.” <i>35th AAAI Conference on Artificial Intelligence, AAAI 2021</i>, vol. 35, no. 9B, AAAI Press, 2021, pp. 8209–16.","apa":"Kungurtsev, V., Egan, M., Chatterjee, B., &#38; Alistarh, D.-A. (2021). Asynchronous optimization methods for efficient training of deep neural networks with guarantees. In <i>35th AAAI Conference on Artificial Intelligence, AAAI 2021</i> (Vol. 35, pp. 8209–8216). Virtual, Online: AAAI Press.","ieee":"V. Kungurtsev, M. Egan, B. Chatterjee, and D.-A. Alistarh, “Asynchronous optimization methods for efficient training of deep neural networks with guarantees,” in <i>35th AAAI Conference on Artificial Intelligence, AAAI 2021</i>, Virtual, Online, 2021, vol. 35, no. 9B, pp. 8209–8216.","chicago":"Kungurtsev, Vyacheslav, Malcolm Egan, Bapi Chatterjee, and Dan-Adrian Alistarh. “Asynchronous Optimization Methods for Efficient Training of Deep Neural Networks with Guarantees.” In <i>35th AAAI Conference on Artificial Intelligence, AAAI 2021</i>, 35:8209–16. AAAI Press, 2021.","short":"V. Kungurtsev, M. Egan, B. Chatterjee, D.-A. Alistarh, in:, 35th AAAI Conference on Artificial Intelligence, AAAI 2021, AAAI Press, 2021, pp. 8209–8216."},"intvolume":"        35","oa":1,"publication_status":"published","main_file_link":[{"open_access":"1","url":" https://doi.org/10.48550/arXiv.1905.11845"}],"date_published":"2021-05-18T00:00:00Z"},{"date_published":"2020-07-28T00:00:00Z","main_file_link":[{"url":"https://arxiv.org/abs/2007.14184","open_access":"1"}],"publication_status":"published","oa":1,"intvolume":"        34","extern":"1","citation":{"ama":"Locatello F, Bauer S, Lucic M, et al. A commentary on the unsupervised learning of disentangled representations. In: <i>The 34th AAAI Conference on Artificial Intelligence</i>. Vol 34. Association for the Advancement of Artificial Intelligence; 2020:13681-13684. doi:<a href=\"https://doi.org/10.1609/aaai.v34i09.7120\">10.1609/aaai.v34i09.7120</a>","ista":"Locatello F, Bauer S, Lucic M, Rätsch G, Gelly S, Schölkopf B, Bachem O. 2020. A commentary on the unsupervised learning of disentangled representations. The 34th AAAI Conference on Artificial Intelligence. AAAI: Conference on Artificial Intelligence vol. 34, 13681–13684.","mla":"Locatello, Francesco, et al. “A Commentary on the Unsupervised Learning of Disentangled Representations.” <i>The 34th AAAI Conference on Artificial Intelligence</i>, vol. 34, no. 9, Association for the Advancement of Artificial Intelligence, 2020, pp. 13681–84, doi:<a href=\"https://doi.org/10.1609/aaai.v34i09.7120\">10.1609/aaai.v34i09.7120</a>.","apa":"Locatello, F., Bauer, S., Lucic, M., Rätsch, G., Gelly, S., Schölkopf, B., &#38; Bachem, O. (2020). A commentary on the unsupervised learning of disentangled representations. In <i>The 34th AAAI Conference on Artificial Intelligence</i> (Vol. 34, pp. 13681–13684). New York, NY, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v34i09.7120\">https://doi.org/10.1609/aaai.v34i09.7120</a>","ieee":"F. Locatello <i>et al.</i>, “A commentary on the unsupervised learning of disentangled representations,” in <i>The 34th AAAI Conference on Artificial Intelligence</i>, New York, NY, United States, 2020, vol. 34, no. 9, pp. 13681–13684.","chicago":"Locatello, Francesco, Stefan Bauer, Mario Lucic, Gunnar Rätsch, Sylvain Gelly, Bernhard Schölkopf, and Olivier Bachem. “A Commentary on the Unsupervised Learning of Disentangled Representations.” In <i>The 34th AAAI Conference on Artificial Intelligence</i>, 34:13681–84. Association for the Advancement of Artificial Intelligence, 2020. <a href=\"https://doi.org/10.1609/aaai.v34i09.7120\">https://doi.org/10.1609/aaai.v34i09.7120</a>.","short":"F. Locatello, S. Bauer, M. Lucic, G. Rätsch, S. Gelly, B. Schölkopf, O. Bachem, in:, The 34th AAAI Conference on Artificial Intelligence, Association for the Advancement of Artificial Intelligence, 2020, pp. 13681–13684."},"external_id":{"arxiv":["2007.14184"]},"status":"public","volume":34,"date_created":"2023-08-22T14:07:26Z","page":"13681-13684","abstract":[{"text":"The goal of the unsupervised learning of disentangled representations is to\r\nseparate the independent explanatory factors of variation in the data without\r\naccess to supervision. In this paper, we summarize the results of Locatello et\r\nal., 2019, and focus on their implications for practitioners. We discuss the\r\ntheoretical result showing that the unsupervised learning of disentangled\r\nrepresentations is fundamentally impossible without inductive biases and the\r\npractical challenges it entails. Finally, we comment on our experimental\r\nfindings, highlighting the limitations of state-of-the-art approaches and\r\ndirections for future research.","lang":"eng"}],"date_updated":"2023-09-12T07:44:48Z","month":"07","oa_version":"Preprint","type":"conference","_id":"14186","year":"2020","doi":"10.1609/aaai.v34i09.7120","quality_controlled":"1","publication_identifier":{"isbn":["9781577358350"],"eissn":["2374-3468"]},"conference":{"start_date":"2020-02-07","location":"New York, NY, United States","name":"AAAI: Conference on Artificial Intelligence","end_date":"2020-02-12"},"language":[{"iso":"eng"}],"issue":"9","title":"A commentary on the unsupervised learning of disentangled representations","arxiv":1,"author":[{"full_name":"Locatello, Francesco","orcid":"0000-0002-4850-0683","id":"26cfd52f-2483-11ee-8040-88983bcc06d4","last_name":"Locatello","first_name":"Francesco"},{"full_name":"Bauer, Stefan","first_name":"Stefan","last_name":"Bauer"},{"first_name":"Mario","last_name":"Lucic","full_name":"Lucic, Mario"},{"last_name":"Rätsch","first_name":"Gunnar","full_name":"Rätsch, Gunnar"},{"last_name":"Gelly","first_name":"Sylvain","full_name":"Gelly, Sylvain"},{"first_name":"Bernhard","last_name":"Schölkopf","full_name":"Schölkopf, Bernhard"},{"full_name":"Bachem, Olivier","last_name":"Bachem","first_name":"Olivier"}],"day":"28","publication":"The 34th AAAI Conference on Artificial Intelligence","article_processing_charge":"No","scopus_import":"1","user_id":"2DF688A6-F248-11E8-B48F-1D18A9856A87","publisher":"Association for the Advancement of Artificial Intelligence","department":[{"_id":"FrLo"}]},{"department":[{"_id":"ToHe"},{"_id":"KrCh"}],"user_id":"c635000d-4b10-11ee-a964-aac5a93f6ac1","publisher":"Association for the Advancement of Artificial Intelligence","article_type":"original","scopus_import":"1","article_processing_charge":"No","publication":"Proceedings of the AAAI Conference on Artificial Intelligence","day":"03","author":[{"first_name":"Guy","last_name":"Avni","full_name":"Avni, Guy","orcid":"0000-0001-5588-8287","id":"463C8BC2-F248-11E8-B48F-1D18A9856A87"},{"orcid":"0000-0003-4783-0389","id":"3B699956-F248-11E8-B48F-1D18A9856A87","full_name":"Ibsen-Jensen, Rasmus","first_name":"Rasmus","last_name":"Ibsen-Jensen"},{"first_name":"Josef","last_name":"Tkadlec","orcid":"0000-0002-1097-9684","id":"3F24CCC8-F248-11E8-B48F-1D18A9856A87","full_name":"Tkadlec, Josef"}],"arxiv":1,"title":"All-pay bidding games on graphs","project":[{"grant_number":"S11402-N23","name":"Rigorous Systems Engineering","call_identifier":"FWF","_id":"25F2ACDE-B435-11E9-9278-68D0E5697425"},{"grant_number":"Z211","name":"The Wittgenstein Prize","call_identifier":"FWF","_id":"25F42A32-B435-11E9-9278-68D0E5697425"},{"name":"Formal Methods meets Algorithmic Game Theory","_id":"264B3912-B435-11E9-9278-68D0E5697425","call_identifier":"FWF","grant_number":"M02369"}],"issue":"02","language":[{"iso":"eng"}],"conference":{"start_date":"2020-02-07","location":"New York, NY, United States","name":"AAAI: Conference on Artificial Intelligence","end_date":"2020-02-12"},"publication_identifier":{"isbn":["9781577358350"],"eissn":["2374-3468"],"issn":["2159-5399"]},"quality_controlled":"1","doi":"10.1609/aaai.v34i02.5546","year":"2020","acknowledgement":"This research was supported by the Austrian Science Fund (FWF) under grants S11402-N23 (RiSE/SHiNE), Z211-N23 (Wittgenstein Award), and M 2369-N33 (Meitner fellowship).","_id":"9197","oa_version":"Preprint","type":"journal_article","month":"04","abstract":[{"lang":"eng","text":"In this paper we introduce and study all-pay bidding games, a class of two player, zero-sum games on graphs. The game proceeds as follows. We place a token on some vertex in the graph and assign budgets to the two players. Each turn, each player submits a sealed legal bid (non-negative and below their remaining budget), which is deducted from their budget and the highest bidder moves the token onto an adjacent vertex. The game ends once a sink is reached, and Player 1 pays Player 2 the outcome that is associated with the sink. The players attempt to maximize their expected outcome. Our games model settings where effort (of no inherent value) needs to be invested in an ongoing and stateful manner. On the negative side, we show that even in simple games on DAGs, optimal strategies may require a distribution over bids with infinite support. A central quantity in bidding games is the ratio of the players budgets. On the positive side, we show a simple FPTAS for DAGs, that, for each budget ratio, outputs an approximation for the optimal strategy for that ratio. We also implement it, show that it performs well, and suggests interesting properties of these games. Then, given an outcome c, we show an algorithm for finding the necessary and sufficient initial ratio for guaranteeing outcome c with probability 1 and a strategy ensuring such. Finally, while the general case has not previously been studied, solving the specific game in which Player 1 wins iff he wins the first two auctions, has been long stated as an open question, which we solve."}],"date_updated":"2023-09-05T12:40:00Z","page":"1798-1805","date_created":"2021-02-25T09:05:18Z","volume":34,"status":"public","external_id":{"arxiv":["1911.08360"]},"citation":{"ista":"Avni G, Ibsen-Jensen R, Tkadlec J. 2020. All-pay bidding games on graphs. Proceedings of the AAAI Conference on Artificial Intelligence. 34(02), 1798–1805.","mla":"Avni, Guy, et al. “All-Pay Bidding Games on Graphs.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 34, no. 02, Association for the Advancement of Artificial Intelligence, 2020, pp. 1798–805, doi:<a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">10.1609/aaai.v34i02.5546</a>.","apa":"Avni, G., Ibsen-Jensen, R., &#38; Tkadlec, J. (2020). All-pay bidding games on graphs. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. New York, NY, United States: Association for the Advancement of Artificial Intelligence. <a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">https://doi.org/10.1609/aaai.v34i02.5546</a>","ama":"Avni G, Ibsen-Jensen R, Tkadlec J. All-pay bidding games on graphs. <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. 2020;34(02):1798-1805. doi:<a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">10.1609/aaai.v34i02.5546</a>","short":"G. Avni, R. Ibsen-Jensen, J. Tkadlec, Proceedings of the AAAI Conference on Artificial Intelligence 34 (2020) 1798–1805.","ieee":"G. Avni, R. Ibsen-Jensen, and J. Tkadlec, “All-pay bidding games on graphs,” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>, vol. 34, no. 02. Association for the Advancement of Artificial Intelligence, pp. 1798–1805, 2020.","chicago":"Avni, Guy, Rasmus Ibsen-Jensen, and Josef Tkadlec. “All-Pay Bidding Games on Graphs.” <i>Proceedings of the AAAI Conference on Artificial Intelligence</i>. Association for the Advancement of Artificial Intelligence, 2020. <a href=\"https://doi.org/10.1609/aaai.v34i02.5546\">https://doi.org/10.1609/aaai.v34i02.5546</a>."},"intvolume":"        34","publication_status":"published","date_published":"2020-04-03T00:00:00Z"}]