Author name cluster

Zhenbing Zeng

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

8 papers

1 author row

AAAI Conference 2026 Conference Paper

Tighter Truncated Rectangular Prism Approximation for RNN Robustness Verification

Xingqi Lin
Liangyu Chen
Min Wu
Min Zhang
Zhenbing Zeng

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.

PDF Details DOI

I&C Journal 2025 Journal Article

An iterative scheme of hybrid controller synthesis for nonlinear systems subject to safety constraints

Niuniu Qi
Xia Zeng
Banglong Liu
Zhengfeng Yang
Xiaochao Tang
Li Zhang
Chao Peng
Zhenbing Zeng

For many safety-critical systems, there is a pressing need for learning the controllers to endow systems with properties of safety. Reinforcement learning (RL) has emerged as a promising approach to synthesizing controllers that satisfy safety requirements by leveraging user-defined reward functions to encode desired system behavior. However, it remains a significant challenge in synthesizing provably correct controllers with safety requirements. To address this issue, we try to design a special hybrid polynomial-NN controller that is easy to verify without losing its expressiveness and flexibility. This paper proposes an iterative framework to synthesize a hybrid controller based on RL, low-degree polynomial fitting and knowledge distillation. By formulating and solving a constrained optimization problem in which the verification conditions produce the barrier certificates, a computational method is given to ensure that every trajectory starting from the initial set of the system with the resulting controller satisfies the given safety requirement. In addition, we have implemented a tool named SynHC and evaluated its performance over a set of benchmark examples. The experimental results demonstrate that our approach efficiently synthesizes safe DNN controllers.

Details DOI

IJCAI Conference 2025 Conference Paper

FGeo-HyperGNet: Geometric Problem Solving Integrating FormalGeo Symbolic System and Hypergraph Neural Network

Xiaokai Zhang
Yang Li
Na Zhu
Cheng Qin
Zhenbing Zeng
Tuo Leng

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.

PDF Details DOI

IJCAI Conference 2023 Conference Paper

A Novel Learnable Interpolation Approach for Scale-Arbitrary Image Super-Resolution

Jiahao Chao
Zhou Zhou
Hongfan Gao
Jiali Gong
Zhenbing Zeng
Zhengfeng Yang

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.

PDF Details DOI

AAAI Conference 2023 Conference Paper

Safety Verification of Nonlinear Systems with Bayesian Neural Network Controllers

Xia Zeng
Zhengfeng Yang
Li Zhang
Xiaochao Tang
Zhenbing Zeng
Zhiming Liu

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.

PDF Details DOI

TCS Journal 2016 Journal Article

Analyzing ultimate positivity for solvable systems

Ming Xu
Cheng-Chao Huang
Zhi-Bin Li
Zhenbing Zeng

The positivity problem is a foundational decision problem. It asks whether a dynamical system would keep the observing expression (over its states) positive. It has a derivative—the ultimate positivity problem, which allows that the observing expression is non-positive within a bounded time interval. For the two problems, most existing results are established on discrete-time dynamical systems, specifically on linear recurrence sequences. In this paper, however, we study the ultimate positivity problem for a class of continuous-time dynamical systems, called solvable systems. They subsume linear systems. For the general solvable system, we present a sufficient condition for inferring ultimate positivity. The validity of the condition can be algorithmically checked. Once it is valid, we can further find the time threshold, after which the observing expression would be always positive. On the other hand, we show that the ultimate positivity problem is decidable for some special classes of solvable systems, such as linear systems of dimension up to five.

Details DOI

TCS Journal 2009 Journal Article

Distance paired-domination problems on subclasses of chordal graphs

Lei Chen
Changhong Lu
Zhenbing Zeng

Let G = ( V, E ) be a graph without isolated vertices. For a positive integer k, a set S ⊆ V is a k -distance paired-dominating set if each vertex in V − S is within distance k of a vertex in S and the subgraph induced by S contains a perfect matching. In this paper, we present two linear time algorithms to find a minimum cardinality k -distance paired-dominating set in interval graphs and block graphs, which are two subclasses of chordal graphs. In addition, we present a characterization of trees with unique minimum k -distance paired-dominating set.

Details DOI

TCS Journal 2009 Journal Article

Hardness results and approximation algorithms for (weighted) paired-domination in graphs

Lei Chen
Changhong Lu
Zhenbing Zeng

Let G = ( V, E ) be a simple graph without isolated vertices. A vertex set S ⊆ V is a paired-dominating set if every vertex in V − S has a neighbor in S and the induced subgraph G [ S ] has a perfect matching. In this paper, we investigate the approximation hardness of paired-domination in graphs. For weighted paired-domination, an approximation algorithm in general graphs and an exact dynamic programming style algorithm in trees are also given.

Details DOI