Author name cluster

Chenyi Zhang

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.

12 papers

1 author row

AAMAS Conference 2025 Conference Paper

Automatic Verification of Linear Integer Planning Programs via Forgetting in LIAUPF

Liangda Fang
Shikang Chen
Xiaoman Wang
Xiaoyou Lin
Chenyi Zhang
Qingliang Chen
Quanlong Guan
Kaile Su

The goal of generalized planning (GP) is to find a generalized solution for a class of planning problems. One of effective means to solve GP is to transform a GP problem into an abstract planning problem, which can be easily solved. Recently, Lin et al. proposed a novel abstract model for GP, namely generalized linear integer numeric planning (GLINP), whose solution is an algorithmic-like structure called a planning program. They also developed an inductive approach to generating planning programs for GLINP. However, it has no theoretical guarantee that the generated planning program holds for infinitely many problem instances. To address this defect, we propose an automatic approach to verify whether the planning program works for infinitely many problem instances in this paper. We translate the planning program into a set of trace axioms finitely represented by linear integer arithmetic with uninterpreted predicate and function symbols (LIAUPF), and reduce the problem to the entailment problem of LIAUPF. Due to the undecidability of entailment problem in LIAUPF, we identify a class of planning programs whose trace axioms can be simplified in linear integer arithmetic (LIA), that is, a decidable fragment of LIAUPF, when reasoning about only the input and output of planning programs. As a result, the correctness verification of this class of programs becomes decidable.

PDF

NeurIPS Conference 2025 Conference Paper

Balancing Gradient and Hessian Queries in Non-Convex Optimization

Deeksha Adil
Brian Bullins
Aaron Sidford
Chenyi Zhang

We develop optimization methods which offer new trade-offs between the number of gradient and Hessian computations needed to compute the critical point of a non-convex function. We provide a method that for a twice-differentiable $f\colon \mathbb{R}^d \rightarrow \mathbb{R}$ with $L_2$-Lipschitz Hessian, and input initial point with $\Delta$-bounded sub-optimality and sufficiently small $\epsilon > 0$ outputs an $\epsilon$-critical point, i. e. , a point $x$ such that $\|\nabla f(x)\| \leq \epsilon$, using $\tilde{O}(\Delta L_2^{1/4} n_H^{-1/2}\epsilon^{-9/4})$ queries to a gradient oracle and $n_H$ queries to a Hessian oracle. As a consequence, we obtain an improved gradient query complexity of $\tilde{O}(d^{1/3}L_2^{1/2}\Delta\epsilon^{-3/2})$ in the case of bounded dimension and of $\tilde{O}(\Delta^{3/2} L_2^{3/4}\epsilon^{-9/4})$ in the case where we are allowed only a single Hessian query. We obtain these results through a more general algorithm which can handle approximate Hessian computations and recovers known prior state-of-the-art bounds of computing an $\epsilon$-critical point, under the additional assumption that $f$ has an $L_1$-Lipschitz gradient, with $O(\Delta L_2^{1/4}\epsilon^{-7/4})$-gradient queries.

PDF Details

NeurIPS Conference 2025 Conference Paper

Isotropic Noise in Stochastic and Quantum Convex Optimization

Annie Marsden
Liam O'Carroll
Aaron Sidford
Chenyi Zhang

We consider the problem of minimizing a $d$-dimensional Lipschitz convex function using a stochastic gradient oracle. We introduce and motivate a setting where the noise of the stochastic gradient is isotropic in that it is bounded in every direction with high probability. We then develop an algorithm for this setting which improves upon prior results by a factor of $d$ in certain regimes, and as a corollary, achieves a new state-of-the-art complexity for sub-exponential noise. We give matching lower bounds (up to polylogarithmic factors) for both results. Additionally, we develop an efficient quantum isotropifier, a quantum algorithm which converts a variance-bounded quantum sampling oracle into one that outputs an unbiased estimate with isotropic error. Combining our results, we obtain improved dimension-dependent rates for quantum stochastic convex optimization.

PDF Details

AAAI Conference 2025 Conference Paper

Memory Efficient Matting with Adaptive Token Routing

Yiheng Lin
Yihan Hu
Chenyi Zhang
Ting Liu
Xiaochao Qu
Luoqi Liu
Yao Zhao
Yunchao Wei

Transformer-based models have recently achieved outstanding performance in image matting. However, their application to high-resolution images remains challenging due to the quadratic complexity of global self-attention. To address this issue, we propose MEMatte, a memory-efficient matting framework for processing high-resolution images. MEMatte incorporates a router before each global attention block, directing informative tokens to the global attention while routing other tokens to a Lightweight Token Refinement Module (LTRM). Specifically, the router employs a local-global strategy to predict the routing probability of each token, and the LTRM utilizes efficient modules to simulate global attention. Additionally, we introduce a Batch-constrained Adaptive Token Routing (BATR) mechanism, which allows each router to dynamically route tokens based on image content and the stages of attention block in the network. Furthermore, we construct an ultra high-resolution image matting dataset, UHR-395, comprising 35,500 training images and 1,000 test images, with an average resolution of 4872 × 6017. This dataset is created by compositing 395 different alpha mattes across 11 categories onto various backgrounds, all with high-quality manual annotation. Extensive experiments demonstrate that MEMatte outperforms existing methods on both high-resolution and real-world datasets, significantly reducing memory usage by approximately 88% and latency by 50% on the Composition-1K benchmark.

PDF Details DOI

NeurIPS Conference 2023 Conference Paper

Quantum speedups for stochastic optimization

Aaron Sidford
Chenyi Zhang

We consider the problem of minimizing a continuous function given given access to a natural quantum generalization of a stochastic gradient oracle. We provide two new methods for the special case of minimizing a Lipschitz convex function. Each method obtains a dimension versus accuracy trade-off which is provably unachievable classically and we prove that one method is asymptotically optimal in low-dimensional settings. Additionally, we provide quantum algorithms for computing a critical point of a smooth non-convex function at rates not known to be achievable classically. To obtain these results we build upon the quantum multivariate mean estimation result of Cornelissen et al. and provide a general quantum variance reduction technique of independent interest.

PDF Details

NeurIPS Conference 2021 Conference Paper

Escape saddle points by a simple gradient-descent based algorithm

Chenyi Zhang
Tongyang Li

Escaping saddle points is a central research topic in nonconvex optimization. In this paper, we propose a simple gradient-based algorithm such that for a smooth function $f\colon\mathbb{R}^n\to\mathbb{R}$, it outputs an $\epsilon$-approximate second-order stationary point in $\tilde{O}(\log n/\epsilon^{1. 75})$ iterations. Compared to the previous state-of-the-art algorithms by Jin et al. with $\tilde{O}(\log^4 n/\epsilon^{2})$ or $\tilde{O}(\log^6 n/\epsilon^{1. 75})$ iterations, our algorithm is polynomially better in terms of $\log n$ and matches their complexities in terms of $1/\epsilon$. For the stochastic setting, our algorithm outputs an $\epsilon$-approximate second-order stationary point in $\tilde{O}(\log^{2} n/\epsilon^{4})$ iterations. Technically, our main contribution is an idea of implementing a robust Hessian power method using only gradients, which can find negative curvature near saddle points and achieve the polynomial speedup in $\log n$ compared to the perturbed gradient descent methods. Finally, we also perform numerical experiments that support our results.

PDF Details

TCS Journal 2016 Journal Article

The complexity of synchronous notions of information flow security

Franck Cassez
Ron van der Meyden
Chenyi Zhang

The paper considers the complexity of verifying that a finite state system satisfies a number of definitions of information flow security. The systems model considered is one in which agents operate synchronously with awareness of the global clock. This enables timing based attacks to be captured, whereas previous work on this topic has dealt primarily with asynchronous systems. Versions of the notions of nondeducibility on inputs, nondeducibility on strategies, and an unwinding based notion are formulated for this model. All three notions are shown to be decidable, and their computational complexity is characterised.

Details DOI

AAAI Conference 2015 Conference Paper

Are Features Equally Representative? A Feature-Centric Recommendation

Chenyi Zhang
Ke Wang
Ee-Peng Lim
Qinneng Xu
Jianling Sun
Hongkun Yu

Typically a user prefers an item (e. g. , a movie) because she likes certain features of the item (e. g. , director, genre, producer). This observation motivates us to consider a featurecentric recommendation approach to item recommendation: instead of directly predicting the rating on items, we predict the rating on the features of items, and use such ratings to derive the rating on an item. This approach offers several advantages over the traditional item-centric approach: it incorporates more information about why a user chooses an item, it generalizes better due to the denser feature rating data, it explains the prediction of item ratings through the predicted feature ratings. Another contribution is turning a principled item-centric solution into a feature-centric solution, instead of inventing a new algorithm that is feature-centric. This approach maximally leverages previous research. We demonstrate this approach by turning the traditional item-centric latent factor model into a feature-centric solution and demonstrate its superiority over item-centric approaches.

PDF Details

TCS Journal 2013 Journal Article

Information flow in systems with schedulers, Part I: Definitions

Ron van der Meyden
Chenyi Zhang

This paper studies information flow security in a synchronous state machine model, in which agents share a global clock and can make observations at all times, but in which an agent’s ability to perform actions is subject to a scheduler. A number of definitions of security for this setting are proposed, depending on whether the attacker is active or passive, whether the security should be robust to discovery of the schedule by the attacker, and on whether the definition is trace-based or bisimulation-based. In particular, the paper studies the dependence of these definitions of security on implementation details of the scheduler. Such independence is shown to hold for the trace-based definitions, but not for bisimulation-based definitions. Stronger versions of the bisimulation-based definitions are proposed that recover implementation-independence. A complete characterization of relationships between the definitions of security introduced in the paper is derived.

Details DOI

TCS Journal 2013 Journal Article

Information flow in systems with schedulers, Part II: Refinement

Ron van der Meyden
Chenyi Zhang

Refinement is a relation on system models: a concrete model is a refinement of a more abstract model if it has fewer behaviors. When properties of the abstract model are guaranteed to be preserved in the concrete model, refinement supports a top-down development process. This paper considers preservation of a range of information flow security properties in synchronous systems with schedulers, when these schedulers are refined. Notions of refinement are defined for both an abstract notion of scheduler as well as for their concrete representation as automata. The security properties that are preserved by refinement over schedulers are then characterized. The results are applied to characterize a number of scheduler independent security properties, which state that a system is secure with respect to all schedulers.

Details DOI

AAAI Conference 2012 Conference Paper

Probabilistic Alternating-Time Temporal Logic of Incomplete Information and Synchronous Perfect Recall

Xiaowei Huang
Kaile Su
Chenyi Zhang

A probabilistic variant of ATL∗ logic is proposed to work with multi-player games of incomplete information and synchronous perfect recall. The semantics of the logic is settled over probabilistic interpreted system and partially observed probabilistic concurrent game structure. While unexpectedly, the model checking problem is in general undecidable even for singlegroup fragment, we find a fragment whose complexity is in 2-EXPTIME. The usefulness of this fragment is shown over a land search scenario.

PDF Details

TCS Journal 2010 Journal Article

A comparison of semantic models for noninterference

Ron van der Meyden
Chenyi Zhang

The literature on definitions of security based on causality-like notions such as noninterference has used several distinct semantic models for systems. Early work was based on state machine and trace-set definitions; more recent work has dealt with definitions of security in two distinct process algebraic settings. Comparisons between the definitions has been carried out mainly within semantic frameworks. This paper studies the relationship between semantic frameworks, by defining mappings between a number of semantic models and studying the relationship between notions of noninterference under these mappings.

Details DOI