技术摘要：AI4SLT：Lean 4 中的经验过程研究

问题陈述

统计学习理论（SLT）数十年来成功指导了机器学习的发展，提供了诸如偏差-方差权衡和正则化等基础概念。然而，随着模型演变为复杂的架构（例如深度神经网络、大语言模型），当代理论分析变得日益复杂，依赖于来自泛函分析和统计物理学的先进数学工具。这种复杂性增加了人类验证的难度，使得追踪逻辑依赖关系和大规模验证中间引理变得困难。

此外，SLT 中的核心技术（如集中不等式和覆盖论证）缺乏结构化的、机器可读的库，限制了其复用性。虽然像 Lean 4 这样的交互式定理证明器为机器可检查的正确性提供了一条路径，但现有的机器学习形式化工作局限于特定领域（例如强化学习、优化）或简化设置（例如通过整个函数类的 Rademacher 复杂度推导泛化界）。目前仍缺乏对**局部经验过程框架（localized empirical process framework）**的全面形式化——这对于在 高维和非参数设置中推导尖锐的极小极大速率（minimax rates）至关重要。该框架需要对标准教科书中经常隐晦处理的测度性、可积性和拓扑假设进行严谨的处理。

方法论

作者提出了 AI4SLT，这是第一个基于 Lean 4 经验过程理论的全面统计学习理论形式化项目。该项目采用了人机协作工作流执行：

• 人类角色： 数学家设计证明策略，分析现有的 Mathlib 基础设施，将复杂的定理分解为易于处理的引理，并验证陈述的一致性。
• AI 角色： AI 智能体（具体为使用 Claude Code 的 Opus-4.5）执行战术证明构建，根据结构化规范填充细节。

该工作流涉及一个结构化规范协议（TASK.md），其中包含目标陈述、基础设施指针、面向形式化的证明计划以及硬性边界。该过程强调迭代优化，即利用 AI 的失败来识别人类遗留的隐性假设，从而实现收敛而非无休止的协作。整个项目耗时约 500 小时的监督开发，最终生成了约 30,000 行无需 sorry（未证明的目标）或自定义公理即可编译通过的 Lean 4 代码。

核心贡献

1. 高斯 Lipschitz 集中工具箱

作者构建了一个完整的高斯 Lipschitz 集中形式化开发，这是高维概率论的基础工具。这需要从头开始构建大量的底层基础设施，包括：

• Efron-Stein 不等式： 进行了形式化，并配备了一个通用的转移引理，以处理具有不同分布的逐坐标更新。
• 高斯 Poincaré 不等式： 利用 Efron-Stein 的基础设施和泰勒展开界限进行推导。
• 密度论证： 形式化了将不等式从光滑紧支撑函数 ($C^\infty_c$) 扩展到一般 Lipschitz 和 $C^1$ 类的方法，通过高斯 Sobolev 空间 ($W^{1,2}$) 和软化（mollification）技术实现。
• 高斯对数 Sobolev 不等式 (LSI)： 利用熵的次可加性，将一维 LSI 形式化推广到 $n$ 维情况。
• 高斯 Lipschitz 集中： 使用 Herbst 论证和 Chernoff 界推导出最终的集中界限。

据作者所知，这构成了任何定理证明器中首次完成的高斯分析工具集的形式化。

2. 针对亚高斯过程的 Dudley 熵积分

本文提供了 Lean 4 中针对亚高斯过程的 Dudley 熵积分定理 的首次形式化。该结果通过涉及度量熵的积分来限制随机过程的期望上确界。

• 形式化挑战： 作者解决了需要严谨链式论证（chaining arguments）的问题，将过程分解为对二进近似（dyadic approximations）的级数求和。他们形式化了度量空间中的覆盖数和填充数，并处理了扩展非负实数 ($\mathbb{R}_{\ge 0}^\infty$) 与实值函数之间的积分问题，确保该界限适用于一般的亚高斯过程。

3. 应用：基于局部经验过程的最小二乘框架

作者通过开发基于局部经验过程的统一最小二乘回归框架，展示了其基础设施的实用性。

• 主误差界： 他们形式化了将预测误差与关键半径 $\delta^*$ 联系起来的关键不等式，该半径由局部高斯复杂度推导而来。
• 尖锐速率： 该框架被应用于线性回归和 $\ell_1$ 约束回归（Lasso）。通过限制覆盖数（使用欧几里得归约和 Maurey 的经验方法处理 $\ell_1$-凸包），作者获得了接近极小极大水平的尖锐速率，恢复了诸如线性回归的 $O(\sigma^2 r/n)$ 以及高维稀疏回归的 $O(R\sqrt{\log d/n})$ 等结果。

4. 人机协作形式化范式

论文详细介绍了大规模形式化的方法论：

• 结构化规范： 通过提供明确的基础设施指针和战术级证明计划，将首次尝试失败率从 ~70% 降低到 ~15%。
• 迭代演进： 利用 AI 的失败来揭示人类隐含的假设（如测度性、可积性、定义域约束），并迭代优化规范。
• 定量分解： 大约 40% 的声明是在完整的自然语言证明计划下完成证明的，30% 是在草图引导下完成的，15% 是自主完成的，另外 15% 需要关键的人类干预（例如纠正错误的数学策略或验证陈述一致性）。

结果

• 代码库： 包含约 30,000 行 Lean 4 代码的库，拥有超过 1,000 个定理和引理。
• 完整性： 所有形式化内容均可在不使用 sorry 或公理的情况下编译，确保了机器可验证的正确性。
• 差距解决： 该形式化过程暴露并解决了标准 SLT 教科书中存在的隐性假设，例如上确界随机变量的测度性条件、熵泛函的可积性以及经验球的非空性。
• 性能： 该框架成功推导了参数化（线性）和非参数化（稀疏）回归设置下的尖锐极小极大速率，验证了局部经验过程方法的效用。

意义

论文声称这项工作建立了一个可复用的统计学习理论形式化基础。通过超越机械性的翻译，转向对理论进行细粒度的、逐行的理解，该项目强制执行了严谨的标准，澄清了逻辑依赖关系和隐藏的假设。

其意义是双重的：

1. 理论严谨性： 它提供了一个用于 SLT 的机器检查库，能够实现对机器学习系统的可扩展、自动化的理论分析，并作为学生掌握 SLT 全套技术栈的原则性训练场。
2. 方法论进步： 它证明了通过精心设计的人机协作，可以显著加速大规模形式化项目，为机器学习理论及其他复杂数学领域未来的发展提供了蓝图。

作者强调，这项工作不仅仅是追求严谨性的练习，更是处理日益复杂的现代机器学习理论所必需的一步，为该领域未来的形式化发展开启了大门。