Shuai Lu

Wei Wang, Shuai Lu, Bernd Hofmann et al.

Measuring the error by an l^1-norm, we analyze under sparsity assumptions an l^0-regularization approach, where the penalty in the Tikhonov functional is complemented by a general stabilizing convex functional. In this context, ill-posed operator equations Ax = y with an injective and bounded linear operator A mapping between l^2 and a Banach space Y are regularized. For sparse solutions, error estimates as well as linear and sublinear convergence rates are derived based on a variational inequality approach, where the regularization parameter can be chosen either a priori in an appropriate way or a posteriori by the sequential discrepancy principle. To further illustrate the balance between the l^0-term and the complementing convex penalty, the important special case of the l^2-norm square penalty is investigated showing explicit dependence between both terms. Finally, some numerical experiments verify and illustrate the sparsity promoting properties of corresponding regularized solutions.

Shuai Lu, Peter Mathé

Spectral Barron spaces, which quantify the absolute value of weighted Fourier coefficients of a function, have gained considerable attention due to their capability for universal approximation across certain function classes. By establishing a connection between these spaces and a specific positive linear operator, we investigate the interpolation and scaling relationships among diverse spectral Barron spaces. Furthermore, we introduce a link condition by relating the spectral Barron space to inverse problems, illustrating this with three exemplary cases. We revisit the notion of universal approximation within the context of spectral Barron spaces and validate an error bound for Tikhonov regularization, penalized by the spectral Barron norm.

Shaonan Wu, Shuai Lu, Yeyun Gong et al.

Formal proofs are challenging to write even for experienced experts. Recent progress in Neural Theorem Proving (NTP) shows promise in expediting this process. However, the formal corpora available on the Internet are limited compared to the general text, posing a significant data scarcity challenge for NTP. To address this issue, this work proposes Alchemy, a general framework for data synthesis that constructs formal theorems through symbolic mutation. Specifically, for each candidate theorem in Mathlib, we identify all invocable theorems that can be used to rewrite or apply to it. Subsequently, we mutate the candidate theorem by replacing the corresponding term in the statement with its equivalent form or antecedent. As a result, our method increases the number of theorems in Mathlib by an order of magnitude, from 110k to 6M. Furthermore, we perform continual pretraining and supervised finetuning on this augmented corpus for large language models. Experimental results demonstrate the effectiveness of our approach, achieving a 4.70% absolute performance improvement on Leandojo benchmark. Additionally, our approach achieves a 2.47% absolute performance gain on the out-of-distribution miniF2F benchmark based on the synthetic data.To provide further insights, we conduct a comprehensive analysis of synthetic data composition and the training paradigm, offering valuable guidance for developing a strong theorem prover.

Shuai Lu, Peter Mathé, Sergiy Pereverzyev

This paper studies a Nyström type subsampling approach to large kernel learning methods in the misspecified case, where the target function is not assumed to belong to the reproducing kernel Hilbert space generated by the underlying kernel. This case is less understood, in spite of its practical importance. To model such a case, the smoothness of target functions is described in terms of general source conditions. It is surprising that almost for the whole range of the source conditions, describing the misspecified case, the corresponding learning rate bounds can be achieved with just one value of the regularization parameter. This observation allows a formulation of mild conditions under which the plain Nyström subsampling can be realized with subquadratic cost maintaining the guaranteed learning rates.