arXiv subjects

Kexing Ying

Publications and source records attributed to Kexing Ying.

6 recordsLinked to original sources

arXiv2026

Non-explosion principles for branched rough differential equations with unbounded coefficients

Expanding upon the work of arXiv:2502.08799, we provide a non-explosion criterion for branched rough differential equations (bRDEs) where we continue to allow for the drift and the rough coefficient to be unbounded in the branched setting. Moreover, by providing a characterization of ``pure area'' branched rough paths -- branched rough paths over the zero path, we provide two different constructions of bRDEs which explode in finite time, and thus demonstrating the sharpness of the criterion. Finally, by realizing a trade-off between the growth of the coefficient of the bRDE and the decay of its higher-order derivatives, we provide a new non-explosion principle for bRDEs which allows for the coefficient to grow even faster than what is provided in arXiv:2502.08799.

math.PR↗

arXiv2026

Central limit theorem for the Allen-Cahn equation with supercritical random initial conditions

We study the large-scale behavior of solutions to the Allen-Cahn reaction-diffusion equation with Gaussian initial data. We consider the case of short-range dependence in the associated supercritical regime with spatial dimension $d \ge 3$. Under diffusive rescaling, the non-linearity formally vanishes on large scales in this case. Accordingly, we prove a central limit theorem for the rescaled solution, more precisely, that it converges to the solution of the heat equation started from a white noise. These initial conditions for the limit depend non-trivially both on the source of randomness and on the non-linearity. Our proof uses estimates obtained by a combination of comparison principles and Malliavin calculus, initiated by Castillo and Dunlap in arXiv:2509.06260 in the critical case. However, the result there is not a fluctuation result but rather an $L^2_\mathbf{P}$ comparison to a McKean-Vlasov problem with Gaussian solutions. Hence the mechanism behind the Gaussianity of the limit differs, and the proof requires new ideas that should be further applicable to other supercritical problems.

math.PR↗

arXiv2026

FormalProofBench: Can Models Write Graduate Level Math Proofs That Are Formally Verified?

We present FormalProofBench, a private benchmark designed to evaluate whether AI models can produce formally verified mathematical proofs at the graduate level. Each task pairs a natural-language problem with a Lean~4 formal statement, and a model must output a Lean proof accepted by the Lean 4 checker. FormalProofBench targets advanced undergraduate and graduate mathematics, with problems drawn from qualifying exams and standard textbooks across topics including analysis, algebra, probability, and logic. We evaluate a range of frontier models with an agentic harness, and find that the best-performing foundation model achieves 33.5% accuracy, with performance dropping rapidly after that. In addition to the accuracy numbers, we also provide empirical analysis of tool-use, failure modes, cost and latency, thereby providing a thorough evaluation of the formal-theorem proving abilities of frontier models.

cs.AI↗

arXiv2025

Fluctuations from a random fractional averaging limit

We consider a system of multiscale stochastic differential equations whose slow component is drivenby a fractional Brownian motion with Hurst parameter H greater than 1/2. Under ergodic assumptions ensuring the applicability of the fractional averaging and fractional homogenization theorems of Hairer and Li (arXiv:1902.11251, arXiv:2109.06948), we establish a fluctuation result. The deviation of the slow motion, scaled by epsilon^{1/2-H}, from its effective, time-dependent random limit converges, as the time-separation scale epsilon tends to zero, to the solution of a stochastic differential equation driven by a fractional Brownian motion and influenced by an additional space--time Gaussian field. Since the averaging principle and the fractional homogenization hold in different modes of convergence, obtaining the required joint convergence is a delicate matter. Moreover, neither the continuity of the Ito--Lyons solution map nor the martingale method is directly applicable for our purposes, so the proof requires several innovations. To establish the fluctuation theorem, we combine cumulant methods with a residue lemma and formulate the enlarged system as a rough differential equation in a suitable space.

math.PR↗

arXiv2025

Strong completeness of SDEs and non-explosion for RDEs with coefficients having unbounded derivatives

We establish a non-explosion result for rough differential equations (RDEs) in which the noise and drift coefficients, together with their derivatives, may grow unboundedly at infinity. In addition, we prove the existence of a global bi-continuous solution flow for stochastic differential equations (SDEs). Finally, the non-explosion results for RDEs are shown to be sharp by constructing counterexamples.

math.PR↗

arXiv2022

A Formalization of Doob's Martingale Convergence Theorems in mathlib

We present the formalization of Doob's martingale convergence theorems in the mathlib library for the Lean theorem prover. These theorems give conditions under which (sub)martingales converge, almost everywhere or in $L^1$. In order to formalize those results, we build a definition of the conditional expectation in Banach spaces and develop the theory of stochastic processes, stopping times and martingales. As an application of the convergence theorems, we also present the formalization of Lévy's generalized Borel-Cantelli lemma. This work on martingale theory is one of the first developments of probability theory in mathlib, and it builds upon diverse parts of that library such as topology, analysis and most importantly measure theory.

cs.LO↗