Sriram Sankaranarayanan

selected publications

1. Static Analysis of ReLU Neural Networks with Tropical Polyhedra

   Eric Goubault, Sebastien Palumby, Sylvie Putot, Louis Rustenholz, and Sriram Sankaranarayanan

   In Static Analysis Symposium (SAS), Lecture Notes in Computer Science Vol. 12913, pp. 166–190, 2021.

   Abs Bib URL

   This paper studies the problem of range analysis for feedforward neural networks, which is a basic primitive for applications such as robustness of neural networks, compliance to specifications and reachability analysis of neural-network feedback systems. Our approach focuses on ReLU (rectified linear unit) feedforward neural nets that present specific difficulties: approaches that exploit derivatives do not apply in general, the number of patterns of neuron activations can be quite large even for small networks, and convex approximations are generally too coarse. In this paper, we employ set-based methods and abstract interpretation that have been very successful in coping with similar difficulties in classical program verification. We present an approach that abstracts ReLU feedforward neural networks using tropical polyhedra. We show that tropical polyhedra can efficiently abstract ReLU activation function, while being able to control the loss of precision due to linear computations. We show how the connection between ReLU networks and tropical rational functions can provide approaches for range analysis of ReLU neural networks.

           @inproceedings{ Goubault+Others/2021/Static,
           title = { Static Analysis of ReLU Neural Networks with Tropical Polyhedra },
           author = {   Goubault, Eric  and    Palumby, Sebastien  and    Putot, Sylvie  and    Rustenholz, Louis  and    Sankaranarayanan, Sriram   },
           booktitle= { Static Analysis Symposium (SAS) },  
           year = { 2021 },  
           publisher = { Springer }, 
           pages = { 166–190 }, 
           
           series = { Lecture Notes in Computer Science },  
           volume = { 12913 },  
           
           
           }
           

2. Reasoning about Uncertainties in Discrete-Time Dynamical Systems using Polynomial Forms

   Sriram Sankaranarayanan, Yi Chou, Eric Goubault, and Sylvie Putot

   In Advances in Neural Information Processing System (NeurIPS), 2020.

   Abs Bib URL Supp

   In this paper, we propose polynomial forms to represent distributions of state variables over time for discrete-time stochastic dynamical systems. This problem arises in a variety of applications in areas ranging from biology to robotics. Our approach allows us to rigorously represent the probability distribution of state variables over time, and provide guaranteed bounds on the expectations, moments and probabilities of tail events involving the state variables. First, we recall ideas from interval arithmetic, and use them to rigorously represent the state variables at time t as a function of the initial state variables and noise symbols that model the random exogenous inputs encountered before time t. Next, we show how concentration of measure inequalities can be employed to prove rigorous bounds on the tail probabilities of these state variables. We demonstrate interesting applications that demonstrate how our approach can be useful in some situations to establish mathematically guaranteed bounds that are of a different nature from those obtained through simulations with pseudo-random numbers.

           @inproceedings{ Sankaranarayanan+Others/2020/Uncertainty,
           title = { Reasoning about Uncertainties in Discrete-Time Dynamical Systems using Polynomial Forms },
           author = {   Sankaranarayanan, Sriram  and    Chou, Yi  and    Goubault, Eric  and    Putot, Sylvie   },
           booktitle= { Advances in Neural Information Processing System (NeurIPS) },  
           year = { 2020 },  
           publisher = { Curran Associates }, 
           
           numpages = { 13 },  
           
           
           
           
           }
           

   Cf. Code and Examples

3. Quantitative Analysis of Programs with Probabilities and Concentration of Measure Inequalities

   Sriram Sankaranarayanan

   In Foundations of Probabilistic Programming (Editors: Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva), 2020.

   Abs Bib URL

   The quantitative analysis of probabilistic programs answers queries involving the expected values of program variables and expressions involving them, as well as bounds on the probabilities of assertions. In this chapter, we will present the use of concentration of measure inequalities to reason about such bounds. First, we will briefly present and motivate standard concentration of measure inequalities. Next, we survey approaches to reason about quantitative properties using concentration of measure inequalities, illustrating these on numerous motivating examples. Finally, we discuss currently open challenges in this area for future work.

           @inproceedings{ Sankaranaranyanan/2020/Concentration,
           title = { Quantitative Analysis of Programs with Probabilities and Concentration of Measure Inequalities },
           author = {   Sankaranarayanan, Sriram   },
           booktitle= { Foundations of Probabilistic Programming (Editors: Gilles Barthe, Joost-Pieter Katoen, and Alexandra Silva) },  
           year = { 2020 },  
           publisher = { Cambridge University Press }, 
           
           numpages = { 30 },  
           
           
           
           
           }
           

4. Reachability Analysis using Message Passing over Tree Decompositions.

   Sriram Sankaranarayanan

   In International Conference on Computer-Aided Verification (CAV), Lecture Notes in Computer Science (LNCS) Vol. 12224, pp. 604–628, 2020.

   Abs Bib URL

   In this paper, we study efficient approaches to reachability analysis for discrete-time nonlinear dynamical systems when the dependencies among the variables of the system have low treewidth. Reachability analysis over nonlinear dynamical systems asks if a given set of target states can be reached, starting from an initial set of states. This is solved by computing conservative over approximations of the reachable set using abstract domains to represent these approximations. However, most approaches must tradeoff the level of conservatism against the cost of performing analysis, especially when the number of system variables increases. This makes reachability analysis challenging for nonlinear systems with a large number of state variables. Our approach works by constructing a dependency graph among the variables of the system. The tree decomposition of this graph builds a tree wherein each node of the tree is labeled with subsets of the state variables of the system. Furthermore, the tree decomposition satisfies important structural properties. Using the tree decomposition, our approach abstracts a set of states of the high dimensional system into a tree of sets of lower dimensional projections of this state. We derive various properties of this abstract domain, including conditions under which the original high dimensional set can be fully recovered from its low dimensional projections. Next, we use ideas from message passing developed originally for belief propagation over Bayesian networks to perform reachability analysis over the full state space in an efficient manner. We illustrate our approach on some interesting nonlinear systems with low treewidth to demonstrate the advantages of our approach.

           @inproceedings{ Sankaranarayanan/2020/Tree,
           title = { Reachability Analysis using Message Passing over Tree Decompositions. },
           author = {   Sankaranarayanan, Sriram   },
           booktitle= { International Conference on Computer-Aided Verification (CAV) },  
           year = { 2020 },  
           publisher = { Springer }, 
           pages = { 604–628 }, 
           
           series = { Lecture Notes in Computer Science (LNCS) },  
           volume = { 12224 },  
           
           
           }