Automated Functional Decomposition for Hybrid Zonotope Over-approximations with Application to LSTM Networks

TL;DR

The paper addresses the challenge of efficiently analyzing high-dimensional nonlinear functions by introducing automated functional decomposition methods that yield compact, tractable representations for set-based over-approximations using hybrid zonotopes. It develops a systematic pipeline from infix expressions to functional decompositions via Reverse Polish Notation, while mitigating redundant observables and excessive unary decompositions, and extending to vector-valued and multi-input cases. The authors apply these methods to over-approximate the input-output graph of an LSTM network and to represent a discrete hybrid automaton, demonstrating the practicality and scalability of the approach with concrete numerical results and complexity metrics. This work enables scalable, rigorous reachability and verification for complex nonlinear and hybrid systems by providing automated, decomposition-driven set representations that can capture rich dynamics without exponential growth in complexity.

Abstract

Functional decomposition is a powerful tool for systems analysis because it can reduce a function of arbitrary input dimensions to the sum and superposition of functions of a single variable, thereby mitigating (or potentially avoiding) the exponential scaling often associated with analyses over high-dimensional spaces. This paper presents automated methods for constructing functional decompositions used to form set-based over-approximations of nonlinear functions, with particular focus on the hybrid zonotope set representation. To demonstrate these methods, we construct a hybrid zonotope set that over-approximates the input-output graph of a long short-term memory neural network, and use functional decomposition to represent a discrete hybrid automaton via a hybrid zonotope.

Figures (5)

• Figure 1: Over-approximations of the graph of \ref{['eqn-ROex-RPN']}, obtained using functional decompositions generated by Algorithm \ref{['alg:RPN2FD']} (dark blue and cyan) and Algorithm \ref{['alg:RPN2FD_mod']} (cyan only).
• Figure 2: Graph representation of \ref{['eq:nested']} being simplified to \ref{['eq:un-nested']} according to Algorithm \ref{['alg:ReduceUUD']}. Gray-filled vertices indicate $V_i$ and $V_j$. Blue and red-outlined vertices indicate elements of the intersection of forward walks $\mathcal{W}_i$ from $V_i$ and reverse walks $\mathcal{M}_j$ from $V_j$, respectively. (a) $V_1 \notin \mathcal{M}_3$. (b) $V_2 \notin \mathcal{M}_3$. (c) $A_{i,j}=0$. (d) This iteration satisfies all conditions in lines 6, 7, and 8 of Algorithm \ref{['alg:ReduceUUD']}. (e) The resulting graph from lines 9 and 10 of Algorithm \ref{['alg:ReduceUUD']}.
• Figure 3: Graph representation of \ref{['eq:nested']} being simplified to \ref{['eq:un-nested']} according to Algorithm \ref{['alg:ReduceUUD']} with $V_4$ and $V_8$ listed as protected vertices.
• Figure 4: The LSTM network $\mathcal{F}$ was trained on the function $f(t)$ given in \ref{['eqn:LSTM_time_eqn']} for values $t\in\{0,1,2,\dots,800\}$, and its predictions were tested against the values for $t\in\{801,802,\dots,1000\}$.
• Figure 5: Hybrid zonotope (HZ) over-approximation of the network $\mathcal{F}$, along with sampled input-output pairs of $\mathcal{F}$, for the first prediction step of the network after training on the first 800 points (i.e., the hidden state and cell state have evolved to the values $h_{800}$ and $c_{800}$).