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.

Safe controller synthesis is crucial for safety-critical applications. This paper presents a novel reinforcement learning approach to synthesize safe controllers for NN-controlled systems. The core idea leverages an iterative scheme that combines controller learning with neural barrier certificate (BC) verification, ultimately producing a provably safe deep neural network (DNN) controller with formal safety guarantees. The process begins by pre-training a well-performing DNN controller as an “oracle” via deep reinforcement learning (DRL). To formally verify the safety properties of the closed-loop system under the base controller, we devise a formal verification procedure that approximates the DNN controller using polynomial inclusion, followed by synthesizing neural BCs via sum-of-squares (SOS) relaxation. In cases where the base controller is insufficient to yield a real BC, the current spurious BC is incorporated as an additional penalty term to reshape the RL reward function, guiding the iterative refinement for new controllers. We implement an automated tool, NBCRL, and experimental results demonstrate the benefits of our method in terms of efficiency and scalability even for a nonlinear system with dimension up to 12.

Geometric problem solving has always been a long-standing challenge in the fields of mathematical reasoning and artificial intelligence. We built a neural-symbolic system, called FGeo-HyperGNet, to automatically perform human-like geometric problem solving. The symbolic component is a formal system built on FormalGeo, which can automatically perform geometric relational reasoning and algebraic calculations and organize the solution into a hypergraph with conditions as hypernodes and theorems as hyperedges. The neural component, called HyperGNet, is a hypergraph neural network based on the attention mechanism, including an encoder to effectively encode the structural and semantic information of the hypergraph and a theorem predictor to provide guidance in solving problems. The neural component predicts theorems according to the hypergraph, and the symbolic component applies theorems and updates the hypergraph, thus forming a predict-apply cycle to ultimately achieve readable and traceable automatic solving of geometric problems. Experiments demonstrate the correctness and effectiveness of this neural-symbolic architecture. We achieved state-of-the-art results with a TPA of 93.50% and a PSSR of 88.36% on the FormalGeo7K dataset.

Controller synthesis for nonlinear systems is an important research issue. Deep Neural Network (DNN) control policies obtained through reinforcement learning (RL), though exhibiting good performance in simulations, cannot be applied to safety-critical systems for lack of formal guarantee. To address this, this paper considers fully utilizing the advantages of RL for complex control tasks to obtain a well-performing DNN controller. Then, using PAC (Probably Approximately Correct) techniques, a polynomial surrogate controller with probabilistically controllable approximation error is obtained. Finally, the safety of the control system under the designed polynomial controller is verified using barrier certificate generation. Experiments demonstrate the effectiveness of our method in generating controllers with safety guarantees for systems with high dimensions and degrees.

There is a pressing need to ensure the safety of closed-loop systems with neural network controllers, as they are often incorporated into safety-critical applications. To address this issue, we propose a novel approach for generating barrier certificates, which combines counterexample-guided learning with efficient Sum-Of-Squares (SOS) based verification. By leveraging barrier certificate candidates obtained from the learning phase, our proposed method offers an efficient verification procedure that solves three Linear Matrix Inequality (LMI) constraint feasibility testing problems, instead of relying on an SMT solver to verify the barrier certificate conditions. We conduct comparison experiments on a set of benchmarks, demonstrating the advantages of our method in terms of efficiency and scalability, which enable effective verification of high-dimensional systems.

Bayesian neural networks (BNNs) retain NN structures with a probability distribution placed over their weights. With the introduced uncertainties and redundancies, BNNs are proper choices of robust controllers for safety-critical control systems. This paper considers the problem of verifying the safety of nonlinear closed-loop systems with BNN controllers over unbounded-time horizon. In essence, we compute a safe weight set such that as long as the BNN controller is always applied with weights sampled from the safe weight set, the controlled system is guaranteed to be safe. We propose a novel two-phase method for the safe weight set computation. First, we construct a reference safe control set that constraints the control inputs, through polynomial approximation to the BNN controller followed by polynomial-optimization-based barrier certificate generation. Then, the computation of safe weight set is reduced to a range inclusion problem of the BNN on the system domain w.r.t. the safe control set, which can be solved incrementally and the set of safe weights can be extracted. Compared with the existing method based on invariant learning and mixed-integer linear programming, we could compute safe weight sets with larger radii on a series of linear benchmarks. Moreover, experiments on a series of widely used nonlinear control tasks show that our method can synthesize large safe weight sets with probability measure as high as 95% even for a large-scale system of dimension 7.

Abstract There is a pressing need for learning controllers to endow systems with properties of safety and goal-reaching, which are crucial for many safety-critical systems. Reinforcement learning (RL) has been deployed successfully to synthesize controllers from user-defined reward functions encoding desired system requirements. However, it remains a significant challenge in synthesizing provably correct controllers with safety and goal-reaching requirements. To address this issue, we try to design a special hybrid polynomial-DNN controller which is easy to verify without losing its expressiveness and flexibility. This paper proposes a novel method to synthesize such a hybrid controller based on RL, low-degree polynomial fitting and knowledge distillation. It also gives a computational approach, by building and solving a constrained optimization problem coming from verification conditions to produce barrier certificates and Lyapunov-like functions, which can guarantee every trajectory from the initial set of the system with the resulted controller satisfies the given safety and goal-reaching requirements. We evaluate the proposed hybrid controller synthesis method on a set of benchmark examples, including several high-dimensional systems. The results validate the effectiveness and applicability of our approach.

In recent years, there has been an increasing demand for real-time super-resolution networks on mobile devices. To address this issue, many lightweight super-resolution models have been proposed. However, these models still contain time-consuming components that increase inference latency, limiting their real-world applications on mobile devices. In this paper, we propose a novel model for single-image super-resolution based on Equivalent Transformation and Dual Stream network construction (ETDS). ET method is proposed to transform time-consuming operators into time-friendly operations, such as convolution and ReLU, on mobile devices. Then, a dual stream network is designed to alleviate redundant parameters resulting from the use of ET and enhance the feature extraction ability. Taking full advantage of the advance of ET and the dual stream network structure, we develop the efficient SR model ETDS for mobile devices. The experimental results demonstrate that our ETDS achieves superior inference speed and reconstruction quality compared to previous lightweight SR methods on mobile devices. The code is available at https://github.com/ECNUSR/ETDS.

There is a pressing need to synthesize provable safety controllers for nonlinear systems as they are embedded in many safety-critical applications. In this paper, we propose a safe Meta Reinforcement Learning (Meta-RL) approach to synthesize deep neural network (DNN) controllers for nonlinear systems subject to safety constraints. Our approach incorporates two phases: Meta-RL for training the controller network, and formal safety verification based on polynomial optimization solving. In the training phase, we provide a training framework which pre-trains a unified meta-initial controller for control systems by meta-learning. An important benefit of the proposed Meta-RL approach lies in that it is much more effective and succeeds in more controller training tasks compared with existing typical RL methods, e.g., Deep Deterministic Policy Gradient (DDPG). To formally verify the safety properties of the closed-loop system with the learned controller, we develop a verification procedure by using polynomial inclusion computation in combination with barrier certificate generation. Experiments on a set of benchmarks, including systems with dimension up to 12, demonstrate the effectiveness and applicability of our method.

Blind super-resolution, different from conventional non-blind super-resolution based on the assumption of fixed degradation, handles various unknown Gaussian blur kernels, and thus is closer to real-world application. The accuracy of kernel estimation and deconvolution directly influences the performance of overall super-resolution results, but recent works usually introduce artifacts during the process. In this paper, we propose our methods of a more accurate kernel estimation module (KEM) and deconvolution module (DM). Additionally, KEM and DM are embedded in kernel estimation and deconvolution structure (KEDS), which improves the results to a large extent once combined with non-blind networks.

Deep convolutional neural networks (CNNs) have achieved unprecedented success in single image super-resolution over the past few years. Meanwhile, there is an increasing demand for single image super-resolution with arbitrary scale factors in real-world scenarios. Many approaches adopt scale-specific multi-path learning to cope with multi-scale super-resolution with a single network. However, these methods require a large number of parameters. To achieve a better balance between the reconstruction quality and parameter amounts, we proposes a learnable interpolation method that leverages the advantages of neural networks and interpolation methods to tackle the scale-arbitrary super-resolution task. The scale factor is treated as a function parameter for generating the kernel weights for the learnable interpolation. We demonstrate that the learnable interpolation builds a bridge between neural networks and traditional interpolation methods. Experiments show that the proposed learnable interpolation requires much fewer parameters and outperforms state-of-the-art super-resolution methods.

With the increasing availability of devices that support ultra-high-definition (UHD) images, Single Image Super Resolution (SISR) has emerged as a crucial problem in the field of computer vision. In recent years, CNN-based super resolution approaches have made significant advances, producing high-quality upscaled images. However, these methods can be computationally and memory intensive, making them impractical for real-time applications such as upscaling to UHD images. The performance and reconstruction quality may suffer due to the complexity and diversity of larger image content. Therefore, there is a need to develop efficient super resolution approaches that can meet the demands of processing high-resolution images. In this paper, we propose a simple network named PCEVAnet by constructing the PCEVA block, which leverages Partial Convolution and Efficient Variance Attention. Partial Convolution is employed to streamline the feature extraction process by minimizing memory access. And Efficient Variance Attention (EVA) captures the high-frequency information and long-range dependency via the variance and max pooling. We conduct extensive experiments to demonstrate that our model achieves a better trade-off between performance and actual running time than previous methods.

Adversarial training is an efficacious defense approach to protect classification model against adversarial attacks. In this paper, we reveal that a significant difference exists between the feature map of the original sample and that of its corresponding adversarial version. Based on this main insight, we propose a novel robust training on feature-based adversarial examples approach called FPAT, where training examples are generated by maximizing the loss function between the clean and the adversarial feature maps. We show via extensive experiments on MNIST, SVHN and CIFAR-10, that our proposed method is as effective as the state-of-the-art robust training methods. Especially, when the adversarial perturbation is of a large radius or the number of adversarial steps of training samples is small, FPAT achieves leading robustness.

Abstract In this paper, we propose a safe reinforcement learning approach to synthesize deep neural network (DNN) controllers for nonlinear systems subject to safety constraints. The proposed approach employs an iterative scheme where alearnerand averifierinteract to synthesize safe DNN controllers. Thelearnertrains a DNN controller via deep reinforcement learning, and theverifiercertifies the learned controller through computing a maximal safe initial region and its corresponding barrier certificate, based on polynomial abstraction and bilinear matrix inequalities solving. Compared with the existing verification-in-the-loop synthesis methods, our iterative framework is a sequential synthesis scheme of controllers and barrier certificates, which can learn safe controllers with adaptive barrier certificates rather than user-defined ones. We implement the tool SRLBC and evaluate its performance over a set of benchmark examples. The experimental results demonstrate that our approach efficiently synthesizes safe DNN controllers even for a nonlinear system with dimension up to 12.

In this paper, we presented a formalization to the Clock Theory of He Jifeng in the Isabelle interactive theorem prover, we described the basic concepts of the theory in Isabelle and proved its soundness for programming hybrid systems.

In this paper, we proved that for any tetrahedron T , there exists at least one, at most eight non-congruent tetrahedra so that they share the same volume, circumradius and four face areas. We used metric invariants of tetrahedra to construct the equation system and investigated the number of its real rootswith symbolic computation. We also posed one open problem on the basis of extensive numerical computation.

In this paper, we present a study on building a special SAARA (Self-Aware Automated Reasoning Agent) system for solving Freudenthal's Sum and Product puzzle, aimed to train the "self-reflection" and "subjective experience" abilities as in the Three Wise Men test performed by the Nao robots in Rensselaer Polytechnic Institute in July 2015. We show the dynamic evolution of corresponding knowledge sets in the automated reasoning process for the Sum and Product puzzle.

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 ISSAC 2000, P. Lisoněk and R.B. Israel [3] asked whether, for any given positive real constants V,R,A1,A2,A3,A4, there are always finitely many tetrahedra, all having these values as their respective volume, circumradius and four face areas. In this paper we present a negative solution to this problem by constructing a family of tetrahedra T(x,y) where $(x,y)$ varies over a component of a cubic curve such that all tetrahedra T(x,y) share the same volume, circumradius and face areas.