Robustness verification is a promising technique for rigorously proving Recurrent Neural Networks (RNNs) robustly. A key challenge is to over-approximate the nonlinear activation functions with linear constraints, which can transform the verification problem into an efficiently solvable linear programming problem. Existing methods over-approximate the nonlinear parts with linear bounding planes individually, which may cause significant over-estimation and lead to lower verification accuracy. In this paper, in order to tightly enclose the three-dimensional nonlinear surface generated by the Hadamard product, we propose a novel truncated rectangular prism formed by two linear relaxation planes and a refinement-driven method to minimize both its volume and surface area for tighter over-approximation. Based on this approximation, we implement a prototype DeepPrism for RNN robustness verification. The experimental results demonstrate that DeepPrism has significant improvement compared with the state-of-the-art approaches in various tasks of image classification, speech recognition and sentiment analysis.

Deep Neural Networks (DNNs) are vulnerable to specially designed attacks due to their limited robustness. Abstraction methods can help extract critical features for learning, thereby reducing the disturbance caused by insignificant information. In this paper, we propose a pixelation-based abstraction method to enhance the empirical robustness of DNNs. The method partitions image pixels into superpixels and assigns each an appropriate colour from a continuously updated palette. Two hyperparameters control the abstraction level, allowing for resolution adjustment. Training and evaluation are conducted on pixelated datasets. Extensive experiments across benchmarks and loss landscape analysis demonstrate that our method (i) reduces attack success rates by up to 26.37% while maintaining high accuracy; (ii) exhibits a significant defense against diverse attack methods; and (iii) achieves smoother loss landscapes, underscoring its potential to enhance model robustness.

Hybrid systems with non-polynomial components are widely used in modeling safety critical applications. Due to the complexity arisen from the non-polynomial expression, safety verification for such systems presents a grand challenge. In this paper, we present a new general approach to synthesizing rational invariants for safety verification of non-polynomial hybrid systems (NPHSs). Through system transformation and rational approximation, a NPHS is transformed into an over-approximate hybrid system in rational form. Then, for the over-approximate rational hybrid system, the proposed framework exploits a symbolic-numeric computation method to generate its exact rational invariants, which guarantees the safety property of the original NPHS. The test results show that the rational invariants yield better performances than those obtained from polynomial invariants.

In this article, we address the problem of safety verification of nonlinear hybrid systems. A hybrid symbolic-numeric method is presented to compute exact inequality invariants of hybrid systems efficiently. Some numerical invariants of a hybrid system can be obtained by solving a bilinear SOS programming via the PENBMI solver or iterative method, then the modified Newton refinement and rational vector recovery techniques are applied to obtain exact polynomial invariants with rational coefficients, which exactly satisfy the conditions of invariants. Experiments on some benchmarks are given to illustrate the efficiency of our algorithm.

We present a method for determining the one-dimensional submodules of a Laurent-Ore module. The method is based on a correspondence between hyperexponential solutions of associated systems and one-dimensional submodules. The hyperexponential solutions are computed recursively by solving a sequence of first-order ordinary matrix equations. As the recursion proceeds, the matrix equations will have constant coefficients with respect to the operators that have been considered.

Picard-Vessiot extensions for ordinary differential and difference equations are well known and are at the core of the associated Galois theories. In this paper, we construct fundamental matrices and Picard-Vessiot extensions for systems of linear partial functional equations having finite linear dimension. We then use those extensions to show that all the solutions of a factor of such a system can be completed to solutions of the original system.