arXiv subjects

Jingwei Liang

Publications and source records attributed to Jingwei Liang.

At least 19 recordsLinked to original sources

arXiv2026

VeriScale: Adversarial Test-Suite Scaling for Verifiable Code Generation

As large language models (LLMs) are increasingly deployed for software engineering, constructing high-quality benchmarks is crucial for evaluating not just the functional correctness, but also the formal verifiability of generated code. However, existing benchmarks are limited by the quantity and quality of positive and negative test cases, leading to an overestimation of model capabilities in generating specifications and implementations. To address this, we propose VeriScale, a novel framework driven by the adversarial implementations. It consists of two stages: test-suite expansion to construct diverse and challenging test cases, and test-suite reduction to distill them into compact yet discriminative suites. While VeriScale is general, we instantiate it on Verina to construct VerinaPlus, which expands the original test suites by over 83$\times$, and VerinaLite, a lightweight 14$\times$ variant. Our experiments across eight state-of-the-art LLMs demonstrate that VerinaPlus exposes substantial model weaknesses hidden by the original benchmark, evidenced by sharp score drops on both SpecGen and CodeGen tasks, whereas VerinaLite maintains this discriminative power at a fraction of the evaluation cost. The enhanced benchmarks and source code are publicly available at https://github.com/XiaoyangLiu-sjtu/VeriScale.

cs.LG↗

arXiv2026

Formalization of Two Fixed-Point Algorithms in Hilbert Spaces

Iterative algorithms are fundamental tools for approximating fixed-points of nonexpansive operators in real Hilbert spaces. Among them, Krasnosel'ski\u{\i}--Mann iteration and Halpern iteration are two widely used schemes. In this work, we formalize the convergence of these two fixed-point algorithms in the interactive theorem prover Lean4 based on type dependent theory. To this end, weak convergence and topological properties in the infinite-dimensional real Hilbert space are formalized. Definition and properties of nonexpansive operators are also provided. As a useful tool in convex analysis, we then formalize the Fej\'{e}r monotone sequence. Building on these foundations, we verify the convergence of both the iteration schemes. Our formalization provides reusable components for machine-checked convergence analysis of fixed-point iterations and theories of convex analysis in real Hilbert spaces. Our code is available at https://github.com/TTony2019/fixed-point-iterations-in-lean.

math.OC↗

arXiv2026

Adaptive Dimension Reduction for Overlapping Group Sparsity

Typical dimension reduction techniques for nonoverlapping sparse optimization involve screening or sieving strategies based on a dual certificate derived from the first-order optimality condition, approximating the gradients or exploiting certain inherent low-dimensional structure of the sparse solution. In comparison, dimension reduction rules for overlapping group sparsity are generally less developed because the subgradient structure is more complex, making the link between sparsity pattern and the dual variable indirect due to the non-separability. In this work, we propose new dual certificates for overlapping group sparsity and a novel adaptive scheme for identifying the support of the overlapping group LASSO. We demonstrate how this scheme can be integrated into and significantly accelerate existing algorithms, including Primal-Dual splitting method, alternating direction method of multipliers and a recently developed variable projection scheme based on over-parameterization. We provide convergence analysis of the method and verify its practical effectiveness through experiments on standard datasets.

math.OC↗

arXiv2025

Model Consistency of the Iterative Regularization of Dual Ascent for Low-Complexity Regularization

Regularization is a core component of modern inverse problems, as it helps establish the well-posedness of the solution of interest. Popular regularization approaches include variational regularization and iterative regularization. The former involves solving a variational optimization problem, which consists of a data-fidelity term and a regularization term, balanced by an appropriate weighting parameter. The latter mitigates overfitting to noise by selecting a suitable stopping time during the iterative process. A key topic in the study of regularization is the relationship between the regularized solution and the original ground truth. When the ground truth possesses a low-complexity structure referred to as the "model" it can be shown that under appropriate regularization promoting the same structure, the solution to the regularized problem is robust to small perturbations. This property is called "model consistency". For variational regularization, model consistency in linear inverse problems has been studied in [1]. However, for iterative regularization, model consistency remains an open question. In this paper, building on recent developments in partial smoothness [1], we show that when the noise level is sufficiently small and an appropriate stopping criterion is used, iterative regularization is model consistent as well. Moreover, we show that the considered algorithm exhibits local linear behavior of the regularization. We provide numerical simulations to support our theoretical findings.

math.OC↗

arXiv2025

A Composed Alternating Relaxed Projection Algorithm for Feasibility Problem

Feasibility problem aims to find a common point of two or more closed (convex) sets whose intersection is nonempty. In the literature, projection based algorithms are widely adopted to solve the problem, such as the method of alternating projection (MAP), and Douglas--Rachford splitting method (DR). The performance of the methods are governed by the geometric properties of the underlying sets. For example, the fixed-point sequence of the Douglas--Rachford splitting method exhibits a spiraling behavior when solving the feasibility problem of two subspaces, leading to a slow convergence speed and slower than MAP. However, when the problem at hand is non-polyhedral, DR can demonstrate significant faster performance. Motivated by the behaviors of the DR method, in this paper we propose a new algorithm for solving convex feasibility problems. The method is designed based on DR method by further incorporating a composition of projection and reflection. A non-stationary version of the method is also designed, aiming to achieve faster practical performance. Theoretical guarantees of the proposed schemes are provided and supported by numerical experiments.

math.OC↗

arXiv2025

Partial Smoothness, Subdifferentials and Set-valued Operators

Over the past decades, the concept "partial smoothness" has been playing as a powerful tool in several fields involving nonsmooth analysis, such as nonsmooth optimization, inverse problems and operation research, etc. The essence of partial smoothness is that it builds an elegant connection between the optimization variable and the objective function value through the subdifferential. Identifiability is the most appealing property of partial smoothness, as locally it allows us to conduct much finer or even sharp analysis, such as linear convergence or sensitivity analysis. However, currently the identifiability relies on non-degeneracy condition and exact dual convergence, which limits the potential application of partial smoothness. In this paper, we provide an alternative characterization of partial smoothness through only subdifferentials. This new perspective enables us to establish stronger identification results, explain identification under degeneracy and non-vanishing error. Moreover, we can generalize this new characterization to set-valued operators, and provide a complement definition of partly smooth operator proposed in [14].

math.OC↗

arXiv2024

A Guide to Stochastic Optimisation for Large-Scale Inverse Problems

Stochastic optimisation algorithms are the de facto standard for machine learning with large amounts of data. Handling only a subset of available data in each optimisation step dramatically reduces the per-iteration computational costs, while still ensuring significant progress towards the solution. Driven by the need to solve large-scale optimisation problems as efficiently as possible, the last decade has witnessed an explosion of research in this area. Leveraging the parallels between machine learning and inverse problems has allowed harnessing the power of this research wave for solving inverse problems. In this survey, we provide a comprehensive account of the state-of-the-art in stochastic optimisation from the viewpoint of variational regularisation for inverse problems where the solution is modelled as minimising an objective function. We present algorithms with diverse modalities of problem randomisation and discuss the roles of variance reduction, acceleration, higher-order methods, and other algorithmic modifications, and compare theoretical results with practical behaviour. We focus on the potential and the challenges for stochastic optimisation that are unique to variational regularisation for inverse imaging problems and are not commonly encountered in machine learning. We conclude the survey with illustrative examples from imaging on linear inverse problems to examine the advantages and disadvantages that this new generation of algorithms bring to the field of inverse problems.

math.NA↗

arXiv2023

Robust Graph Representation Learning for Local Corruption Recovery

The performance of graph representation learning is affected by the quality of graph input. While existing research usually pursues a globally smoothed graph embedding, we believe the rarely observed anomalies are as well harmful to an accurate prediction. This work establishes a graph learning scheme that automatically detects (locally) corrupted feature attributes and recovers robust embedding for prediction tasks. The detection operation leverages a graph autoencoder, which does not make any assumptions about the distribution of the local corruptions. It pinpoints the positions of the anomalous node attributes in an unbiased mask matrix, where robust estimations are recovered with sparsity promoting regularizer. The optimizer approaches a new embedding that is sparse in the framelet domain and conditionally close to input observations. Extensive experiments are provided to validate our proposed model can recover a robust graph representation from black-box poisoning and achieve excellent performance.

cs.LG↗

arXiv2023

Federated Primal Dual Fixed Point Algorithm

Federated learning (FL) is a distributed learning paradigm that allows several clients to learn a global model without sharing their private data. In this paper, we generalize a primal dual fixed point (PDFP) \cite{PDFP} method to federated learning setting and propose an algorithm called Federated PDFP (FPDFP) for solving composite optimization problems. In addition, a quantization scheme is applied to reduce the communication overhead during the learning process. An $O(\frac{1}{k})$ convergence rate (where $k$ is the communication round) of the proposed FPDFP is provided. Numerical experiments, including graph-guided logistic regression, 3D Computed Tomography (CT) reconstruction are considered to evaluate the proposed algorithm.

math.OC↗

arXiv2022

Screening for Sparse Online Learning

Sparsity promoting regularizers are widely used to impose low-complexity structure (e.g. l1-norm for sparsity) to the regression coefficients of supervised learning. In the realm of deterministic optimization, the sequence generated by iterative algorithms (such as proximal gradient descent) exhibit "finite activity identification", namely, they can identify the low-complexity structure in a finite number of iterations. However, most online algorithms (such as proximal stochastic gradient descent) do not have the property owing to the vanishing step-size and non-vanishing variance. In this paper, by combining with a screening rule, we show how to eliminate useless features of the iterates generated by online algorithms, and thereby enforce finite activity identification. One consequence is that when combined with any convergent online algorithm, sparsity properties imposed by the regularizer can be exploited for computational gains. Numerically, significant acceleration can be obtained.

cs.LG↗

arXiv2022

An Adaptive Rank Continuation Algorithm for General Weighted Low-rank Recovery

This paper is devoted to proposing a general weighted low-rank recovery model and designing a fast SVD-free computational scheme to solve it. First, our generic weighted low-rank recovery model unifies several existing approaches in the literature.~Moreover, our model readily extends to the non-convex setting. Algorithm-wise, most first-order proximal algorithms in the literature for low-rank recoveries require computing singular value decomposition (SVD). As SVD does not scale appropriately with the dimension of the matrices, these algorithms become slower when the problem size becomes larger. By incorporating the variational formulation of the nuclear norm into the sub-problem of proximal gradient descent, we avoid computing SVD, which results in significant speed-up. Moreover, our algorithm preserves the rank identification property of nuclear norm [33] which further allows us to design a rank continuation scheme that asymptotically achieves the minimal iteration complexity. Numerical experiments on both toy examples and real-world problems, including structure from motion (SfM) and photometric stereo, background estimation, and matrix completion, demonstrate the superiority of our proposed algorithm.

math.OC↗

arXiv2021

TFPnP: Tuning-free Plug-and-Play Proximal Algorithm with Applications to Inverse Imaging Problems

Plug-and-Play (PnP) is a non-convex optimization framework that combines proximal algorithms, for example, the alternating direction method of multipliers (ADMM), with advanced denoising priors. Over the past few years, great empirical success has been obtained by PnP algorithms, especially for the ones that integrate deep learning-based denoisers. However, a key challenge of PnP approaches is the need for manual parameter tweaking as it is essential to obtain high-quality results across the high discrepancy in imaging conditions and varying scene content. In this work, we present a class of tuning-free PnP proximal algorithms that can determine parameters such as denoising strength, termination time, and other optimization-specific parameters automatically. A core part of our approach is a policy network for automated parameter search which can be effectively learned via a mixture of model-free and model-based deep reinforcement learning strategies. We demonstrate, through rigorous numerical and visual experiments, that the learned policy can customize parameters to different settings, and is often more efficient and effective than existing handcrafted criteria. Moreover, we discuss several practical considerations of PnP denoisers, which together with our learned policy yield state-of-the-art results. This advanced performance is prevalent on both linear and nonlinear exemplar inverse imaging problems, and in particular shows promising results on compressed sensing MRI, sparse-view CT, single-photon imaging, and phase retrieval.

cs.CV↗

arXiv2021

Improving "Fast Iterative Shrinkage-Thresholding Algorithm": Faster, Smarter and Greedier

The "fast iterative shrinkage-thresholding algorithm", a.k.a. FISTA, is one of the most well-known first-order optimisation scheme in the literature, as it achieves the worst-case $O(1/k^2)$ optimal convergence rate in terms of objective function value. However, despite such an optimal theoretical convergence rate, in practice the (local) oscillatory behaviour of FISTA often damps its efficiency. Over the past years, various efforts are made in the literature to improve the practical performance of FISTA, such as monotone FISTA, restarting FISTA and backtracking strategies. In this paper, we propose a simple yet effective modification to the original FISTA scheme which has two advantages: it allows us to 1) prove the convergence of generated sequence; 2) design a so-called "lazy-start" strategy which can up to an order faster than the original scheme. Moreover, by exploring the properties of FISTA scheme, we propose novel adaptive and greedy strategies which probes the limit of the algorithm. The advantages of the proposed schemes are tested through problems arising from inverse problem, machine learning and signal/image processing.

math.OC↗

arXiv2021

The Fun is Finite: Douglas-Rachford and Sudoku Puzzle -- Finite Termination and Local Linear Convergence

In recent years, the Douglas-Rachford splitting method has been shown to be effective at solving many non-convex optimization problems. In this paper we present a local convergence analysis for non-convex feasibility problems and show that both finite termination and local linear convergence are obtained. For a generalization of the Sudoku puzzle, we prove that the local linear rate of convergence of Douglas-Rachford is exactly $\frac{\sqrt{5}}{5}$ and independent of puzzle size. For the $s$-queens problem we prove that Douglas-Rachford converges after a finite number of iterations. Numerical results on solving Sudoku puzzles and $s$-queens puzzles are provided to support our theoretical findings.

math.OC↗

arXiv2021

SPRING: A fast stochastic proximal alternating method for non-smooth non-convex optimization

We introduce SPRING, a novel stochastic proximal alternating linearized minimization algorithm for solving a class of non-smooth and non-convex optimization problems. Large-scale imaging problems are becoming increasingly prevalent due to advances in data acquisition and computational capabilities. Motivated by the success of stochastic optimization methods, we propose a stochastic variant of proximal alternating linearized minimization (PALM) algorithm \cite{bolte2014proximal}. We provide global convergence guarantees, demonstrating that our proposed method with variance-reduced stochastic gradient estimators, such as SAGA \cite{SAGA} and SARAH \cite{sarah}, achieves state-of-the-art oracle complexities. We also demonstrate the efficacy of our algorithm via several numerical examples including sparse non-negative matrix factorization, sparse principal component analysis, and blind image deconvolution.

math.OC↗

arXiv2020

A Stochastic Alternating Direction Method of Multipliers for Non-smooth and Non-convex Optimization

Alternating direction method of multipliers (ADMM) is a popular first-order method owing to its simplicity and efficiency. However, similar to other proximal splitting methods, the performance of ADMM degrades significantly when the scale of the optimization problems to solve becomes large. In this paper, we consider combining ADMM with a class of stochastic gradient with variance reduction for solving large-scale non-convex and non-smooth optimization problems. Global convergence of the generated sequence is established under the extra additional assumption that the object function satisfies Kurdyka-Lojasiewicz (KL) property. Numerical experiments on graph-guided fused Lasso and computed tomography are presented to demonstrate the performance of the proposed methods.

math.OC↗

arXiv2020

Tuning-free Plug-and-Play Proximal Algorithm for Inverse Imaging Problems

Plug-and-play (PnP) is a non-convex framework that combines ADMM or other proximal algorithms with advanced denoiser priors. Recently, PnP has achieved great empirical success, especially with the integration of deep learning-based denoisers. However, a key problem of PnP based approaches is that they require manual parameter tweaking. It is necessary to obtain high-quality results across the high discrepancy in terms of imaging conditions and varying scene content. In this work, we present a tuning-free PnP proximal algorithm, which can automatically determine the internal parameters including the penalty parameter, the denoising strength and the terminal time. A key part of our approach is to develop a policy network for automatic search of parameters, which can be effectively learned via mixed model-free and model-based deep reinforcement learning. We demonstrate, through numerical and visual experiments, that the learned policy can customize different parameters for different states, and often more efficient and effective than existing handcrafted criteria. Moreover, we discuss the practical considerations of the plugged denoisers, which together with our learned policy yield state-of-the-art results. This is prevalent on both linear and nonlinear exemplary inverse imaging problems, and in particular, we show promising results on Compressed Sensing MRI and phase retrieval.

eess.IV↗

arXiv2020

Geometry of First-Order Methods and Adaptive Acceleration

First-order operator splitting methods are ubiquitous among many fields through science and engineering, such as inverse problems, signal/image processing, statistics, data science and machine learning, to name a few. In this paper, we study a geometric property of first-order methods when applying to solve non-smooth optimization problems. With the tool of "partial smoothness", we design a framework to analyze the trajectory of the fixed-point sequence generated by first-order methods and show that locally, the fixed-point sequence settles onto a regular trajectory such as a straight line or a spiral. Based on this finding, we discuss the limitation of current widely used "inertial acceleration" technique, and propose a trajectory following adaptive acceleration algorithm. Global convergence is established for the proposed acceleration scheme based on the perturbation of fixed-point iteration. Locally, we first build connections between the acceleration scheme and the well-studied "vector extrapolation technique" in the field of numerical analysis, and then discuss local acceleration guarantees of the proposed acceleration scheme. Moreover, our result provides a geometric interpretation of these vector extrapolation techniques. Numerical experiments on various first-order methods are provided to demonstrate the advantage of the proposed adaptive acceleration scheme.

math.OC↗