Persistence Pays: Square-root condition-number dependence for Metropolis-adjusted kinetic Langevin Monte Carlo with a non-reversibly updated accept/reject uniform
Nawaf Bou-Rabee
math.PR
Oct 26, 2026 · v1
math.NA stat.CO
TL;DR
Main theorems and key propositions, with their supporting definitions, are formalized and checked in Lean 4 against Mathlib; sources are in a public repository.
Abstract
We prove accelerated mixing for a Metropolis-adjusted kinetic Langevin sampler: the OBABO splitting with friction $2\sqrt m$, adjusted with Neal's non-reversibly updated uniform, which is redrawn after every epoch of $E$ steps. For targets $e^{-U}$ on $\mathbb{R}^d$ with $mI\preceq\nabla^2U\preceq LI$ and an $L_H$-Lipschitz Hessian, started from a Gaussian at an approximate minimizer, the chain reaches total variation accuracy $\varepsilon$ after $\tilde O\big(\sqrt{κd}+\sqrt{L_H}(d/m)^{3/4}\big)$ gradient evaluations, where $κ=L/m$ and $\tilde O$ hides logarithmic factors. The $\sqrtκ$ term is necessary, already on Gaussian targets. The proof discretizes Lu's entropic hypocoercivity by means of an entropy inequality for free transport, so that the relative entropy of the unadjusted chain decays at a rate of order $\sqrt m$ up to a discretization bias. With the non-reversibly updated uniform, the leading energy errors of velocity Verlet telescope along a path. A coupling argument combines the two. On Bayesian logistic regression posteriors for two standard data sets, which satisfy these assumptions, the gradient cost of the chain with the non-reversibly updated uniform grows roughly like the square root of the condition number at the posterior mode, and that of standard adjusted OBABO roughly like its $3/4$ power.
Problem
It is an open question whether the square-root condition-number acceleration of kinetic Langevin dynamics survives numerical discretization with Metropolis adjustment for strongly log-concave targets. The work addresses this for Metropolis-adjusted OBABO under a Lipschitz-Hessian assumption, started from a warm start.
Approach
The sampler uses OBABO with friction 2√m and Neal's non-reversibly updated accept/reject uniform, redrawn once per epoch. The proof discretizes Lu's entropic hypocoercivity using a new entropy inequality for free transport. It exploits the fact that leading velocity Verlet energy errors telescope along a path under the persistent uniform, and combines this with a coupling argument. The main theorems and Propositions 2.4 and 3.1 are formalized in Lean 4 with Mathlib, using only the standard axioms.
Results
The chain reaches total variation accuracy ε after Õ(√(κd) + √L_H (d/m)^{3/4}) gradient evaluations, and the √κ term is shown to be necessary. On Bayesian logistic regression posteriors, the measured cost grows roughly like √κ, compared with κ^{3/4} for standard adjusted OBABO.