arXiv subjects

Lijun Zhang

Publications and source records attributed to Lijun Zhang.

At least 163 records · Page 9Linked to original sources

arXiv2023

Provable Reach-avoid Controllers Synthesis Based on Inner-approximating Controlled Reach-avoid Sets

In this paper, we propose an approach for synthesizing provable reach-avoid controllers, which drive a deterministic system operating in an unknown environment to safely reach a desired target set. The approach falls within the reachability analysis framework and is based on the computation of inner-approximations of controlled reach-avoid sets(CRSs). Given a target set and a safe set, the controlled reach-avoid set is the set of states such that starting from each of them, there exists at least one controller to ensure that the system can enter the target set while staying inside the safe set before the target hitting time. Therefore, the boundary of the controlled reach-avoid set acts as a barrier, which separating states capable of achieving the reach-avoid objective from those that are not, and thus the computed inner-approximation provides a viable space for the system to achieve the reach-avoid objective. Our approach for synthesizing reach-avoid controllers mainly consists of three steps. We first learn a safe set of states in the unknown environment from sensor measurements based on a support vector machine approach. Then, based on the learned safe set and target set, we compute an inner-approximation of the CRS. Finally, we synthesize controllers online to ensure that the system will reach the target set by evolving inside the computed inner-approximation. The proposed method is demonstrated on a Dubin's car system.

eess.SY↗

arXiv2023

Structured Pruning for Multi-Task Deep Neural Networks

Although multi-task deep neural network (DNN) models have computation and storage benefits over individual single-task DNN models, they can be further optimized via model compression. Numerous structured pruning methods are already developed that can readily achieve speedups in single-task models, but the pruning of multi-task networks has not yet been extensively studied. In this work, we investigate the effectiveness of structured pruning on multi-task models. We use an existing single-task filter pruning criterion and also introduce an MTL-based filter pruning criterion for estimating the filter importance scores. We prune the model using an iterative pruning strategy with both pruning methods. We show that, with careful hyper-parameter tuning, architectures obtained from different pruning methods do not have significant differences in their performances across tasks when the number of parameters is similar. We also show that iterative structure pruning may not be the best way to achieve a well-performing pruned model because, at extreme pruning levels, there is a high drop in performance across all tasks. But when the same models are randomly initialized and re-trained, they show better results.

cs.LG↗

arXiv2023

Vehicle Trajectory Prediction based Predictive Collision Risk Assessment for Autonomous Driving in Highway Scenarios

For driving safely and efficiently in highway scenarios, autonomous vehicles (AVs) must be able to predict future behaviors of surrounding object vehicles (OVs), and assess collision risk accurately for reasonable decision-making. Aiming at autonomous driving in highway scenarios, a predictive collision risk assessment method based on trajectory prediction of OVs is proposed in this paper. Firstly, the vehicle trajectory prediction is formulated as a sequence generation task with long short-term memory (LSTM) encoder-decoder framework. Convolutional social pooling (CSP) and graph attention network (GAN) are adopted for extracting local spatial vehicle interactions and distant spatial vehicle interactions, respectively. Then, two basic risk metrics, time-to-collision (TTC) and minimal distance margin (MDM), are calculated between the predicted trajectory of OV and the candidate trajectory of AV. Consequently, a time-continuous risk function is constructed with temporal and spatial risk metrics. Finally, the vehicle trajectory prediction model CSP-GAN-LSTM is evaluated on two public highway datasets. The quantitative results indicate that the proposed CSP-GAN-LSTM model outperforms the existing state-of-the-art (SOTA) methods in terms of position prediction accuracy. Besides, simulation results in typical highway scenarios further validate the feasibility and effectiveness of the proposed predictive collision risk assessment method.

cs.RO↗

arXiv2023

On the Power of Finite Ambiguity in Büchi Complementation

In this work, we exploit the power of \emph{finite ambiguity} for the complementation problem of Büchi automata by using reduced run directed acyclic graphs (DAGs) over infinite words, in which each vertex has at most one predecessor; these reduced run DAGs have only a finite number of infinite runs, thus obtaining the finite ambiguity in Büchi complementation. We show how to use this type of reduced run DAGs as a unified tool to optimize both rank-based and slice-based complementation constructions for Büchi automata with a finite degree of ambiguity. As a result, given a Büchi automaton with $n$ states and a finite degree of ambiguity, the number of states in the complementary Büchi automaton constructed by the classical rank-based and slice-based complementation constructions can be improved from $2^{\mathsf{O}(n \log n)}$ and $\mathsf{O}((3n)^{n})$ to $\mathsf{O}(6^{n}) \subseteq 2^{\mathsf{O}(n)}$ and $\mathsf{O}(4^{n})$, respectively. We further show how to construct such reduced run DAGs for limit deterministic Büchi automata and obtain a specialized complementation algorithm, thus demonstrating the generality of the power of finite ambiguity.

cs.FL↗

arXiv2023

Realization of the transient dynamics of dimension-varying control systems

Dynamic evolution behaviors of dimension-varying control systems often appear in the genetic regulatory network and the vehicle clutch system etc. An interesting and significant study on dimension-varying control systems is how to realize the dimension-varying (the transient dynamics) process smoothly between the different dimensional subsystems. The quotient space approach is considered as an effective tool to model the transient dynamics of dimension-varying control systems.This paper investigates the realization problem of the transient dynamics of dimension-varying control systems. By revealing the structure of the controllable subspace for the linear system on quotient space, we propose the condition for the realization of the transient dynamics of dimension-varying control systems, based on which a new scheme for modeling the transient dynamics is given. Moreover, the proposed scheme justifies the existing result for the strategy for modelling the transient dynamics. A numeric example is given to illustrate our theoretical results.

math.OC↗

arXiv2023

Variant Plateau Law in Atomically Thin Transition Metal Dichalcogenide Dome Networks

Since its fundamental inception from soap bubbles, Plateau law has sparked extensive research in equilibrated states. However, most studies primarily relied on liquids, foams or cellular structures, whereas its applicability has yet to be explored in nano-scale solid films. Here, we observed a variant Plateau law in networks of atomically thin domes made of solid two-dimensional (2D) transition metal dichalcogenides (TMDs). Discrete layer-dependent van der Waals (vdWs) interaction energies were experimentally and theoretically obtained for domes protruding in different TMD layers. Significant surface tension differences from layer-dependent vdWs interaction energies manifest in a variant of this fundamental law. Meanwhile, the remarkable mechanical properties, gas impermeability and interlayer vdWs interaction energy of TMD films enable domes and the networks to sustain high gas pressure and exist in a fundamentally variant nature for several years. Our findings pave the way towards exploring variant discretised states with applications in opto-electro-mechanical devices.

cond-mat.mtrl-sci↗

arXiv2023

Incremental Satisfiability Modulo Theory for Verification of Deep Neural Networks

Constraint solving is an elementary way for verification of deep neural networks (DNN). In the domain of AI safety, a DNN might be modified in its structure and parameters for its repair or attack. For such situations, we propose the incremental DNN verification problem, which asks whether a safety property still holds after the DNN is modified. To solve the problem, we present an incremental satisfiability modulo theory (SMT) algorithm based on the Reluplex framework. We simulate the most important features of the configurations that infers the verification result of the searching branches in the old solving procedure (with respect to the original network), and heuristically check whether the proofs are still valid for the modified DNN. We implement our algorithm as an incremental solver called DeepInc, and exerimental results show that DeepInc is more efficient in most cases. For the cases that the property holds both before and after modification, the acceleration can be faster by several orders of magnitude, showing that DeepInc is outstanding in incrementally searching for counterexamples. Moreover, based on the framework, we propose the multi-objective DNN repair problem and give an algorithm based on our incremental SMT solving algorithm. Our repair method preserves more potential safety properties on the repaired DNNs compared with state-of-the-art.

cs.AI↗

arXiv2023

Large-scale Stochastic Optimization of NDCG Surrogates for Deep Learning with Provable Convergence

NDCG, namely Normalized Discounted Cumulative Gain, is a widely used ranking metric in information retrieval and machine learning. However, efficient and provable stochastic methods for maximizing NDCG are still lacking, especially for deep models. In this paper, we propose a principled approach to optimize NDCG and its top-$K$ variant. First, we formulate a novel compositional optimization problem for optimizing the NDCG surrogate, and a novel bilevel compositional optimization problem for optimizing the top-$K$ NDCG surrogate. Then, we develop efficient stochastic algorithms with provable convergence guarantees for the non-convex objectives. Different from existing NDCG optimization methods, the per-iteration complexity of our algorithms scales with the mini-batch size instead of the number of total items. To improve the effectiveness for deep learning, we further propose practical strategies by using initial warm-up and stop gradient operator. Experimental results on multiple datasets demonstrate that our methods outperform prior ranking approaches in terms of NDCG. To the best of our knowledge, this is the first time that stochastic algorithms are proposed to optimize NDCG with a provable convergence guarantee. Our proposed methods are implemented in the LibAUC library at https://libauc.org/.

cs.LG↗

arXiv2023

Uplifting Message Passing Neural Network with Graph Original Information

Message passing neural networks (MPNNs) learn the representation of graph-structured data based on graph original information, including node features and graph structures, and have shown astonishing improvement in node classification tasks. However, the expressive power of MPNNs is upper bounded by the first-order Weisfeiler-Leman test and its accuracy still has room for improvement. This work studies how to improve MPNNs' expressiveness and generalizability by fully exploiting graph original information both theoretically and empirically. It further proposes a new GNN model called INGNN (INformation-enhanced Graph Neural Network) that leverages the insights to improve node classification performance. Extensive experiments on both synthetic and real datasets demonstrate the superiority (average rank 1.78) of our INGNN compared with state-of-the-art methods.

cs.LG↗

arXiv2023

ECSAS: Exploring Critical Scenarios from Action Sequence in Autonomous Driving

Critical scenario generation requires the ability of sampling critical combinations from the infinite parameter space in the logic scenario. Existing solutions aim to explore the correlation of action parameters in the initial scenario rather than action sequences. How to model action sequences so that one can further consider the effects of different action parameters in the scenario is the bottleneck of the problem. In this paper, we attack the problem by proposing the ECSAS framework. Specifically, we first propose a description language, BTScenario, allowing us to model action sequences of the scenarios. We then use reinforcement learning to search for combinations of critical action parameters. To increase efficiency, we further propose several optimizations, including action masking and replay buffer. We have implemented ECSAS, and experimental results show that it is more efficient than native approaches such as random and combination testing in various nontrivial scenarios.

cs.AI↗

arXiv2022

Multi-block-Single-probe Variance Reduced Estimator for Coupled Compositional Optimization

Variance reduction techniques such as SPIDER/SARAH/STORM have been extensively studied to improve the convergence rates of stochastic non-convex optimization, which usually maintain and update a sequence of estimators for a single function across iterations. What if we need to track multiple functional mappings across iterations but only with access to stochastic samples of $\mathcal{O}(1)$ functional mappings at each iteration? There is an important application in solving an emerging family of coupled compositional optimization problems in the form of $\sum_{i=1}^m f_i(g_i(\mathbf{w}))$, where $g_i$ is accessible through a stochastic oracle. The key issue is to track and estimate a sequence of $\mathbf g(\mathbf{w})=(g_1(\mathbf{w}), \ldots, g_m(\mathbf{w}))$ across iterations, where $\mathbf g(\mathbf{w})$ has $m$ blocks and it is only allowed to probe $\mathcal{O}(1)$ blocks to attain their stochastic values and Jacobians. To improve the complexity for solving these problems, we propose a novel stochastic method named Multi-block-Single-probe Variance Reduced (MSVR) estimator to track the sequence of $\mathbf g(\mathbf{w})$. It is inspired by STORM but introduces a customized error correction term to alleviate the noise not only in stochastic samples for the selected blocks but also in those blocks that are not sampled. With the help of the MSVR estimator, we develop several algorithms for solving the aforementioned compositional problems with improved complexities across a spectrum of settings with non-convex/convex/strongly convex/Polyak-Łojasiewicz (PL) objectives. Our results improve upon prior ones in several aspects, including the order of sample complexities and dependence on the strong convexity parameter. Empirical studies on multi-task deep AUC maximization demonstrate the better performance of using the new estimator.

cs.LG↗

arXiv2022

Safety Analysis of Autonomous Driving Systems Based on Model Learning

We present a practical verification method for safety analysis of the autonomous driving system (ADS). The main idea is to build a surrogate model that quantitatively depicts the behaviour of an ADS in the specified traffic scenario. The safety properties proved in the resulting surrogate model apply to the original ADS with a probabilistic guarantee. Furthermore, we explore the safe and the unsafe parameter space of the traffic scenario for driving hazards. We demonstrate the utility of the proposed approach by evaluating safety properties on the state-of-the-art ADS in literature, with a variety of simulated traffic scenarios.

cs.AI↗

arXiv2022

Optimal Algorithms for Stochastic Multi-Level Compositional Optimization

In this paper, we investigate the problem of stochastic multi-level compositional optimization, where the objective function is a composition of multiple smooth but possibly non-convex functions. Existing methods for solving this problem either suffer from sub-optimal sample complexities or need a huge batch size. To address these limitations, we propose a Stochastic Multi-level Variance Reduction method (SMVR), which achieves the optimal sample complexity of $\mathcal{O}\left(1 / ε^{3}\right)$ to find an $ε$-stationary point for non-convex objectives. Furthermore, when the objective function satisfies the convexity or Polyak-Łojasiewicz (PL) condition, we propose a stage-wise variant of SMVR and improve the sample complexity to $\mathcal{O}\left(1 / ε^{2}\right)$ for convex functions or $\mathcal{O}\left(1 /\left(με\right)\right)$ for non-convex functions satisfying the $μ$-PL condition. The latter result implies the same complexity for $μ$-strongly convex functions. To make use of adaptive learning rates, we also develop Adaptive SMVR, which achieves the same complexities but converges faster in practice. All our complexities match the lower bounds not only in terms of $ε$ but also in terms of $μ$ (for PL or strongly convex functions), without using a large batch size in each iteration.

cs.LG↗

arXiv2022

AutoMTL: A Programming Framework for Automating Efficient Multi-Task Learning

Multi-task learning (MTL) jointly learns a set of tasks by sharing parameters among tasks. It is a promising approach for reducing storage costs while improving task accuracy for many computer vision tasks. The effective adoption of MTL faces two main challenges. The first challenge is to determine what parameters to share across tasks to optimize for both memory efficiency and task accuracy. The second challenge is to automatically apply MTL algorithms to an arbitrary CNN backbone without requiring time-consuming manual re-implementation and significant domain expertise. This paper addresses the challenges by developing the first programming framework AutoMTL that automates efficient MTL model development for vision tasks. AutoMTL takes as inputs an arbitrary backbone convolutional neural network (CNN) and a set of tasks to learn, and automatically produces a multi-task model that achieves high accuracy and small memory footprint simultaneously. Experiments on three popular MTL benchmarks (CityScapes, NYUv2, Tiny-Taskonomy) demonstrate the effectiveness of AutoMTL over state-of-the-art approaches as well as the generalizability of AutoMTL across CNNs. AutoMTL is open-sourced and available at https://github.com/zhanglijun95/AutoMTL.

cs.LG↗

arXiv2022

Provable Stochastic Optimization for Global Contrastive Learning: Small Batch Does Not Harm Performance

In this paper, we study contrastive learning from an optimization perspective, aiming to analyze and address a fundamental issue of existing contrastive learning methods that either rely on a large batch size or a large dictionary of feature vectors. We consider a global objective for contrastive learning, which contrasts each positive pair with all negative pairs for an anchor point. From the optimization perspective, we explain why existing methods such as SimCLR require a large batch size in order to achieve a satisfactory result. In order to remove such requirement, we propose a memory-efficient Stochastic Optimization algorithm for solving the Global objective of Contrastive Learning of Representations, named SogCLR. We show that its optimization error is negligible under a reasonable condition after a sufficient number of iterations or is diminishing for a slightly different global contrastive objective. Empirically, we demonstrate that SogCLR with small batch size (e.g., 256) can achieve similar performance as SimCLR with large batch size (e.g., 8192) on self-supervised learning task on ImageNet-1K. We also attempt to show that the proposed optimization technique is generic and can be applied to solving other contrastive losses, e.g., two-way contrastive losses for bimodal contrastive learning. The proposed method is implemented in our open-sourced library LibAUC (www.libauc.org).

cs.LG↗

arXiv2022

Weight Expansion: A New Perspective on Dropout and Generalization

While dropout is known to be a successful regularization technique, insights into the mechanisms that lead to this success are still lacking. We introduce the concept of \emph{weight expansion}, an increase in the signed volume of a parallelotope spanned by the column or row vectors of the weight covariance matrix, and show that weight expansion is an effective means of increasing the generalization in a PAC-Bayesian setting. We provide a theoretical argument that dropout leads to weight expansion and extensive empirical support for the correlation between dropout and weight expansion. To support our hypothesis that weight expansion can be regarded as an \emph{indicator} of the enhanced generalization capability endowed by dropout, and not just as a mere by-product, we have studied other methods that achieve weight expansion (resp.\ contraction), and found that they generally lead to an increased (resp.\ decreased) generalization ability. This suggests that dropout is an attractive regularizer, because it is a computationally cheap method for obtaining weight expansion. This insight justifies the role of dropout as a regularizer, while paving the way for identifying regularizers that promise improved generalization through weight expansion.

cs.LG↗

arXiv2022

Divide-and-Conquer Determinization of Büchi Automata based on SCC Decomposition

The determinization of a nondeterministic Büchi automaton (NBA) is a fundamental construction of automata theory, with applications to probabilistic verification and reactive synthesis. The standard determinization constructions, such as the ones based on the Safra-Piterman's approach, work on the whole NBA. In this work we propose a divide-and-conquer determinization approach. To this end, we first classify the strongly connected components (SCCs) of the given NBA as inherently weak, deterministic accepting, and nondeterministic accepting. We then present how to determinize each type of SCC independently from the others; this results in an easier handling of the determinization algorithm that takes advantage of the structure of that SCC. Once all SCCs have been determinized, we show how to compose them so to obtain the final equivalent deterministic Emerson-Lei automaton, which can be converted into a deterministic Rabin automaton without blow-up of states and transitions. We implement our algorithm in a our tool COLA and empirically evaluate COLA with the state-of-the-art tools Spot and OWL on a large set of benchmarks from the literature. The experimental results show that our prototype COLA outperforms Spot and OWL regarding the number of states and transitions.

cs.FL↗

arXiv2022

Projection-free Distributed Online Learning with Sublinear Communication Complexity

To deal with complicated constraints via locally light computations in distributed online learning, a recent study has presented a projection-free algorithm called distributed online conditional gradient (D-OCG), and achieved an $O(T^{3/4})$ regret bound for convex losses, where $T$ is the number of total rounds. However, it requires $T$ communication rounds, and cannot utilize the strong convexity of losses. In this paper, we propose an improved variant of D-OCG, namely D-BOCG, which can attain the same $O(T^{3/4})$ regret bound with only $O(\sqrt{T})$ communication rounds for convex losses, and a better regret bound of $O(T^{2/3}(\log T)^{1/3})$ with fewer $O(T^{1/3}(\log T)^{2/3})$ communication rounds for strongly convex losses. The key idea is to adopt a delayed update mechanism that reduces the communication complexity, and redefine the surrogate loss function in D-OCG for exploiting the strong convexity. Furthermore, we provide lower bounds to demonstrate that the $O(\sqrt{T})$ communication rounds required by D-BOCG are optimal (in terms of $T$) for achieving the $O(T^{3/4})$ regret with convex losses, and the $O(T^{1/3}(\log T)^{2/3})$ communication rounds required by D-BOCG are near-optimal (in terms of $T$) for achieving the $O(T^{2/3}(\log T)^{1/3})$ regret with strongly convex losses up to polylogarithmic factors. Finally, to handle the more challenging bandit setting, in which only the loss value is available, we incorporate the classical one-point gradient estimator into D-BOCG, and obtain similar theoretical guarantees.

cs.LG↗