More Like this

1. Output Range Analysis for Deep Feedforward Neural Networks

   https://doi.org/10.1007/978-3-319-77935-5_9  

   Dutta, Souradeep; Jha, Susmit; Sankaranarayanan, Sriram; Tiwari, Ashish (January 2018, NASA Formal Methods)

   Given a neural network (NN) and a set of possible inputs to the network described by polyhedral constraints, we aim to compute a safe over-approximation of the set of possible output values. This operation is a fundamental primitive enabling the formal analysis of neural networks that are extensively used in a variety of machine learning tasks such as perception and control of autonomous systems. Increasingly, they are deployed in high-assurance applications, leading to a compelling use case for formal verification approaches. In this paper, we present an efficient range estimation algorithm that iterates between an expensive global combinatorial search using mixed-integer linear programming problems, and a relatively inexpensive local optimization that repeatedly seeks a local optimum of the function represented by the NN. We implement our approach and compare it with Reluplex, a recently proposed solver for deep neural networks. We demonstrate applications of our approach to computing flowpipes for neural network-based feedback controllers. We show that the use of local search in conjunction with mixed-integer linear programming solvers effectively reduces the combinatorial search over possible combinations of active neurons in the network by pruning away suboptimal nodes. 

   more » « less
2. Safe Robot Learning in Assistive Devices through Neural Network Repair

   Keyvan Majd, Geoffrey Mitchell (August 2023, Proceedings of Machine Learning Research)

   Assistive robotic devices are a particularly promising field of application for neural networks (NN) due to the need for personalization and hard-to-model human-machine interaction dynamics. However, NN based estimators and controllers may produce potentially unsafe outputs over previously unseen data points. In this paper, we introduce an algorithm for updating NN control policies to satisfy a given set of formal safety constraints, while also optimizing the original loss function. Given a set of mixed-integer linear constraints, we define the NN repair problem as a Mixed Integer Quadratic Program (MIQP). In extensive experiments, we demonstrate the efficacy of our repair method in generating safe policies for a lower-leg prosthesis. 

   more » « less
3. Verifying the Safety of Autonomous Systems with Neural Network Controllers

   https://doi.org/10.1145/3419742  

   Ivanov, Radoslav; Carpenter, Taylor J.; Weimer, James; Alur, Rajeev; Pappas, George J.; Lee, Insup (January 2021, ACM Transactions on Embedded Computing Systems)

   This article addresses the problem of verifying the safety of autonomous systems with neural network (NN) controllers. We focus on NNs with sigmoid/tanh activations and use the fact that the sigmoid/tanh is the solution to a quadratic differential equation. This allows us to convert the NN into an equivalent hybrid system and cast the problem as a hybrid system verification problem, which can be solved by existing tools. Furthermore, we improve the scalability of the proposed method by approximating the sigmoid with a Taylor series with worst-case error bounds. Finally, we provide an evaluation over four benchmarks, including comparisons with alternative approaches based on mixed integer linear programming as well as on star sets. 

   more » « less
4. Learning to Allocate Time-Bound and Dynamic Tasks to Multiple Robots Using Covariant Attention Neural Networks

   https://doi.org/10.1115/1.4065883  

   Paul, Steve; Chowdhury, Souma (September 2024, Journal of Computing and Information Science in Engineering)

   Abstract In various applications of multi-robotics in disaster response, warehouse management, and manufacturing, tasks that are known a priori and tasks added during run time need to be assigned efficiently and without conflicts to robots in the team. This multi-robot task allocation (MRTA) process presents itself as a combinatorial optimization (CO) problem that is usually challenging to be solved in meaningful timescales using typical (mixed)integer (non)linear programming tools. Building on a growing body of work in using graph reinforcement learning to learn search heuristics for such complex CO problems, this paper presents a new graph neural network architecture called the covariant attention mechanism (CAM). CAM can not only generalize but also scale to larger problems than that encountered in training, and handle dynamic tasks. This architecture combines the concept of covariant compositional networks used here to embed the local structures in task graphs, with a context module that encodes the robots’ states. The encoded information is passed onto a decoder designed using multi-head attention mechanism. When applied to a class of MRTA problems with time deadlines, robot ferry range constraints, and multi-trip settings, CAM surpasses a state-of-the-art graph learning approach based on the attention mechanism, as well as a feasible random-walk baseline across various generalizability and scalability tests. Performance of CAM is also found to be at par with a high-performing non-learning baseline called BiG-MRTA, while noting up to a 70-fold improvement in decision-making efficiency over this baseline. 

   more » « less
5. Fast Globally Optimal Catalog Matching using MIQCP

   https://doi.org/10.3847/1538-3881/acf5e2  

   Feitelberg, Jacob; Basu, Amitabh; Budavári, Tamás (September 2023, The Astronomical Journal)

   We propose a novel exact method to solve the probabilistic catalog matching problem faster than previously possible. Our new approach uses mixed integer programming and introduces quadratic constraints to shrink the problem by multiple orders of magnitude. We also provide a method to use a feasible solution to dramatically speed up our algorithm. This gain in performance is dependent on how close to optimal the feasible solution is. Also, we are able to provide good solutions by stopping our mixed integer programming solver early. Using simulated catalogs, we empirically show that our new mixed integer program with quadratic constraints is able to be set up and solved much faster than previous large linear formulations. We also demonstrate our new approach on real-world data from the Hubble Source Catalog. This paper is accompanied by publicly available software to demonstrate the proposed method. 

   more » « less