💬 NLP

Lean Formalization of Generalization Error Bound by Rademacher Complexity and Dudley's Entropy Integral

本文在 Lean 4 中形式化了基于 Rademacher 复杂度和 Dudley 熵积分的泛化误差界，呈现了一条从测度论基础到高概率一致偏差界及其在线性预测器中应用的机械验证流程。

原作者： Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda

发布于 2026-05-26

📖 1 分钟阅读☕ 轻松阅读

原作者： Sho Sonoda, Kazumi Kasaura, Yuma Mizuno, Kei Tsukamoto, Naoto Onda

原始论文采用 CC BY 4.0 许可（http://creativecommons.org/licenses/by/4.0/）。 ✨ 这是对下方论文的AI生成解释。它不是由作者撰写或认可的。如需技术准确性，请参阅原始论文。阅读完整免责声明

想象你是一位刚刚发明了新食谱的厨师。你已经在厨房里烹饪了 100 次（即训练数据），每次味道都完美无缺。但你想确认：如果你为餐厅里的一百万陌生人烹饪同一道食谱（即测试数据），它是否依然美味？

在机器学习领域，这被称为泛化问题。你所询问的这篇论文，是一份经过严格计算机验证的证明，旨在以数学确定性帮助我们回答这个问题。

以下是这篇论文的故事，将其拆解为简单的概念和类比。

1. 问题：“厨房与餐厅”之间的差距

当计算机学习时，它试图寻找一条能拟合其所见数据的规则（即假设）。

训练误差：规则拟合其已见数据的程度（你的 100 次厨房试验）。
测试误差：规则在尚未见过的新数据上的表现（餐厅的顾客）。

危险在于过拟合。这就像一位厨师记住了自己 100 次试验的确切味道，却未能理解烹饪的原理。如果他们在餐厅遇到略有不同的食材，菜肴就会失败。我们需要一种方法来保证“厨房的成功”能转化为“餐厅的成功”。

2. 工具：拉德马赫复杂度（“抛硬币测试”）

为了衡量食谱过拟合的可能性，数学家使用一种称为拉德马赫复杂度的工具。

想象你有一袋硬币。你抛掷它们，它们完全随机地落在正面（+1）或反面（-1）。

测试：你问你的食谱（即学习算法）：“你能预测这些随机的抛硬币结果吗？”
逻辑：如果你的食谱是一条简单、稳健的规则，它就不应该能够预测随机噪声。它应该仅凭运气猜对约 50%。
危险信号：如果你的食谱过于复杂（就像一位记住了每一个细微细节的厨师），它可能会在随机的抛硬币结果中偶然“发现某种模式”，从而以高于随机的准确率进行预测。

拉德马赫复杂度精确衡量了一个模型能通过拟合随机噪声来“作弊”的程度。该数值越低，模型在新数据上表现良好的可能性就越大。

3. 成就：“数字双重检查”

这篇论文的作者不仅将这些数学证明写在纸上，还将它们构建在一个名为Lean 4的计算机程序中。

将 Lean 4 想象为一位超级严格、目不转睛的编辑。

旧方法：数学家在纸上写出证明。人类审稿人阅读它。如果人类漏掉了一个微小的逻辑缺口，即使证明略有错误，也可能被接受。
新方法（本文）：作者将他们的整个证明输入到 Lean 中。计算机检查了每一个步骤、每一个定义和每一个假设。如果存在哪怕一个微小的缺失环节（例如“这个函数是可测的吗？”），计算机就会拒绝它。

该论文声称构建了一个机械验证流水线。它从基本定义开始，经过一个“对称化”技巧（一种巧妙的数学洗牌），最终以高置信度的保证结束，确保测试误差不会比训练误差差太多。

4. 大障碍：“无限图书馆”问题

在现实世界中，机器学习模型往往拥有无限的可能性（例如权重的连续数值范围）。

问题：在数学中，检查有限的项目列表（如 100 种食谱）很容易。但检查无限列表则困难得多。在计算机术语中，检查无限列表的“最大值”有时会破坏逻辑规则（可测性问题）。
论文的解决方案：作者创造了一个巧妙的“桥梁”。他们首先针对可数（有限或可列举）的假设集证明了数学。然后，他们表明，对于许多现实世界的模型（它们是“可分的”拓扑空间），你可以使用可数稠密子集来近似无限集（就像使用非常精细的网格来近似平滑曲线）。
类比：想象试图测量世界上所有可能的身高。测量每个人是不可能的。但如果你测量每一个身高恰好相差 1 厘米的人，你就可以在数学上证明，你的测量以高精度覆盖了所有其他人。论文将这种“网格”技巧形式化，以便计算机能够接受它。

5. 结果：他们证明了什么？

一旦“引擎”构建完成，他们将其应用于三个具体场景以展示其有效性：

带有 $\ell_2$ 正则化的线性预测器：这就像是一个被强制保持其“食材”（权重）小且平衡的模型。论文证明了该模型的标准数学界限。
带有 $\ell_1$ 正则化的线性预测器：这迫使模型变得“稀疏”（仅使用少量食材）。他们证明了该模型的界限，这涉及略微不同的计算（涉及特征数量的平方根）。
Dudley 熵积分：这是一种更高级、更通用的工具。想象你有一个非常杂乱、复杂的形状。与其测量整个形状，不如用更小、更简单的形状覆盖它（就像用光滑的鹅卵石覆盖一块凹凸不平的岩石）。论文形式化了如何根据覆盖该形状所需的“鹅卵石”数量来计算复杂度。

总结

这篇论文是一项基础性的工程壮举。

他们做了什么：他们将关于机器学习模型如何泛化（拉德马赫复杂度）的复杂教科书理论，转化为计算机可以 100% 确定验证的语言。
为何重要：它消除了人工智能最关键的安全保证中的“人为错误”。它证明，如果你遵循这些特定的数学规则，你的模型就不会仅仅记忆过去；它将真正为未来而学习。
隐喻：他们不仅写了一份安全蛋糕的食谱；他们建造了一个机器人，检查食谱中的每一种食材和每一步骤，以确保无论谁吃这块蛋糕，它都永远不会坍塌。

技术摘要：基于 Rademacher 复杂度和 Dudley 熵积分的泛化误差界的形式化

问题陈述

本文解决的核心挑战是机器学习中泛化性能的形式化验证。具体而言，作者旨在利用测度论框架，从训练误差（经验风险）推导出测试误差（总体风险）的理论估计。虽然经典方法依赖于 Vapnik–Chervonenkis (VC) 维，但这些方法通常与数据无关且专为二分类任务设计。现代学习理论越来越多地利用Rademacher 复杂度，它提供了适用于实值损失和多样化函数类（例如深度学习、核方法）的尖锐且依赖于数据的界。然而，由于需要严格处理可测性（特别是针对不可数假设类上的上确界）、乘积测度以及集中不等式，在证明助手（proof assistants）中形式化这些论证颇具难度。

方法论

作者在 Lean 4 中形式化了泛化误差界，利用了 Mathlib 库中丰富的测度论概率基础设施。该开发遵循教科书中（如 Mohri 等人、Wainwright）标准的“对称化 + 有界差分”流程，但针对形式化验证的约束进行了调整：

测度论设置：该框架通过概率空间 $(\Omega, m_\Omega, \mu)$ 和随机变量 $X: \Omega \to \mathcal{X}$ 对数据生成过程进行建模。样本被建模为函数 $\omega: \text{Fin } n \to \Omega$ ，通过推前（pushed forward）得到 $S = X \circ \omega$ 。
核心定义：
- Rademacher 复杂度：针对经验情况（在固定样本 $S$ 上）和期望情况（在乘积测度 $\mu^n$ 上）均进行了定义。经验版本对所有符号向量 $\sigma \in \{-1, 1\}^n$ 进行平均。
- 一致偏差：定义为在假设类 $F = \{f_i\}_{i \in \iota}$ 上，经验均值与总体均值之差的绝对值的上确界。
对称化：一个形式化定理（abs_symmetrization_equation）用符号翻转和的平均值替换了两个独立样本之间差分的上确界，从而将一致偏差与 Rademacher 复杂度联系起来。
集中性：作者在 Lean 中从头证明了McDiarmid 不等式。他们确立了一致偏差泛函满足有界差分性质（改变一个样本点最多使值改变 $2b/n$ ），从而能够推导出高概率尾部界。
处理不可数索引集：一个关键的技术障碍是不可数索引集 $\iota$ $ι$ 上上确界的可测性。Mathlib 提供了可数索引的可测性，但并未自动提供不可数索引的可测性。作者通过以下方式解决了这一问题：
- 首先针对可数索引集证明定理。
- 通过可数稠密归约将结果扩展到可分拓扑索引集。这涉及证明对于连续函数，在可分空间上的上确界等于在可数稠密子集上的上确界，前提是积分下保持连续性（通过一致控制来保证）。

主要贡献

本文首次系统性地形式化了基于 Rademacher 复杂度的泛化分析。具体贡献包括：

可重用的形式化基础设施：一个经过机械验证的流程，涵盖经验/期望 Rademacher 复杂度、对称化、有界差分分析以及 McDiarmid 不等式。
可测性解决方案：一种可重用的机制，用于将结果从可数假设类提升到可分拓扑参数空间。该机制明确封装了使不可数上确界可测所需的充分条件（可分性、第一可数性、一致控制以及积分下的连续性），而这些条件在非形式化证明中通常是隐含的。
形式化的集中工具：McDiarmid 不等式的完整证明，以及支持最大不等式、Massart 引理和覆盖数的引理。
实例化应用：
- 线性预测器：形式化了 $\ell_2$ 正则化预测器的标准 $O(1/\sqrt{n})$ 界，以及 $\ell_1$ 正则化预测器的 $O(\sqrt{\log(d)/n})$ 界。
- Dudley 熵积分：形式化了通过链式构造（chaining construction）将 Rademacher 复杂度与覆盖数联系起来的 Dudley 型界。这需要定义经验伪度量，并处理从离散链式求和到积分界的过渡。

结果

该形式化工作产出了经过机械验证的标准学习理论界：

期望界： $E[\text{UD}_n(F)] \leq 2 R_n(F)$ ，其中 $R_n(F)$ 是 Rademacher 复杂度。
高概率界：对于任意 $\delta \in (0, 1)$ ，以至少 $1-\delta$ 的概率：
$\text{UD}_n(F) \leq 2 R_n(F) + b \sqrt{\frac{2 \log(1/\delta)}{n}}$
具体界：该仓库提供了 $\ell_2$ 和 $\ell_1$ 约束下线性预测器的经验 Rademacher 复杂度的具体证明，以及 Dudley 熵积分界。

意义与主张

作者将这项工作定位为迈向可信、可认证机器学习理论的基础性步骤。

连接理论与验证：这项工作表明，现代测度论学习理论（依赖于乘积测度、包络的可积性以及集中性）可以在证明助手中进行形式化，而无需诉诸过度简化的离散代理。
阐明隐含假设：主要贡献在于明确识别了处理不可数假设类所需的条件。形式化工作隔离了“可数 - 稠密归约”以及所需的特定连续性/可积性假设，而这些在标准教科书中往往被略过。
模块化：该开发设计使得抽象的 Rademacher 流程可被重用。具体界成为“可执行的推论”，通过实例化函数类并消除特定的分析估计（例如范数约束）来获得。
与先前工作的比较：与先前局限于有限假设类（例如 Bagnall & Stewart）或特定算法案例（例如决策桩）的形式化工作不同，这项工作处理了具有实值损失的一般、可能不可数的函数类。

本文结论指出，虽然数学界本身是经典的，但形式化工作阐明了其在严格设定下有效所需的精确逻辑结构和侧面条件，为未来的扩展（如 Lipschitz 收缩不等式以及与高斯复杂度的联系）奠定了基础。