Searcharxiv⌕ Search

arXiv subjects

Oliver Butterley

Publications and source records attributed to Oliver Butterley.

18 recordsLinked to original sources
arXiv2025

A benchmark for vericoding: formally verified program synthesis

We present and test the largest benchmark for vericoding, LLM-generation of formally verified code from formal specifications - in contrast to vibe coding, which generates potentially buggy code from a natural language description. Our benchmark contains 12,504 formal specifications, with 3,029 in Dafny, 2,334 in Verus/Rust and 7,141 in Lean. Of these, 6,174 are new unseen problems. We find vericoding success rates of 27% in Lean, 44% in Verus/Rust and 82% in Dafny using off-the-shelf LLMs. Adding natural-language descriptions does not significantly improve performance. We also find that LLM progress has improved progress on pure Dafny verification from 68% to 96% over the past year. The benchmark and vericoding results are shared at https://github.com/Beneficial-AI-Foundation/vericoding-benchmark

cs.SE↗
arXiv2023

Exponential mixing for singular skew-products

We study skew-products of the form $(x,u) \mapsto (fx, u + \varphi(x))$ where $f$ is a non-uniformly expanding map on a manifold $X$ and $\varphi: X \to \mathbb{S}^1$ is piecewise $\mathcal{C}^1$. If the systems satisfies mild assumptions (in particular singular behaviour of $\varphi$ is permitted) then we prove that the map mixes exponentially with respect to the unique SRB measure. This extends previous results by allowing singular behaviour in the fibre map.

math.DS↗
arXiv2023

Anisotropic spaces and nil-automorphisms

We introduce a family of geometric anisotropic Banach spaces on Heisenberg nilmanifolds and study the spectrum of the composition operator associated to partially hyperbolic automorphisms. Choosing amongst the family of Banach spaces, it is possible to make the essential spectral radius arbitrarily small. We show that the exterior part of the discrete spectrum coincides with the spectrum restricted to the kernel of one of the operators associated to the nil-automorphism. Moreover we show that the remainder of the discrete spectrum is self-similar, it is given by scaled copies of the exterior part.

math.DS↗
arXiv2023

Discontinuities cause essential spectrum on surfaces

Two-dimensional maps with discontinuities are considered. It is shown that, in the presence of discontinuities, the essential spectrum of the transfer operator is large whenever it acts on a Banach space with norm that is stronger than \(L^\infty\) or \(BV\). Three classes of examples are introduced and studied, both expanding and partially expanding. In two dimensions there is complication due to the geometry of the discontinuities, an issue not present in the one-dimensional case and which is explored in this work.

math.DS↗
arXiv2022

Discontinuities cause essential spectrum

We study transfer operators associated to piecewise monotone interval transformations and show that the essential spectrum is large whenever the Banach space bounds $L^\infty$ and the transformation fails to be Markov. Constructing a family of Banach spaces we show that the lower bound on the essential spectral radius is optimal. Indeed, these Banach spaces realise an essential spectral radius as close as desired to the theoretical best possible case.

math.DS↗
arXiv2021

Locating Ruelle-Pollicott resonances

We study the spectrum of transfer operators associated to various dynamical systems. Our aim is to obtain precise information on the discrete spectrum. To this end we propose a unitary approach. We consider various settings where new information can be obtained following different branches along the proposed path. These settings include affine expanding Markov maps, uniformly expanding Markov maps, non-uniformly expanding or simply monotone maps, hyperbolic diffeomorphisms. We believe this approach could be greatly generalized.

math.DS↗
arXiv2019

Parabolic Flows Renormalized by Partially Hyperbolic Maps

We consider parabolic flows on 3-dimensional manifolds which are renormalized by circle extensions of Anosov diffeormorphisms. This class of flows includes nilflows on the Heisenberg nilmanifold which are renormalized by partially hyperbolic automorphisms. The transfer operators associated to the renormalization maps, acting on anisotropic Sobolev spaces, are known to have good spectral properties (this relies on ideas which have some resemblance to representation theory but also apply to non-algebraic systems). The spectral information is used to describe the deviation of ergodic averages and solutions of the cohomological equation for the parabolic flow.

math.DS↗
arXiv2017

Open Sets of Exponentially Mixing Anosov Flows

We prove that an Anosov flow with $\mathcal{C}^{1}$ stable bundle mixes exponentially whenever the stable and unstable bundles are not jointly integrable. This allows us to show that if a flow is sufficiently close to a volume-preserving Anosov flow and $\operatorname{dim} \mathbb{E}_s = 1$, $\operatorname{dim} \mathbb{E}_u \geq 2$ then the flow mixes exponentially whenever the stable and unstable bundles are not jointly integrable.This implies the existence of non-empty open sets of exponentially mixing Anosov flows. As part of the proof of this result we show that $\mathcal{C}^{1+}$ uniformly-expanding suspension semiflows (in any dimension) mix exponentially when the return time in not cohomologous to a piecewise constant.

math.DS↗
arXiv2016

Disintegration of Invariant Measures for Hyperbolic Skew Products

We study hyperbolic skew products and the disintegration of the SRB measure into measures supported on local stable manifolds. Such a disintegration gives a method for passing from an observable $v$ on the skew product to an observable $\bar v$ on the system quotiented along stable manifolds. Under mild assumptions on the system we prove that the disintegration preserves the smoothness of $v$, firstly in the case where $v$ is Hölder and secondly in the case where $v$ is $\mathcal{C}^{1}$.

math.DS↗
arXiv2016

A Note on Operator Semigroups Associated to Chaotic Flows

The transfer operator associated to a flow (continuous time dynamical system) is a one-parameter operator semigroup. We consider the operator-valued Laplace transform of this one-parameter semigroup. Estimates on the Laplace transform have be used in various settings in order to show the rate at which the flow mixes. Here we consider the case of exponential mixing or rapid mixing (super polynomial). We develop the operator theory framework amenable to this setting and show that the same estimates may be used to produce results, in terms of the operators, which go beyond the results for the rate of mixing. Such results are useful for obtaining other statistical properties of the dynamical system.

math.DS↗
arXiv2014

Exponential Mixing for Skew Products with Discontinuities

We consider the skew product $F: (x,u) \mapsto (f(x), u + τ(x))$, where the base map $f : \mathbb{T}^{1} \to \mathbb{T}^{1}$ is piecewise $\mathcal{C}^{2}$, covering and uniformly expanding, and the fibre map $τ: \mathbb{T}^{1} \to \mathbb{R}$ is piecewise $\mathcal{C}^{2}$. We show the dichotomy that either this system mixes exponentially or $τ$ is cohomologous (via a Lipschitz function) to a piecewise constant.

math.DS↗
arXiv2013

Robustly invariant sets in fibre contracting bundle flows

We provide abstract conditions which imply the existence of a robustly invariant neighbourhood of a global section of a fibre bundle flow. We then apply such a result to the bundle flow generated by an Anosov flow when the fibre is the space of jets (which are described by local manifolds). As a consequence we obtain sets of manifolds (e.g. approximations of stable manifolds) that are left invariant, {\bf for all} negative times, by the flow and its small perturbations. Finally, we show that the latter result can be used to easily fix a mistake recently uncovered in the paper {\em Smooth Anosov flows: correlation spectra and stability}, \cite{BuL}, by the present authors.

math.DS↗
arXiv2012

Area expanding C^{1+α} Suspension Semiflows

We study a large class of suspension semiflows which contains the Lorenz semiflows. This is a class with low regularity (merely C^{1+α}) and where the return map is discontinuous and the return time is unbounded. We establish the functional analytic framework which is typically employed to study rates of mixing. The Laplace transform of the correlation function is shown to admit a meromorphic extension to a strip about he imaginary axis. As part of this argument we give a new result concerning the quasi-compactness of weighted transfer operators for piecewise C^{1+α} expanding interval maps.

math.DS↗
arXiv2012

An Alternative Approach to Generalised BV and the Application to Expanding Interval Maps

We introduce a family of Banach spaces of measures, each containing the set of measures with density of bounded variation. These spaces are suitable for the study of weighted transfer operators of piecewise-smooth maps of the interval where the weighting used in the transfer operator is not better than piecewise Hölder continuous and the partition on which the map is continuous may possess a countable number of elements. For such weighted transfer operators we give upper bounds for both the spectral radius and for the essential spectral radius.

math.DS↗
arXiv2012

Expanding Semiflows on Branched Surfaces and One-Parameter Semigroups of Operators

We consider expanding semiflows on branched surfaces. The family of transfer operators associated to the semiflow is a one-parameter semigroup of operators. The transfer operators may also be viewed as an operator-valued function of time and so, in the appropriate norm, we may consider the vector-valued Laplace transform of this function. We obtain a spectral result on these operators and relate this to the spectrum of the generator of this semigroup. Issues of strong continuity of the semigroup are avoided. The main result is the improvement to the machinery associated with studying semiflows as one-parameter semigroups of operators and the study of the smoothness properties of semiflows defined on branched manifolds, without encoding as a suspension semiflow.

math.DS↗