arXiv subjects
Publications and source records attributed to Marcelo Forets.
We study the problem of computing the preimage of a set under a neural network with piecewise-affine activation functions. We recall an old result that the preimage of a polyhedral set is again a union of polyhedral sets and can be effectively computed. We show several applications of computing the preimage for analysis and interpretability of neural networks.
We study the verification problem for closed-loop dynamical systems with neural-network controllers (NNCS). This problem is commonly reduced to computing the set of reachable states. When considering dynamical systems and neural networks in isolation, there exist precise approaches for that task based on set representations respectively called Taylor models and zonotopes. However, the combination of these approaches to NNCS is non-trivial because, when converting between the set representations, dependency information gets lost in each control cycle and the accumulated approximation error quickly renders the result useless. We present an algorithm to chain approaches based on Taylor models and zonotopes, yielding a precise reachability algorithm for NNCS. Because the algorithm only acts at the interface of the isolated approaches, it is applicable to general dynamical systems and neural networks and can benefit from future advances in these areas. Our implementation delivers state-of-the-art performance and is the first to successfully analyze all benchmark problems of an annual reachability competition for NNCS.
We present the first review of methods to overapproximate the set of reachable states of linear time-invariant systems subject to uncertain initial states and input signals for short time horizons. These methods are fundamental to state-of-the-art reachability algorithms for long time horizons, which proceed in two steps: First they use such a method to discretize the system for a short time horizon, and then they efficiently obtain a solution of the new discrete system for the long time horizon. Traditionally, both qualitative and quantitative comparison between different reachability algorithms has only considered the combination of both steps. In this paper we study the first step in isolation. We perform a variety of numerical experiments for six fundamental discretization methods from the literature. As we show, these methods have different trade-offs regarding accuracy and computational cost and, depending on the characteristics of the system, some methods may be preferred over others. We also discuss preprocessing steps to improve the results and efficient implementation strategies.
LazySets.jl is a Julia library that provides ways to symbolically represent sets of points as geometric shapes, with a special focus on convex sets and polyhedral approximations. LazySets provides methods to apply common set operations, convert between different set representations, and efficiently compute with sets in high dimensions using specialized algorithms based on the set types. LazySets is the core library of JuliaReach, a cutting-edge software addressing the fundamental problem of reachability analysis: computing the set of states that are reachable by a dynamical system from all initial states and for all admissible inputs and parameters. While the library was originally designed for reachability and formal verification, its scope goes beyond such topics. LazySets is an easy-to-use, general-purpose and scalable library for computations that mix symbolics and numerics. In this article we showcase the basic functionality, highlighting some of the key design choices.
In this article we introduce a solution method for a special class of nonlinear initial-value problems using set-based propagation techniques. The novelty of the approach is that we employ a particular embedding (Carleman linearization) to leverage recent advances of high-dimensional reachability solvers for linear ordinary differential equations based on the support function. Using a global error bound for the Carleman linearization abstraction, we are able to describe the full set of behaviors of the system for sets of initial conditions and in dense time.
The Finite Element Method (FEM) is the gold standard for spatial discretization in numerical simulations for a wide spectrum of real-world engineering problems. Prototypical areas of interest include linear heat transfer and linear structural dynamics problems modeled with partial differential equations (PDEs). While different algorithms for direct integration of the equations of motion exist, exploring all feasible behaviors for varying loads, initial states and fluxes in models with large numbers of degrees of freedom remains a challenging task. In this article we propose a novel approach, based in set propagation methods and motivated by recent advances in the field of Reachability Analysis. Assuming a set of initial states and inputs, the proposed method consists in the construction of a union of sets (flowpipe) that enclose the infinite number of solutions of the spatially discretized PDE. We present the numerical results obtained in five examples to illustrate the capabilities of our approach, and compare its performance against reference numerical integration methods. We conclude that, for problems with single known initial conditions, the proposed method is accurate. For problems with uncertain initial conditions included in sets, the proposed method can compute all the solutions of the system more efficiently than numerical integration methods.
Efficiently handling time-triggered and possibly nondeterministic switches for hybrid systems reachability is a challenging task. In this paper we present an approach based on conservative set-based enclosure of the dynamics that can handle systems with uncertain parameters and inputs, where the uncertainties are bound to given intervals. The method is evaluated on the plant model of an experimental electro-mechanical braking system with periodic controller. In this model, the fast-switching controller dynamics requires simulation time scales of the order of nanoseconds. Accurate set-based computations for relatively large time horizons are known to be expensive. However, by appropriately decoupling the time variable with respect to the spatial variables, and enclosing the uncertain parameters using interval matrix maps acting on zonotopes, we show that the computation time can be lowered to 5000 times faster with respect to previous works. This is a step forward in formal verification of hybrid systems because reduced run-times allow engineers to introduce more expressiveness in their models with a relatively inexpensive computational cost.
Reachability analysis aims at identifying states reachable by a system within a given time horizon. This task is known to be computationally expensive for linear hybrid systems. Reachability analysis works by iteratively applying continuous and discrete post operators to compute states reachable according to continuous and discrete dynamics, respectively. In this paper, we enhance both of these operators and make sure that most of the involved computations are performed in low-dimensional state space. In particular, we improve the continuous-post operator by performing computations in high-dimensional state space only for time intervals relevant for the subsequent application of the discrete-post operator. Furthermore, the new discrete-post operator performs low-dimensional computations by leveraging the structure of the guard and assignment of a considered transition. We illustrate the potential of our approach on a number of challenging benchmarks.
We present JuliaReach, a toolbox for set-based reachability analysis of dynamical systems. JuliaReach consists of two main packages: Reachability, containing implementations of reachability algorithms for continuous and hybrid systems, and LazySets, a standalone library that implements state-of-the-art algorithms for calculus with convex sets. The library offers both concrete and lazy set representations, where the latter stands for the ability to delay set computations until they are needed. The choice of the programming language Julia and the accompanying documentation of our toolbox allow researchers to easily translate set-based algorithms from mathematics to software in a platform-independent way, while achieving runtime performance that is comparable to statically compiled languages. Combining lazy operations in high dimensions and explicit computations in low dimensions, JuliaReach can be applied to solve complex, large-scale problems.
We consider the problem of approximating numerically the moments and the supports of measures which are invariant with respect to the dynamics of continuous- and discrete-time polynomial systems, under semialgebraic set constraints. First, we address the problem of approximating the density and hence the support of an invariant measure which is absolutely continuous with respect to the Lebesgue measure. Then, we focus on the approximation of the support of an invariant measure which is singular with respect to the Lebesgue measure. Each problem is handled through an appropriate reformulation into a linear optimization problem over measures, solved in practice with two hierarchies of finite-dimensional semidefinite moment-sum-of-square relaxations, also called Lasserre hierarchies. Under specific assumptions, the first Lasserre hierarchy allows to approximate the moments of an absolutely continuous invariant measure as close as desired and to extract a sequence of polynomials converging weakly to the density of this measure. The second Lasserre hierarchy allows to approximate as close as desired in the Hausdorff metric the support of a singular invariant measure with the level sets of the Christoffel polynomials associated to the moment matrices of this measure. We also present some application examples together with numerical results for several dynamical systems admitting either absolutely continuous or singular invariant measures.
Approximating the set of reachable states of a dynamical system is an algorithmic yet mathematically rigorous way to reason about its safety. Although progress has been made in the development of efficient algorithms for affine dynamical systems, available algorithms still lack scalability to ensure their wide adoption in the industrial setting. While modern linear algebra packages are efficient for matrices with tens of thousands of dimensions, set-based image computations are limited to a few hundred. We propose to decompose reach set computations such that set operations are performed in low dimensions, while matrix operations like exponentiation are carried out in the full dimension. Our method is applicable both in dense- and discrete-time settings. For a set of standard benchmarks, it shows a speed-up of up to two orders of magnitude compared to the respective state-of-the art tools, with only modest losses in accuracy. For the dense-time case, we show an experiment with more than 10.000 variables, roughly two orders of magnitude higher than possible with previous approaches.
We revisit the method of Carleman linearization for systems of ordinary differential equations with polynomial right-hand sides. This transformation provides an approximate linearization in a higher-dimensional space through the exact embedding of polynomial nonlinearities into an infinite-dimensional linear system, which is then truncated to obtain a finite-dimensional representation with an additive error. To the best of our knowledge, no explicit calculation of the error bound has been studied. In this paper, we propose two strategies to obtain a time-dependent function that locally bounds the truncation error. In the first approach, we proceed by iterative backwards-integration of the truncated system. However, the resulting error bound requires an a priori estimate of the norm of the exact solution for the given time horizon. To overcome this difficulty, we construct a combinatorial approach and solve it using generating functions, obtaining a local error bound that can be computed effectively.
Mechanistic models in biology often involve numerous parameters about which we do not have direct experimental information. The traditional approach is to fit these parameters using extensive numerical simulations (e.g. by the Monte-Carlo method), and eventually revising the model if the predictions do not correspond to the actual measurements. In this work we propose a methodology for hybrid automaton model revision, when new type of functions are needed to capture time varying parameters. To this end, we formulate a hybrid optimal control problem with intermediate points as successive infinite-dimensional linear programs (LP) on occupation measures. Then, these infinite-dimensional LPs are solved using a hierarchy of semidefinite relaxations. The whole procedure is exposed on a recent model for haemoglobin production in erythrocytes.
A discrete-time Quantum Walk (QW) is essentially a unitary operator driving the evolution of a single particle on the lattice. Some QWs admit a continuum limit, leading to familiar PDEs (e.g. the Dirac equation). In this paper, we study the continuum limit of a wide class of QWs, and show that it leads to an entire class of PDEs, encompassing the Hamiltonian form of the massive Dirac equation in $(1+1)$ curved spacetime. Therefore a certain QW, which we make explicit, provides us with a unitary discrete toy model of a test particle in curved spacetime, in spite of the fixed background lattice. Mathematically we have introduced two novel ingredients for taking the continuum limit of a QW, but which apply to any quantum cellular automata: encoding and grouping.
We formalize a notion of discrete Lorentz transforms for Quantum Walks (QW) and Quantum Cellular Automata (QCA), in (1 + 1)-dimensional discrete spacetime. The theory admits a diagrammatic representation in terms of a few local, circuit equivalence rules. Within this framework, we show the first-order-only covariance of the Dirac QW. We then introduce the Clock QW and the Clock QCA, and prove that they are exactly discrete Lorentz covariant. The theory also allows for non-homogeneous Lorentz transforms, between non-inertial frames.
The Dirac equation can be modelled as a quantum walk, with the quantum walk being: discrete in time and space (i.e. a unitary evolution of the wave-function of a particle on a lattice); homogeneous (i.e. translation-invariant and time-independent), and causal (i.e. information propagates at a bounded speed, in a strict sense). This quantum walk model was proposed independently by Succi and Benzi, Bialynicki-Birula and Meyer: we rederive it in a simple way in all dimensions and for hyperbolic symmetric systems in general. We then prove that for any time t, the model converges to the continuous solution of the Dirac equation at time t, i.e. the probability of observing a discrepancy between the model and the solution is an O(ε^2), with ε the discretization step. At the practical level, this result is of interest for the quantum simulation of relativistic particles. At the theoretical level, it reinforces the status of this quantum walk model as a simple, discrete toy model of relativistic particles. Keywords: Friedrichs symmetric hyperbolic systems, Quantum Walk, Quantum Lattice Gas Automata, Quantum Computation, Trotter-Kato, Baker-Campbell-Thomson, Operator splitting, Lax theorem