用数学验证工具形式化了机器学习泛化误差的理论边界
Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral
- 通过可计算的测度论框架，形式化了Rademacher复杂度的推导过程
- 给出了线性模型在ℓ₂和ℓ₁正则下的泛化误差上界
- 支持从可数类推广到可分拓扑空间，适用于更广泛模型
理解并认证机器学习算法的泛化性能——即从训练误差推导测试误差的理论估计——是统计学习理论的核心问题。在众多用于推导此类保证的复杂度度量中，Rademacher复杂度能给出尖锐的、依赖数据的界，且远超经典VC维理论的应用范围。本研究在Lean 4中形式化了基于Rademacher复杂度的泛化误差界，依托Mathlib库中的测度论概率理论。我们的开发构建了一个机械验证的完整流程：从经验与期望Rademacher复杂度的定义出发，经过形式化的对称化论证和有界差异分析，最终通过形式证明的McDiarmid不等式获得高概率一致偏差界。关键技术贡献在于建立了一种可复用机制，将结果从可数假设类（其中上确界可测性在Mathlib中直接成立）推广到可分拓扑索引集，通过归约到可数稠密子集实现。作为抽象定理的具体应用，我们机械化实现了ℓ₂和ℓ₁正则下线性预测器的标准经验Rademacher界，并进一步形式化了基于覆盖数和链式构造的Dudley型熵积分界。
原文摘要 · Abstract (English)
Understanding and certifying the generalization performance of machine learning algorithms -- i.e. obtaining theoretical estimates of the test error from the training error -- is a central theme of statistical learning theory. Among the many complexity measures used to derive such guarantees, Rademacher complexity yields sharp, data-dependent bounds that apply well beyond classical VC-dimension theory. In this study, we formalize the generalization error bound by Rademacher complexity in Lean 4, building on measure-theoretic probability theory available in the Mathlib library. Our development provides a mechanically-checked pipeline from the definitions of empirical and expected Rademacher complexity, through a formal symmetrization argument and a bounded-differences analysis, to high-probability uniform deviation bounds via a formally proved McDiarmid inequality. A key technical contribution is a reusable mechanism for lifting results from countable hypothesis classes (where measurability of suprema is straightforward in Mathlib) to separable topological index sets via a reduction to a countable dense subset. As worked applications of the abstract theorem, we mechanize standard empirical Rademacher bounds for linear predictors under $\ell_2$ and $\ell_1$ regularizations, and we also formalize a Dudley-type entropy integral bound based on covering numbers and a chaining construction.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。