发表机构
Imperial College London（伦敦帝国理工学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本研究利用形式化认证方法，通过新的集中不等式连接样本特定稳定性与分布性分析，为学习算法提供紧致可靠的泛化界，显著优于现有计算方法。
AI 中文摘要
我们研究了使用形式化方法来为学习算法提供紧致且可靠的泛化界。通过将传统的算法稳定性概念视为待验证的规范，我们证明了可达性分析的最新进展可以为给定模型和算法在样本数据集上的泛化提供可证明的界。由于样本特定的算法稳定性不足以界定通常的分布性泛化概念，我们开发了一种新的集中不等式，将形式化认证算法的样本特定结果与所需的分布性分析联系起来，以界定期望泛化差距。所得到的框架使得对先前泛化界的分析能够远远超出其原始的限制性假设。我们的方法在常数次算法运行中计算期望泛化差距的可靠界，而无需对算法做出任何分析性假设；为了实现非空洞的界，我们仅要求认证的可达参数集是有界的——这一条件我们不是假设而是形式化验证。在实践中，我们证明了我们的框架在从玩具数据集到在现代大型语言模型之上微调分类头的各种规模上，提供了比替代性可靠计算方法紧致数个数量级的形式化泛化保证。虽然我们实现了若干著名稳定性结果的认证增强版本，但我们方法的未来扩展将能够实现更紧致的界，并增强在现代泛化界谱系中的实际采用。
英文摘要
We investigate the use of formal methods to provide tight and sound generalization bounds for learning algorithms. By casting the traditional notion of algorithmic stability as a specification to be verified, we demonstrate that recent advances in reachability analysis can yield provable bounds on the generalization of a given model and algorithm on a sample dataset. As sample-specific algorithmic stability is insufficient to bound the usual distributional notion of generalization, we develop a novel concentration inequality to connect the sample-specific results of formal certification algorithms to the required distributional analysis for bounding the expected generalization gap. The resulting framework enables the analysis of prior generalization bounds to extend far beyond their original restrictive assumptions. Our approach computes sound bounds on the expected generalization gap in a constant number of algorithm runs without making any analytical assumptions on the algorithm; to achieve non-vacuous bounds we only require that the certified reachable parameter set is bounded --- a condition that we do not assume but formally verify. In practice, we demonstrate that our framework provides formal generalization guarantees that are orders of magnitude tighter than alternative sound computational approaches at scales ranging from toy datasets to fine-tuning classification heads on top of modern large language models. While we implement certification-enhanced versions of several well-known stability results, future extensions of our approach will enable tighter bounds and enhanced practical adoption across the spectrum of modern generalization bounds.
CommentsAccepted at NeurIPS 2026
