@phdthesis{11362, abstract = {Deep learning has enabled breakthroughs in challenging computing problems and has emerged as the standard problem-solving tool for computer vision and natural language processing tasks. One exception to this trend is safety-critical tasks where robustness and resilience requirements contradict the black-box nature of neural networks. To deploy deep learning methods for these tasks, it is vital to provide guarantees on neural network agents' safety and robustness criteria. This can be achieved by developing formal verification methods to verify the safety and robustness properties of neural networks. Our goal is to design, develop and assess safety verification methods for neural networks to improve their reliability and trustworthiness in real-world applications. This thesis establishes techniques for the verification of compressed and adversarially trained models as well as the design of novel neural networks for verifiably safe decision-making. First, we establish the problem of verifying quantized neural networks. Quantization is a technique that trades numerical precision for the computational efficiency of running a neural network and is widely adopted in industry. We show that neglecting the reduced precision when verifying a neural network can lead to wrong conclusions about the robustness and safety of the network, highlighting that novel techniques for quantized network verification are necessary. We introduce several bit-exact verification methods explicitly designed for quantized neural networks and experimentally confirm on realistic networks that the network's robustness and other formal properties are affected by the quantization. Furthermore, we perform a case study providing evidence that adversarial training, a standard technique for making neural networks more robust, has detrimental effects on the network's performance. This robustness-accuracy tradeoff has been studied before regarding the accuracy obtained on classification datasets where each data point is independent of all other data points. On the other hand, we investigate the tradeoff empirically in robot learning settings where a both, a high accuracy and a high robustness, are desirable. Our results suggest that the negative side-effects of adversarial training outweigh its robustness benefits in practice. Finally, we consider the problem of verifying safety when running a Bayesian neural network policy in a feedback loop with systems over the infinite time horizon. Bayesian neural networks are probabilistic models for learning uncertainties in the data and are therefore often used on robotic and healthcare applications where data is inherently stochastic. We introduce a method for recalibrating Bayesian neural networks so that they yield probability distributions over safe decisions only. Our method learns a safety certificate that guarantees safety over the infinite time horizon to determine which decisions are safe in every possible state of the system. We demonstrate the effectiveness of our approach on a series of reinforcement learning benchmarks.}, author = {Lechner, Mathias}, isbn = {978-3-99078-017-6}, keywords = {neural networks, verification, machine learning}, pages = {124}, publisher = {Institute of Science and Technology Austria}, title = {{Learning verifiable representations}}, doi = {10.15479/at:ista:11362}, year = {2022}, } @inproceedings{12302, abstract = {We propose a novel algorithm to decide the language inclusion between (nondeterministic) Büchi automata, a PSPACE-complete problem. Our approach, like others before, leverage a notion of quasiorder to prune the search for a counterexample by discarding candidates which are subsumed by others for the quasiorder. Discarded candidates are guaranteed to not compromise the completeness of the algorithm. The novelty of our work lies in the quasiorder used to discard candidates. We introduce FORQs (family of right quasiorders) that we obtain by adapting the notion of family of right congruences put forward by Maler and Staiger in 1993. We define a FORQ-based inclusion algorithm which we prove correct and instantiate it for a specific FORQ, called the structural FORQ, induced by the Büchi automaton to the right of the inclusion sign. The resulting implementation, called FORKLIFT, scales up better than the state-of-the-art on a variety of benchmarks including benchmarks from program verification and theorem proving for word combinatorics. Artifact: https://doi.org/10.5281/zenodo.6552870}, author = {Doveri, Kyveli and Ganty, Pierre and Mazzocchi, Nicolas Adrien}, booktitle = {Computer Aided Verification}, isbn = {9783031131875}, issn = {1611-3349}, location = {Haifa, Israel}, pages = {109--129}, publisher = {Springer Nature}, title = {{FORQ-based language inclusion formal testing}}, doi = {10.1007/978-3-031-13188-2_6}, volume = {13372}, year = {2022}, } @inproceedings{12175, abstract = {An automaton is history-deterministic (HD) if one can safely resolve its non-deterministic choices on the fly. In a recent paper, Henzinger, Lehtinen and Totzke studied this in the context of Timed Automata [9], where it was conjectured that the class of timed ω-languages recognised by HD-timed automata strictly extends that of deterministic ones. We provide a proof for this fact.}, author = {Bose, Sougata and Henzinger, Thomas A and Lehtinen, Karoliina and Schewe, Sven and Totzke, Patrick}, booktitle = {16th International Conference on Reachability Problems}, isbn = {9783031191343}, issn = {1611-3349}, location = {Kaiserslautern, Germany}, pages = {67--76}, publisher = {Springer Nature}, title = {{History-deterministic timed automata are not determinizable}}, doi = {10.1007/978-3-031-19135-0_5}, volume = {13608}, year = {2022}, } @article{12510, abstract = {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. 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. 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.}, author = {Gruenbacher, Sophie A. and Lechner, Mathias and Hasani, Ramin and Rus, Daniela and Henzinger, Thomas A and Smolka, Scott A. and Grosu, Radu}, isbn = {978577358350}, issn = {2374-3468}, journal = {Proceedings of the AAAI Conference on Artificial Intelligence}, keywords = {General Medicine}, number = {6}, pages = {6755--6764}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{GoTube: Scalable statistical verification of continuous-depth models}}, doi = {10.1609/aaai.v36i6.20631}, volume = {36}, year = {2022}, } @article{12511, abstract = {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. 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. We prove that our approach guarantees a.s. asymptotic stability of the system and provides the first method to obtain bounds on the stabilization time, which stochastic Lyapunov functions do not. Finally, we validate our approach experimentally on a set of nonlinear stochastic reinforcement learning environments with neural network policies.}, author = {Lechner, Mathias and Zikelic, Dorde and Chatterjee, Krishnendu and Henzinger, Thomas A}, isbn = {9781577358350}, issn = {2374-3468}, journal = {Proceedings of the AAAI Conference on Artificial Intelligence}, keywords = {General Medicine}, number = {7}, pages = {7326--7336}, publisher = {Association for the Advancement of Artificial Intelligence}, title = {{Stability verification in stochastic control systems via neural network supermartingales}}, doi = {10.1609/aaai.v36i7.20695}, volume = {36}, year = {2022}, } @unpublished{14601, abstract = {In this work, we address the problem of learning provably stable neural network policies for stochastic control systems. While recent work has demonstrated the feasibility of certifying given policies using martingale theory, the problem of how to learn such policies is little explored. Here, we study the effectiveness of jointly learning a policy together with a martingale certificate that proves its stability using a single learning algorithm. We observe that the joint optimization problem becomes easily stuck in local minima when starting from a randomly initialized policy. Our results suggest that some form of pre-training of the policy is required for the joint optimization to repair and verify the policy successfully.}, author = {Zikelic, Dorde and Lechner, Mathias and Chatterjee, Krishnendu and Henzinger, Thomas A}, booktitle = {arXiv}, title = {{Learning stabilizing policies in stochastic control systems}}, doi = {10.48550/arXiv.2205.11991}, year = {2022}, } @unpublished{14600, abstract = {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.}, author = {Zikelic, Dorde and Lechner, Mathias and Henzinger, Thomas A and Chatterjee, Krishnendu}, booktitle = {arXiv}, title = {{Learning control policies for stochastic systems with reach-avoid guarantees}}, doi = {10.48550/ARXIV.2210.05308}, year = {2022}, } @article{10153, abstract = {Gradual typing is a principled means for mixing typed and untyped code. But typed and untyped code often exhibit different programming patterns. There is already substantial research investigating gradually giving types to code exhibiting typical untyped patterns, and some research investigating gradually removing types from code exhibiting typical typed patterns. This paper investigates how to extend these established gradual-typing concepts to give formal guarantees not only about how to change types as code evolves but also about how to change such programming patterns as well. In particular, we explore mixing untyped "structural" code with typed "nominal" code in an object-oriented language. But whereas previous work only allowed "nominal" objects to be treated as "structural" objects, we also allow "structural" objects to dynamically acquire certain nominal types, namely interfaces. We present a calculus that supports such "cross-paradigm" code migration and interoperation in a manner satisfying both the static and dynamic gradual guarantees, and demonstrate that the calculus can be implemented efficiently.}, author = {Mühlböck, Fabian and Tate, Ross}, issn = {2475-1421}, journal = {Proceedings of the ACM on Programming Languages}, keywords = {gradual typing, gradual guarantee, nominal, structural, call tags}, location = {Chicago, IL, United States}, publisher = {Association for Computing Machinery}, title = {{Transitioning from structural to nominal code with efficient gradual typing}}, doi = {10.1145/3485504}, volume = {5}, year = {2021}, } @inproceedings{10669, abstract = {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 abstraction-based technique for constructing a tight Reachtube (an over-approximation of the set of reachable states over 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.}, author = {Grunbacher, Sophie and Hasani, Ramin and Lechner, Mathias and Cyranka, Jacek and Smolka, Scott A and Grosu, Radu}, booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence}, isbn = {978-1-57735-866-4}, issn = {2374-3468}, location = {Virtual}, number = {13}, pages = {11525--11535}, publisher = {AAAI Press}, title = {{On the verification of neural ODEs with stochastic guarantees}}, volume = {35}, year = {2021}, } @inproceedings{10671, abstract = {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.}, author = {Hasani, Ramin and Lechner, Mathias and Amini, Alexander and Rus, Daniela and Grosu, Radu}, booktitle = {Proceedings of the AAAI Conference on Artificial Intelligence}, isbn = {978-1-57735-866-4}, issn = {2374-3468}, location = {Virtual}, number = {9}, pages = {7657--7666}, publisher = {AAAI Press}, title = {{Liquid time-constant networks}}, volume = {35}, year = {2021}, }