On the Accuracy of Approximate Leave-One-Out with Blockwise Nonsmooth Regularization in High-dimensions
Honghao Lin, Songbin Liu, Arian Maleki, Vahab Mirrokni, Chen Shang, David P. Woodruff, Hanbo Yang, Wenjin Zhang
math.ST
Oct 20, 2026 · v1
stat.ME stat.ML
TL;DR
The main theorem's proof, initially produced by an automated agentic system, comes with a Lean 4 verification provided as a linked artifact.
Abstract
Approximate leave-one-out (ALO) refers to methods that provide computationally efficient and statistically accurate approximations to leave-one-out risk estimation. These methods have recently attracted increased attention because of their connections to other important problems, including machine unlearning and data valuation. For empirical risk minimization, ALO methods often rely on a few Newton steps and therefore require smooth loss functions and regularizers. In high-dimensional problems, however, regularizers are frequently non-smooth. This has motivated the development of heuristic ALO methods for non-smooth regularization, whose empirical accuracy is often strong but whose theoretical justification remains limited. In this paper, we study the accuracy of a heuristic ALO method for a broad class of non-differentiable penalties that promote block sparsity in the proportional high-dimensional regime. Assuming uniformly bounded block sizes, we prove that the expected average absolute discrepancy between the exact leave-one-out loss and its ALO approximation is $O(\log^{3/2}(en)/\sqrt{n})$. Our proof technique differs substantially from existing approaches and relies on obtaining sharp bounds on the number of active groups whose status changes between the full-data and leave-one-out estimators. In addition to yielding stronger guarantees under weaker assumptions than prior work, our analysis provides new insight into the stability of sparse estimators under perturbations of the training data.
Problem
Approximate leave-one-out (ALO) methods estimate leave-one-out risk cheaply, but heuristic ALO for non-smooth, block-sparsity-promoting regularizers lacks theoretical justification in the proportional high-dimensional regime.
Approach
The authors analyze a heuristic ALO method for a broad class of non-differentiable blockwise penalties, assuming uniformly bounded block sizes. The proof combines deterministic comparison bounds with probabilistic control of blocks near activation boundaries, bounding how many active groups change status between the full-data and leave-one-out estimators. The proof was first generated by an automated agentic system, and a Lean 4 verification of the main theorem is provided.
Results
The expected average absolute discrepancy between exact LO and ALO is O(log^{3/2}(en)/sqrt(n)). The guarantee is stronger and holds under weaker assumptions than prior work, and the analysis also gives insight into the stability of sparse estimators.